# Stuck in a proof about sum types and nonempty lists

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.
- 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?

I don't have Coq installed to check, but I believe cons (inr (inl 1)) (sngl (inl 2)) should be a counterexample as filter (map flatten l) will be inl 2 and flatten (app_r filter (filter l)) will be inl 1.