3
$\begingroup$

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?

$\endgroup$

1 Answer 1

3
$\begingroup$

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.

$\endgroup$
1
  • 1
    $\begingroup$ You are right. Thanks! $\endgroup$
    – Dave
    Feb 22 at 19:46

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.