From Tealeaves Require Import
  Classes.Categorical.Monad
  Classes.Coalgebraic.TraversableFunctor
  Adapters.KleisliToCoalgebraic.TraversableFunctor
  Classes.Kleisli.Theory.TraversableFunctor
  Classes.Kleisli.Theory.TraversableMonad
  Classes.Categorical.ContainerFunctor
  Classes.Categorical.ShapelyFunctor.

From Tealeaves Require Export
  Functors.Early.List
  Functors.Early.Subset.

Import ContainerFunctor.Notations.
Import TraversableMonad.Notations.
Import List.ListNotations.
Import Monoid.Notations.
Import Subset.Notations.
Import Applicative.Notations.
Export EqNotations.

#[local] Generalizable Variables M A B G ϕ.

(** *** List <<traverse>> is compatible with its <<tosubset_list>> *)
(**********************************************************************)
#[export] Instance Compat_ToSubset_Traverse_list:
  Compat_ToSubset_Traverse (ToSubset_inst := ToSubset_list) list.
Compat_ToSubset_Traverse list
Proof.
Compat_ToSubset_Traverse list
  unfold Compat_ToSubset_Traverse.
ToSubset_list = ToSubset_Traverse
  unfold_ops @ToSubset_list.
(fun (A : Type) (l : list A) (a : A) => List.In a l) =
ToSubset_Traverse
  unfold_ops @ToSubset_Traverse.
(fun (A : Type) (l : list A) (a : A) => List.In a l) =
(fun A : Type => mapReduce ret)
  ext A l.
A: Type
l: list A
(fun a : A => List.In a l) = mapReduce ret l
  rewrite mapReduce_eq_mapReduce_list.
A: Type
l: list A
(fun a : A => List.In a l) = mapReduce_list ret l
  induction l.
A: Type
(fun a : A => List.In a []) = mapReduce_list ret []
A: Type
a: A
l: list A
IHl: (fun a : A => List.In a l) = mapReduce_list ret l
(fun a0 : A => List.In a0 (a :: l)) =
mapReduce_list ret (a :: l)
  -
A: Type
(fun a : A => List.In a []) = mapReduce_list ret [] simpl_list.
A: Type
(fun a : A => List.In a []) = Ƶ
    reflexivity.
  -
A: Type
a: A
l: list A
IHl: (fun a : A => List.In a l) = mapReduce_list ret l
(fun a0 : A => List.In a0 (a :: l)) =
mapReduce_list ret (a :: l) simpl_list.
A: Type
a: A
l: list A
IHl: (fun a : A => List.In a l) = mapReduce_list ret l
(fun a0 : A => List.In a0 (a :: l)) =
ret a ● mapReduce_list ret l
    cbn.
A: Type
a: A
l: list A
IHl: (fun a : A => List.In a l) = mapReduce_list ret l
(fun a0 : A => a = a0 \/ List.In a0 l) =
ret a ● mapReduce_list ret l
    rewrite <- IHl.
A: Type
a: A
l: list A
IHl: (fun a : A => List.In a l) = mapReduce_list ret l
(fun a0 : A => a = a0 \/ List.In a0 l) =
ret a ● (fun a : A => List.In a l)
    reflexivity.
Qed.

(** * <<toBatch>> Instance *)
(**********************************************************************)
#[export] Instance ToBatch_list: ToBatch list :=
  DerivedOperations.ToBatch_Traverse.

(** * <<map>> equality inversion lemmas *)
(** Some lemmas for reasoning backwards from equality between two
    similarly-concatenated lists.  *)
(**********************************************************************)
Lemma map_app_inv_l: forall {A B} {f g: A -> B} (l1 l2: list A),
    map f (l1 ++ l2) = map g (l1 ++ l2) ->
    map f l1 = map g l1.
forall (A B : Type) (f g : A -> B) (l1 l2 : list A),
map f (l1 ++ l2) = map g (l1 ++ l2) ->
map f l1 = map g l1
Proof.
forall (A B : Type) (f g : A -> B) (l1 l2 : list A),
map f (l1 ++ l2) = map g (l1 ++ l2) ->
map f l1 = map g l1
  intros.
A, B: Type
f, g: A -> B
l1, l2: list A
H: map f (l1 ++ l2) = map g (l1 ++ l2)
map f l1 = map g l1 induction l1.
A, B: Type
f, g: A -> B
l2: list A
H: map f ([] ++ l2) = map g ([] ++ l2)
map f [] = map g []
A, B: Type
f, g: A -> B
a: A
l1, l2: list A
H: map f ((a :: l1) ++ l2) = map g ((a :: l1) ++ l2)
IHl1: map f (l1 ++ l2) = map g (l1 ++ l2) ->
map f l1 = map g l1
map f (a :: l1) = map g (a :: l1)
  -
A, B: Type
f, g: A -> B
l2: list A
H: map f ([] ++ l2) = map g ([] ++ l2)
map f [] = map g [] reflexivity.
  -
A, B: Type
f, g: A -> B
a: A
l1, l2: list A
H: map f ((a :: l1) ++ l2) = map g ((a :: l1) ++ l2)
IHl1: map f (l1 ++ l2) = map g (l1 ++ l2) ->
map f l1 = map g l1
map f (a :: l1) = map g (a :: l1) simpl_list in *.
A, B: Type
f, g: A -> B
a: A
l1, l2: list A
H: (f a :: map f l1) ++ map f l2 =
(g a :: map g l1) ++ map g l2
IHl1: map f l1 ++ map f l2 = map g l1 ++ map g l2 ->
map f l1 = map g l1
f a :: map f l1 = g a :: map g l1 rewrite IHl1.
A, B: Type
f, g: A -> B
a: A
l1, l2: list A
H: (f a :: map f l1) ++ map f l2 =
(g a :: map g l1) ++ map g l2
IHl1: map f l1 ++ map f l2 = map g l1 ++ map g l2 ->
map f l1 = map g l1
f a :: map g l1 = g a :: map g l1
A, B: Type
f, g: A -> B
a: A
l1, l2: list A
H: (f a :: map f l1) ++ map f l2 =
(g a :: map g l1) ++ map g l2
IHl1: map f l1 ++ map f l2 = map g l1 ++ map g l2 ->
map f l1 = map g l1
map f l1 ++ map f l2 = map g l1 ++ map g l2
    +
A, B: Type
f, g: A -> B
a: A
l1, l2: list A
H: (f a :: map f l1) ++ map f l2 =
(g a :: map g l1) ++ map g l2
IHl1: map f l1 ++ map f l2 = map g l1 ++ map g l2 ->
map f l1 = map g l1
f a :: map g l1 = g a :: map g l1 fequal.
A, B: Type
f, g: A -> B
a: A
l1, l2: list A
H: (f a :: map f l1) ++ map f l2 =
(g a :: map g l1) ++ map g l2
IHl1: map f l1 ++ map f l2 = map g l1 ++ map g l2 ->
map f l1 = map g l1
f a = g a simpl in H.
A, B: Type
f, g: A -> B
a: A
l1, l2: list A
H: f a :: map f l1 ++ map f l2 =
g a :: map g l1 ++ map g l2
IHl1: map f l1 ++ map f l2 = map g l1 ++ map g l2 ->
map f l1 = map g l1
f a = g a inversion H; auto.
    +
A, B: Type
f, g: A -> B
a: A
l1, l2: list A
H: (f a :: map f l1) ++ map f l2 =
(g a :: map g l1) ++ map g l2
IHl1: map f l1 ++ map f l2 = map g l1 ++ map g l2 ->
map f l1 = map g l1
map f l1 ++ map f l2 = map g l1 ++ map g l2 simpl in H.
A, B: Type
f, g: A -> B
a: A
l1, l2: list A
H: f a :: map f l1 ++ map f l2 =
g a :: map g l1 ++ map g l2
IHl1: map f l1 ++ map f l2 = map g l1 ++ map g l2 ->
map f l1 = map g l1
map f l1 ++ map f l2 = map g l1 ++ map g l2 inversion H.
A, B: Type
f, g: A -> B
a: A
l1, l2: list A
H: f a :: map f l1 ++ map f l2 =
g a :: map g l1 ++ map g l2
IHl1: map f l1 ++ map f l2 = map g l1 ++ map g l2 ->
map f l1 = map g l1
H1: f a = g a
H2: map f l1 ++ map f l2 = map g l1 ++ map g l2
map f l1 ++ map f l2 = map f l1 ++ map f l2 auto.
Qed.

Lemma map_app_inv_r: forall {A B} {f g: A -> B} (l1 l2: list A),
    map f (l1 ++ l2) = map g (l1 ++ l2) ->
    map f l2 = map g l2.
forall (A B : Type) (f g : A -> B) (l1 l2 : list A),
map f (l1 ++ l2) = map g (l1 ++ l2) ->
map f l2 = map g l2
Proof.
forall (A B : Type) (f g : A -> B) (l1 l2 : list A),
map f (l1 ++ l2) = map g (l1 ++ l2) ->
map f l2 = map g l2
  intros.
A, B: Type
f, g: A -> B
l1, l2: list A
H: map f (l1 ++ l2) = map g (l1 ++ l2)
map f l2 = map g l2
  assert (heads_equal: map f l1 = map g l1).
A, B: Type
f, g: A -> B
l1, l2: list A
H: map f (l1 ++ l2) = map g (l1 ++ l2)
map f l1 = map g l1
A, B: Type
f, g: A -> B
l1, l2: list A
H: map f (l1 ++ l2) = map g (l1 ++ l2)
heads_equal: map f l1 = map g l1
map f l2 = map g l2
  {
A, B: Type
f, g: A -> B
l1, l2: list A
H: map f (l1 ++ l2) = map g (l1 ++ l2)
map f l1 = map g l1 eauto using map_app_inv_l. }
A, B: Type
f, g: A -> B
l1, l2: list A
H: map f (l1 ++ l2) = map g (l1 ++ l2)
heads_equal: map f l1 = map g l1
map f l2 = map g l2
  simpl_list in *.
A, B: Type
f, g: A -> B
l1, l2: list A
H: map f l1 ++ map f l2 = map g l1 ++ map g l2
heads_equal: map f l1 = map g l1
map f l2 = map g l2
  rewrite heads_equal in H.
A, B: Type
f, g: A -> B
l1, l2: list A
H: map g l1 ++ map f l2 = map g l1 ++ map g l2
heads_equal: map f l1 = map g l1
map f l2 = map g l2
  eauto using List.app_inv_head.
Qed.

Lemma map_app_inv: forall {A B} {f g: A -> B} (l1 l2: list A),
    map f (l1 ++ l2) = map g (l1 ++ l2) ->
    map f l1 = map g l1 /\ map f l2 = map g l2.
forall (A B : Type) (f g : A -> B) (l1 l2 : list A),
map f (l1 ++ l2) = map g (l1 ++ l2) ->
map f l1 = map g l1 /\ map f l2 = map g l2
Proof.
forall (A B : Type) (f g : A -> B) (l1 l2 : list A),
map f (l1 ++ l2) = map g (l1 ++ l2) ->
map f l1 = map g l1 /\ map f l2 = map g l2
  intros; split; eauto using map_app_inv_l, map_app_inv_r.
Qed.

#[local] Generalizable Variable F.

(** * Shapely Functor Instance for [list] *)
(** As a reasonability check, we prove that [list] is a listable functor. *)
(**********************************************************************)
Section ShapelyFunctor_list.

  Instance Tolist_list: Tolist list := fun A l => l.

  Instance: Natural (@tolist list _).
Natural (@tolist list Tolist_list)
  Proof.
Natural (@tolist list Tolist_list)
    constructor; try typeclasses eauto.
forall (A B : Type) (f : A -> B),
map f ∘ tolist = tolist ∘ map f
    reflexivity.
  Qed.

  Theorem shapeliness_list: shapeliness list.
shapeliness list
  Proof.
shapeliness list
    intros A t1 t2.
A: Type
t1, t2: list A
shape t1 = shape t2 /\ tolist t1 = tolist t2 ->
t1 = t2 intuition.
  Qed.

  Instance: ShapelyFunctor list :=
    {| shp_shapeliness := shapeliness_list;
    |}.

End ShapelyFunctor_list.

(** ** Rewriting [shape] on Lists *)
(**********************************************************************)
Section list_shape_rewrite.

  Lemma shape_nil: forall A,
      shape (@nil A) = @nil unit.
forall A : Type, shape [] = []
  Proof.
forall A : Type, shape [] = []
    reflexivity.
  Qed.

  Lemma shape_cons: forall A (a: A) (l: list A),
      shape (a :: l) = tt :: shape l.
forall (A : Type) (a : A) (l : list A),
shape (a :: l) = tt :: shape l
  Proof.
forall (A : Type) (a : A) (l : list A),
shape (a :: l) = tt :: shape l
    reflexivity.
  Qed.

  Lemma shape_one: forall A (a: A),
      shape [ a ] = [ tt ].
forall (A : Type) (a : A), shape [a] = [tt]
  Proof.
forall (A : Type) (a : A), shape [a] = [tt]
    reflexivity.
  Qed.

  Lemma shape_app: forall A (l1 l2: list A),
      shape (l1 ++ l2) = shape l1 ++ shape l2.
forall (A : Type) (l1 l2 : list A),
shape (l1 ++ l2) = shape l1 ++ shape l2
  Proof.
forall (A : Type) (l1 l2 : list A),
shape (l1 ++ l2) = shape l1 ++ shape l2
    intros.
A: Type
l1, l2: list A
shape (l1 ++ l2) = shape l1 ++ shape l2 unfold shape.
A: Type
l1, l2: list A
map (const tt) (l1 ++ l2) =
map (const tt) l1 ++ map (const tt) l2 now rewrite map_list_app.
  Qed.

  Lemma shape_nil_iff: forall A (l: list A),
      shape l = @nil unit <-> l = [].
forall (A : Type) (l : list A),
shape l = [] <-> l = []
  Proof.
forall (A : Type) (l : list A),
shape l = [] <-> l = []
    induction l.
A: Type
shape [] = [] <-> [] = []
A: Type
a: A
l: list A
IHl: shape l = [] <-> l = []
shape (a :: l) = [] <-> a :: l = [] intuition.
A: Type
a: A
l: list A
IHl: shape l = [] <-> l = []
shape (a :: l) = [] <-> a :: l = []
    split; intro contra; now inverts contra.
  Qed.

End list_shape_rewrite.

#[export] Hint Rewrite
  @shape_nil @shape_cons @shape_one @shape_app: tea_list.

(** ** Reasoning Princples for <<shape>> on Lists *)
(**********************************************************************)
Section list_shape_lemmas.

  Theorem list_shape_equal_iff: forall (A: Type) (l1 l2: list A),
      shape l1 = shape l2 <->
        List.length l1 = List.length l2.
forall (A : Type) (l1 l2 : list A),
shape l1 = shape l2 <-> length l1 = length l2
  Proof.
forall (A : Type) (l1 l2 : list A),
shape l1 = shape l2 <-> length l1 = length l2
    intros.
A: Type
l1, l2: list A
shape l1 = shape l2 <-> length l1 = length l2 generalize dependent l2.
A: Type
l1: list A
forall l2 : list A,
shape l1 = shape l2 <-> length l1 = length l2
    induction l1.
A: Type
forall l2 : list A,
shape [] = shape l2 <-> length [] = length l2
A: Type
a: A
l1: list A
IHl1: forall l2 : list A,
shape l1 = shape l2 <-> length l1 = length l2
forall l2 : list A,
shape (a :: l1) = shape l2 <->
length (a :: l1) = length l2
    -
A: Type
forall l2 : list A,
shape [] = shape l2 <-> length [] = length l2 destruct l2.
A: Type
shape [] = shape [] <-> length [] = length []
A: Type
a: A
l2: list A
shape [] = shape (a :: l2) <->
length [] = length (a :: l2)
      +
A: Type
shape [] = shape [] <-> length [] = length [] split; reflexivity.
      +
A: Type
a: A
l2: list A
shape [] = shape (a :: l2) <->
length [] = length (a :: l2) split; inversion 1.
    -
A: Type
a: A
l1: list A
IHl1: forall l2 : list A,
shape l1 = shape l2 <-> length l1 = length l2
forall l2 : list A,
shape (a :: l1) = shape l2 <->
length (a :: l1) = length l2 cbn.
A: Type
a: A
l1: list A
IHl1: forall l2 : list A,
shape l1 = shape l2 <-> length l1 = length l2
forall l2 : list A,
const tt a :: shape l1 = shape l2 <->
S (length l1) = length l2 intro l2; destruct l2.
A: Type
a: A
l1: list A
IHl1: forall l2 : list A,
shape l1 = shape l2 <-> length l1 = length l2
const tt a :: shape l1 = shape [] <->
S (length l1) = length []
A: Type
a: A
l1: list A
IHl1: forall l2 : list A,
shape l1 = shape l2 <-> length l1 = length l2
a0: A
l2: list A
const tt a :: shape l1 = shape (a0 :: l2) <->
S (length l1) = length (a0 :: l2)
      +
A: Type
a: A
l1: list A
IHl1: forall l2 : list A,
shape l1 = shape l2 <-> length l1 = length l2
const tt a :: shape l1 = shape [] <->
S (length l1) = length [] cbn.
A: Type
a: A
l1: list A
IHl1: forall l2 : list A,
shape l1 = shape l2 <-> length l1 = length l2
const tt a :: shape l1 = [] <-> S (length l1) = 0 split; inversion 1.
      +
A: Type
a: A
l1: list A
IHl1: forall l2 : list A,
shape l1 = shape l2 <-> length l1 = length l2
a0: A
l2: list A
const tt a :: shape l1 = shape (a0 :: l2) <->
S (length l1) = length (a0 :: l2) cbn.
A: Type
a: A
l1: list A
IHl1: forall l2 : list A,
shape l1 = shape l2 <-> length l1 = length l2
a0: A
l2: list A
const tt a :: shape l1 = const tt a0 :: shape l2 <->
S (length l1) = S (length l2) split; inversion 1.
A: Type
a: A
l1: list A
IHl1: forall l2 : list A,
shape l1 = shape l2 <-> length l1 = length l2
a0: A
l2: list A
H: const tt a :: shape l1 = const tt a0 :: shape l2
H1: shape l1 = shape l2
S (length l1) = S (length l2)
A: Type
a: A
l1: list A
IHl1: forall l2 : list A,
shape l1 = shape l2 <-> length l1 = length l2
a0: A
l2: list A
H: S (length l1) = S (length l2)
H1: length l1 = length l2
const tt a :: shape l1 = const tt a0 :: shape l2
        *
A: Type
a: A
l1: list A
IHl1: forall l2 : list A,
shape l1 = shape l2 <-> length l1 = length l2
a0: A
l2: list A
H: const tt a :: shape l1 = const tt a0 :: shape l2
H1: shape l1 = shape l2
S (length l1) = S (length l2) fequal.
A: Type
a: A
l1: list A
IHl1: forall l2 : list A,
shape l1 = shape l2 <-> length l1 = length l2
a0: A
l2: list A
H: const tt a :: shape l1 = const tt a0 :: shape l2
H1: shape l1 = shape l2
length l1 = length l2 apply IHl1.
A: Type
a: A
l1: list A
IHl1: forall l2 : list A,
shape l1 = shape l2 <-> length l1 = length l2
a0: A
l2: list A
H: const tt a :: shape l1 = const tt a0 :: shape l2
H1: shape l1 = shape l2
shape l1 = shape l2 auto.
        *
A: Type
a: A
l1: list A
IHl1: forall l2 : list A,
shape l1 = shape l2 <-> length l1 = length l2
a0: A
l2: list A
H: S (length l1) = S (length l2)
H1: length l1 = length l2
const tt a :: shape l1 = const tt a0 :: shape l2 fequal.
A: Type
a: A
l1: list A
IHl1: forall l2 : list A,
shape l1 = shape l2 <-> length l1 = length l2
a0: A
l2: list A
H: S (length l1) = S (length l2)
H1: length l1 = length l2
shape l1 = shape l2 apply IHl1.
A: Type
a: A
l1: list A
IHl1: forall l2 : list A,
shape l1 = shape l2 <-> length l1 = length l2
a0: A
l2: list A
H: S (length l1) = S (length l2)
H1: length l1 = length l2
length l1 = length l2 auto.
  Qed.

  Theorem shape_eq_app_r: forall (A: Type) (l1 l2 r1 r2: list A),
      shape r1 = shape r2 ->
      (shape (l1 ++ r1) = shape (l2 ++ r2) <->
         shape l1 = shape l2).
forall (A : Type) (l1 l2 r1 r2 : list A),
shape r1 = shape r2 ->
shape (l1 ++ r1) = shape (l2 ++ r2) <->
shape l1 = shape l2
  Proof.
forall (A : Type) (l1 l2 r1 r2 : list A),
shape r1 = shape r2 ->
shape (l1 ++ r1) = shape (l2 ++ r2) <->
shape l1 = shape l2
    introv heq.
A: Type
l1, l2, r1, r2: list A
heq: shape r1 = shape r2
shape (l1 ++ r1) = shape (l2 ++ r2) <->
shape l1 = shape l2 rewrite 2(shape_app).
A: Type
l1, l2, r1, r2: list A
heq: shape r1 = shape r2
shape l1 ++ shape r1 = shape l2 ++ shape r2 <->
shape l1 = shape l2 rewrite heq.
A: Type
l1, l2, r1, r2: list A
heq: shape r1 = shape r2
shape l1 ++ shape r2 = shape l2 ++ shape r2 <->
shape l1 = shape l2
    split.
A: Type
l1, l2, r1, r2: list A
heq: shape r1 = shape r2
shape l1 ++ shape r2 = shape l2 ++ shape r2 ->
shape l1 = shape l2
A: Type
l1, l2, r1, r2: list A
heq: shape r1 = shape r2
shape l1 = shape l2 ->
shape l1 ++ shape r2 = shape l2 ++ shape r2 intros; eauto using List.app_inv_tail.
A: Type
l1, l2, r1, r2: list A
heq: shape r1 = shape r2
shape l1 = shape l2 ->
shape l1 ++ shape r2 = shape l2 ++ shape r2
    intros hyp; now rewrite hyp.
  Qed.

  Theorem shape_eq_app_l: forall (A: Type) (l1 l2 r1 r2: list A),
      shape l1 = shape l2 ->
      (shape (l1 ++ r1) = shape (l2 ++ r2) <->
         shape r1 = shape r2).
forall (A : Type) (l1 l2 r1 r2 : list A),
shape l1 = shape l2 ->
shape (l1 ++ r1) = shape (l2 ++ r2) <->
shape r1 = shape r2
  Proof.
forall (A : Type) (l1 l2 r1 r2 : list A),
shape l1 = shape l2 ->
shape (l1 ++ r1) = shape (l2 ++ r2) <->
shape r1 = shape r2
    introv heq.
A: Type
l1, l2, r1, r2: list A
heq: shape l1 = shape l2
shape (l1 ++ r1) = shape (l2 ++ r2) <->
shape r1 = shape r2 rewrite 2(shape_app).
A: Type
l1, l2, r1, r2: list A
heq: shape l1 = shape l2
shape l1 ++ shape r1 = shape l2 ++ shape r2 <->
shape r1 = shape r2 rewrite heq.
A: Type
l1, l2, r1, r2: list A
heq: shape l1 = shape l2
shape l2 ++ shape r1 = shape l2 ++ shape r2 <->
shape r1 = shape r2
    split.
A: Type
l1, l2, r1, r2: list A
heq: shape l1 = shape l2
shape l2 ++ shape r1 = shape l2 ++ shape r2 ->
shape r1 = shape r2
A: Type
l1, l2, r1, r2: list A
heq: shape l1 = shape l2
shape r1 = shape r2 ->
shape l2 ++ shape r1 = shape l2 ++ shape r2 intros; eauto using List.app_inv_head.
A: Type
l1, l2, r1, r2: list A
heq: shape l1 = shape l2
shape r1 = shape r2 ->
shape l2 ++ shape r1 = shape l2 ++ shape r2
    intros hyp; now rewrite hyp.
  Qed.

  Theorem shape_eq_cons_iff: forall (A: Type) (l1 l2: list A) (x y: A),
      shape (x :: l1) = shape (y :: l2) <->
        shape l1 = shape l2.
forall (A : Type) (l1 l2 : list A) (x y : A),
shape (x :: l1) = shape (y :: l2) <->
shape l1 = shape l2
  Proof.
forall (A : Type) (l1 l2 : list A) (x y : A),
shape (x :: l1) = shape (y :: l2) <->
shape l1 = shape l2
    intros.
A: Type
l1, l2: list A
x, y: A
shape (x :: l1) = shape (y :: l2) <->
shape l1 = shape l2 rewrite 2(shape_cons).
A: Type
l1, l2: list A
x, y: A
tt :: shape l1 = tt :: shape l2 <->
shape l1 = shape l2
    split; intros hyp.
A: Type
l1, l2: list A
x, y: A
hyp: tt :: shape l1 = tt :: shape l2
shape l1 = shape l2
A: Type
l1, l2: list A
x, y: A
hyp: shape l1 = shape l2
tt :: shape l1 = tt :: shape l2 now inverts hyp.
A: Type
l1, l2: list A
x, y: A
hyp: shape l1 = shape l2
tt :: shape l1 = tt :: shape l2
    now rewrite hyp.
  Qed.

  Theorem inv_app_eq_ll: forall (A: Type) (l1 l2 r1 r2: list A),
      shape l1 = shape l2 ->
      (l1 ++ r1 = l2 ++ r2) ->
      l1 = l2.
forall (A : Type) (l1 l2 r1 r2 : list A),
shape l1 = shape l2 -> l1 ++ r1 = l2 ++ r2 -> l1 = l2
  Proof.
forall (A : Type) (l1 l2 r1 r2 : list A),
shape l1 = shape l2 -> l1 ++ r1 = l2 ++ r2 -> l1 = l2
    intros A.
A: Type
forall l1 l2 r1 r2 : list A,
shape l1 = shape l2 -> l1 ++ r1 = l2 ++ r2 -> l1 = l2 induction l1 as [| ? ? IHl1 ];
      induction l2 as [| ? ? IHl2 ].
A: Type
forall r1 r2 : list A,
shape [] = shape [] -> [] ++ r1 = [] ++ r2 -> [] = []
A: Type
a: A
l2: list A
IHl2: forall r1 r2 : list A,
shape [] = shape l2 ->
[] ++ r1 = l2 ++ r2 -> [] = l2
forall r1 r2 : list A,
shape [] = shape (a :: l2) ->
[] ++ r1 = (a :: l2) ++ r2 -> [] = a :: l2
A: Type
a: A
l1: list A
IHl1: forall l2 r1 r2 : list A,
shape l1 = shape l2 ->
l1 ++ r1 = l2 ++ r2 -> l1 = l2
forall r1 r2 : list A,
shape (a :: l1) = shape [] ->
(a :: l1) ++ r1 = [] ++ r2 -> a :: l1 = []
A: Type
a: A
l1: list A
IHl1: forall l2 r1 r2 : list A,
shape l1 = shape l2 ->
l1 ++ r1 = l2 ++ r2 -> l1 = l2
a0: A
l2: list A
IHl2: forall r1 r2 : list A,
shape (a :: l1) = shape l2 ->
(a :: l1) ++ r1 = l2 ++ r2 -> a :: l1 = l2
forall r1 r2 : list A,
shape (a :: l1) = shape (a0 :: l2) ->
(a :: l1) ++ r1 = (a0 :: l2) ++ r2 ->
a :: l1 = a0 :: l2
    -
A: Type
forall r1 r2 : list A,
shape [] = shape [] -> [] ++ r1 = [] ++ r2 -> [] = [] reflexivity.
    -
A: Type
a: A
l2: list A
IHl2: forall r1 r2 : list A,
shape [] = shape l2 ->
[] ++ r1 = l2 ++ r2 -> [] = l2
forall r1 r2 : list A,
shape [] = shape (a :: l2) ->
[] ++ r1 = (a :: l2) ++ r2 -> [] = a :: l2 introv shape_eq.
A: Type
a: A
l2: list A
IHl2: forall r1 r2 : list A,
shape [] = shape l2 ->
[] ++ r1 = l2 ++ r2 -> [] = l2
r1, r2: list A
shape_eq: shape [] = shape (a :: l2)
[] ++ r1 = (a :: l2) ++ r2 -> [] = a :: l2 now inverts shape_eq.
    -
A: Type
a: A
l1: list A
IHl1: forall l2 r1 r2 : list A,
shape l1 = shape l2 ->
l1 ++ r1 = l2 ++ r2 -> l1 = l2
forall r1 r2 : list A,
shape (a :: l1) = shape [] ->
(a :: l1) ++ r1 = [] ++ r2 -> a :: l1 = [] introv shape_eq.
A: Type
a: A
l1: list A
IHl1: forall l2 r1 r2 : list A,
shape l1 = shape l2 ->
l1 ++ r1 = l2 ++ r2 -> l1 = l2
r1, r2: list A
shape_eq: shape (a :: l1) = shape []
(a :: l1) ++ r1 = [] ++ r2 -> a :: l1 = [] now inverts shape_eq.
    -
A: Type
a: A
l1: list A
IHl1: forall l2 r1 r2 : list A,
shape l1 = shape l2 ->
l1 ++ r1 = l2 ++ r2 -> l1 = l2
a0: A
l2: list A
IHl2: forall r1 r2 : list A,
shape (a :: l1) = shape l2 ->
(a :: l1) ++ r1 = l2 ++ r2 -> a :: l1 = l2
forall r1 r2 : list A,
shape (a :: l1) = shape (a0 :: l2) ->
(a :: l1) ++ r1 = (a0 :: l2) ++ r2 ->
a :: l1 = a0 :: l2 introv shape_eq heq.
A: Type
a: A
l1: list A
IHl1: forall l2 r1 r2 : list A,
shape l1 = shape l2 ->
l1 ++ r1 = l2 ++ r2 -> l1 = l2
a0: A
l2: list A
IHl2: forall r1 r2 : list A,
shape (a :: l1) = shape l2 ->
(a :: l1) ++ r1 = l2 ++ r2 -> a :: l1 = l2
r1, r2: list A
shape_eq: shape (a :: l1) = shape (a0 :: l2)
heq: (a :: l1) ++ r1 = (a0 :: l2) ++ r2
a :: l1 = a0 :: l2
      rewrite shape_eq_cons_iff in shape_eq.
A: Type
a: A
l1: list A
IHl1: forall l2 r1 r2 : list A,
shape l1 = shape l2 ->
l1 ++ r1 = l2 ++ r2 -> l1 = l2
a0: A
l2: list A
IHl2: forall r1 r2 : list A,
shape (a :: l1) = shape l2 ->
(a :: l1) ++ r1 = l2 ++ r2 -> a :: l1 = l2
r1, r2: list A
shape_eq: shape l1 = shape l2
heq: (a :: l1) ++ r1 = (a0 :: l2) ++ r2
a :: l1 = a0 :: l2
      rewrite <- 2(List.app_comm_cons) in heq.
A: Type
a: A
l1: list A
IHl1: forall l2 r1 r2 : list A,
shape l1 = shape l2 ->
l1 ++ r1 = l2 ++ r2 -> l1 = l2
a0: A
l2: list A
IHl2: forall r1 r2 : list A,
shape (a :: l1) = shape l2 ->
(a :: l1) ++ r1 = l2 ++ r2 -> a :: l1 = l2
r1, r2: list A
shape_eq: shape l1 = shape l2
heq: a :: l1 ++ r1 = a0 :: l2 ++ r2
a :: l1 = a0 :: l2
      inverts heq.
A: Type
l1: list A
IHl1: forall l2 r1 r2 : list A,
shape l1 = shape l2 ->
l1 ++ r1 = l2 ++ r2 -> l1 = l2
a0: A
l2: list A
IHl2: forall r1 r2 : list A,
shape (a0 :: l1) = shape l2 ->
(a0 :: l1) ++ r1 = l2 ++ r2 -> a0 :: l1 = l2
r1, r2: list A
shape_eq: shape l1 = shape l2
H1: l1 ++ r1 = l2 ++ r2
a0 :: l1 = a0 :: l2 fequal.
A: Type
l1: list A
IHl1: forall l2 r1 r2 : list A,
shape l1 = shape l2 ->
l1 ++ r1 = l2 ++ r2 -> l1 = l2
a0: A
l2: list A
IHl2: forall r1 r2 : list A,
shape (a0 :: l1) = shape l2 ->
(a0 :: l1) ++ r1 = l2 ++ r2 -> a0 :: l1 = l2
r1, r2: list A
shape_eq: shape l1 = shape l2
H1: l1 ++ r1 = l2 ++ r2
l1 = l2 eauto.
  Qed.

  Theorem inv_app_eq_rl: forall (A: Type) (l1 l2 r1 r2: list A),
      shape r1 = shape r2 ->
      (l1 ++ r1 = l2 ++ r2) ->
      l1 = l2.
forall (A : Type) (l1 l2 r1 r2 : list A),
shape r1 = shape r2 -> l1 ++ r1 = l2 ++ r2 -> l1 = l2
  Proof.
forall (A : Type) (l1 l2 r1 r2 : list A),
shape r1 = shape r2 -> l1 ++ r1 = l2 ++ r2 -> l1 = l2
    intros A.
A: Type
forall l1 l2 r1 r2 : list A,
shape r1 = shape r2 -> l1 ++ r1 = l2 ++ r2 -> l1 = l2 induction l1 as [| ? ? IHl1 ];
      induction l2 as [| ? ? IHl2 ].
A: Type
forall r1 r2 : list A,
shape r1 = shape r2 -> [] ++ r1 = [] ++ r2 -> [] = []
A: Type
a: A
l2: list A
IHl2: forall r1 r2 : list A,
shape r1 = shape r2 ->
[] ++ r1 = l2 ++ r2 -> [] = l2
forall r1 r2 : list A,
shape r1 = shape r2 ->
[] ++ r1 = (a :: l2) ++ r2 -> [] = a :: l2
A: Type
a: A
l1: list A
IHl1: forall l2 r1 r2 : list A,
shape r1 = shape r2 ->
l1 ++ r1 = l2 ++ r2 -> l1 = l2
forall r1 r2 : list A,
shape r1 = shape r2 ->
(a :: l1) ++ r1 = [] ++ r2 -> a :: l1 = []
A: Type
a: A
l1: list A
IHl1: forall l2 r1 r2 : list A,
shape r1 = shape r2 ->
l1 ++ r1 = l2 ++ r2 -> l1 = l2
a0: A
l2: list A
IHl2: forall r1 r2 : list A,
shape r1 = shape r2 ->
(a :: l1) ++ r1 = l2 ++ r2 -> a :: l1 = l2
forall r1 r2 : list A,
shape r1 = shape r2 ->
(a :: l1) ++ r1 = (a0 :: l2) ++ r2 ->
a :: l1 = a0 :: l2
    -
A: Type
forall r1 r2 : list A,
shape r1 = shape r2 -> [] ++ r1 = [] ++ r2 -> [] = [] reflexivity.
    -
A: Type
a: A
l2: list A
IHl2: forall r1 r2 : list A,
shape r1 = shape r2 ->
[] ++ r1 = l2 ++ r2 -> [] = l2
forall r1 r2 : list A,
shape r1 = shape r2 ->
[] ++ r1 = (a :: l2) ++ r2 -> [] = a :: l2 introv shape_eq heq.
A: Type
a: A
l2: list A
IHl2: forall r1 r2 : list A,
shape r1 = shape r2 ->
[] ++ r1 = l2 ++ r2 -> [] = l2
r1, r2: list A
shape_eq: shape r1 = shape r2
heq: [] ++ r1 = (a :: l2) ++ r2
[] = a :: l2 apply inv_app_eq_ll with (r1 := r1) (r2 := r2).
A: Type
a: A
l2: list A
IHl2: forall r1 r2 : list A,
shape r1 = shape r2 ->
[] ++ r1 = l2 ++ r2 -> [] = l2
r1, r2: list A
shape_eq: shape r1 = shape r2
heq: [] ++ r1 = (a :: l2) ++ r2
shape [] = shape (a :: l2)
A: Type
a: A
l2: list A
IHl2: forall r1 r2 : list A,
shape r1 = shape r2 ->
[] ++ r1 = l2 ++ r2 -> [] = l2
r1, r2: list A
shape_eq: shape r1 = shape r2
heq: [] ++ r1 = (a :: l2) ++ r2
[] ++ r1 = (a :: l2) ++ r2
      +
A: Type
a: A
l2: list A
IHl2: forall r1 r2 : list A,
shape r1 = shape r2 ->
[] ++ r1 = l2 ++ r2 -> [] = l2
r1, r2: list A
shape_eq: shape r1 = shape r2
heq: [] ++ r1 = (a :: l2) ++ r2
shape [] = shape (a :: l2) rewrite <- shape_eq_app_r.
A: Type
a: A
l2: list A
IHl2: forall r1 r2 : list A,
shape r1 = shape r2 ->
[] ++ r1 = l2 ++ r2 -> [] = l2
r1, r2: list A
shape_eq: shape r1 = shape r2
heq: [] ++ r1 = (a :: l2) ++ r2
shape ([] ++ ?Goal3) = shape ((a :: l2) ++ ?Goal4)
A: Type
a: A
l2: list A
IHl2: forall r1 r2 : list A,
shape r1 = shape r2 ->
[] ++ r1 = l2 ++ r2 -> [] = l2
r1, r2: list A
shape_eq: shape r1 = shape r2
heq: [] ++ r1 = (a :: l2) ++ r2
shape ?Goal3 = shape ?Goal4 now rewrite heq.
A: Type
a: A
l2: list A
IHl2: forall r1 r2 : list A,
shape r1 = shape r2 ->
[] ++ r1 = l2 ++ r2 -> [] = l2
r1, r2: list A
shape_eq: shape r1 = shape r2
heq: [] ++ r1 = (a :: l2) ++ r2
shape r1 = shape r2 auto.
      +
A: Type
a: A
l2: list A
IHl2: forall r1 r2 : list A,
shape r1 = shape r2 ->
[] ++ r1 = l2 ++ r2 -> [] = l2
r1, r2: list A
shape_eq: shape r1 = shape r2
heq: [] ++ r1 = (a :: l2) ++ r2
[] ++ r1 = (a :: l2) ++ r2 assumption.
    -
A: Type
a: A
l1: list A
IHl1: forall l2 r1 r2 : list A,
shape r1 = shape r2 ->
l1 ++ r1 = l2 ++ r2 -> l1 = l2
forall r1 r2 : list A,
shape r1 = shape r2 ->
(a :: l1) ++ r1 = [] ++ r2 -> a :: l1 = [] introv shape_eq heq.
A: Type
a: A
l1: list A
IHl1: forall l2 r1 r2 : list A,
shape r1 = shape r2 ->
l1 ++ r1 = l2 ++ r2 -> l1 = l2
r1, r2: list A
shape_eq: shape r1 = shape r2
heq: (a :: l1) ++ r1 = [] ++ r2
a :: l1 = [] apply inv_app_eq_ll with (r1 := r1) (r2 := r2).
A: Type
a: A
l1: list A
IHl1: forall l2 r1 r2 : list A,
shape r1 = shape r2 ->
l1 ++ r1 = l2 ++ r2 -> l1 = l2
r1, r2: list A
shape_eq: shape r1 = shape r2
heq: (a :: l1) ++ r1 = [] ++ r2
shape (a :: l1) = shape []
A: Type
a: A
l1: list A
IHl1: forall l2 r1 r2 : list A,
shape r1 = shape r2 ->
l1 ++ r1 = l2 ++ r2 -> l1 = l2
r1, r2: list A
shape_eq: shape r1 = shape r2
heq: (a :: l1) ++ r1 = [] ++ r2
(a :: l1) ++ r1 = [] ++ r2
      +
A: Type
a: A
l1: list A
IHl1: forall l2 r1 r2 : list A,
shape r1 = shape r2 ->
l1 ++ r1 = l2 ++ r2 -> l1 = l2
r1, r2: list A
shape_eq: shape r1 = shape r2
heq: (a :: l1) ++ r1 = [] ++ r2
shape (a :: l1) = shape [] rewrite <- shape_eq_app_r.
A: Type
a: A
l1: list A
IHl1: forall l2 r1 r2 : list A,
shape r1 = shape r2 ->
l1 ++ r1 = l2 ++ r2 -> l1 = l2
r1, r2: list A
shape_eq: shape r1 = shape r2
heq: (a :: l1) ++ r1 = [] ++ r2
shape ((a :: l1) ++ ?Goal2) = shape ([] ++ ?Goal3)
A: Type
a: A
l1: list A
IHl1: forall l2 r1 r2 : list A,
shape r1 = shape r2 ->
l1 ++ r1 = l2 ++ r2 -> l1 = l2
r1, r2: list A
shape_eq: shape r1 = shape r2
heq: (a :: l1) ++ r1 = [] ++ r2
shape ?Goal2 = shape ?Goal3 now rewrite heq.
A: Type
a: A
l1: list A
IHl1: forall l2 r1 r2 : list A,
shape r1 = shape r2 ->
l1 ++ r1 = l2 ++ r2 -> l1 = l2
r1, r2: list A
shape_eq: shape r1 = shape r2
heq: (a :: l1) ++ r1 = [] ++ r2
shape r1 = shape r2 auto.
      +
A: Type
a: A
l1: list A
IHl1: forall l2 r1 r2 : list A,
shape r1 = shape r2 ->
l1 ++ r1 = l2 ++ r2 -> l1 = l2
r1, r2: list A
shape_eq: shape r1 = shape r2
heq: (a :: l1) ++ r1 = [] ++ r2
(a :: l1) ++ r1 = [] ++ r2 assumption.
    -
A: Type
a: A
l1: list A
IHl1: forall l2 r1 r2 : list A,
shape r1 = shape r2 ->
l1 ++ r1 = l2 ++ r2 -> l1 = l2
a0: A
l2: list A
IHl2: forall r1 r2 : list A,
shape r1 = shape r2 ->
(a :: l1) ++ r1 = l2 ++ r2 -> a :: l1 = l2
forall r1 r2 : list A,
shape r1 = shape r2 ->
(a :: l1) ++ r1 = (a0 :: l2) ++ r2 ->
a :: l1 = a0 :: l2 introv shape_eq heq.
A: Type
a: A
l1: list A
IHl1: forall l2 r1 r2 : list A,
shape r1 = shape r2 ->
l1 ++ r1 = l2 ++ r2 -> l1 = l2
a0: A
l2: list A
IHl2: forall r1 r2 : list A,
shape r1 = shape r2 ->
(a :: l1) ++ r1 = l2 ++ r2 -> a :: l1 = l2
r1, r2: list A
shape_eq: shape r1 = shape r2
heq: (a :: l1) ++ r1 = (a0 :: l2) ++ r2
a :: l1 = a0 :: l2
      rewrite <- 2(List.app_comm_cons) in heq.
A: Type
a: A
l1: list A
IHl1: forall l2 r1 r2 : list A,
shape r1 = shape r2 ->
l1 ++ r1 = l2 ++ r2 -> l1 = l2
a0: A
l2: list A
IHl2: forall r1 r2 : list A,
shape r1 = shape r2 ->
(a :: l1) ++ r1 = l2 ++ r2 -> a :: l1 = l2
r1, r2: list A
shape_eq: shape r1 = shape r2
heq: a :: l1 ++ r1 = a0 :: l2 ++ r2
a :: l1 = a0 :: l2
      inverts heq.
A: Type
l1: list A
IHl1: forall l2 r1 r2 : list A,
shape r1 = shape r2 ->
l1 ++ r1 = l2 ++ r2 -> l1 = l2
a0: A
l2: list A
IHl2: forall r1 r2 : list A,
shape r1 = shape r2 ->
(a0 :: l1) ++ r1 = l2 ++ r2 -> a0 :: l1 = l2
r1, r2: list A
shape_eq: shape r1 = shape r2
H1: l1 ++ r1 = l2 ++ r2
a0 :: l1 = a0 :: l2 fequal.
A: Type
l1: list A
IHl1: forall l2 r1 r2 : list A,
shape r1 = shape r2 ->
l1 ++ r1 = l2 ++ r2 -> l1 = l2
a0: A
l2: list A
IHl2: forall r1 r2 : list A,
shape r1 = shape r2 ->
(a0 :: l1) ++ r1 = l2 ++ r2 -> a0 :: l1 = l2
r1, r2: list A
shape_eq: shape r1 = shape r2
H1: l1 ++ r1 = l2 ++ r2
l1 = l2 eauto.
  Qed.

  Theorem inv_app_eq_lr: forall (A: Type) (l1 l2 r1 r2: list A),
      shape l1 = shape l2 ->
      (l1 ++ r1 = l2 ++ r2) ->
      r1 = r2.
forall (A : Type) (l1 l2 r1 r2 : list A),
shape l1 = shape l2 -> l1 ++ r1 = l2 ++ r2 -> r1 = r2
  Proof.
forall (A : Type) (l1 l2 r1 r2 : list A),
shape l1 = shape l2 -> l1 ++ r1 = l2 ++ r2 -> r1 = r2
    introv hyp1 hyp2.
A: Type
l1, l2, r1, r2: list A
hyp1: shape l1 = shape l2
hyp2: l1 ++ r1 = l2 ++ r2
r1 = r2 enough (l1 = l2).
A: Type
l1, l2, r1, r2: list A
hyp1: shape l1 = shape l2
hyp2: l1 ++ r1 = l2 ++ r2
H: l1 = l2
r1 = r2
A: Type
l1, l2, r1, r2: list A
hyp1: shape l1 = shape l2
hyp2: l1 ++ r1 = l2 ++ r2
l1 = l2
    {
A: Type
l1, l2, r1, r2: list A
hyp1: shape l1 = shape l2
hyp2: l1 ++ r1 = l2 ++ r2
H: l1 = l2
r1 = r2 subst.
A: Type
l2, r1, r2: list A
hyp2: l2 ++ r1 = l2 ++ r2
hyp1: shape l2 = shape l2
r1 = r2 eauto using List.app_inv_head. }
A: Type
l1, l2, r1, r2: list A
hyp1: shape l1 = shape l2
hyp2: l1 ++ r1 = l2 ++ r2
l1 = l2
    {
A: Type
l1, l2, r1, r2: list A
hyp1: shape l1 = shape l2
hyp2: l1 ++ r1 = l2 ++ r2
l1 = l2 eauto using inv_app_eq_ll. }
  Qed.

  Theorem inv_app_eq_rr: forall (A: Type) (l1 l2 r1 r2: list A),
      shape r1 = shape r2 ->
      (l1 ++ r1 = l2 ++ r2) ->
      r1 = r2.
forall (A : Type) (l1 l2 r1 r2 : list A),
shape r1 = shape r2 -> l1 ++ r1 = l2 ++ r2 -> r1 = r2
  Proof.
forall (A : Type) (l1 l2 r1 r2 : list A),
shape r1 = shape r2 -> l1 ++ r1 = l2 ++ r2 -> r1 = r2
    introv hyp1 hyp2.
A: Type
l1, l2, r1, r2: list A
hyp1: shape r1 = shape r2
hyp2: l1 ++ r1 = l2 ++ r2
r1 = r2 enough (l1 = l2).
A: Type
l1, l2, r1, r2: list A
hyp1: shape r1 = shape r2
hyp2: l1 ++ r1 = l2 ++ r2
H: l1 = l2
r1 = r2
A: Type
l1, l2, r1, r2: list A
hyp1: shape r1 = shape r2
hyp2: l1 ++ r1 = l2 ++ r2
l1 = l2
    {
A: Type
l1, l2, r1, r2: list A
hyp1: shape r1 = shape r2
hyp2: l1 ++ r1 = l2 ++ r2
H: l1 = l2
r1 = r2 subst.
A: Type
l2, r1, r2: list A
hyp1: shape r1 = shape r2
hyp2: l2 ++ r1 = l2 ++ r2
r1 = r2 eauto using List.app_inv_head. }
A: Type
l1, l2, r1, r2: list A
hyp1: shape r1 = shape r2
hyp2: l1 ++ r1 = l2 ++ r2
l1 = l2
    {
A: Type
l1, l2, r1, r2: list A
hyp1: shape r1 = shape r2
hyp2: l1 ++ r1 = l2 ++ r2
l1 = l2 eauto using inv_app_eq_rl. }
  Qed.

  Theorem inv_app_eq: forall (A: Type) (l1 l2 r1 r2: list A),
      shape l1 = shape l2 \/ shape r1 = shape r2 ->
      (l1 ++ r1 = l2 ++ r2) <-> (l1 = l2 /\ r1 = r2).
forall (A : Type) (l1 l2 r1 r2 : list A),
shape l1 = shape l2 \/ shape r1 = shape r2 ->
l1 ++ r1 = l2 ++ r2 <-> l1 = l2 /\ r1 = r2
  Proof.
forall (A : Type) (l1 l2 r1 r2 : list A),
shape l1 = shape l2 \/ shape r1 = shape r2 ->
l1 ++ r1 = l2 ++ r2 <-> l1 = l2 /\ r1 = r2
    introv [hyp | hyp]; split.
A: Type
l1, l2, r1, r2: list A
hyp: shape l1 = shape l2
l1 ++ r1 = l2 ++ r2 -> l1 = l2 /\ r1 = r2
A: Type
l1, l2, r1, r2: list A
hyp: shape l1 = shape l2
l1 = l2 /\ r1 = r2 -> l1 ++ r1 = l2 ++ r2
A: Type
l1, l2, r1, r2: list A
hyp: shape r1 = shape r2
l1 ++ r1 = l2 ++ r2 -> l1 = l2 /\ r1 = r2
A: Type
l1, l2, r1, r2: list A
hyp: shape r1 = shape r2
l1 = l2 /\ r1 = r2 -> l1 ++ r1 = l2 ++ r2
    -
A: Type
l1, l2, r1, r2: list A
hyp: shape l1 = shape l2
l1 ++ r1 = l2 ++ r2 -> l1 = l2 /\ r1 = r2 introv heq.
A: Type
l1, l2, r1, r2: list A
hyp: shape l1 = shape l2
heq: l1 ++ r1 = l2 ++ r2
l1 = l2 /\ r1 = r2 split.
A: Type
l1, l2, r1, r2: list A
hyp: shape l1 = shape l2
heq: l1 ++ r1 = l2 ++ r2
l1 = l2
A: Type
l1, l2, r1, r2: list A
hyp: shape l1 = shape l2
heq: l1 ++ r1 = l2 ++ r2
r1 = r2 eapply inv_app_eq_ll; eauto.
A: Type
l1, l2, r1, r2: list A
hyp: shape l1 = shape l2
heq: l1 ++ r1 = l2 ++ r2
r1 = r2
      eapply inv_app_eq_lr; eauto.
    -
A: Type
l1, l2, r1, r2: list A
hyp: shape l1 = shape l2
l1 = l2 /\ r1 = r2 -> l1 ++ r1 = l2 ++ r2 introv [? ?].
A: Type
l1, l2, r1, r2: list A
hyp: shape l1 = shape l2
H: l1 = l2
H0: r1 = r2
l1 ++ r1 = l2 ++ r2 now subst.
    -
A: Type
l1, l2, r1, r2: list A
hyp: shape r1 = shape r2
l1 ++ r1 = l2 ++ r2 -> l1 = l2 /\ r1 = r2 introv heq.
A: Type
l1, l2, r1, r2: list A
hyp: shape r1 = shape r2
heq: l1 ++ r1 = l2 ++ r2
l1 = l2 /\ r1 = r2 split.
A: Type
l1, l2, r1, r2: list A
hyp: shape r1 = shape r2
heq: l1 ++ r1 = l2 ++ r2
l1 = l2
A: Type
l1, l2, r1, r2: list A
hyp: shape r1 = shape r2
heq: l1 ++ r1 = l2 ++ r2
r1 = r2 eapply inv_app_eq_rl; eauto.
A: Type
l1, l2, r1, r2: list A
hyp: shape r1 = shape r2
heq: l1 ++ r1 = l2 ++ r2
r1 = r2
      eapply inv_app_eq_rr; eauto.
    -
A: Type
l1, l2, r1, r2: list A
hyp: shape r1 = shape r2
l1 = l2 /\ r1 = r2 -> l1 ++ r1 = l2 ++ r2 introv [? ?].
A: Type
l1, l2, r1, r2: list A
hyp: shape r1 = shape r2
H: l1 = l2
H0: r1 = r2
l1 ++ r1 = l2 ++ r2 now subst.
  Qed.

  Lemma list_app_inv_r: forall (A: Type) (l l1 l2: list A),
      l ++ l1 = l ++ l2 -> l1 = l2.
forall (A : Type) (l l1 l2 : list A),
l ++ l1 = l ++ l2 -> l1 = l2
  Proof.
forall (A : Type) (l l1 l2 : list A),
l ++ l1 = l ++ l2 -> l1 = l2
    introv hyp.
A: Type
l, l1, l2: list A
hyp: l ++ l1 = l ++ l2
l1 = l2 induction l.
A: Type
l1, l2: list A
hyp: [] ++ l1 = [] ++ l2
l1 = l2
A: Type
a: A
l, l1, l2: list A
hyp: (a :: l) ++ l1 = (a :: l) ++ l2
IHl: l ++ l1 = l ++ l2 -> l1 = l2
l1 = l2
    -
A: Type
l1, l2: list A
hyp: [] ++ l1 = [] ++ l2
l1 = l2 cbn in hyp.
A: Type
l1, l2: list A
hyp: l1 = l2
l1 = l2 auto.
    -
A: Type
a: A
l, l1, l2: list A
hyp: (a :: l) ++ l1 = (a :: l) ++ l2
IHl: l ++ l1 = l ++ l2 -> l1 = l2
l1 = l2 inversion hyp.
A: Type
a: A
l, l1, l2: list A
hyp: (a :: l) ++ l1 = (a :: l) ++ l2
IHl: l ++ l1 = l ++ l2 -> l1 = l2
H0: l ++ l1 = l ++ l2
l1 = l2 auto.
  Qed.

  Lemma list_app_inv_l: forall (A: Type) (l l1 l2: list A),
      l1 ++ l = l2 ++ l -> l1 = l2.
forall (A : Type) (l l1 l2 : list A),
l1 ++ l = l2 ++ l -> l1 = l2
  Proof.
forall (A : Type) (l l1 l2 : list A),
l1 ++ l = l2 ++ l -> l1 = l2
    introv hyp.
A: Type
l, l1, l2: list A
hyp: l1 ++ l = l2 ++ l
l1 = l2 eapply inv_app_eq_rl.
A: Type
l, l1, l2: list A
hyp: l1 ++ l = l2 ++ l
shape ?r1 = shape ?r2
A: Type
l, l1, l2: list A
hyp: l1 ++ l = l2 ++ l
l1 ++ ?r1 = l2 ++ ?r2
    2: eauto.
A: Type
l, l1, l2: list A
hyp: l1 ++ l = l2 ++ l
shape l = shape l reflexivity.
  Qed.

  Lemma list_app_inv_l2: forall (A: Type) (l1 l2: list A) (a1 a2: A),
      l1 ++ ret a1 = l2 ++ ret a2 ->
      l1 = l2.
forall (A : Type) (l1 l2 : list A) (a1 a2 : A),
l1 ++ ret a1 = l2 ++ ret a2 -> l1 = l2
  Proof.
forall (A : Type) (l1 l2 : list A) (a1 a2 : A),
l1 ++ ret a1 = l2 ++ ret a2 -> l1 = l2
    intros.
A: Type
l1, l2: list A
a1, a2: A
H: l1 ++ ret a1 = l2 ++ ret a2
l1 = l2 eapply inv_app_eq_rl; [|eauto]; auto.
  Qed.

  Lemma list_app_inv_r2: forall (A: Type) (l1 l2: list A) (a1 a2: A),
      l1 ++ [a1] = l2 ++ [a2] ->
      a1 = a2.
forall (A : Type) (l1 l2 : list A) (a1 a2 : A),
l1 ++ [a1] = l2 ++ [a2] -> a1 = a2
  Proof.
forall (A : Type) (l1 l2 : list A) (a1 a2 : A),
l1 ++ [a1] = l2 ++ [a2] -> a1 = a2
    introv.
A: Type
l1, l2: list A
a1, a2: A
l1 ++ [a1] = l2 ++ [a2] -> a1 = a2 introv hyp.
A: Type
l1, l2: list A
a1, a2: A
hyp: l1 ++ [a1] = l2 ++ [a2]
a1 = a2
    apply inv_app_eq_rr in hyp.
A: Type
l1, l2: list A
a1, a2: A
hyp: [a1] = [a2]
a1 = a2
A: Type
l1, l2: list A
a1, a2: A
hyp: l1 ++ [a1] = l2 ++ [a2]
shape [a1] = shape [a2]
    now inversion hyp.
A: Type
l1, l2: list A
a1, a2: A
hyp: l1 ++ [a1] = l2 ++ [a2]
shape [a1] = shape [a2] easy.
  Qed.

End list_shape_lemmas.

(** * Reasoning principles for <<shape>> on listable functors *)
(**********************************************************************)
Section listable_shape_lemmas.

  Context
    `{Functor F}
    `{Tolist F}
    `{! Natural (@tolist F _)}.

  (* Values with the same shape have equal-length contents *)
  Lemma shape_tolist: forall `(t: F A) `(u: F B),
      shape t = shape u ->
      shape (tolist t) = shape (tolist u).
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
forall (A : Type) (t : F A) (B : Type) (u : F B),
shape t = shape u ->
shape (tolist t) = shape (tolist u)
  Proof.
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
forall (A : Type) (t : F A) (B : Type) (u : F B),
shape t = shape u ->
shape (tolist t) = shape (tolist u)
    introv heq.
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
A: Type
t: F A
B: Type
u: F B
heq: shape t = shape u
shape (tolist t) = shape (tolist u) compose near t.
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
A: Type
t: F A
B: Type
u: F B
heq: shape t = shape u
(shape ∘ tolist) t = shape (tolist u) compose near u.
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
A: Type
t: F A
B: Type
u: F B
heq: shape t = shape u
(shape ∘ tolist) t = (shape ∘ tolist) u
    unfold shape in *.
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
A: Type
t: F A
B: Type
u: F B
heq: map (const tt) t = map (const tt) u
(map (const tt) ∘ tolist) t =
(map (const tt) ∘ tolist) u rewrite 2(natural).
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
A: Type
t: F A
B: Type
u: F B
heq: map (const tt) t = map (const tt) u
(tolist ∘ map (const tt)) t =
(tolist ∘ map (const tt)) u
    unfold compose.
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
A: Type
t: F A
B: Type
u: F B
heq: map (const tt) t = map (const tt) u
tolist (map (const tt) t) = tolist (map (const tt) u)
    fequal.
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
A: Type
t: F A
B: Type
u: F B
heq: map (const tt) t = map (const tt) u
map (const tt) t = map (const tt) u apply heq.
  Qed.

  Corollary shape_l: forall (A: Type) (l1 l2: F A) (x y: list A),
      shape l1 = shape l2 ->
      (tolist l1 ++ x = tolist l2 ++ y) ->
      tolist l1 = tolist l2.
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
forall (A : Type) (l1 l2 : F A) (x y : list A),
shape l1 = shape l2 ->
tolist l1 ++ x = tolist l2 ++ y ->
tolist l1 = tolist l2
  Proof.
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
forall (A : Type) (l1 l2 : F A) (x y : list A),
shape l1 = shape l2 ->
tolist l1 ++ x = tolist l2 ++ y ->
tolist l1 = tolist l2
    introv shape_eq heq.
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
A: Type
l1, l2: F A
x, y: list A
shape_eq: shape l1 = shape l2
heq: tolist l1 ++ x = tolist l2 ++ y
tolist l1 = tolist l2
    eauto using inv_app_eq_ll, shape_tolist.
  Qed.

  Corollary shape_r: forall (A: Type) (l1 l2: F A) (x y: list A),
      shape l1 = shape l2 ->
      (x ++ tolist l1 = y ++ tolist l2) ->
      tolist l1 = tolist l2.
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
forall (A : Type) (l1 l2 : F A) (x y : list A),
shape l1 = shape l2 ->
x ++ tolist l1 = y ++ tolist l2 ->
tolist l1 = tolist l2
  Proof.
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
forall (A : Type) (l1 l2 : F A) (x y : list A),
shape l1 = shape l2 ->
x ++ tolist l1 = y ++ tolist l2 ->
tolist l1 = tolist l2
    introv shape_eq heq.
F: Type -> Type
Map_F: Map F
H: Functor F
H0: Tolist F
Natural0: Natural (@tolist F H0)
A: Type
l1, l2: F A
x, y: list A
shape_eq: shape l1 = shape l2
heq: x ++ tolist l1 = y ++ tolist l2
tolist l1 = tolist l2
    eauto using inv_app_eq_rr, shape_tolist.
  Qed.

End listable_shape_lemmas.

(** * Quantification Over Elements *)
(* TODO: There is no real purpose for this at this point is there? *)
(**********************************************************************)
Section quantification.

  Definition Forall_List `(P: A -> Prop): list A -> Prop :=
    mapReduce_list (op := Monoid_op_and) (unit := Monoid_unit_true) P.

  Definition Forany_List `(P: A -> Prop): list A -> Prop :=
    mapReduce_list (op := Monoid_op_or) (unit := Monoid_unit_false) P.

  Lemma forall_iff `(P: A -> Prop) (l: list A):
    Forall_List P l <-> forall (a: A), a ∈ l -> P a.
A: Type
P: A -> Prop
l: list A
Forall_List P l <-> (forall a : A, a ∈ l -> P a)
  Proof.
A: Type
P: A -> Prop
l: list A
Forall_List P l <-> (forall a : A, a ∈ l -> P a)
    unfold Forall_List.
A: Type
P: A -> Prop
l: list A
mapReduce_list P l <-> (forall a : A, a ∈ l -> P a)
    induction l; autorewrite with tea_list tea_set.
A: Type
P: A -> Prop
Ƶ <-> (forall a : A, a ∈ [] -> P a)
A: Type
P: A -> Prop
a: A
l: list A
IHl: mapReduce_list P l <-> (forall a : A, a ∈ l -> P a)
P a ● mapReduce_list P l <->
(forall a0 : A, a0 ∈ (a :: l) -> P a0)
    -
A: Type
P: A -> Prop
Ƶ <-> (forall a : A, a ∈ [] -> P a) split.
A: Type
P: A -> Prop
Ƶ -> forall a : A, a ∈ [] -> P a
A: Type
P: A -> Prop
(forall a : A, a ∈ [] -> P a) -> Ƶ
      +
A: Type
P: A -> Prop
Ƶ -> forall a : A, a ∈ [] -> P a intros tt a contra.
A: Type
P: A -> Prop
tt: Ƶ
a: A
contra: a ∈ []
P a inversion contra.
      +
A: Type
P: A -> Prop
(forall a : A, a ∈ [] -> P a) -> Ƶ intros.
A: Type
P: A -> Prop
H: forall a : A, a ∈ [] -> P a
Ƶ exact I.
    -
A: Type
P: A -> Prop
a: A
l: list A
IHl: mapReduce_list P l <-> (forall a : A, a ∈ l -> P a)
P a ● mapReduce_list P l <->
(forall a0 : A, a0 ∈ (a :: l) -> P a0) setoid_rewrite element_of_list_cons.
A: Type
P: A -> Prop
a: A
l: list A
IHl: mapReduce_list P l <-> (forall a : A, a ∈ l -> P a)
P a ● mapReduce_list P l <->
(forall a0 : A, a0 = a \/ a0 ∈ l -> P a0)
      rewrite IHl.
A: Type
P: A -> Prop
a: A
l: list A
IHl: mapReduce_list P l <-> (forall a : A, a ∈ l -> P a)
P a ● (forall a : A, a ∈ l -> P a) <->
(forall a0 : A, a0 = a \/ a0 ∈ l -> P a0) split.
A: Type
P: A -> Prop
a: A
l: list A
IHl: mapReduce_list P l <-> (forall a : A, a ∈ l -> P a)
P a ● (forall a : A, a ∈ l -> P a) ->
forall a0 : A, a0 = a \/ a0 ∈ l -> P a0
A: Type
P: A -> Prop
a: A
l: list A
IHl: mapReduce_list P l <-> (forall a : A, a ∈ l -> P a)
(forall a0 : A, a0 = a \/ a0 ∈ l -> P a0) ->
P a ● (forall a : A, a ∈ l -> P a)
      +
A: Type
P: A -> Prop
a: A
l: list A
IHl: mapReduce_list P l <-> (forall a : A, a ∈ l -> P a)
P a ● (forall a : A, a ∈ l -> P a) ->
forall a0 : A, a0 = a \/ a0 ∈ l -> P a0 intros [Hpa Hrest].
A: Type
P: A -> Prop
a: A
l: list A
IHl: mapReduce_list P l <-> (forall a : A, a ∈ l -> P a)
Hpa: P a
Hrest: forall a : A, a ∈ l -> P a
forall a0 : A, a0 = a \/ a0 ∈ l -> P a0
        intros x [Heq | Hin].
A: Type
P: A -> Prop
a: A
l: list A
IHl: mapReduce_list P l <-> (forall a : A, a ∈ l -> P a)
Hpa: P a
Hrest: forall a : A, a ∈ l -> P a
x: A
Heq: x = a
P x
A: Type
P: A -> Prop
a: A
l: list A
IHl: mapReduce_list P l <->
(forall a : A, a ∈ l -> P a)
Hpa: P a
Hrest: forall a : A, a ∈ l -> P a
x: A
Hin: x ∈ l
P x
        now subst.
A: Type
P: A -> Prop
a: A
l: list A
IHl: mapReduce_list P l <-> (forall a : A, a ∈ l -> P a)
Hpa: P a
Hrest: forall a : A, a ∈ l -> P a
x: A
Hin: x ∈ l
P x auto.
      +
A: Type
P: A -> Prop
a: A
l: list A
IHl: mapReduce_list P l <-> (forall a : A, a ∈ l -> P a)
(forall a0 : A, a0 = a \/ a0 ∈ l -> P a0) ->
P a ● (forall a : A, a ∈ l -> P a) intros H.
A: Type
P: A -> Prop
a: A
l: list A
IHl: mapReduce_list P l <-> (forall a : A, a ∈ l -> P a)
H: forall a0 : A, a0 = a \/ a0 ∈ l -> P a0
P a ● (forall a : A, a ∈ l -> P a) split; auto.
  Qed.

  Lemma forany_iff `(P: A -> Prop) (l: list A):
    Forany_List P l <-> exists (a: A), a ∈ l /\ P a.
A: Type
P: A -> Prop
l: list A
Forany_List P l <-> (exists a : A, a ∈ l /\ P a)
  Proof.
A: Type
P: A -> Prop
l: list A
Forany_List P l <-> (exists a : A, a ∈ l /\ P a)
    unfold Forany_List.
A: Type
P: A -> Prop
l: list A
mapReduce_list P l <-> (exists a : A, a ∈ l /\ P a)
    induction l.
A: Type
P: A -> Prop
mapReduce_list P [] <-> (exists a : A, a ∈ [] /\ P a)
A: Type
P: A -> Prop
a: A
l: list A
IHl: mapReduce_list P l <-> (exists a : A, a ∈ l /\ P a)
mapReduce_list P (a :: l) <->
(exists a0 : A, a0 ∈ (a :: l) /\ P a0)
    -
A: Type
P: A -> Prop
mapReduce_list P [] <-> (exists a : A, a ∈ [] /\ P a) split.
A: Type
P: A -> Prop
mapReduce_list P [] -> exists a : A, a ∈ [] /\ P a
A: Type
P: A -> Prop
(exists a : A, a ∈ [] /\ P a) -> mapReduce_list P []
      +
A: Type
P: A -> Prop
mapReduce_list P [] -> exists a : A, a ∈ [] /\ P a intros [].
      +
A: Type
P: A -> Prop
(exists a : A, a ∈ [] /\ P a) -> mapReduce_list P [] intros [x [contra Hrest]].
A: Type
P: A -> Prop
x: A
contra: x ∈ []
Hrest: P x
mapReduce_list P [] inversion contra.
    -
A: Type
P: A -> Prop
a: A
l: list A
IHl: mapReduce_list P l <-> (exists a : A, a ∈ l /\ P a)
mapReduce_list P (a :: l) <->
(exists a0 : A, a0 ∈ (a :: l) /\ P a0) autorewrite with tea_list tea_set.
A: Type
P: A -> Prop
a: A
l: list A
IHl: mapReduce_list P l <-> (exists a : A, a ∈ l /\ P a)
P a ● mapReduce_list P l <->
(exists a0 : A, a0 ∈ (a :: l) /\ P a0)
      setoid_rewrite element_of_list_cons.
A: Type
P: A -> Prop
a: A
l: list A
IHl: mapReduce_list P l <-> (exists a : A, a ∈ l /\ P a)
P a ● mapReduce_list P l <->
(exists a0 : A, (a0 = a \/ a0 ∈ l) /\ P a0)
      unfold subset_one.
A: Type
P: A -> Prop
a: A
l: list A
IHl: mapReduce_list P l <-> (exists a : A, a ∈ l /\ P a)
P a ● mapReduce_list P l <->
(exists a0 : A, (a0 = a \/ a0 ∈ l) /\ P a0)
      rewrite IHl.
A: Type
P: A -> Prop
a: A
l: list A
IHl: mapReduce_list P l <-> (exists a : A, a ∈ l /\ P a)
P a ● (exists a : A, a ∈ l /\ P a) <->
(exists a0 : A, (a0 = a \/ a0 ∈ l) /\ P a0) split.
A: Type
P: A -> Prop
a: A
l: list A
IHl: mapReduce_list P l <-> (exists a : A, a ∈ l /\ P a)
P a ● (exists a : A, a ∈ l /\ P a) ->
exists a0 : A, (a0 = a \/ a0 ∈ l) /\ P a0
A: Type
P: A -> Prop
a: A
l: list A
IHl: mapReduce_list P l <-> (exists a : A, a ∈ l /\ P a)
(exists a0 : A, (a0 = a \/ a0 ∈ l) /\ P a0) ->
P a ● (exists a : A, a ∈ l /\ P a)
      +
A: Type
P: A -> Prop
a: A
l: list A
IHl: mapReduce_list P l <-> (exists a : A, a ∈ l /\ P a)
P a ● (exists a : A, a ∈ l /\ P a) ->
exists a0 : A, (a0 = a \/ a0 ∈ l) /\ P a0 intros [Hpa | Hrest].
A: Type
P: A -> Prop
a: A
l: list A
IHl: mapReduce_list P l <-> (exists a : A, a ∈ l /\ P a)
Hpa: P a
exists a0 : A, (a0 = a \/ a0 ∈ l) /\ P a0
A: Type
P: A -> Prop
a: A
l: list A
IHl: mapReduce_list P l <-> (exists a : A, a ∈ l /\ P a)
Hrest: exists a : A, a ∈ l /\ P a
exists a0 : A, (a0 = a \/ a0 ∈ l) /\ P a0
        exists a.
A: Type
P: A -> Prop
a: A
l: list A
IHl: mapReduce_list P l <-> (exists a : A, a ∈ l /\ P a)
Hpa: P a
(a = a \/ a ∈ l) /\ P a
A: Type
P: A -> Prop
a: A
l: list A
IHl: mapReduce_list P l <-> (exists a : A, a ∈ l /\ P a)
Hrest: exists a : A, a ∈ l /\ P a
exists a0 : A, (a0 = a \/ a0 ∈ l) /\ P a0 auto.
A: Type
P: A -> Prop
a: A
l: list A
IHl: mapReduce_list P l <-> (exists a : A, a ∈ l /\ P a)
Hrest: exists a : A, a ∈ l /\ P a
exists a0 : A, (a0 = a \/ a0 ∈ l) /\ P a0
        destruct Hrest as [x [H1 H2]].
A: Type
P: A -> Prop
a: A
l: list A
IHl: mapReduce_list P l <-> (exists a : A, a ∈ l /\ P a)
x: A
H1: x ∈ l
H2: P x
exists a0 : A, (a0 = a \/ a0 ∈ l) /\ P a0
        exists x.
A: Type
P: A -> Prop
a: A
l: list A
IHl: mapReduce_list P l <-> (exists a : A, a ∈ l /\ P a)
x: A
H1: x ∈ l
H2: P x
(x = a \/ x ∈ l) /\ P x auto.
      +
A: Type
P: A -> Prop
a: A
l: list A
IHl: mapReduce_list P l <-> (exists a : A, a ∈ l /\ P a)
(exists a0 : A, (a0 = a \/ a0 ∈ l) /\ P a0) ->
P a ● (exists a : A, a ∈ l /\ P a) intros [x [[H1 | H2] H3]].
A: Type
P: A -> Prop
a: A
l: list A
IHl: mapReduce_list P l <-> (exists a : A, a ∈ l /\ P a)
x: A
H1: x = a
H3: P x
P a ● (exists a : A, a ∈ l /\ P a)
A: Type
P: A -> Prop
a: A
l: list A
IHl: mapReduce_list P l <-> (exists a : A, a ∈ l /\ P a)
x: A
H2: x ∈ l
H3: P x
P a ● (exists a : A, a ∈ l /\ P a)
        subst.
A: Type
P: A -> Prop
a: A
l: list A
IHl: mapReduce_list P l <-> (exists a : A, a ∈ l /\ P a)
H3: P a
P a ● (exists a : A, a ∈ l /\ P a)
A: Type
P: A -> Prop
a: A
l: list A
IHl: mapReduce_list P l <-> (exists a : A, a ∈ l /\ P a)
x: A
H2: x ∈ l
H3: P x
P a ● (exists a : A, a ∈ l /\ P a) now left.
A: Type
P: A -> Prop
a: A
l: list A
IHl: mapReduce_list P l <-> (exists a : A, a ∈ l /\ P a)
x: A
H2: x ∈ l
H3: P x
P a ● (exists a : A, a ∈ l /\ P a)
        right.
A: Type
P: A -> Prop
a: A
l: list A
IHl: mapReduce_list P l <-> (exists a : A, a ∈ l /\ P a)
x: A
H2: x ∈ l
H3: P x
exists a : A, a ∈ l /\ P a eexists; eauto.
  Qed.

End quantification.

(** ** <<a ∈ ->> in terms of <<mapReduce_list>> *)
(**********************************************************************)
Lemma element_to_mapReduce_list1: forall (A: Type),
    tosubset = mapReduce_list (ret (T := subset) (A := A)).
forall A : Type, tosubset = mapReduce_list ret
Proof.
forall A : Type, tosubset = mapReduce_list ret
  intros.
A: Type
tosubset = mapReduce_list ret ext l.
A: Type
l: list A
tosubset l = mapReduce_list ret l induction l.
A: Type
tosubset [] = mapReduce_list ret []
A: Type
a: A
l: list A
IHl: tosubset l = mapReduce_list ret l
tosubset (a :: l) = mapReduce_list ret (a :: l)
  -
A: Type
tosubset [] = mapReduce_list ret [] reflexivity.
  -
A: Type
a: A
l: list A
IHl: tosubset l = mapReduce_list ret l
tosubset (a :: l) = mapReduce_list ret (a :: l) cbn.
A: Type
a: A
l: list A
IHl: tosubset l = mapReduce_list ret l
tosubset (a :: l) = ret a ● crush_list (map ret l) autorewrite with tea_list.
A: Type
a: A
l: list A
IHl: tosubset l = mapReduce_list ret l
{{a}} ∪ tosubset l = ret a ● crush_list (map ret l)
    rewrite IHl.
A: Type
a: A
l: list A
IHl: tosubset l = mapReduce_list ret l
{{a}} ∪ mapReduce_list ret l =
ret a ● crush_list (map ret l)
    reflexivity.
Qed.

Lemma element_to_mapReduce_list2: forall (A: Type) (l: list A) (a: A),
    tosubset l a = mapReduce_list (op := or) (unit := False) (eq a) l.
forall (A : Type) (l : list A) (a : A),
tosubset l a = mapReduce_list (eq a) l
Proof.
forall (A : Type) (l : list A) (a : A),
tosubset l a = mapReduce_list (eq a) l
  intros.
A: Type
l: list A
a: A
tosubset l a = mapReduce_list (eq a) l rewrite element_to_mapReduce_list1.
A: Type
l: list A
a: A
mapReduce_list ret l a = mapReduce_list (eq a) l
  (*
    change_left ((evalAt a ∘ mapReduce_list (ret (T := subset))) l).
   *)
  induction l.
A: Type
a: A
mapReduce_list ret [] a = mapReduce_list (eq a) []
A: Type
a0: A
l: list A
a: A
IHl: mapReduce_list ret l a = mapReduce_list (eq a) l
mapReduce_list ret (a0 :: l) a =
mapReduce_list (eq a) (a0 :: l)
  -
A: Type
a: A
mapReduce_list ret [] a = mapReduce_list (eq a) [] reflexivity.
  -
A: Type
a0: A
l: list A
a: A
IHl: mapReduce_list ret l a = mapReduce_list (eq a) l
mapReduce_list ret (a0 :: l) a =
mapReduce_list (eq a) (a0 :: l) rewrite mapReduce_list_cons.
A: Type
a0: A
l: list A
a: A
IHl: mapReduce_list ret l a = mapReduce_list (eq a) l
(ret a0 ● mapReduce_list ret l) a =
mapReduce_list (eq a) (a0 :: l)
    rewrite mapReduce_list_cons.
A: Type
a0: A
l: list A
a: A
IHl: mapReduce_list ret l a = mapReduce_list (eq a) l
(ret a0 ● mapReduce_list ret l) a =
(a = a0) ● mapReduce_list (eq a) l
    rewrite <- IHl.
A: Type
a0: A
l: list A
a: A
IHl: mapReduce_list ret l a = mapReduce_list (eq a) l
(ret a0 ● mapReduce_list ret l) a =
(a = a0) ● mapReduce_list ret l a
    replace (a = a0) with (a0 = a) by (propext; auto).
A: Type
a0: A
l: list A
a: A
IHl: mapReduce_list ret l a = mapReduce_list (eq a) l
(ret a0 ● mapReduce_list ret l) a =
(a0 = a) ● mapReduce_list ret l a
    reflexivity.
Qed.

(** ** Rewriting Laws for <<mapReduce>> *)
(**********************************************************************)
Section mapReduce_rw.

  Context
    {A M: Type}
    `{Monoid M}
    (f: A -> M).

  Lemma mapReduce_nil: mapReduce f (@nil A) = Ƶ.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
f: A -> M
mapReduce f [] = Ƶ
  Proof.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
f: A -> M
mapReduce f [] = Ƶ
    reflexivity.
  Qed.

  Lemma mapReduce_cons: forall (x: A) (xs: list A),
      mapReduce f (x :: xs) = f x ● mapReduce f xs.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
f: A -> M
forall (x : A) (xs : list A),
mapReduce f (x :: xs) = f x ● mapReduce f xs
  Proof.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
f: A -> M
forall (x : A) (xs : list A),
mapReduce f (x :: xs) = f x ● mapReduce f xs
    intros.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
f: A -> M
x: A
xs: list A
mapReduce f (x :: xs) = f x ● mapReduce f xs
    rewrite mapReduce_eq_mapReduce_list.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
f: A -> M
x: A
xs: list A
mapReduce_list f (x :: xs) = f x ● mapReduce_list f xs
    simpl_list.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
f: A -> M
x: A
xs: list A
f x ● mapReduce_list f xs = f x ● mapReduce_list f xs
    reflexivity.
  Qed.

  Lemma mapReduce_one (a: A): mapReduce f [ a ] = f a.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
f: A -> M
a: A
mapReduce f [a] = f a
  Proof.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
f: A -> M
a: A
mapReduce f [a] = f a
    rewrite mapReduce_eq_mapReduce_list.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
f: A -> M
a: A
mapReduce_list f [a] = f a
    simpl_list; auto.
  Qed.

  Lemma mapReduce_ret: mapReduce f ∘ ret = f.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
f: A -> M
mapReduce f ∘ ret = f
  Proof.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
f: A -> M
mapReduce f ∘ ret = f
    rewrite mapReduce_eq_mapReduce_list.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
f: A -> M
mapReduce_list f ∘ ret = f
    rewrite mapReduce_list_ret.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
f: A -> M
f = f
    reflexivity.
  Qed.

  Lemma mapReduce_app: forall (l1 l2: list A),
      mapReduce f (l1 ++ l2) = mapReduce f l1 ● mapReduce f l2.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
f: A -> M
forall l1 l2 : list A,
mapReduce f (l1 ++ l2) =
mapReduce f l1 ● mapReduce f l2
  Proof.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
f: A -> M
forall l1 l2 : list A,
mapReduce f (l1 ++ l2) =
mapReduce f l1 ● mapReduce f l2
    intros.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
f: A -> M
l1, l2: list A
mapReduce f (l1 ++ l2) =
mapReduce f l1 ● mapReduce f l2
    rewrite mapReduce_eq_mapReduce_list.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
f: A -> M
l1, l2: list A
mapReduce_list f (l1 ++ l2) =
mapReduce_list f l1 ● mapReduce_list f l2
    rewrite mapReduce_list_app.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
f: A -> M
l1, l2: list A
mapReduce_list f l1 ● mapReduce_list f l2 =
mapReduce_list f l1 ● mapReduce_list f l2
    reflexivity.
  Qed.

End mapReduce_rw.

#[export] Hint Rewrite @mapReduce_nil @mapReduce_cons
  @mapReduce_one @mapReduce_app: tea_list.

Lemma mapReduce_ret_id: forall A, mapReduce (@ret list _ A) = id.
forall A : Type, mapReduce ret = id
Proof.
forall A : Type, mapReduce ret = id
  intros.
A: Type
mapReduce ret = id
  rewrite mapReduce_eq_mapReduce_list.
A: Type
mapReduce_list ret = id
  apply mapReduce_list_ret_id.
Qed.

(** * Specification of <<Permutation>> *)
(**********************************************************************)
From Coq Require Import Sorting.Permutation.

Theorem permutation_spec: forall {A} {l1 l2: list A},
    Permutation l1 l2 -> (forall a, a ∈ l1 <-> a ∈ l2).
forall (A : Type) (l1 l2 : list A),
Permutation l1 l2 -> forall a : A, a ∈ l1 <-> a ∈ l2
Proof.
forall (A : Type) (l1 l2 : list A),
Permutation l1 l2 -> forall a : A, a ∈ l1 <-> a ∈ l2
  introv perm.
A: Type
l1, l2: list A
perm: Permutation l1 l2
forall a : A, a ∈ l1 <-> a ∈ l2 induction perm; firstorder.
Qed.

(*
(** * SameSet *)
(**********************************************************************)
Inductive SameSetRight {A: Type}: list A -> list A -> Prop :=
| ssetr_nil: SameSetRight [] []
| ssetr_skip: forall (x: A) (l l': list A), SameSetRight l l' -> SameSetRight (x :: l) (x :: l')
| ssetr_swap: forall (x y: A) (l: list A), SameSetRight (y :: x :: l) (x :: y :: l)
| ssetr_dup_r: forall (x: A) (l: list A), SameSetRight (x :: l) (x :: x :: l)
| ssetr_trans: forall l l' l'': list A, SameSetRight l l' -> SameSetRight l' l'' -> SameSetRight l l''.

From Tealeaves Require Import Classes.EqDec_eq.

Lemma sameset_refl: forall (A: Type) (l: list A),
    SameSet l l.
Proof.
  intros. induction l.
  - apply sset_nil.
  - apply sset_skip.
    assumption.
Qed.

Lemma sameset_nil: forall (A: Type) (l: list A),
    SameSet [] l -> l = [].
Proof.
  intros. remember [] as l'.
  induction H; subst; try solve [inversion Heql'].
  - reflexivity.
  - specialize (IHSameSet1 ltac:(reflexivity)).
    subst. auto.
Qed.

Lemma sametset_dup_right: forall (A: Type) (a: A) (l: list A),
    SameSet (a :: l) (a :: a :: l).
Proof.
  intros. apply sset_dup_r.
Qed.

Example ex1: forall (A: Type) (a: A),
    SameSet [a; a] [a].
Proof.
  intros. apply sset_dup_l.
Qed.

Lemma sameset_sym: forall (A: Type) (l l': list A),
    SameSet l l' -> SameSet l' l.
Proof.
  intros. induction H.
  - apply sset_nil.
  - apply sset_skip. auto.
  - apply sset_swap.
  - apply sset_dup_l.
  - apply sset_dup_r.
  - eapply sset_trans; eauto.
Qed.

(*
  Lemma sameset_spec_one: forall (A: Type) `{EqDec_eq A} (l: list A) (a: A),
  (forall (a0: A), a0 ∈ l <-> a0 = a) -> SameSet [a] l.
  Proof.
  introv Heq Hsame. induction l.
  - specialize (Hsame a).
  autorewrite with tea_list in Hsame. tauto.
  - assert (a0 = a).
  { apply (Hsame a0). now left. }
  subst; clear Hsame.
  destruct l.
  + apply sameset_refl.
  + destruct_eq_args a a0.
  * admit.
  * admit.
  Abort.

  Theorem sameset_spec: forall {A} `{EqDec_eq A} {l1 l2: list A},
  (forall a, a ∈ l1 <-> a ∈ l2) -> SameSet l1 l2.
  Proof.
  introv Heqdec Hsame.
  assert (Hsame1: forall a: A, a ∈ l1 -> a ∈ l2).
  { intro a. apply Hsame. }
  assert (Hsame2: forall a: A, a ∈ l2 -> a ∈ l1).
  { intro a. apply Hsame. }
  clear Hsame.
  generalize dependent l2.
  induction l1; intros l2 Hsame1 Hsame2.
  - induction l2.
  + apply sset_nil.
  + false.
  apply (Hsame2 a).
  now left.
  - destruct l1.
  + clear IHl1.
  Abort.

  TODO Cleanup
 *)
 *)

(** * Miscellaneous *)
(**********************************************************************)
Lemma map_preserve_length:
  forall (A B: Type) (f: A -> B) (l: list A),
    length (map f l) = length l.
forall (A B : Type) (f : A -> B) (l : list A),
length (map f l) = length l
Proof.
forall (A B : Type) (f : A -> B) (l : list A),
length (map f l) = length l
  intros.
A, B: Type
f: A -> B
l: list A
length (map f l) = length l
  induction l.
A, B: Type
f: A -> B
length (map f []) = length []
A, B: Type
f: A -> B
a: A
l: list A
IHl: length (map f l) = length l
length (map f (a :: l)) = length (a :: l)
  -
A, B: Type
f: A -> B
length (map f []) = length [] reflexivity.
  -
A, B: Type
f: A -> B
a: A
l: list A
IHl: length (map f l) = length l
length (map f (a :: l)) = length (a :: l) cbn.
A, B: Type
f: A -> B
a: A
l: list A
IHl: length (map f l) = length l
S (length (map f l)) = S (length l)
    rewrite <- IHl.
A, B: Type
f: A -> B
a: A
l: list A
IHl: length (map f l) = length l
S (length (map f l)) = S (length (map f l))
    reflexivity.
Qed.

Definition decide_length {A}: forall (n: nat) (l: list A),
    {length l = n} + { length l = n -> False}.
A: Type
forall (n : nat) (l : list A),
{length l = n} + {length l = n -> False}
Proof.
A: Type
forall (n : nat) (l : list A),
{length l = n} + {length l = n -> False}
  intros.
A: Type
n: nat
l: list A
{length l = n} + {length l = n -> False}
  remember (Nat.eqb (length l) n) as b.
A: Type
n: nat
l: list A
b: bool
Heqb: b = Nat.eqb (length l) n
{length l = n} + {length l = n -> False}
  symmetry in Heqb.
A: Type
n: nat
l: list A
b: bool
Heqb: Nat.eqb (length l) n = b
{length l = n} + {length l = n -> False}
  destruct b.
A: Type
n: nat
l: list A
Heqb: Nat.eqb (length l) n = true
{length l = n} + {length l = n -> False}
A: Type
n: nat
l: list A
Heqb: Nat.eqb (length l) n = false
{length l = n} + {length l = n -> False}
  -
A: Type
n: nat
l: list A
Heqb: Nat.eqb (length l) n = true
{length l = n} + {length l = n -> False} left.
A: Type
n: nat
l: list A
Heqb: Nat.eqb (length l) n = true
length l = n
    apply (PeanoNat.Nat.eqb_eq (length l) n).
A: Type
n: nat
l: list A
Heqb: Nat.eqb (length l) n = true
PeanoNat.Nat.eqb (length l) n = true
    assumption.
  -
A: Type
n: nat
l: list A
Heqb: Nat.eqb (length l) n = false
{length l = n} + {length l = n -> False} right.
A: Type
n: nat
l: list A
Heqb: Nat.eqb (length l) n = false
length l = n -> False
    apply (PeanoNat.Nat.eqb_neq (length l) n).
A: Type
n: nat
l: list A
Heqb: Nat.eqb (length l) n = false
PeanoNat.Nat.eqb (length l) n = false
    assumption.
Defined.

(** * Un-con-sing Nonempty Lists *)
(**********************************************************************)
Lemma S_uncons {n m}: S n = S m -> n = m.
n, m: nat
S n = S m -> n = m
Proof.
n, m: nat
S n = S m -> n = m
  now inversion 1.
Defined.

Definition zero_not_S {n} {anything}:
  0 = S n -> anything :=
  fun pf => match pf with
         | eq_refl =>
             let false: False :=
               eq_ind 0
                 (fun e: nat => match e with
                           | 0 => True
                           | S _ => False
                           end) I (S n) pf
             in (False_rect anything false)
         end.

Lemma list_uncons_exists:
  forall (A: Type) (n: nat)
         (v: list A) (vlen: length v = S n),
  exists (a: A) (v': list A),
    v = cons a v'.
forall (A : Type) (n : nat) (v : list A),
length v = S n ->
exists (a : A) (v' : list A), v = a :: v'
Proof.
forall (A : Type) (n : nat) (v : list A),
length v = S n ->
exists (a : A) (v' : list A), v = a :: v'
  intros.
A: Type
n: nat
v: list A
vlen: length v = S n
exists (a : A) (v' : list A), v = a :: v'
  destruct v.
A: Type
n: nat
vlen: length [] = S n
exists (a : A) (v' : list A), [] = a :: v'
A: Type
n: nat
a: A
v: list A
vlen: length (a :: v) = S n
exists (a0 : A) (v' : list A), a :: v = a0 :: v'
  -
A: Type
n: nat
vlen: length [] = S n
exists (a : A) (v' : list A), [] = a :: v' inversion vlen.
  -
A: Type
n: nat
a: A
v: list A
vlen: length (a :: v) = S n
exists (a0 : A) (v' : list A), a :: v = a0 :: v' exists a v.
A: Type
n: nat
a: A
v: list A
vlen: length (a :: v) = S n
a :: v = a :: v reflexivity.
Qed.

Definition list_uncons {n A} (l: list A) (vlen: length l = S n):
  A * list A :=
  match l return (length l = S n -> A * list A) with
  | nil => zero_not_S
  | cons a rest => fun vlen => (a, rest)
  end vlen.

Definition list_uncons_sigma {n A} (l: list A) (vlen: length l = S n):
  A * {l: list A | length l = n} :=
  match l return
        (length l = S n -> A * {l: list A | length l = n})
  with
  | nil => zero_not_S
  | cons hd tl => fun vlen => (hd, exist _ tl (S_uncons vlen))
  end vlen.

Definition list_uncons_sigma2 {n A} (l: list A) (vlen: length l = S n):
  {p: A * list A | l = uncurry cons p} :=
  match l return
        (length l = S n -> {p: A * list A | l = uncurry cons p})
  with
  | nil => zero_not_S
  | cons hd tl => fun vlen => exist _ (hd, tl) eq_refl
  end vlen.

(** ** Total Head and Tail Functions for Nonempty Lists *)
(**********************************************************************)
Definition list_hd {n A} :=
  fun (l: list A) (vlen: length l = S n) =>
    fst (list_uncons l vlen).

Definition list_tl {n A} :=
  fun (l: list A) (vlen: length l = S n) =>
    snd (list_uncons l vlen).

(** *** Proof irrelevance and rewriting laws *)
(**********************************************************************)
Lemma list_hd_proof_irrelevance
  {n m A}
  (l: list A)
  (vlen1: length l = S n)
  (vlen2: length l = S m):
  list_hd l vlen1 = list_hd l vlen2.
n, m: nat
A: Type
l: list A
vlen1: length l = S n
vlen2: length l = S m
list_hd l vlen1 = list_hd l vlen2
Proof.
n, m: nat
A: Type
l: list A
vlen1: length l = S n
vlen2: length l = S m
list_hd l vlen1 = list_hd l vlen2
  induction l.
n, m: nat
A: Type
vlen1: length [] = S n
vlen2: length [] = S m
list_hd [] vlen1 = list_hd [] vlen2
n, m: nat
A: Type
a: A
l: list A
vlen1: length (a :: l) = S n
vlen2: length (a :: l) = S m
IHl: forall (vlen1 : length l = S n)
  (vlen2 : length l = S m),
list_hd l vlen1 = list_hd l vlen2
list_hd (a :: l) vlen1 = list_hd (a :: l) vlen2
  -
n, m: nat
A: Type
vlen1: length [] = S n
vlen2: length [] = S m
list_hd [] vlen1 = list_hd [] vlen2 inversion vlen1.
  -
n, m: nat
A: Type
a: A
l: list A
vlen1: length (a :: l) = S n
vlen2: length (a :: l) = S m
IHl: forall (vlen1 : length l = S n)
  (vlen2 : length l = S m),
list_hd l vlen1 = list_hd l vlen2
list_hd (a :: l) vlen1 = list_hd (a :: l) vlen2 reflexivity.
Qed.

Lemma list_tl_proof_irrelevance
  {n m A}
  (l: list A)
  (vlen1: length l = S n)
  (vlen2: length l = S m):
  list_tl l vlen1 = list_tl l vlen2.
n, m: nat
A: Type
l: list A
vlen1: length l = S n
vlen2: length l = S m
list_tl l vlen1 = list_tl l vlen2
Proof.
n, m: nat
A: Type
l: list A
vlen1: length l = S n
vlen2: length l = S m
list_tl l vlen1 = list_tl l vlen2
  induction l.
n, m: nat
A: Type
vlen1: length [] = S n
vlen2: length [] = S m
list_tl [] vlen1 = list_tl [] vlen2
n, m: nat
A: Type
a: A
l: list A
vlen1: length (a :: l) = S n
vlen2: length (a :: l) = S m
IHl: forall (vlen1 : length l = S n)
  (vlen2 : length l = S m),
list_tl l vlen1 = list_tl l vlen2
list_tl (a :: l) vlen1 = list_tl (a :: l) vlen2
  -
n, m: nat
A: Type
vlen1: length [] = S n
vlen2: length [] = S m
list_tl [] vlen1 = list_tl [] vlen2 inversion vlen1.
  -
n, m: nat
A: Type
a: A
l: list A
vlen1: length (a :: l) = S n
vlen2: length (a :: l) = S m
IHl: forall (vlen1 : length l = S n)
  (vlen2 : length l = S m),
list_tl l vlen1 = list_tl l vlen2
list_tl (a :: l) vlen1 = list_tl (a :: l) vlen2 reflexivity.
Qed.

(** Rewrite a [list_hd] subterm by pushing a type coercion into the
    length proof *)
Lemma list_hd_rw
  {n A}
  {l1 l2: list A}
  (Heq: l1 = l2)
  {vlen: length l1 = S n}:
  list_hd l1 vlen =
    list_hd l2 (rew [fun l1 => length l1 = S n] Heq in vlen).
n: nat
A: Type
l1, l2: list A
Heq: l1 = l2
vlen: length l1 = S n
list_hd l1 vlen =
list_hd l2
  (rew [fun l1 : list A => length l1 = S n] Heq in
   vlen)
Proof.
n: nat
A: Type
l1, l2: list A
Heq: l1 = l2
vlen: length l1 = S n
list_hd l1 vlen =
list_hd l2
  (rew [fun l1 : list A => length l1 = S n] Heq in
   vlen)
  subst.
n: nat
A: Type
l2: list A
vlen: length l2 = S n
list_hd l2 vlen =
list_hd l2
  (rew [fun l1 : list A => length l1 = S n] eq_refl in
   vlen)
  apply list_hd_proof_irrelevance.
Qed.

(** Rewrite a [list_tl] subterm by pushing a type coercion into the
    length proof *)
Lemma list_tl_rw
  {n A}
  {l1 l2: list A}
  (Heq: l1 = l2)
  {vlen: length l1 = S n}:
  list_tl l1 vlen =
    list_tl l2 (rew [fun l1 => length l1 = S n] Heq in vlen).
n: nat
A: Type
l1, l2: list A
Heq: l1 = l2
vlen: length l1 = S n
list_tl l1 vlen =
list_tl l2
  (rew [fun l1 : list A => length l1 = S n] Heq in
   vlen)
Proof.
n: nat
A: Type
l1, l2: list A
Heq: l1 = l2
vlen: length l1 = S n
list_tl l1 vlen =
list_tl l2
  (rew [fun l1 : list A => length l1 = S n] Heq in
   vlen)
  subst.
n: nat
A: Type
l2: list A
vlen: length l2 = S n
list_tl l2 vlen =
list_tl l2
  (rew [fun l1 : list A => length l1 = S n] eq_refl in
   vlen)
  apply list_tl_proof_irrelevance.
Qed.

Lemma list_tl_length {n} `(l: list A) (vlen: length l = S n):
  length (list_tl l vlen) = n.
n: nat
A: Type
l: list A
vlen: length l = S n
length (list_tl l vlen) = n
Proof.
n: nat
A: Type
l: list A
vlen: length l = S n
length (list_tl l vlen) = n
  destruct l.
n: nat
A: Type
vlen: length [] = S n
length (list_tl [] vlen) = n
n: nat
A: Type
a: A
l: list A
vlen: length (a :: l) = S n
length (list_tl (a :: l) vlen) = n
  -
n: nat
A: Type
vlen: length [] = S n
length (list_tl [] vlen) = n inversion vlen.
  -
n: nat
A: Type
a: A
l: list A
vlen: length (a :: l) = S n
length (list_tl (a :: l) vlen) = n cbn.
n: nat
A: Type
a: A
l: list A
vlen: length (a :: l) = S n
length l = n now inversion vlen.
Qed.

(** *** Surjective pairing properties *)
(**********************************************************************)
Lemma list_surjective_pairing {n} `(l: list A) `(vlen: length l = S n):
  list_uncons l vlen = (list_hd l vlen, list_tl l vlen).
n: nat
A: Type
l: list A
vlen: length l = S n
list_uncons l vlen = (list_hd l vlen, list_tl l vlen)
Proof.
n: nat
A: Type
l: list A
vlen: length l = S n
list_uncons l vlen = (list_hd l vlen, list_tl l vlen)
  destruct l.
n: nat
A: Type
vlen: length [] = S n
list_uncons [] vlen =
(list_hd [] vlen, list_tl [] vlen)
n: nat
A: Type
a: A
l: list A
vlen: length (a :: l) = S n
list_uncons (a :: l) vlen =
(list_hd (a :: l) vlen, list_tl (a :: l) vlen)
  -
n: nat
A: Type
vlen: length [] = S n
list_uncons [] vlen =
(list_hd [] vlen, list_tl [] vlen) inversion vlen.
  -
n: nat
A: Type
a: A
l: list A
vlen: length (a :: l) = S n
list_uncons (a :: l) vlen =
(list_hd (a :: l) vlen, list_tl (a :: l) vlen) reflexivity.
Qed.

Lemma list_surjective_pairing2 {n} `(l: list A) `(vlen: length l = S n):
  l = cons (list_hd l vlen) (list_tl l vlen).
n: nat
A: Type
l: list A
vlen: length l = S n
l = list_hd l vlen :: list_tl l vlen
Proof.
n: nat
A: Type
l: list A
vlen: length l = S n
l = list_hd l vlen :: list_tl l vlen
  destruct l.
n: nat
A: Type
vlen: length [] = S n
[] = list_hd [] vlen :: list_tl [] vlen
n: nat
A: Type
a: A
l: list A
vlen: length (a :: l) = S n
a :: l =
list_hd (a :: l) vlen :: list_tl (a :: l) vlen
  -
n: nat
A: Type
vlen: length [] = S n
[] = list_hd [] vlen :: list_tl [] vlen inversion vlen.
  -
n: nat
A: Type
a: A
l: list A
vlen: length (a :: l) = S n
a :: l =
list_hd (a :: l) vlen :: list_tl (a :: l) vlen reflexivity.
Qed.

(** * Filtering Lists *)
(**********************************************************************)
Fixpoint filter `(P: A -> bool) (l: list A): list A :=
  match l with
  | nil => nil
  | cons a rest =>
      if P a then a :: filter P rest else filter P rest
  end.

(** ** Rewriting Laws for [filter] *)
(**********************************************************************)
Section filter_lemmas.

  Context
    `(P: A -> bool).

  Lemma filter_nil:
    filter P nil = nil.
A: Type
P: A -> bool
filter P [] = []
  Proof.
A: Type
P: A -> bool
filter P [] = []
    reflexivity.
  Qed.

  Lemma filter_cons: forall (a: A) (l: list A),
      filter P (a :: l) = if P a then a :: filter P l else filter P l.
A: Type
P: A -> bool
forall (a : A) (l : list A),
filter P (a :: l) =
(if P a then a :: filter P l else filter P l)
  Proof.
A: Type
P: A -> bool
forall (a : A) (l : list A),
filter P (a :: l) =
(if P a then a :: filter P l else filter P l)
    reflexivity.
  Qed.

  Lemma filter_one: forall (a: A),
      filter P [a] = if P a then [a] else nil.
A: Type
P: A -> bool
forall a : A, filter P [a] = (if P a then [a] else [])
  Proof.
A: Type
P: A -> bool
forall a : A, filter P [a] = (if P a then [a] else [])
    reflexivity.
  Qed.

  Lemma filter_app: forall (l1 l2: list A),
      filter P (l1 ++ l2) = filter P l1 ++ filter P l2.
A: Type
P: A -> bool
forall l1 l2 : list A,
filter P (l1 ++ l2) = filter P l1 ++ filter P l2
  Proof.
A: Type
P: A -> bool
forall l1 l2 : list A,
filter P (l1 ++ l2) = filter P l1 ++ filter P l2
    intros.
A: Type
P: A -> bool
l1, l2: list A
filter P (l1 ++ l2) = filter P l1 ++ filter P l2 induction l1.
A: Type
P: A -> bool
l2: list A
filter P ([] ++ l2) = filter P [] ++ filter P l2
A: Type
P: A -> bool
a: A
l1, l2: list A
IHl1: filter P (l1 ++ l2) =
filter P l1 ++ filter P l2
filter P ((a :: l1) ++ l2) =
filter P (a :: l1) ++ filter P l2
    -
A: Type
P: A -> bool
l2: list A
filter P ([] ++ l2) = filter P [] ++ filter P l2 reflexivity.
    -
A: Type
P: A -> bool
a: A
l1, l2: list A
IHl1: filter P (l1 ++ l2) =
filter P l1 ++ filter P l2
filter P ((a :: l1) ++ l2) =
filter P (a :: l1) ++ filter P l2 cbn.
A: Type
P: A -> bool
a: A
l1, l2: list A
IHl1: filter P (l1 ++ l2) =
filter P l1 ++ filter P l2
(if P a
 then a :: filter P (l1 ++ l2)
 else filter P (l1 ++ l2)) =
(if P a then a :: filter P l1 else filter P l1) ++
filter P l2 rewrite IHl1.
A: Type
P: A -> bool
a: A
l1, l2: list A
IHl1: filter P (l1 ++ l2) =
filter P l1 ++ filter P l2
(if P a
 then a :: filter P l1 ++ filter P l2
 else filter P l1 ++ filter P l2) =
(if P a then a :: filter P l1 else filter P l1) ++
filter P l2 now destruct (P a).
  Qed.

End filter_lemmas.

#[export] Hint Rewrite
  @filter_nil @filter_cons @filter_app @filter_one: tea_list.