I have a hard time proving an apparently simple property or finding a counterexample. It is about sum types and nonempty lists.
I first define two basic functions about sum types:
Definition app_r {A B C : Type} (f : B -> C) (s : A + B) : A + C :=
match s with
| inl a => inl a
| inr b => inr (f b)
end.
Definition flatten {A B : Type} (s : A + (A + B)) : A + B :=
match s with inr s' => s' | inl a => inl a end.
Then I define the nonempty list type and its map:
Set Implicit Arguments.
Inductive list (A : Type) : Type :=
| sngl : A -> list A
| cons : A -> list A -> list A.
Fixpoint map {A B : Type} (f : A -> B) (l : list A) : list B :=
match l with
| sngl x => sngl (f x)
| cons x l' => cons (f x) (map f l')
end.
The lemma I want to prove is about the following function that essentially removes the inls from a list of sums:
Fixpoint filter {A B : Type} (w : list (A + B)) : A + list B :=
match w with
| sngl (inl a) => inl a
| sngl (inr b) => inr (sngl b)
| cons (inl _) l' => filter l'
| cons (inr b) l' => match filter l' with
| inl _ => inr (sngl b)
| inr l'' => inr (cons b l'')
end
end.
The investigated property is the following:
Goal forall (A B : Type) (l : list (A + (A + B))),
filter (map flatten l) = flatten (app_r filter (filter l)).
I tried to find a counter-example but failed. For example a possible candidate was:
Example l :=
cons (inl 1) (cons (inr (@inl nat bool 2)) (sngl (inr (inl 3)))).
However it is not a counterexample as the two following commands return inl 3:
Compute filter (map flatten l).
Compute flatten (app_r filter (filter l)).
Here is my attempt at proving the goal:
Proof.
induction l as [[ | [ | ]] | [ | [ | ]] l IH]; auto.
- cbn.
rewrite IH.
destruct (filter l) as [l' | e'] eqn: Hfilter; [ | reflexivity].
cbn.
admit.
- cbn.
rewrite IH.
destruct (filter l) as [l' | ]; [ | reflexivity].
cbn.
reflexivity.
Abort.
If it is true, then it appears that it cannot be proved by a simple structural induction.
Would you have a proof? A counterexample? A hint?
