Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.Paths Types.Unit Types.Prod.
Require Export Spaces.List.Core.

(** * Theory of Lists and List Operations *)

(** In this file we collect lemmas about lists and their operations. We don't include those in [List.Core] so that file can stay lightweight on dependencies. *)

(** We generally try to keep the order the same as the concepts appeared in [List.Core]. *)

Local Open Scope list_scope.

(** ** Concatenation *)

(** Associativity of list concatenation. *)
Definition app_assoc {A} (x y z : list A)
  : app x (app y z) = app (app x y) z.
A: Type
x, y, z: list A
x ++ y ++ z = (x ++ y) ++ z
Proof.
A: Type
x, y, z: list A
x ++ y ++ z = (x ++ y) ++ z
  induction x as [|a x IHx] in |- *.
A: Type
y, z: list A
nil ++ y ++ z = (nil ++ y) ++ z
A: Type
a: A
x, y, z: list A
IHx: x ++ y ++ z = (x ++ y) ++ z
(a :: x) ++ y ++ z = ((a :: x) ++ y) ++ z
  -
A: Type
y, z: list A
nil ++ y ++ z = (nil ++ y) ++ z reflexivity.
  -
A: Type
a: A
x, y, z: list A
IHx: x ++ y ++ z = (x ++ y) ++ z
(a :: x) ++ y ++ z = ((a :: x) ++ y) ++ z exact (ap (cons a) IHx).
Defined.

(** The type of lists has a monoidal structure given by concatenation. *)
Definition list_pentagon {A} (w x y z : list A)
  : app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
    = ap (fun l => w ++ l) (app_assoc x y z)
    @ app_assoc w (x ++ y) z
    @ ap (fun l => l ++ z) (app_assoc w x y).
A: Type
w, x, y, z: list A
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z =
(ap (fun l : list A => w ++ l) (app_assoc x y z) @
 app_assoc w (x ++ y) z) @
ap (fun l : list A => l ++ z) (app_assoc w x y)
Proof.
A: Type
w, x, y, z: list A
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z =
(ap (fun l : list A => w ++ l) (app_assoc x y z) @
 app_assoc w (x ++ y) z) @
ap (fun l : list A => l ++ z) (app_assoc w x y)
  symmetry.
A: Type
w, x, y, z: list A
(ap (fun l : list A => w ++ l) (app_assoc x y z) @
 app_assoc w (x ++ y) z) @
ap (fun l : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
  induction w as [|? w IHw] in x, y, z |- *.
A: Type
x, y, z: list A
(ap (fun l : list A => nil ++ l) (app_assoc x y z) @
 app_assoc nil (x ++ y) z) @
ap (fun l : list A => l ++ z) (app_assoc nil x y) =
app_assoc nil x (y ++ z) @ app_assoc (nil ++ x) y z
A: Type
a: A
w, x, y, z: list A
IHw: forall x y z : list A,
(ap (fun l : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (fun l : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
(ap (fun l : list A => (a :: w) ++ l)
   (app_assoc x y z) @ app_assoc (a :: w) (x ++ y) z) @
ap (fun l : list A => l ++ z) (app_assoc (a :: w) x y) =
app_assoc (a :: w) x (y ++ z) @
app_assoc ((a :: w) ++ x) y z
  -
A: Type
x, y, z: list A
(ap (fun l : list A => nil ++ l) (app_assoc x y z) @
 app_assoc nil (x ++ y) z) @
ap (fun l : list A => l ++ z) (app_assoc nil x y) =
app_assoc nil x (y ++ z) @ app_assoc (nil ++ x) y z simpl.
A: Type
x, y, z: list A
(ap idmap (app_assoc x y z) @ 1) @ 1 =
1 @ app_assoc x y z
    apply equiv_p1_1q.
A: Type
x, y, z: list A
ap idmap (app_assoc x y z) @ 1 = app_assoc x y z
    lhs nrapply concat_p1.
A: Type
x, y, z: list A
ap idmap (app_assoc x y z) = app_assoc x y z
    apply ap_idmap.
  -
A: Type
a: A
w, x, y, z: list A
IHw: forall x y z : list A,
(ap (fun l : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (fun l : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
(ap (fun l : list A => (a :: w) ++ l)
   (app_assoc x y z) @ app_assoc (a :: w) (x ++ y) z) @
ap (fun l : list A => l ++ z) (app_assoc (a :: w) x y) =
app_assoc (a :: w) x (y ++ z) @
app_assoc ((a :: w) ++ x) y z simpl.
A: Type
a: A
w, x, y, z: list A
IHw: forall x y z : list A,
(ap (fun l : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (fun l : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
(ap (fun l : list A => a :: w ++ l) (app_assoc x y z) @
 ap (cons a) (app_assoc w (x ++ y) z)) @
ap (fun l : list A => l ++ z)
  (ap (cons a) (app_assoc w x y)) =
ap (cons a) (app_assoc w x (y ++ z)) @
ap (cons a) (app_assoc (w ++ x) y z)
    rhs_V nrapply ap_pp.
A: Type
a: A
w, x, y, z: list A
IHw: forall x y z : list A,
(ap (fun l : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (fun l : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
(ap (fun l : list A => a :: w ++ l) (app_assoc x y z) @
 ap (cons a) (app_assoc w (x ++ y) z)) @
ap (fun l : list A => l ++ z)
  (ap (cons a) (app_assoc w x y)) =
ap (cons a)
  (app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z)
    rhs_V nrapply (ap (ap (cons a)) (IHw x y z)).
A: Type
a: A
w, x, y, z: list A
IHw: forall x y z : list A,
(ap (fun l : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (fun l : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
(ap (fun l : list A => a :: w ++ l) (app_assoc x y z) @
 ap (cons a) (app_assoc w (x ++ y) z)) @
ap (fun l : list A => l ++ z)
  (ap (cons a) (app_assoc w x y)) =
ap (cons a)
  ((ap (fun l : list A => w ++ l) (app_assoc x y z) @
    app_assoc w (x ++ y) z) @
   ap (fun l : list A => l ++ z) (app_assoc w x y))
    rhs nrapply ap_pp.
A: Type
a: A
w, x, y, z: list A
IHw: forall x y z : list A,
(ap (fun l : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (fun l : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
(ap (fun l : list A => a :: w ++ l) (app_assoc x y z) @
 ap (cons a) (app_assoc w (x ++ y) z)) @
ap (fun l : list A => l ++ z)
  (ap (cons a) (app_assoc w x y)) =
ap (cons a)
  (ap (fun l : list A => w ++ l) (app_assoc x y z) @
   app_assoc w (x ++ y) z) @
ap (cons a)
  (ap (fun l : list A => l ++ z) (app_assoc w x y))
    f_ap.
A: Type
a: A
w, x, y, z: list A
IHw: forall x y z : list A,
(ap (fun l : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (fun l : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
ap (fun l : list A => a :: w ++ l) (app_assoc x y z) @
ap (cons a) (app_assoc w (x ++ y) z) =
ap (cons a)
  (ap (fun l : list A => w ++ l) (app_assoc x y z) @
   app_assoc w (x ++ y) z)
A: Type
a: A
w, x, y, z: list A
IHw: forall x y z : list A,
(ap (fun l : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (fun l : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
ap (fun l : list A => l ++ z)
  (ap (cons a) (app_assoc w x y)) =
ap (cons a)
  (ap (fun l : list A => l ++ z) (app_assoc w x y))
    {
A: Type
a: A
w, x, y, z: list A
IHw: forall x y z : list A,
(ap (fun l : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (fun l : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
ap (fun l : list A => a :: w ++ l) (app_assoc x y z) @
ap (cons a) (app_assoc w (x ++ y) z) =
ap (cons a)
  (ap (fun l : list A => w ++ l) (app_assoc x y z) @
   app_assoc w (x ++ y) z) rhs nrapply ap_pp.
A: Type
a: A
w, x, y, z: list A
IHw: forall x y z : list A,
(ap (fun l : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (fun l : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
ap (fun l : list A => a :: w ++ l) (app_assoc x y z) @
ap (cons a) (app_assoc w (x ++ y) z) =
ap (cons a)
  (ap (fun l : list A => w ++ l) (app_assoc x y z)) @
ap (cons a) (app_assoc w (x ++ y) z)
      f_ap.
A: Type
a: A
w, x, y, z: list A
IHw: forall x y z : list A,
(ap (fun l : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (fun l : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
ap (fun l : list A => a :: w ++ l) (app_assoc x y z) =
ap (cons a)
  (ap (fun l : list A => w ++ l) (app_assoc x y z))
      apply ap_compose. }
A: Type
a: A
w, x, y, z: list A
IHw: forall x y z : list A,
(ap (fun l : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (fun l : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
ap (fun l : list A => l ++ z)
  (ap (cons a) (app_assoc w x y)) =
ap (cons a)
  (ap (fun l : list A => l ++ z) (app_assoc w x y))
    lhs_V nrapply ap_compose.
A: Type
a: A
w, x, y, z: list A
IHw: forall x y z : list A,
(ap (fun l : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (fun l : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
ap (fun x : list A => (a :: x) ++ z) (app_assoc w x y) =
ap (cons a)
  (ap (fun l : list A => l ++ z) (app_assoc w x y))
    nrapply (ap_compose (fun l => l ++ z)).
Defined.

(** ** Folding *)

Lemma fold_left_app {A B} (f : A -> B -> A) (l l' : list B) (i : A)
  : fold_left f (l ++ l') i = fold_left f l' (fold_left f l i).
A, B: Type
f: A -> B -> A
l, l': list B
i: A
fold_left f (l ++ l') i =
fold_left f l' (fold_left f l i)
Proof.
A, B: Type
f: A -> B -> A
l, l': list B
i: A
fold_left f (l ++ l') i =
fold_left f l' (fold_left f l i)
  induction l in i |- *.
A, B: Type
f: A -> B -> A
l': list B
i: A
fold_left f (nil ++ l') i =
fold_left f l' (fold_left f nil i)
A, B: Type
f: A -> B -> A
a: B
l, l': list B
i: A
IHl: forall i : A, fold_left f (l ++ l') i = fold_left f l' (fold_left f l i)
fold_left f ((a :: l) ++ l') i =
fold_left f l' (fold_left f (a :: l) i)
  1: reflexivity.
A, B: Type
f: A -> B -> A
a: B
l, l': list B
i: A
IHl: forall i : A, fold_left f (l ++ l') i = fold_left f l' (fold_left f l i)
fold_left f ((a :: l) ++ l') i =
fold_left f l' (fold_left f (a :: l) i)
  apply IHl.
Defined.

Lemma fold_right_app {A B} (f : B -> A -> A) (i : A) (l l' : list B)
  : fold_right f i (l ++ l') = fold_right f (fold_right f i l') l.
A, B: Type
f: B -> A -> A
i: A
l, l': list B
fold_right f i (l ++ l') =
fold_right f (fold_right f i l') l
Proof.
A, B: Type
f: B -> A -> A
i: A
l, l': list B
fold_right f i (l ++ l') =
fold_right f (fold_right f i l') l
  induction l in i |- *.
A, B: Type
f: B -> A -> A
i: A
l': list B
fold_right f i (nil ++ l') =
fold_right f (fold_right f i l') nil
A, B: Type
f: B -> A -> A
i: A
a: B
l, l': list B
IHl: forall i : A, fold_right f i (l ++ l') = fold_right f (fold_right f i l') l
fold_right f i ((a :: l) ++ l') =
fold_right f (fold_right f i l') (a :: l)
  1: reflexivity.
A, B: Type
f: B -> A -> A
i: A
a: B
l, l': list B
IHl: forall i : A, fold_right f i (l ++ l') = fold_right f (fold_right f i l') l
fold_right f i ((a :: l) ++ l') =
fold_right f (fold_right f i l') (a :: l)
  exact (ap (f a) (IHl _)).
Defined.

(** ** Maps *)

Lemma map_id {A} (f : A -> A) (Hf : forall x, f x = x) (l : list A)
  :  map f l = l.
A: Type
f: A -> A
Hf: forall x : A, f x = x
l: list A
map f l = l
Proof.
A: Type
f: A -> A
Hf: forall x : A, f x = x
l: list A
map f l = l
  induction l as [|x l IHl].
A: Type
f: A -> A
Hf: forall x : A, f x = x
map f nil = nil
A: Type
f: A -> A
Hf: forall x : A, f x = x
x: A
l: list A
IHl: map f l = l
map f (x :: l) = x :: l
  -
A: Type
f: A -> A
Hf: forall x : A, f x = x
map f nil = nil reflexivity.
  -
A: Type
f: A -> A
Hf: forall x : A, f x = x
x: A
l: list A
IHl: map f l = l
map f (x :: l) = x :: l simpl.
A: Type
f: A -> A
Hf: forall x : A, f x = x
x: A
l: list A
IHl: map f l = l
f x :: map f l = x :: l
    nrapply ap011.
A: Type
f: A -> A
Hf: forall x : A, f x = x
x: A
l: list A
IHl: map f l = l
f x = x
A: Type
f: A -> A
Hf: forall x : A, f x = x
x: A
l: list A
IHl: map f l = l
map f l = l
    +
A: Type
f: A -> A
Hf: forall x : A, f x = x
x: A
l: list A
IHl: map f l = l
f x = x exact (Hf _).
    +
A: Type
f: A -> A
Hf: forall x : A, f x = x
x: A
l: list A
IHl: map f l = l
map f l = l exact IHl.
Defined.

Lemma map2_cons {A B C} (f : A -> B -> C) defl defr x l1 y l2
  :  map2 f defl defr (x :: l1) (y :: l2)
    = (f x y) :: map2 f defl defr l1 l2.
A, B, C: Type
f: A -> B -> C
defl: list A -> list C
defr: list B -> list C
x: A
l1: list A
y: B
l2: list B
map2 f defl defr (x :: l1) (y :: l2) =
f x y :: map2 f defl defr l1 l2
Proof.
A, B, C: Type
f: A -> B -> C
defl: list A -> list C
defr: list B -> list C
x: A
l1: list A
y: B
l2: list B
map2 f defl defr (x :: l1) (y :: l2) =
f x y :: map2 f defl defr l1 l2
  reflexivity.
Defined.

(** ** Forall *)

Lemma for_all_trivial {A} (P : A -> Type) : (forall x, P x) ->
  forall l, for_all P l.
A: Type
P: A -> Type
(forall x : A, P x) -> forall l : list A, for_all P l
Proof.
A: Type
P: A -> Type
(forall x : A, P x) -> forall l : list A, for_all P l
  intros HP l; induction l as [|x l IHl]; split; auto.
Defined.

Lemma for_all_map {A B} P Q (f : A -> B) (Hf : forall x, P x -> Q (f x))
 : forall l, for_all P l -> for_all Q (map f l).
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
Hf: forall x : A, P x -> Q (f x)
forall l : list A, for_all P l -> for_all Q (map f l)
Proof.
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
Hf: forall x : A, P x -> Q (f x)
forall l : list A, for_all P l -> for_all Q (map f l)
  intros l;induction l as [|x l IHl];simpl.
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
Hf: forall x : A, P x -> Q (f x)
Unit -> Unit
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
Hf: forall x : A, P x -> Q (f x)
x: A
l: list A
IHl: for_all P l -> for_all Q (map f l)
P x * for_all P l -> Q (f x) * for_all Q (map f l)
  -
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
Hf: forall x : A, P x -> Q (f x)
Unit -> Unit auto.
  -
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
Hf: forall x : A, P x -> Q (f x)
x: A
l: list A
IHl: for_all P l -> for_all Q (map f l)
P x * for_all P l -> Q (f x) * for_all Q (map f l) intros [Hx Hl].
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
Hf: forall x : A, P x -> Q (f x)
x: A
l: list A
IHl: for_all P l -> for_all Q (map f l)
Hx: P x
Hl: for_all P l
Q (f x) * for_all Q (map f l) split; auto.
Defined.

Lemma for_all_map2 {A B C}
  (P : A -> Type) (Q : B -> Type) (R : C -> Type)
  (f : A -> B -> C) (Hf : forall x y, P x -> Q y -> R (f x y))
  def_l (Hdefl : forall l1, for_all P l1 -> for_all R (def_l l1))
  def_r (Hdefr : forall l2, for_all Q l2 -> for_all R (def_r l2))
  (l1 : list A) (l2 : list B)
  : for_all P l1 -> for_all Q l2
    -> for_all R (map2 f def_l def_r l1 l2).
A, B, C: Type
P: A -> Type
Q: B -> Type
R: C -> Type
f: A -> B -> C
Hf: forall (x : A) (y : B), P x -> Q y -> R (f x y)
def_l: list A -> list C
Hdefl: forall l1 : list A,
for_all P l1 -> for_all R (def_l l1)
def_r: list B -> list C
Hdefr: forall l2 : list B,
for_all Q l2 -> for_all R (def_r l2)
l1: list A
l2: list B
for_all P l1 ->
for_all Q l2 -> for_all R (map2 f def_l def_r l1 l2)
Proof.
A, B, C: Type
P: A -> Type
Q: B -> Type
R: C -> Type
f: A -> B -> C
Hf: forall (x : A) (y : B), P x -> Q y -> R (f x y)
def_l: list A -> list C
Hdefl: forall l1 : list A,
for_all P l1 -> for_all R (def_l l1)
def_r: list B -> list C
Hdefr: forall l2 : list B,
for_all Q l2 -> for_all R (def_r l2)
l1: list A
l2: list B
for_all P l1 ->
for_all Q l2 -> for_all R (map2 f def_l def_r l1 l2)
  induction l1 as [|x l1 IHl1] in l2 |- *.
A, B, C: Type
P: A -> Type
Q: B -> Type
R: C -> Type
f: A -> B -> C
Hf: forall (x : A) (y : B), P x -> Q y -> R (f x y)
def_l: list A -> list C
Hdefl: forall l1 : list A,
for_all P l1 -> for_all R (def_l l1)
def_r: list B -> list C
Hdefr: forall l2 : list B,
for_all Q l2 -> for_all R (def_r l2)
l2: list B
for_all P nil ->
for_all Q l2 -> for_all R (map2 f def_l def_r nil l2)
A, B, C: Type
P: A -> Type
Q: B -> Type
R: C -> Type
f: A -> B -> C
Hf: forall (x : A) (y : B), P x -> Q y -> R (f x y)
def_l: list A -> list C
Hdefl: forall l1 : list A,
for_all P l1 -> for_all R (def_l l1)
def_r: list B -> list C
Hdefr: forall l2 : list B,
for_all Q l2 -> for_all R (def_r l2)
x: A
l1: list A
l2: list B
IHl1: forall l2 : list B,
for_all P l1 ->
for_all Q l2 ->
for_all R (map2 f def_l def_r l1 l2)
for_all P (x :: l1) ->
for_all Q l2 ->
for_all R (map2 f def_l def_r (x :: l1) l2)
  -
A, B, C: Type
P: A -> Type
Q: B -> Type
R: C -> Type
f: A -> B -> C
Hf: forall (x : A) (y : B), P x -> Q y -> R (f x y)
def_l: list A -> list C
Hdefl: forall l1 : list A,
for_all P l1 -> for_all R (def_l l1)
def_r: list B -> list C
Hdefr: forall l2 : list B,
for_all Q l2 -> for_all R (def_r l2)
l2: list B
for_all P nil ->
for_all Q l2 -> for_all R (map2 f def_l def_r nil l2) destruct l2 as [|y l2]; cbn; auto.
  -
A, B, C: Type
P: A -> Type
Q: B -> Type
R: C -> Type
f: A -> B -> C
Hf: forall (x : A) (y : B), P x -> Q y -> R (f x y)
def_l: list A -> list C
Hdefl: forall l1 : list A,
for_all P l1 -> for_all R (def_l l1)
def_r: list B -> list C
Hdefr: forall l2 : list B,
for_all Q l2 -> for_all R (def_r l2)
x: A
l1: list A
l2: list B
IHl1: forall l2 : list B,
for_all P l1 ->
for_all Q l2 ->
for_all R (map2 f def_l def_r l1 l2)
for_all P (x :: l1) ->
for_all Q l2 ->
for_all R (map2 f def_l def_r (x :: l1) l2) simpl.
A, B, C: Type
P: A -> Type
Q: B -> Type
R: C -> Type
f: A -> B -> C
Hf: forall (x : A) (y : B), P x -> Q y -> R (f x y)
def_l: list A -> list C
Hdefl: forall l1 : list A,
for_all P l1 -> for_all R (def_l l1)
def_r: list B -> list C
Hdefr: forall l2 : list B,
for_all Q l2 -> for_all R (def_r l2)
x: A
l1: list A
l2: list B
IHl1: forall l2 : list B,
for_all P l1 ->
for_all Q l2 ->
for_all R (map2 f def_l def_r l1 l2)
P x * for_all P l1 ->
for_all Q l2 ->
for_all R
  match l2 with
  | nil => def_l (x :: l1)
  | y :: l2 => f x y :: map2 f def_l def_r l1 l2
  end destruct l2 as [|y l2]; intros [Hx Hl1];
      [intros _ | intros [Hy Hl2] ]; simpl; auto.
A, B, C: Type
P: A -> Type
Q: B -> Type
R: C -> Type
f: A -> B -> C
Hf: forall (x : A) (y : B), P x -> Q y -> R (f x y)
def_l: list A -> list C
Hdefl: forall l1 : list A,
for_all P l1 -> for_all R (def_l l1)
def_r: list B -> list C
Hdefr: forall l2 : list B,
for_all Q l2 -> for_all R (def_r l2)
x: A
l1: list A
IHl1: forall l2 : list B,
for_all P l1 ->
for_all Q l2 ->
for_all R (map2 f def_l def_r l1 l2)
Hx: P x
Hl1: for_all P l1
for_all R (def_l (x :: l1))
    apply Hdefl.
A, B, C: Type
P: A -> Type
Q: B -> Type
R: C -> Type
f: A -> B -> C
Hf: forall (x : A) (y : B), P x -> Q y -> R (f x y)
def_l: list A -> list C
Hdefl: forall l1 : list A,
for_all P l1 -> for_all R (def_l l1)
def_r: list B -> list C
Hdefr: forall l2 : list B,
for_all Q l2 -> for_all R (def_r l2)
x: A
l1: list A
IHl1: forall l2 : list B,
for_all P l1 ->
for_all Q l2 ->
for_all R (map2 f def_l def_r l1 l2)
Hx: P x
Hl1: for_all P l1
for_all P (x :: l1)
    simpl; auto.
Defined.

Lemma fold_preserves {A B} P Q (f : A -> B -> A)
  (Hf : forall x y, P x -> Q y -> P (f x y))
  (acc : A) (Ha : P acc) (l : list B) (Hl : for_all Q l)
  : P (fold_left f l acc).
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B -> A
Hf: forall (x : A) (y : B), P x -> Q y -> P (f x y)
acc: A
Ha: P acc
l: list B
Hl: for_all Q l
P (fold_left f l acc)
Proof.
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B -> A
Hf: forall (x : A) (y : B), P x -> Q y -> P (f x y)
acc: A
Ha: P acc
l: list B
Hl: for_all Q l
P (fold_left f l acc)
  induction l as [|x l IHl] in acc, Ha, Hl |- *.
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B -> A
Hf: forall (x : A) (y : B), P x -> Q y -> P (f x y)
acc: A
Ha: P acc
Hl: for_all Q nil
P (fold_left f nil acc)
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B -> A
Hf: forall (x : A) (y : B), P x -> Q y -> P (f x y)
acc: A
Ha: P acc
x: B
l: list B
Hl: for_all Q (x :: l)
IHl: forall acc : A, P acc -> for_all Q l -> P (fold_left f l acc)
P (fold_left f (x :: l) acc)
  -
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B -> A
Hf: forall (x : A) (y : B), P x -> Q y -> P (f x y)
acc: A
Ha: P acc
Hl: for_all Q nil
P (fold_left f nil acc) exact Ha.
  -
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B -> A
Hf: forall (x : A) (y : B), P x -> Q y -> P (f x y)
acc: A
Ha: P acc
x: B
l: list B
Hl: for_all Q (x :: l)
IHl: forall acc : A, P acc -> for_all Q l -> P (fold_left f l acc)
P (fold_left f (x :: l) acc) simpl.
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B -> A
Hf: forall (x : A) (y : B), P x -> Q y -> P (f x y)
acc: A
Ha: P acc
x: B
l: list B
Hl: for_all Q (x :: l)
IHl: forall acc : A, P acc -> for_all Q l -> P (fold_left f l acc)
P (fold_left f l (f acc x))
    destruct Hl as [Qx Hl].
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B -> A
Hf: forall (x : A) (y : B), P x -> Q y -> P (f x y)
acc: A
Ha: P acc
x: B
l: list B
Qx: Q x
Hl: for_all Q l
IHl: forall acc : A, P acc -> for_all Q l -> P (fold_left f l acc)
P (fold_left f l (f acc x))
    apply IHl; auto.
Defined.

Global Instance for_all_trunc {A} {n} (P : A -> Type) (l : list A)
  : for_all (fun x => IsTrunc n (P x)) l -> IsTrunc n (for_all P l).
A: Type
n: trunc_index
P: A -> Type
l: list A
for_all (fun x : A => IsTrunc n (P x)) l ->
IsTrunc n (for_all P l)
Proof.
A: Type
n: trunc_index
P: A -> Type
l: list A
for_all (fun x : A => IsTrunc n (P x)) l ->
IsTrunc n (for_all P l)
  induction l as [|x l IHl]; simpl.
A: Type
n: trunc_index
P: A -> Type
Unit -> IsTrunc n Unit
A: Type
n: trunc_index
P: A -> Type
x: A
l: list A
IHl: for_all (fun x : A => IsTrunc n (P x)) l -> IsTrunc n (for_all P l)
IsTrunc n (P x) *
for_all (fun x : A => IsTrunc n (P x)) l ->
IsTrunc n (P x * for_all P l)
  -
A: Type
n: trunc_index
P: A -> Type
Unit -> IsTrunc n Unit destruct n; exact _.
  -
A: Type
n: trunc_index
P: A -> Type
x: A
l: list A
IHl: for_all (fun x : A => IsTrunc n (P x)) l -> IsTrunc n (for_all P l)
IsTrunc n (P x) *
for_all (fun x : A => IsTrunc n (P x)) l ->
IsTrunc n (P x * for_all P l) intros [Hx Hl].
A: Type
n: trunc_index
P: A -> Type
x: A
l: list A
IHl: for_all (fun x : A => IsTrunc n (P x)) l -> IsTrunc n (for_all P l)
Hx: IsTrunc n (P x)
Hl: for_all (fun x : A => IsTrunc n (P x)) l
IsTrunc n (P x * for_all P l)
    apply IHl in Hl.
A: Type
n: trunc_index
P: A -> Type
x: A
l: list A
IHl: for_all (fun x : A => IsTrunc n (P x)) l -> IsTrunc n (for_all P l)
Hx: IsTrunc n (P x)
Hl: IsTrunc n (for_all P l)
IsTrunc n (P x * for_all P l)
    exact _.
Defined.