Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.TruncRequire Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc
  Basics.Equivalences Basics.Decidable Basics.Iff.
Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum
  Types.Empty Types.Option.
Require Export Spaces.List.Core Spaces.Nat.Core.

Local Set Universe Minimization ToSet.
Local Set Polymorphic Inductive Cumulativity.

(** * 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.
Local Open Scope nat_scope.

(** ** Length *)

(** A list of length zero must be the empty list. *)
Definition length_0 {A : Type} (l : list A) (H : length l = 0)
  : l = nil.
A: Type
l: list A
H: length l = 0
l = nil
Proof.
A: Type
l: list A
H: length l = 0
l = nil
  destruct l.
A: Type
H: length nil = 0
nil = nil
A: Type
a: A
l: list A
H: length (a :: l) = 0
a :: l = nil
  -
A: Type
H: length nil = 0
nil = nil reflexivity.
  -
A: Type
a: A
l: list A
H: length (a :: l) = 0
a :: l = nil discriminate.
Defined.

(** ** Concatenation *)

(** Concatenating the empty list on the right is the identity. *)
Definition app_nil {A : Type} (l : list A)
  : l ++ nil = l.
A: Type
l: list A
l ++ nil = l
Proof.
A: Type
l: list A
l ++ nil = l
  induction l as [|a l IHl].
A: Type
nil ++ nil = nil
A: Type
a: A
l: list A
IHl: l ++ nil = l
(a :: l) ++ nil = a :: l
  1: reflexivity.
A: Type
a: A
l: list A
IHl: l ++ nil = l
(a :: l) ++ nil = a :: l
  simpl; f_ap.
Defined.

(** Associativity of list concatenation. *)
Definition app_assoc {A : Type} (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 : Type} (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 x0 y0 z0 : list A,
(ap (fun l : list A => w ++ l) (app_assoc x0 y0 z0) @
 app_assoc w (x0 ++ y0) z0) @
ap (fun l : list A => l ++ z0) (app_assoc w x0 y0) =
app_assoc w x0 (y0 ++ z0) @ app_assoc (w ++ x0) y0 z0
(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 napply 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 x0 y0 z0 : list A,
(ap (fun l : list A => w ++ l) (app_assoc x0 y0 z0) @
 app_assoc w (x0 ++ y0) z0) @
ap (fun l : list A => l ++ z0) (app_assoc w x0 y0) =
app_assoc w x0 (y0 ++ z0) @ app_assoc (w ++ x0) y0 z0
(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 x0 y0 z0 : list A,
(ap (fun l : list A => w ++ l) (app_assoc x0 y0 z0) @
 app_assoc w (x0 ++ y0) z0) @
ap (fun l : list A => l ++ z0) (app_assoc w x0 y0) =
app_assoc w x0 (y0 ++ z0) @ app_assoc (w ++ x0) y0 z0
(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 napply ap_pp.
A: Type
a: A
w, x, y, z: list A
IHw: forall x0 y0 z0 : list A,
(ap (fun l : list A => w ++ l) (app_assoc x0 y0 z0) @
 app_assoc w (x0 ++ y0) z0) @
ap (fun l : list A => l ++ z0) (app_assoc w x0 y0) =
app_assoc w x0 (y0 ++ z0) @ app_assoc (w ++ x0) y0 z0
(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 exact (ap (ap (cons a)) (IHw x y z)).
A: Type
a: A
w, x, y, z: list A
IHw: forall x0 y0 z0 : list A,
(ap (fun l : list A => w ++ l) (app_assoc x0 y0 z0) @
 app_assoc w (x0 ++ y0) z0) @
ap (fun l : list A => l ++ z0) (app_assoc w x0 y0) =
app_assoc w x0 (y0 ++ z0) @ app_assoc (w ++ x0) y0 z0
(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 napply ap_pp.
A: Type
a: A
w, x, y, z: list A
IHw: forall x0 y0 z0 : list A,
(ap (fun l : list A => w ++ l) (app_assoc x0 y0 z0) @
 app_assoc w (x0 ++ y0) z0) @
ap (fun l : list A => l ++ z0) (app_assoc w x0 y0) =
app_assoc w x0 (y0 ++ z0) @ app_assoc (w ++ x0) y0 z0
(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 x0 y0 z0 : list A,
(ap (fun l : list A => w ++ l) (app_assoc x0 y0 z0) @
 app_assoc w (x0 ++ y0) z0) @
ap (fun l : list A => l ++ z0) (app_assoc w x0 y0) =
app_assoc w x0 (y0 ++ z0) @ app_assoc (w ++ x0) y0 z0
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 x0 y0 z0 : list A,
(ap (fun l : list A => w ++ l) (app_assoc x0 y0 z0) @
 app_assoc w (x0 ++ y0) z0) @
ap (fun l : list A => l ++ z0) (app_assoc w x0 y0) =
app_assoc w x0 (y0 ++ z0) @ app_assoc (w ++ x0) y0 z0
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 x0 y0 z0 : list A,
(ap (fun l : list A => w ++ l) (app_assoc x0 y0 z0) @
 app_assoc w (x0 ++ y0) z0) @
ap (fun l : list A => l ++ z0) (app_assoc w x0 y0) =
app_assoc w x0 (y0 ++ z0) @ app_assoc (w ++ x0) y0 z0
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 napply ap_pp.
A: Type
a: A
w, x, y, z: list A
IHw: forall x0 y0 z0 : list A,
(ap (fun l : list A => w ++ l) (app_assoc x0 y0 z0) @
 app_assoc w (x0 ++ y0) z0) @
ap (fun l : list A => l ++ z0) (app_assoc w x0 y0) =
app_assoc w x0 (y0 ++ z0) @ app_assoc (w ++ x0) y0 z0
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 x0 y0 z0 : list A,
(ap (fun l : list A => w ++ l) (app_assoc x0 y0 z0) @
 app_assoc w (x0 ++ y0) z0) @
ap (fun l : list A => l ++ z0) (app_assoc w x0 y0) =
app_assoc w x0 (y0 ++ z0) @ app_assoc (w ++ x0) y0 z0
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 x0 y0 z0 : list A,
(ap (fun l : list A => w ++ l) (app_assoc x0 y0 z0) @
 app_assoc w (x0 ++ y0) z0) @
ap (fun l : list A => l ++ z0) (app_assoc w x0 y0) =
app_assoc w x0 (y0 ++ z0) @ app_assoc (w ++ x0) y0 z0
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 napply ap_compose.
A: Type
a: A
w, x, y, z: list A
IHw: forall x0 y0 z0 : list A,
(ap (fun l : list A => w ++ l) (app_assoc x0 y0 z0) @
 app_assoc w (x0 ++ y0) z0) @
ap (fun l : list A => l ++ z0) (app_assoc w x0 y0) =
app_assoc w x0 (y0 ++ z0) @ app_assoc (w ++ x0) y0 z0
ap (fun x0 : list A => (a :: x0) ++ z) (app_assoc w x y) =
ap (cons a) (ap (fun l : list A => l ++ z) (app_assoc w x y))
    napply (ap_compose (fun l => l ++ z)).
Defined.

(** The length of a concatenated list is the sum of the lengths of the two lists. *)
Definition length_app {A : Type} (l l' : list A)
  : length (l ++ l') = length l + length l'.
A: Type
l, l': list A
length (l ++ l') = length l + length l'
Proof.
A: Type
l, l': list A
length (l ++ l') = length l + length l'
  induction l as [|a l IHl] using list_ind.
A: Type
l': list A
length (nil ++ l') = length nil + length l'
A: Type
a: A
l, l': list A
IHl: length (l ++ l') = length l + length l'
length ((a :: l) ++ l') = length (a :: l) + length l'
  1: reflexivity.
A: Type
a: A
l, l': list A
IHl: length (l ++ l') = length l + length l'
length ((a :: l) ++ l') = length (a :: l) + length l'
  simpl.
A: Type
a: A
l, l': list A
IHl: length (l ++ l') = length l + length l'
(length (l ++ l')).+1 = (length l + length l').+1
  exact (ap S IHl).
Defined.

(** An element of a concatenated list is equivalently either in the first list or in the second list. *)
Definition equiv_inlist_app {A : Type} (l l' : list A) (x : A)
  : InList x l + InList x l' <~> InList x (l ++ l').
A: Type
l, l': list A
x: A
InList x l + InList x l' <~> InList x (l ++ l')
Proof.
A: Type
l, l': list A
x: A
InList x l + InList x l' <~> InList x (l ++ l')
  induction l as [|a l IHl].
A: Type
l': list A
x: A
InList x nil + InList x l' <~> InList x (nil ++ l')
A: Type
a: A
l, l': list A
x: A
IHl: InList x l + InList x l' <~> InList x (l ++ l')
InList x (a :: l) + InList x l' <~> InList x ((a :: l) ++ l')
  -
A: Type
l': list A
x: A
InList x nil + InList x l' <~> InList x (nil ++ l') apply sum_empty_l.
  -
A: Type
a: A
l, l': list A
x: A
IHl: InList x l + InList x l' <~> InList x (l ++ l')
InList x (a :: l) + InList x l' <~> InList x ((a :: l) ++ l') cbn; nrefine (_ oE equiv_sum_assoc _ _ _).
A: Type
a: A
l, l': list A
x: A
IHl: InList x l + InList x l' <~> InList x (l ++ l')
(a = x) + (InList x l + InList x l') <~> (a = x) + InList x (l ++ l')
    by apply equiv_functor_sum_l.
Defined.

(** ** Folding *)

(** A left fold over a concatenated list is equivalent to folding over the first followed by folding over the second. *)
Lemma fold_left_app {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).
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 i0 : A, fold_left f (l ++ l') i0 = fold_left f l' (fold_left f l i0)
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 i0 : A, fold_left f (l ++ l') i0 = fold_left f l' (fold_left f l i0)
fold_left f ((a :: l) ++ l') i = fold_left f l' (fold_left f (a :: l) i)
  apply IHl.
Defined.

(** A right fold over a concatenated list is equivalent to folding over the second followed by folding over the first. *)
Lemma fold_right_app {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.
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 i0 : A,
fold_right f i0 (l ++ l') = fold_right f (fold_right f i0 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 i0 : A,
fold_right f i0 (l ++ l') = fold_right f (fold_right f i0 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 *)

(** The length of a mapped list is the same as the length of the original list. *)
Definition length_list_map {A B : Type} (f : A -> B) (l : list A)
  : length (list_map f l) = length l.
A, B: Type
f: A -> B
l: list A
length (list_map f l) = length l
Proof.
A, B: Type
f: A -> B
l: list A
length (list_map f l) = length l
  induction l as [|x l IHl] using list_ind.
A, B: Type
f: A -> B
length (list_map f nil) = length nil
A, B: Type
f: A -> B
x: A
l: list A
IHl: length (list_map f l) = length l
length (list_map f (x :: l)) = length (x :: l)
  -
A, B: Type
f: A -> B
length (list_map f nil) = length nil reflexivity.
  -
A, B: Type
f: A -> B
x: A
l: list A
IHl: length (list_map f l) = length l
length (list_map f (x :: l)) = length (x :: l) simpl.
A, B: Type
f: A -> B
x: A
l: list A
IHl: length (list_map f l) = length l
(length (list_map f l)).+1 = (length l).+1
    exact (ap S IHl).
Defined.

(** A function applied to an element of a list is an element of the mapped list. *)
Definition inlist_map {A B : Type} (f : A -> B) (l : list A) (x : A)
  : InList x l -> InList (f x) (list_map f l).
A, B: Type
f: A -> B
l: list A
x: A
InList x l -> InList (f x) (list_map f l)
Proof.
A, B: Type
f: A -> B
l: list A
x: A
InList x l -> InList (f x) (list_map f l)
  simple_list_induction l y l IHl.
A, B: Type
f: A -> B
x: A
InList x nil -> InList (f x) (list_map f nil)
A, B: Type
f: A -> B
x: A
l: list A
IHl: InList x l -> InList (f x) (list_map f l)
y: A
InList x (y :: l) -> InList (f x) (list_map f (y :: l))
  1: contradiction.
A, B: Type
f: A -> B
x: A
l: list A
IHl: InList x l -> InList (f x) (list_map f l)
y: A
InList x (y :: l) -> InList (f x) (list_map f (y :: l))
  intros [p | i].
A, B: Type
f: A -> B
x: A
l: list A
IHl: InList x l -> InList (f x) (list_map f l)
y: A
p: y = x
InList (f x) (list_map f (y :: l))
A, B: Type
f: A -> B
x: A
l: list A
IHl: InList x l -> InList (f x) (list_map f l)
y: A
i: InList x l
InList (f x) (list_map f (y :: l))
  -
A, B: Type
f: A -> B
x: A
l: list A
IHl: InList x l -> InList (f x) (list_map f l)
y: A
p: y = x
InList (f x) (list_map f (y :: l)) left.
A, B: Type
f: A -> B
x: A
l: list A
IHl: InList x l -> InList (f x) (list_map f l)
y: A
p: y = x
f y = f x  exact (ap f p).
  -
A, B: Type
f: A -> B
x: A
l: list A
IHl: InList x l -> InList (f x) (list_map f l)
y: A
i: InList x l
InList (f x) (list_map f (y :: l)) right.
A, B: Type
f: A -> B
x: A
l: list A
IHl: InList x l -> InList (f x) (list_map f l)
y: A
i: InList x l
InList (f x) (list_map f l) exact (IHl i).
Defined.

(** An element of a mapped list is equal to the function applied to some element of the original list. *)
Definition inlist_map' {A B : Type} (f : A -> B) (l : list A) (x : B)
  : InList x (list_map f l) -> { y : A & prod (f y = x) (InList y l) }.
A, B: Type
f: A -> B
l: list A
x: B
InList x (list_map f l) -> {y : A & ((f y = x) * InList y l)%type}
Proof.
A, B: Type
f: A -> B
l: list A
x: B
InList x (list_map f l) -> {y : A & ((f y = x) * InList y l)%type}
  induction l as [|y l IHl].
A, B: Type
f: A -> B
x: B
InList x (list_map f nil) -> {y : A & ((f y = x) * InList y nil)%type}
A, B: Type
f: A -> B
y: A
l: list A
x: B
IHl: InList x (list_map f l) -> {y0 : A & ((f y0 = x) * InList y0 l)%type}
InList x (list_map f (y :: l)) ->
{y0 : A & ((f y0 = x) * InList y0 (y :: l))%type}
  1: contradiction.
A, B: Type
f: A -> B
y: A
l: list A
x: B
IHl: InList x (list_map f l) -> {y0 : A & ((f y0 = x) * InList y0 l)%type}
InList x (list_map f (y :: l)) ->
{y0 : A & ((f y0 = x) * InList y0 (y :: l))%type}
  intros [p | i].
A, B: Type
f: A -> B
y: A
l: list A
x: B
IHl: InList x (list_map f l) -> {y0 : A & ((f y0 = x) * InList y0 l)%type}
p: f y = x
{y0 : A & ((f y0 = x) * InList y0 (y :: l))%type}
A, B: Type
f: A -> B
y: A
l: list A
x: B
IHl: InList x (list_map f l) -> {y0 : A & ((f y0 = x) * InList y0 l)%type}
i: InList x (list_map f l)
{y0 : A & ((f y0 = x) * InList y0 (y :: l))%type}
  -
A, B: Type
f: A -> B
y: A
l: list A
x: B
IHl: InList x (list_map f l) -> {y0 : A & ((f y0 = x) * InList y0 l)%type}
p: f y = x
{y0 : A & ((f y0 = x) * InList y0 (y :: l))%type} exact (y; (p, inl idpath)).
  -
A, B: Type
f: A -> B
y: A
l: list A
x: B
IHl: InList x (list_map f l) -> {y0 : A & ((f y0 = x) * InList y0 l)%type}
i: InList x (list_map f l)
{y0 : A & ((f y0 = x) * InList y0 (y :: l))%type} destruct (IHl i) as [y' [p i']].
A, B: Type
f: A -> B
y: A
l: list A
x: B
IHl: InList x (list_map f l) -> {y0 : A & ((f y0 = x) * InList y0 l)%type}
i: InList x (list_map f l)
y': A
p: f y' = x
i': InList y' l
{y0 : A & ((f y0 = x) * InList y0 (y :: l))%type}
    exact (y'; (p, inr i')).
Defined.

(** Mapping a function over a concatenated list is the concatenation of the mapped lists. *)
Definition list_map_app {A B : Type} (f : A -> B) (l l' : list A)
  : list_map f (l ++ l') = list_map f l ++ list_map f l'.
A, B: Type
f: A -> B
l, l': list A
list_map f (l ++ l') = list_map f l ++ list_map f l'
Proof.
A, B: Type
f: A -> B
l, l': list A
list_map f (l ++ l') = list_map f l ++ list_map f l'
  induction l as [|a l IHl].
A, B: Type
f: A -> B
l': list A
list_map f (nil ++ l') = list_map f nil ++ list_map f l'
A, B: Type
f: A -> B
a: A
l, l': list A
IHl: list_map f (l ++ l') = list_map f l ++ list_map f l'
list_map f ((a :: l) ++ l') = list_map f (a :: l) ++ list_map f l'
  1: reflexivity.
A, B: Type
f: A -> B
a: A
l, l': list A
IHl: list_map f (l ++ l') = list_map f l ++ list_map f l'
list_map f ((a :: l) ++ l') = list_map f (a :: l) ++ list_map f l'
  simpl; f_ap.
Defined.

(** A function that acts as the identity on the elements of a list is the identity on the mapped list. *)
Lemma list_map_id {A : Type} (f : A -> A) (l : list A)
  (Hf : forall x, InList x l -> f x = x)
  :  list_map f l = l.
A: Type
f: A -> A
l: list A
Hf: forall x : A, InList x l -> f x = x
list_map f l = l
Proof.
A: Type
f: A -> A
l: list A
Hf: forall x : A, InList x l -> f x = x
list_map f l = l
  induction l as [|x l IHl].
A: Type
f: A -> A
Hf: forall x : A, InList x nil -> f x = x
list_map f nil = nil
A: Type
f: A -> A
x: A
l: list A
Hf: forall x0 : A, InList x0 (x :: l) -> f x0 = x0
IHl: (forall x0 : A, InList x0 l -> f x0 = x0) -> list_map f l = l
list_map f (x :: l) = x :: l
  -
A: Type
f: A -> A
Hf: forall x : A, InList x nil -> f x = x
list_map f nil = nil reflexivity.
  -
A: Type
f: A -> A
x: A
l: list A
Hf: forall x0 : A, InList x0 (x :: l) -> f x0 = x0
IHl: (forall x0 : A, InList x0 l -> f x0 = x0) -> list_map f l = l
list_map f (x :: l) = x :: l simpl.
A: Type
f: A -> A
x: A
l: list A
Hf: forall x0 : A, InList x0 (x :: l) -> f x0 = x0
IHl: (forall x0 : A, InList x0 l -> f x0 = x0) -> list_map f l = l
f x :: list_map f l = x :: l
    napply ap011.
A: Type
f: A -> A
x: A
l: list A
Hf: forall x0 : A, InList x0 (x :: l) -> f x0 = x0
IHl: (forall x0 : A, InList x0 l -> f x0 = x0) -> list_map f l = l
f x = x
A: Type
f: A -> A
x: A
l: list A
Hf: forall x0 : A, InList x0 (x :: l) -> f x0 = x0
IHl: (forall x0 : A, InList x0 l -> f x0 = x0) -> list_map f l = l
list_map f l = l
    +
A: Type
f: A -> A
x: A
l: list A
Hf: forall x0 : A, InList x0 (x :: l) -> f x0 = x0
IHl: (forall x0 : A, InList x0 l -> f x0 = x0) -> list_map f l = l
f x = x exact (Hf _ (inl idpath)).
    +
A: Type
f: A -> A
x: A
l: list A
Hf: forall x0 : A, InList x0 (x :: l) -> f x0 = x0
IHl: (forall x0 : A, InList x0 l -> f x0 = x0) -> list_map f l = l
list_map f l = l apply IHl.
A: Type
f: A -> A
x: A
l: list A
Hf: forall x0 : A, InList x0 (x :: l) -> f x0 = x0
IHl: (forall x0 : A, InList x0 l -> f x0 = x0) -> list_map f l = l
forall x0 : A, InList x0 l -> f x0 = x0
      intros y Hy.
A: Type
f: A -> A
x: A
l: list A
Hf: forall x0 : A, InList x0 (x :: l) -> f x0 = x0
IHl: (forall x0 : A, InList x0 l -> f x0 = x0) -> list_map f l = l
y: A
Hy: InList y l
f y = y
      apply Hf.
A: Type
f: A -> A
x: A
l: list A
Hf: forall x0 : A, InList x0 (x :: l) -> f x0 = x0
IHl: (forall x0 : A, InList x0 l -> f x0 = x0) -> list_map f l = l
y: A
Hy: InList y l
InList y (x :: l)
      by right.
Defined.

(** A [list_map] of a composition is the composition of the maps. *)
Definition list_map_compose {A B C} (f : A -> B) (g : B -> C) (l : list A)
  : list_map (fun x => g (f x)) l = list_map g (list_map f l).
A, B, C: Type
f: A -> B
g: B -> C
l: list A
list_map (fun x : A => g (f x)) l = list_map g (list_map f l)
Proof.
A, B, C: Type
f: A -> B
g: B -> C
l: list A
list_map (fun x : A => g (f x)) l = list_map g (list_map f l)
  induction l as [|a l IHl].
A, B, C: Type
f: A -> B
g: B -> C
list_map (fun x : A => g (f x)) nil = list_map g (list_map f nil)
A, B, C: Type
f: A -> B
g: B -> C
a: A
l: list A
IHl: list_map (fun x : A => g (f x)) l = list_map g (list_map f l)
list_map (fun x : A => g (f x)) (a :: l) = list_map g (list_map f (a :: l))
  1: reflexivity.
A, B, C: Type
f: A -> B
g: B -> C
a: A
l: list A
IHl: list_map (fun x : A => g (f x)) l = list_map g (list_map f l)
list_map (fun x : A => g (f x)) (a :: l) = list_map g (list_map f (a :: l))
  simpl; f_ap.
Defined.

(** TODO: generalize as max *)
(** The length of a [list_map2] is the same as the length of the original lists. *)
Definition length_list_map2@{i j k|} {A : Type@{i}} {B : Type@{j}} {C : Type@{k}}
  (f : A -> B -> C) defl defr l1 l2
  : length l1 = length l2
    -> length (list_map2 f defl defr l1 l2) = length l1.
A, B, C: Type
f: A -> B -> C
defl: list A -> list C
defr: list B -> list C
l1: list A
l2: list B
length l1 = length l2 -> length (list_map2 f defl defr l1 l2) = length l1
Proof.
A, B, C: Type
f: A -> B -> C
defl: list A -> list C
defr: list B -> list C
l1: list A
l2: list B
length l1 = length l2 -> length (list_map2 f defl defr l1 l2) = length l1
  intros p.
A, B, C: Type
f: A -> B -> C
defl: list A -> list C
defr: list B -> list C
l1: list A
l2: list B
p: length l1 = length l2
length (list_map2 f defl defr l1 l2) = length l1
  induction l1 as [|x l1 IHl1] in l2, p |- * using list_ind@{i j}.
A, B, C: Type
f: A -> B -> C
defl: list A -> list C
defr: list B -> list C
l2: list B
p: length nil = length l2
length (list_map2 f defl defr nil l2) = length nil
A, B, C: Type
f: A -> B -> C
defl: list A -> list C
defr: list B -> list C
x: A
l1: list A
l2: list B
p: length (x :: l1) = length l2
IHl1: forall l0 : list B,
length l1 = length l0 -> length (list_map2 f defl defr l1 l0) = length l1
length (list_map2 f defl defr (x :: l1) l2) = length (x :: l1)
  -
A, B, C: Type
f: A -> B -> C
defl: list A -> list C
defr: list B -> list C
l2: list B
p: length nil = length l2
length (list_map2 f defl defr nil l2) = length nil destruct l2.
A, B, C: Type
f: A -> B -> C
defl: list A -> list C
defr: list B -> list C
p: length nil = length nil
length (list_map2 f defl defr nil nil) = length nil
A, B, C: Type
f: A -> B -> C
defl: list A -> list C
defr: list B -> list C
b: B
l2: list B
p: length nil = length (b :: l2)
length (list_map2 f defl defr nil (b :: l2)) = length nil
    +
A, B, C: Type
f: A -> B -> C
defl: list A -> list C
defr: list B -> list C
p: length nil = length nil
length (list_map2 f defl defr nil nil) = length nil reflexivity.
    +
A, B, C: Type
f: A -> B -> C
defl: list A -> list C
defr: list B -> list C
b: B
l2: list B
p: length nil = length (b :: l2)
length (list_map2 f defl defr nil (b :: l2)) = length nil inversion p.
  -
A, B, C: Type
f: A -> B -> C
defl: list A -> list C
defr: list B -> list C
x: A
l1: list A
l2: list B
p: length (x :: l1) = length l2
IHl1: forall l0 : list B,
length l1 = length l0 -> length (list_map2 f defl defr l1 l0) = length l1
length (list_map2 f defl defr (x :: l1) l2) = length (x :: l1) destruct l2.
A, B, C: Type
f: A -> B -> C
defl: list A -> list C
defr: list B -> list C
x: A
l1: list A
p: length (x :: l1) = length nil
IHl1: forall l2 : list B,
length l1 = length l2 -> length (list_map2 f defl defr l1 l2) = length l1
length (list_map2 f defl defr (x :: l1) nil) = length (x :: l1)
A, B, C: Type
f: A -> B -> C
defl: list A -> list C
defr: list B -> list C
x: A
l1: list A
b: B
l2: list B
p: length (x :: l1) = length (b :: l2)
IHl1: forall l0 : list B,
length l1 = length l0 -> length (list_map2 f defl defr l1 l0) = length l1
length (list_map2 f defl defr (x :: l1) (b :: l2)) = length (x :: l1)
    +
A, B, C: Type
f: A -> B -> C
defl: list A -> list C
defr: list B -> list C
x: A
l1: list A
p: length (x :: l1) = length nil
IHl1: forall l2 : list B,
length l1 = length l2 -> length (list_map2 f defl defr l1 l2) = length l1
length (list_map2 f defl defr (x :: l1) nil) = length (x :: l1) inversion p.
    +
A, B, C: Type
f: A -> B -> C
defl: list A -> list C
defr: list B -> list C
x: A
l1: list A
b: B
l2: list B
p: length (x :: l1) = length (b :: l2)
IHl1: forall l0 : list B,
length l1 = length l0 -> length (list_map2 f defl defr l1 l0) = length l1
length (list_map2 f defl defr (x :: l1) (b :: l2)) = length (x :: l1) cbn; f_ap.
A, B, C: Type
f: A -> B -> C
defl: list A -> list C
defr: list B -> list C
x: A
l1: list A
b: B
l2: list B
p: length (x :: l1) = length (b :: l2)
IHl1: forall l0 : list B,
length l1 = length l0 -> length (list_map2 f defl defr l1 l0) = length l1
length (list_map2 f defl defr l1 l2) = length l1
      by apply IHl1, path_nat_succ.
Defined.

(** An element of a [list_map2] is the result of applying the function to some elements of the original lists. *)
Definition inlist_map2@{i j k u | i <= u, j <= u, k <= u}
  {A : Type@{i}} {B : Type@{j}} {C : Type@{k}}
  (f : A -> B -> C) defl defr l1 l2 x
  : InList x (list_map2 f defl defr l1 l2) -> length l1 = length l2
    -> { y : A & { z : B &
                        prod@{k u} ((f y z) = x) (InList y l1 * InList z l2) } }.
A, B, C: Type
f: A -> B -> C
defl: list A -> list C
defr: list B -> list C
l1: list A
l2: list B
x: C
InList x (list_map2 f defl defr l1 l2) ->
length l1 = length l2 ->
{y : A & {z : B & ((f y z = x) * (InList y l1 * InList z l2))%type}}
Proof.
A, B, C: Type
f: A -> B -> C
defl: list A -> list C
defr: list B -> list C
l1: list A
l2: list B
x: C
InList x (list_map2 f defl defr l1 l2) ->
length l1 = length l2 ->
{y : A & {z : B & ((f y z = x) * (InList y l1 * InList z l2))%type}}
  intros H p.
A, B, C: Type
f: A -> B -> C
defl: list A -> list C
defr: list B -> list C
l1: list A
l2: list B
x: C
H: InList x (list_map2 f defl defr l1 l2)
p: length l1 = length l2
{y : A & {z : B & ((f y z = x) * (InList y l1 * InList z l2))%type}}
  induction l1 as [|y l1 IHl1] in l2, x, H, p |- * using list_ind@{i u}.
A, B, C: Type
f: A -> B -> C
defl: list A -> list C
defr: list B -> list C
l2: list B
x: C
H: InList x (list_map2 f defl defr nil l2)
p: length nil = length l2
{y : A & {z : B & ((f y z = x) * (InList y nil * InList z l2))%type}}
A, B, C: Type
f: A -> B -> C
defl: list A -> list C
defr: list B -> list C
y: A
l1: list A
l2: list B
x: C
H: InList x (list_map2 f defl defr (y :: l1) l2)
p: length (y :: l1) = length l2
IHl1: forall (l0 : list B) (x0 : C),
InList x0 (list_map2 f defl defr l1 l0) ->
length l1 = length l0 ->
{y0 : A & {z : B & ((f y0 z = x0) * (InList y0 l1 * InList z l0))%type}}
{y0 : A &
{z : B & ((f y0 z = x) * (InList y0 (y :: l1) * InList z l2))%type}}
  -
A, B, C: Type
f: A -> B -> C
defl: list A -> list C
defr: list B -> list C
l2: list B
x: C
H: InList x (list_map2 f defl defr nil l2)
p: length nil = length l2
{y : A & {z : B & ((f y z = x) * (InList y nil * InList z l2))%type}} destruct l2.
A, B, C: Type
f: A -> B -> C
defl: list A -> list C
defr: list B -> list C
x: C
H: InList x (list_map2 f defl defr nil nil)
p: length nil = length nil
{y : A & {z : B & ((f y z = x) * (InList y nil * InList z nil))%type}}
A, B, C: Type
f: A -> B -> C
defl: list A -> list C
defr: list B -> list C
b: B
l2: list B
x: C
H: InList x (list_map2 f defl defr nil (b :: l2))
p: length nil = length (b :: l2)
{y : A & {z : B & ((f y z = x) * (InList y nil * InList z (b :: l2)))%type}}
    1: contradiction.
A, B, C: Type
f: A -> B -> C
defl: list A -> list C
defr: list B -> list C
b: B
l2: list B
x: C
H: InList x (list_map2 f defl defr nil (b :: l2))
p: length nil = length (b :: l2)
{y : A & {z : B & ((f y z = x) * (InList y nil * InList z (b :: l2)))%type}}
    inversion p.
  -
A, B, C: Type
f: A -> B -> C
defl: list A -> list C
defr: list B -> list C
y: A
l1: list A
l2: list B
x: C
H: InList x (list_map2 f defl defr (y :: l1) l2)
p: length (y :: l1) = length l2
IHl1: forall (l0 : list B) (x0 : C),
InList x0 (list_map2 f defl defr l1 l0) ->
length l1 = length l0 ->
{y0 : A & {z : B & ((f y0 z = x0) * (InList y0 l1 * InList z l0))%type}}
{y0 : A &
{z : B & ((f y0 z = x) * (InList y0 (y :: l1) * InList z l2))%type}} destruct l2 as [| z].
A, B, C: Type
f: A -> B -> C
defl: list A -> list C
defr: list B -> list C
y: A
l1: list A
x: C
H: InList x (list_map2 f defl defr (y :: l1) nil)
p: length (y :: l1) = length nil
IHl1: forall (l2 : list B) (x0 : C),
InList x0 (list_map2 f defl defr l1 l2) ->
length l1 = length l2 ->
{y0 : A & {z : B & ((f y0 z = x0) * (InList y0 l1 * InList z l2))%type}}
{y0 : A &
{z : B & ((f y0 z = x) * (InList y0 (y :: l1) * InList z nil))%type}}
A, B, C: Type
f: A -> B -> C
defl: list A -> list C
defr: list B -> list C
y: A
l1: list A
z: B
l2: list B
x: C
H: InList x (list_map2 f defl defr (y :: l1) (z :: l2))
p: length (y :: l1) = length (z :: l2)
IHl1: forall (l0 : list B) (x0 : C),
InList x0 (list_map2 f defl defr l1 l0) ->
length l1 = length l0 ->
{y0 : A & {z0 : B & ((f y0 z0 = x0) * (InList y0 l1 * InList z0 l0))%type}}
{y0 : A &
{z0 : B & ((f y0 z0 = x) * (InList y0 (y :: l1) * InList z0 (z :: l2)))%type}}
    1: inversion p.
A, B, C: Type
f: A -> B -> C
defl: list A -> list C
defr: list B -> list C
y: A
l1: list A
z: B
l2: list B
x: C
H: InList x (list_map2 f defl defr (y :: l1) (z :: l2))
p: length (y :: l1) = length (z :: l2)
IHl1: forall (l0 : list B) (x0 : C),
InList x0 (list_map2 f defl defr l1 l0) ->
length l1 = length l0 ->
{y0 : A & {z0 : B & ((f y0 z0 = x0) * (InList y0 l1 * InList z0 l0))%type}}
{y0 : A &
{z0 : B & ((f y0 z0 = x) * (InList y0 (y :: l1) * InList z0 (z :: l2)))%type}}
    destruct H as [q | i].
A, B, C: Type
f: A -> B -> C
defl: list A -> list C
defr: list B -> list C
y: A
l1: list A
z: B
l2: list B
x: C
q: f y z = x
p: length (y :: l1) = length (z :: l2)
IHl1: forall (l0 : list B) (x0 : C),
InList x0 (list_map2 f defl defr l1 l0) ->
length l1 = length l0 ->
{y0 : A & {z0 : B & ((f y0 z0 = x0) * (InList y0 l1 * InList z0 l0))%type}}
{y0 : A &
{z0 : B & ((f y0 z0 = x) * (InList y0 (y :: l1) * InList z0 (z :: l2)))%type}}
A, B, C: Type
f: A -> B -> C
defl: list A -> list C
defr: list B -> list C
y: A
l1: list A
z: B
l2: list B
x: C
i: InList x (list_map2 f defl defr l1 l2)
p: length (y :: l1) = length (z :: l2)
IHl1: forall (l0 : list B) (x0 : C),
InList x0 (list_map2 f defl defr l1 l0) ->
length l1 = length l0 ->
{y0 : A & {z0 : B & ((f y0 z0 = x0) * (InList y0 l1 * InList z0 l0))%type}}
{y0 : A &
{z0 : B & ((f y0 z0 = x) * (InList y0 (y :: l1) * InList z0 (z :: l2)))%type}}
    1: exact (y; z; (q, (inl idpath, inl idpath))).
A, B, C: Type
f: A -> B -> C
defl: list A -> list C
defr: list B -> list C
y: A
l1: list A
z: B
l2: list B
x: C
i: InList x (list_map2 f defl defr l1 l2)
p: length (y :: l1) = length (z :: l2)
IHl1: forall (l0 : list B) (x0 : C),
InList x0 (list_map2 f defl defr l1 l0) ->
length l1 = length l0 ->
{y0 : A & {z0 : B & ((f y0 z0 = x0) * (InList y0 l1 * InList z0 l0))%type}}
{y0 : A &
{z0 : B & ((f y0 z0 = x) * (InList y0 (y :: l1) * InList z0 (z :: l2)))%type}}
    destruct (IHl1 l2 x i) as [y' [z' [q [r s]]]].
A, B, C: Type
f: A -> B -> C
defl: list A -> list C
defr: list B -> list C
y: A
l1: list A
z: B
l2: list B
x: C
i: InList x (list_map2 f defl defr l1 l2)
p: length (y :: l1) = length (z :: l2)
IHl1: forall (l0 : list B) (x0 : C),
InList x0 (list_map2 f defl defr l1 l0) ->
length l1 = length l0 ->
{y0 : A & {z0 : B & ((f y0 z0 = x0) * (InList y0 l1 * InList z0 l0))%type}}
length l1 = length l2
A, B, C: Type
f: A -> B -> C
defl: list A -> list C
defr: list B -> list C
y: A
l1: list A
z: B
l2: list B
x: C
i: InList x (list_map2 f defl defr l1 l2)
p: length (y :: l1) = length (z :: l2)
IHl1: forall (l0 : list B) (x0 : C),
InList x0 (list_map2 f defl defr l1 l0) ->
length l1 = length l0 ->
{y0 : A & {z0 : B & ((f y0 z0 = x0) * (InList y0 l1 * InList z0 l0))%type}}
y': A
z': B
q: f y' z' = x
r: InList y' l1
s: InList z' l2
{y0 : A &
{z0 : B & ((f y0 z0 = x) * (InList y0 (y :: l1) * InList z0 (z :: l2)))%type}}
    1: apply path_nat_succ, p.
A, B, C: Type
f: A -> B -> C
defl: list A -> list C
defr: list B -> list C
y: A
l1: list A
z: B
l2: list B
x: C
i: InList x (list_map2 f defl defr l1 l2)
p: length (y :: l1) = length (z :: l2)
IHl1: forall (l0 : list B) (x0 : C),
InList x0 (list_map2 f defl defr l1 l0) ->
length l1 = length l0 ->
{y0 : A & {z0 : B & ((f y0 z0 = x0) * (InList y0 l1 * InList z0 l0))%type}}
y': A
z': B
q: f y' z' = x
r: InList y' l1
s: InList z' l2
{y0 : A &
{z0 : B & ((f y0 z0 = x) * (InList y0 (y :: l1) * InList z0 (z :: l2)))%type}}
    exact (y'; z'; (q, (inr r, inr s))).
Defined.

(** [list_map2] is a [list_map] if the first list is a repeated value. *)
Definition list_map2_repeat_l {A B C} (f : A -> B -> C) (x : A) l {defl defr}
  : list_map2 f defl defr (repeat x (length l)) l = list_map (f x) l.
A, B, C: Type
f: A -> B -> C
x: A
l: list B
defl: list A -> list C
defr: list B -> list C
list_map2 f defl defr (repeat x (length l)) l = list_map (f x) l
Proof.
A, B, C: Type
f: A -> B -> C
x: A
l: list B
defl: list A -> list C
defr: list B -> list C
list_map2 f defl defr (repeat x (length l)) l = list_map (f x) l
  induction l as [|y l IHl].
A, B, C: Type
f: A -> B -> C
x: A
defl: list A -> list C
defr: list B -> list C
list_map2 f defl defr (repeat x (length nil)) nil = list_map (f x) nil
A, B, C: Type
f: A -> B -> C
x: A
y: B
l: list B
defl: list A -> list C
defr: list B -> list C
IHl: list_map2 f defl defr (repeat x (length l)) l = list_map (f x) l
list_map2 f defl defr (repeat x (length (y :: l))) (y :: l) =
list_map (f x) (y :: l)
  -
A, B, C: Type
f: A -> B -> C
x: A
defl: list A -> list C
defr: list B -> list C
list_map2 f defl defr (repeat x (length nil)) nil = list_map (f x) nil reflexivity.
  -
A, B, C: Type
f: A -> B -> C
x: A
y: B
l: list B
defl: list A -> list C
defr: list B -> list C
IHl: list_map2 f defl defr (repeat x (length l)) l = list_map (f x) l
list_map2 f defl defr (repeat x (length (y :: l))) (y :: l) =
list_map (f x) (y :: l) cbn; f_ap.
Defined.

(** [list_map2] is a [list_map] if the second list is a repeated value. *)
Definition list_map2_repeat_r {A B C} (f : A -> B -> C) (y : B) l {defl defr}
  : list_map2 f defl defr l (repeat y (length l)) = list_map (fun x => f x y) l.
A, B, C: Type
f: A -> B -> C
y: B
l: list A
defl: list A -> list C
defr: list B -> list C
list_map2 f defl defr l (repeat y (length l)) =
list_map (fun x : A => f x y) l
Proof.
A, B, C: Type
f: A -> B -> C
y: B
l: list A
defl: list A -> list C
defr: list B -> list C
list_map2 f defl defr l (repeat y (length l)) =
list_map (fun x : A => f x y) l
  induction l as [|x l IHl].
A, B, C: Type
f: A -> B -> C
y: B
defl: list A -> list C
defr: list B -> list C
list_map2 f defl defr nil (repeat y (length nil)) =
list_map (fun x : A => f x y) nil
A, B, C: Type
f: A -> B -> C
y: B
x: A
l: list A
defl: list A -> list C
defr: list B -> list C
IHl: list_map2 f defl defr l (repeat y (length l)) =
list_map (fun x0 : A => f x0 y) l
list_map2 f defl defr (x :: l) (repeat y (length (x :: l))) =
list_map (fun x0 : A => f x0 y) (x :: l)
  -
A, B, C: Type
f: A -> B -> C
y: B
defl: list A -> list C
defr: list B -> list C
list_map2 f defl defr nil (repeat y (length nil)) =
list_map (fun x : A => f x y) nil reflexivity.
  -
A, B, C: Type
f: A -> B -> C
y: B
x: A
l: list A
defl: list A -> list C
defr: list B -> list C
IHl: list_map2 f defl defr l (repeat y (length l)) =
list_map (fun x0 : A => f x0 y) l
list_map2 f defl defr (x :: l) (repeat y (length (x :: l))) =
list_map (fun x0 : A => f x0 y) (x :: l) cbn; f_ap.
Defined.

(** ** Reversal *)

(** The length of [reverse_acc] is the sum of the lengths of the two lists. *)
Definition length_reverse_acc@{i|} {A : Type@{i}} (acc l : list A)
  : length (reverse_acc acc l) = length acc + length l.
A: Type
acc, l: list A
length (reverse_acc acc l) = length acc + length l
Proof.
A: Type
acc, l: list A
length (reverse_acc acc l) = length acc + length l
  symmetry.
A: Type
acc, l: list A
length acc + length l = length (reverse_acc acc l)
  induction l as [|x l IHl] in acc |- * using list_ind@{i i}.
A: Type
acc: list A
length acc + length nil = length (reverse_acc acc nil)
A: Type
acc: list A
x: A
l: list A
IHl: forall acc0 : list A, length acc0 + length l = length (reverse_acc acc0 l)
length acc + length (x :: l) = length (reverse_acc acc (x :: l))
  -
A: Type
acc: list A
length acc + length nil = length (reverse_acc acc nil) apply nat_add_zero_r.
  -
A: Type
acc: list A
x: A
l: list A
IHl: forall acc0 : list A, length acc0 + length l = length (reverse_acc acc0 l)
length acc + length (x :: l) = length (reverse_acc acc (x :: l)) rhs_V napply IHl.
A: Type
acc: list A
x: A
l: list A
IHl: forall acc0 : list A, length acc0 + length l = length (reverse_acc acc0 l)
length acc + length (x :: l) = length (x :: acc) + length l
    apply nat_add_succ_r.
Defined.

(** The length of [reverse] is the same as the length of the original list. *)
Definition length_reverse {A : Type} (l : list A)
  : length (reverse l) = length l.
A: Type
l: list A
length (reverse l) = length l
Proof.
A: Type
l: list A
length (reverse l) = length l
  rapply length_reverse_acc.
Defined.

(** The [list_map] of a [reverse_acc] is the [reverse_acc] of the [list_map] of the two lists. *)
Definition list_map_reverse_acc {A B : Type}
  (f : A -> B) (l l' : list A)
  : list_map f (reverse_acc l' l) = reverse_acc (list_map f l') (list_map f l).
A, B: Type
f: A -> B
l, l': list A
list_map f (reverse_acc l' l) = reverse_acc (list_map f l') (list_map f l)
Proof.
A, B: Type
f: A -> B
l, l': list A
list_map f (reverse_acc l' l) = reverse_acc (list_map f l') (list_map f l)
  revert l'; simple_list_induction l a l IHl; intro l'.
A, B: Type
f: A -> B
l': list A
list_map f (reverse_acc l' nil) =
reverse_acc (list_map f l') (list_map f nil)
A, B: Type
f: A -> B
l: list A
IHl: forall l'0 : list A,
list_map f (reverse_acc l'0 l) = reverse_acc (list_map f l'0) (list_map f l)
a: A
l': list A
list_map f (reverse_acc l' (a :: l)) =
reverse_acc (list_map f l') (list_map f (a :: l))
  1: reflexivity.
A, B: Type
f: A -> B
l: list A
IHl: forall l'0 : list A,
list_map f (reverse_acc l'0 l) = reverse_acc (list_map f l'0) (list_map f l)
a: A
l': list A
list_map f (reverse_acc l' (a :: l)) =
reverse_acc (list_map f l') (list_map f (a :: l))
  apply IHl.
Defined.

(** The [list_map] of a reversed list is the reversed [list_map]. *)
Definition list_map_reverse {A B} (f : A -> B) (l : list A)
  : list_map f (reverse l) = reverse (list_map f l).
A, B: Type
f: A -> B
l: list A
list_map f (reverse l) = reverse (list_map f l)
Proof.
A, B: Type
f: A -> B
l: list A
list_map f (reverse l) = reverse (list_map f l)
  napply list_map_reverse_acc.
Defined.

(** [reverse_acc] is the same as concatenating the reversed list with the accumulator. *)
Definition reverse_acc_cons {A : Type} (l l' : list A)
  : reverse_acc l' l = reverse l ++ l'.
A: Type
l, l': list A
reverse_acc l' l = reverse l ++ l'
Proof.
A: Type
l, l': list A
reverse_acc l' l = reverse l ++ l'
  induction l as [|a l IHl] in l' |- *.
A: Type
l': list A
reverse_acc l' nil = reverse nil ++ l'
A: Type
a: A
l, l': list A
IHl: forall l'0 : list A, reverse_acc l'0 l = reverse l ++ l'0
reverse_acc l' (a :: l) = reverse (a :: l) ++ l'
  1: reflexivity.
A: Type
a: A
l, l': list A
IHl: forall l'0 : list A, reverse_acc l'0 l = reverse l ++ l'0
reverse_acc l' (a :: l) = reverse (a :: l) ++ l'
  lhs napply IHl.
A: Type
a: A
l, l': list A
IHl: forall l'0 : list A, reverse_acc l'0 l = reverse l ++ l'0
reverse l ++ a :: l' = reverse (a :: l) ++ l'
  lhs napply (app_assoc _ [a]).
A: Type
a: A
l, l': list A
IHl: forall l'0 : list A, reverse_acc l'0 l = reverse l ++ l'0
(reverse l ++ [a]) ++ l' = reverse (a :: l) ++ l'
  f_ap; symmetry.
A: Type
a: A
l, l': list A
IHl: forall l'0 : list A, reverse_acc l'0 l = reverse l ++ l'0
reverse (a :: l) = reverse l ++ [a]
  apply IHl.
Defined.

(** The [reverse] of a [cons] is the concatenation of the [reverse] with the head. *)
Definition reverse_cons {A : Type} (a : A) (l : list A)
  : reverse (a :: l) = reverse l ++ [a].
A: Type
a: A
l: list A
reverse (a :: l) = reverse l ++ [a]
Proof.
A: Type
a: A
l: list A
reverse (a :: l) = reverse l ++ [a]
  induction l as [|b l IHl] in a |- *.
A: Type
a: A
reverse [a] = reverse nil ++ [a]
A: Type
a, b: A
l: list A
IHl: forall a0 : A, reverse (a0 :: l) = reverse l ++ [a0]
reverse (a :: b :: l) = reverse (b :: l) ++ [a]
  1: reflexivity.
A: Type
a, b: A
l: list A
IHl: forall a0 : A, reverse (a0 :: l) = reverse l ++ [a0]
reverse (a :: b :: l) = reverse (b :: l) ++ [a]
  rewrite IHl.
A: Type
a, b: A
l: list A
IHl: forall a0 : A, reverse (a0 :: l) = reverse l ++ [a0]
reverse (a :: b :: l) = (reverse l ++ [b]) ++ [a]
  rewrite <- app_assoc.
A: Type
a, b: A
l: list A
IHl: forall a0 : A, reverse (a0 :: l) = reverse l ++ [a0]
reverse (a :: b :: l) = reverse l ++ [b] ++ [a]
  cbn; apply reverse_acc_cons.
Defined.

(** The [reverse] of a concatenated list is the concatenation of the reversed lists in reverse order. *)
Definition reverse_app {A : Type} (l l' : list A)
  : reverse (l ++ l') = reverse l' ++ reverse l.
A: Type
l, l': list A
reverse (l ++ l') = reverse l' ++ reverse l
Proof.
A: Type
l, l': list A
reverse (l ++ l') = reverse l' ++ reverse l
  induction l as [|a l IHl] in l' |- *.
A: Type
l': list A
reverse (nil ++ l') = reverse l' ++ reverse nil
A: Type
a: A
l, l': list A
IHl: forall l'0 : list A, reverse (l ++ l'0) = reverse l'0 ++ reverse l
reverse ((a :: l) ++ l') = reverse l' ++ reverse (a :: l)
  1: symmetry; apply app_nil.
A: Type
a: A
l, l': list A
IHl: forall l'0 : list A, reverse (l ++ l'0) = reverse l'0 ++ reverse l
reverse ((a :: l) ++ l') = reverse l' ++ reverse (a :: l)
  simpl.
A: Type
a: A
l, l': list A
IHl: forall l'0 : list A, reverse (l ++ l'0) = reverse l'0 ++ reverse l
reverse (a :: l ++ l') = reverse l' ++ reverse (a :: l)
  lhs napply reverse_cons.
A: Type
a: A
l, l': list A
IHl: forall l'0 : list A, reverse (l ++ l'0) = reverse l'0 ++ reverse l
reverse (l ++ l') ++ [a] = reverse l' ++ reverse (a :: l)
  rhs napply ap.
A: Type
a: A
l, l': list A
IHl: forall l'0 : list A, reverse (l ++ l'0) = reverse l'0 ++ reverse l
reverse (l ++ l') ++ [a] = reverse l' ++ ?Goal
A: Type
a: A
l, l': list A
IHl: forall l'0 : list A, reverse (l ++ l'0) = reverse l'0 ++ reverse l
reverse (a :: l) = ?Goal
  2: napply reverse_cons.
A: Type
a: A
l, l': list A
IHl: forall l'0 : list A, reverse (l ++ l'0) = reverse l'0 ++ reverse l
reverse (l ++ l') ++ [a] = reverse l' ++ reverse l ++ [a]
  rhs napply app_assoc.
A: Type
a: A
l, l': list A
IHl: forall l'0 : list A, reverse (l ++ l'0) = reverse l'0 ++ reverse l
reverse (l ++ l') ++ [a] = (reverse l' ++ reverse l) ++ [a]
  napply (ap (fun l => l ++ [a])).
A: Type
a: A
l, l': list A
IHl: forall l'0 : list A, reverse (l ++ l'0) = reverse l'0 ++ reverse l
reverse (l ++ l') = reverse l' ++ reverse l
  exact (IHl l').
Defined.

(** [reverse] is involutive. *)
Definition reverse_reverse {A : Type} (l : list A)
  : reverse (reverse l) = l.
A: Type
l: list A
reverse (reverse l) = l
Proof.
A: Type
l: list A
reverse (reverse l) = l
  induction l.
A: Type
reverse (reverse nil) = nil
A: Type
a: A
l: list A
IHl: reverse (reverse l) = l
reverse (reverse (a :: l)) = a :: l
  1: reflexivity.
A: Type
a: A
l: list A
IHl: reverse (reverse l) = l
reverse (reverse (a :: l)) = a :: l
  lhs napply ap.
A: Type
a: A
l: list A
IHl: reverse (reverse l) = l
reverse (a :: l) = ?Goal
A: Type
a: A
l: list A
IHl: reverse (reverse l) = l
reverse ?Goal = a :: l
  1: napply reverse_cons.
A: Type
a: A
l: list A
IHl: reverse (reverse l) = l
reverse (reverse l ++ [a]) = a :: l
  lhs napply reverse_app.
A: Type
a: A
l: list A
IHl: reverse (reverse l) = l
reverse [a] ++ reverse (reverse l) = a :: l
  exact (ap _ IHl).
Defined.

(** ** Getting elements *)

(** A variant of [nth] that returns an element of the list and a proof that it is the [n]-th element. *)
Definition nth_lt@{i|} {A : Type@{i}} (l : list A) (n : nat)
  (H : n < length l)
  : { x : A & nth l n = Some x }.
A: Type
l: list A
n: nat
H: n < length l
{x : A & nth l n = Some x}
Proof.
A: Type
l: list A
n: nat
H: n < length l
{x : A & nth l n = Some x}
  induction l as [|a l IHa] in n, H |- * using list_ind@{i i}.
A: Type
n: nat
H: n < length nil
{x : A & nth nil n = Some x}
A: Type
a: A
l: list A
n: nat
H: n < length (a :: l)
IHa: forall n0 : nat, n0 < length l -> {x : A & nth l n0 = Some x}
{x : A & nth (a :: l) n = Some x}
  1: destruct (not_lt_zero_r _ H).
A: Type
a: A
l: list A
n: nat
H: n < length (a :: l)
IHa: forall n0 : nat, n0 < length l -> {x : A & nth l n0 = Some x}
{x : A & nth (a :: l) n = Some x}
  destruct n.
A: Type
a: A
l: list A
H: 0 < length (a :: l)
IHa: forall n : nat, n < length l -> {x : A & nth l n = Some x}
{x : A & nth (a :: l) 0 = Some x}
A: Type
a: A
l: list A
n: nat
H: n.+1 < length (a :: l)
IHa: forall n0 : nat, n0 < length l -> {x : A & nth l n0 = Some x}
{x : A & nth (a :: l) n.+1 = Some x}
  1: by exists a.
A: Type
a: A
l: list A
n: nat
H: n.+1 < length (a :: l)
IHa: forall n0 : nat, n0 < length l -> {x : A & nth l n0 = Some x}
{x : A & nth (a :: l) n.+1 = Some x}
  apply IHa.
A: Type
a: A
l: list A
n: nat
H: n.+1 < length (a :: l)
IHa: forall n0 : nat, n0 < length l -> {x : A & nth l n0 = Some x}
n < length l
  apply leq_pred'.
A: Type
a: A
l: list A
n: nat
H: n.+1 < length (a :: l)
IHa: forall n0 : nat, n0 < length l -> {x : A & nth l n0 = Some x}
n.+2 <= (length l).+1
  exact H.
Defined.

(** A variant of [nth] that always returns an element when we know that the index is in the list. *)
Definition nth' {A : Type} (l : list A) (n : nat) (H : n < length l) : A
  := pr1 (nth_lt l n H).

(** The [nth'] element doesn't depend on the proof that [n < length l]. *)
Definition nth'_nth' {A} (l : list A) (n : nat) (H H' : n < length l)
  : nth' l n H = nth' l n H'.
A: Type
l: list A
n: nat
H, H': n < length l
nth' l n H = nth' l n H'
Proof.
A: Type
l: list A
n: nat
H, H': n < length l
nth' l n H = nth' l n H'
  apply ap, path_ishprop.
Defined.

(** Two equal lists have the same elements in the same positions. *)
Definition nth'_path_list {A : Type} {l1 l2 : list A}
  (p : l1 = l2) {n : nat} (Hn1 : n < length l1) (Hn2 : n < length l2)
  : nth' l1 n Hn1 = nth' l2 n Hn2.
A: Type
l1, l2: list A
p: l1 = l2
n: nat
Hn1: n < length l1
Hn2: n < length l2
nth' l1 n Hn1 = nth' l2 n Hn2
Proof.
A: Type
l1, l2: list A
p: l1 = l2
n: nat
Hn1: n < length l1
Hn2: n < length l2
nth' l1 n Hn1 = nth' l2 n Hn2
  destruct p.
A: Type
l1: list A
n: nat
Hn1, Hn2: n < length l1
nth' l1 n Hn1 = nth' l1 n Hn2
  by apply nth'_nth'.
Defined.

(** The [nth'] element of a list is in the list. *)
Definition inlist_nth'@{i|} {A : Type@{i}} (l : list A) (n : nat)
  (H : n < length l)
  : InList (nth' l n H) l.
A: Type
l: list A
n: nat
H: n < length l
InList (nth' l n H) l
Proof.
A: Type
l: list A
n: nat
H: n < length l
InList (nth' l n H) l
  induction l as [|a l IHa] in n, H |- * using list_ind@{i i}.
A: Type
n: nat
H: n < length nil
InList (nth' nil n H) nil
A: Type
a: A
l: list A
n: nat
H: n < length (a :: l)
IHa: forall (n0 : nat) (H0 : n0 < length l), InList (nth' l n0 H0) l
InList (nth' (a :: l) n H) (a :: l)
  1: destruct (not_lt_zero_r _ H).
A: Type
a: A
l: list A
n: nat
H: n < length (a :: l)
IHa: forall (n0 : nat) (H0 : n0 < length l), InList (nth' l n0 H0) l
InList (nth' (a :: l) n H) (a :: l)
  destruct n.
A: Type
a: A
l: list A
H: 0 < length (a :: l)
IHa: forall (n : nat) (H0 : n < length l), InList (nth' l n H0) l
InList (nth' (a :: l) 0 H) (a :: l)
A: Type
a: A
l: list A
n: nat
H: n.+1 < length (a :: l)
IHa: forall (n0 : nat) (H0 : n0 < length l), InList (nth' l n0 H0) l
InList (nth' (a :: l) n.+1 H) (a :: l)
  1: by left.
A: Type
a: A
l: list A
n: nat
H: n.+1 < length (a :: l)
IHa: forall (n0 : nat) (H0 : n0 < length l), InList (nth' l n0 H0) l
InList (nth' (a :: l) n.+1 H) (a :: l)
  right.
A: Type
a: A
l: list A
n: nat
H: n.+1 < length (a :: l)
IHa: forall (n0 : nat) (H0 : n0 < length l), InList (nth' l n0 H0) l
InList (nth' (a :: l) n.+1 H) l
  apply IHa.
Defined.

(** The [nth'] element of a list is the same as the one given by [nth]. *)
Definition nth_nth' {A} (l : list A) (n : nat) (H : n < length l)
  : nth l n = Some (nth' l n H).
A: Type
l: list A
n: nat
H: n < length l
nth l n = Some (nth' l n H)
Proof.
A: Type
l: list A
n: nat
H: n < length l
nth l n = Some (nth' l n H)
  exact (nth_lt l n H).2.
Defined.

(** The [nth'] element of a [cons] indexed at [n.+1] is the same as the [nth'] element of the tail indexed at [n]. *)
Definition nth'_cons {A : Type} (l : list A) (n : nat) (x : A)
  (H : n < length l) (H' : n.+1 < length (x :: l))
  : nth' (x :: l) n.+1 H' = nth' l n H.
A: Type
l: list A
n: nat
x: A
H: n < length l
H': n.+1 < length (x :: l)
nth' (x :: l) n.+1 H' = nth' l n H
Proof.
A: Type
l: list A
n: nat
x: A
H: n < length l
H': n.+1 < length (x :: l)
nth' (x :: l) n.+1 H' = nth' l n H
  apply isinj_some.
A: Type
l: list A
n: nat
x: A
H: n < length l
H': n.+1 < length (x :: l)
Some (nth' (x :: l) n.+1 H') = Some (nth' l n H)
  nrefine (_^ @ _ @ _).
A: Type
l: list A
n: nat
x: A
H: n < length l
H': n.+1 < length (x :: l)
?Goal0 = Some (nth' (x :: l) n.+1 H')
A: Type
l: list A
n: nat
x: A
H: n < length l
H': n.+1 < length (x :: l)
?Goal0 = ?Goal
A: Type
l: list A
n: nat
x: A
H: n < length l
H': n.+1 < length (x :: l)
?Goal = Some (nth' l n H)
  1,3: rapply nth_nth'.
A: Type
l: list A
n: nat
x: A
H: n < length l
H': n.+1 < length (x :: l)
nth (x :: l) n.+1 = nth l n
  reflexivity.
Defined.

(** The [nth' n] element of a concatenated list [l ++ l'] where [n < length l] is the [nth'] element of [l]. *)
Definition nth'_app@{i|} {A : Type@{i}} (l l' : list A) (n : nat)
  (H : n < length l) (H' : n < length (l ++ l'))
  : nth' (l ++ l') n H' = nth' l n H.
A: Type
l, l': list A
n: nat
H: n < length l
H': n < length (l ++ l')
nth' (l ++ l') n H' = nth' l n H
Proof.
A: Type
l, l': list A
n: nat
H: n < length l
H': n < length (l ++ l')
nth' (l ++ l') n H' = nth' l n H
  induction l as [|a l IHl] in l', n, H, H' |- * using list_ind@{i i}.
A: Type
l': list A
n: nat
H: n < length nil
H': n < length (nil ++ l')
nth' (nil ++ l') n H' = nth' nil n H
A: Type
a: A
l, l': list A
n: nat
H: n < length (a :: l)
H': n < length ((a :: l) ++ l')
IHl: forall (l'0 : list A) (n0 : nat) (H0 : n0 < length l)
(H'0 : n0 < length (l ++ l'0)), nth' (l ++ l'0) n0 H'0 = nth' l n0 H0
nth' ((a :: l) ++ l') n H' = nth' (a :: l) n H
  1: destruct (not_lt_zero_r _ H).
A: Type
a: A
l, l': list A
n: nat
H: n < length (a :: l)
H': n < length ((a :: l) ++ l')
IHl: forall (l'0 : list A) (n0 : nat) (H0 : n0 < length l)
(H'0 : n0 < length (l ++ l'0)), nth' (l ++ l'0) n0 H'0 = nth' l n0 H0
nth' ((a :: l) ++ l') n H' = nth' (a :: l) n H
  destruct n.
A: Type
a: A
l, l': list A
H: 0 < length (a :: l)
H': 0 < length ((a :: l) ++ l')
IHl: forall (l'0 : list A) (n : nat) (H0 : n < length l)
(H'0 : n < length (l ++ l'0)), nth' (l ++ l'0) n H'0 = nth' l n H0
nth' ((a :: l) ++ l') 0 H' = nth' (a :: l) 0 H
A: Type
a: A
l, l': list A
n: nat
H: n.+1 < length (a :: l)
H': n.+1 < length ((a :: l) ++ l')
IHl: forall (l'0 : list A) (n0 : nat) (H0 : n0 < length l)
(H'0 : n0 < length (l ++ l'0)), nth' (l ++ l'0) n0 H'0 = nth' l n0 H0
nth' ((a :: l) ++ l') n.+1 H' = nth' (a :: l) n.+1 H
  1: reflexivity.
A: Type
a: A
l, l': list A
n: nat
H: n.+1 < length (a :: l)
H': n.+1 < length ((a :: l) ++ l')
IHl: forall (l'0 : list A) (n0 : nat) (H0 : n0 < length l)
(H'0 : n0 < length (l ++ l'0)), nth' (l ++ l'0) n0 H'0 = nth' l n0 H0
nth' ((a :: l) ++ l') n.+1 H' = nth' (a :: l) n.+1 H
  by apply IHl.
Defined.

(** The index of an element in a list is the [n] such that the [nth'] element is the element. *)
Definition index_of@{i|} {A : Type@{i}} (l : list A) (x : A)
  : InList x l
    -> sig@{Set i} (fun n : nat => { H : n < length l & nth' l n H = x }).
A: Type
l: list A
x: A
InList x l -> {n : nat & {H : n < length l & nth' l n H = x}}
Proof.
A: Type
l: list A
x: A
InList x l -> {n : nat & {H : n < length l & nth' l n H = x}}
  induction l as [|a l IHl] using list_ind@{i i}.
A: Type
x: A
InList x nil -> {n : nat & {H : n < length nil & nth' nil n H = x}}
A: Type
a: A
l: list A
x: A
IHl: InList x l -> {n : nat & {H : n < length l & nth' l n H = x}}
InList x (a :: l) ->
{n : nat & {H : n < length (a :: l) & nth' (a :: l) n H = x}}
  1: intros x'; destruct x'.
A: Type
a: A
l: list A
x: A
IHl: InList x l -> {n : nat & {H : n < length l & nth' l n H = x}}
InList x (a :: l) ->
{n : nat & {H : n < length (a :: l) & nth' (a :: l) n H = x}}
  intros [| i].
A: Type
a: A
l: list A
x: A
IHl: InList x l -> {n : nat & {H : n < length l & nth' l n H = x}}
p: a = x
{n : nat & {H : n < length (a :: l) & nth' (a :: l) n H = x}}
A: Type
a: A
l: list A
x: A
IHl: InList x l -> {n : nat & {H : n < length l & nth' l n H = x}}
i: InList x l
{n : nat & {H : n < length (a :: l) & nth' (a :: l) n H = x}}
  -
A: Type
a: A
l: list A
x: A
IHl: InList x l -> {n : nat & {H : n < length l & nth' l n H = x}}
p: a = x
{n : nat & {H : n < length (a :: l) & nth' (a :: l) n H = x}} revert a p.
A: Type
l: list A
x: A
IHl: InList x l -> {n : nat & {H : n < length l & nth' l n H = x}}
forall a : A,
a = x -> {n : nat & {H : n < length (a :: l) & nth' (a :: l) n H = x}}
    snapply paths_ind_r@{i i}.
A: Type
l: list A
x: A
IHl: InList x l -> {n : nat & {H : n < length l & nth' l n H = x}}
(fun (y : A) (_ : y = x) =>
 {n : nat & {H : n < length (y :: l) & nth' (y :: l) n H = x}}) x 1
    snrefine (exist@{i i} _ 0 _).
A: Type
l: list A
x: A
IHl: InList x l -> {n : nat & {H : n < length l & nth' l n H = x}}
(fun n : nat => {H : n < length (x :: l) & nth' (x :: l) n H = x}) 0
    snrefine (exist _ _ idpath).
A: Type
l: list A
x: A
IHl: InList x l -> {n : nat & {H : n < length l & nth' l n H = x}}
0 < length (x :: l)
    apply leq_succ.
A: Type
l: list A
x: A
IHl: InList x l -> {n : nat & {H : n < length l & nth' l n H = x}}
0 <=
(fix length (A0 : Type) (l0 : list A0) {struct l0} : nat :=
   match l0 with
   | nil => 0
   | _ :: l1 => (length A0 l1).+1
   end)
  A l
    exact _.
  -
A: Type
a: A
l: list A
x: A
IHl: InList x l -> {n : nat & {H : n < length l & nth' l n H = x}}
i: InList x l
{n : nat & {H : n < length (a :: l) & nth' (a :: l) n H = x}} destruct (IHl i) as [n [H H']].
A: Type
a: A
l: list A
x: A
IHl: InList x l -> {n0 : nat & {H0 : n0 < length l & nth' l n0 H0 = x}}
i: InList x l
n: nat
H: n < length l
H': nth' l n H = x
{n0 : nat & {H0 : n0 < length (a :: l) & nth' (a :: l) n0 H0 = x}}
    snrefine (exist@{i i} _ n.+1 _).
A: Type
a: A
l: list A
x: A
IHl: InList x l -> {n0 : nat & {H0 : n0 < length l & nth' l n0 H0 = x}}
i: InList x l
n: nat
H: n < length l
H': nth' l n H = x
(fun n0 : nat => {H0 : n0 < length (a :: l) & nth' (a :: l) n0 H0 = x}) n.+1
    snrefine (_; _); cbn.
A: Type
a: A
l: list A
x: A
IHl: InList x l -> {n0 : nat & {H0 : n0 < length l & nth' l n0 H0 = x}}
i: InList x l
n: nat
H: n < length l
H': nth' l n H = x
n.+1 < (length l).+1
A: Type
a: A
l: list A
x: A
IHl: InList x l -> {n0 : nat & {H0 : n0 < length l & nth' l n0 H0 = x}}
i: InList x l
n: nat
H: n < length l
H': nth' l n H = x
nth' (a :: l) n.+1 ?Goal = x
    1: apply leq_succ, H.
A: Type
a: A
l: list A
x: A
IHl: InList x l -> {n0 : nat & {H0 : n0 < length l & nth' l n0 H0 = x}}
i: InList x l
n: nat
H: n < length l
H': nth' l n H = x
nth' (a :: l) n.+1 (leq_succ H) = x
    refine (_ @ H').
A: Type
a: A
l: list A
x: A
IHl: InList x l -> {n0 : nat & {H0 : n0 < length l & nth' l n0 H0 = x}}
i: InList x l
n: nat
H: n < length l
H': nth' l n H = x
nth' (a :: l) n.+1 (leq_succ H) = nth' l n H
    apply nth'_cons.
Defined.

(** The [nth] element of a map is the function applied optionally to the [nth] element of the original list. *)
Definition nth_list_map@{i j|} {A : Type@{i}} {B : Type@{j}}
  (f : A -> B) (l : list A) (n : nat)
  : nth (list_map f l) n = functor_option f (nth l n).
A, B: Type
f: A -> B
l: list A
n: nat
nth (list_map f l) n = functor_option f (nth l n)
Proof.
A, B: Type
f: A -> B
l: list A
n: nat
nth (list_map f l) n = functor_option f (nth l n)
  induction l as [|a l IHl] in n |- * using list_ind@{i j}.
A, B: Type
f: A -> B
n: nat
nth (list_map f nil) n = functor_option f (nth nil n)
A, B: Type
f: A -> B
a: A
l: list A
n: nat
IHl: forall n0 : nat, nth (list_map f l) n0 = functor_option f (nth l n0)
nth (list_map f (a :: l)) n = functor_option f (nth (a :: l) n)
  1: by destruct n.
A, B: Type
f: A -> B
a: A
l: list A
n: nat
IHl: forall n0 : nat, nth (list_map f l) n0 = functor_option f (nth l n0)
nth (list_map f (a :: l)) n = functor_option f (nth (a :: l) n)
  destruct n.
A, B: Type
f: A -> B
a: A
l: list A
IHl: forall n : nat, nth (list_map f l) n = functor_option f (nth l n)
nth (list_map f (a :: l)) 0 = functor_option f (nth (a :: l) 0)
A, B: Type
f: A -> B
a: A
l: list A
n: nat
IHl: forall n0 : nat, nth (list_map f l) n0 = functor_option f (nth l n0)
nth (list_map f (a :: l)) n.+1 = functor_option f (nth (a :: l) n.+1)
  1: reflexivity.
A, B: Type
f: A -> B
a: A
l: list A
n: nat
IHl: forall n0 : nat, nth (list_map f l) n0 = functor_option f (nth l n0)
nth (list_map f (a :: l)) n.+1 = functor_option f (nth (a :: l) n.+1)
  apply IHl.
Defined.

(** The [nth'] element of a [list_map] is the function applied to the [nth'] element of the original list. *)
Definition nth'_list_map@{i j|} {A : Type@{i}} {B : Type@{j}}
  (f : A -> B) (l : list A) (n : nat) (H : n < length l)
  (H' : n < length (list_map f l))
  : nth' (list_map f l) n H' = f (nth' l n H).
A, B: Type
f: A -> B
l: list A
n: nat
H: n < length l
H': n < length (list_map f l)
nth' (list_map f l) n H' = f (nth' l n H)
Proof.
A, B: Type
f: A -> B
l: list A
n: nat
H: n < length l
H': n < length (list_map f l)
nth' (list_map f l) n H' = f (nth' l n H)
  induction l as [|a l IHl] in n, H, H' |- * using list_ind@{i j}.
A, B: Type
f: A -> B
n: nat
H: n < length nil
H': n < length (list_map f nil)
nth' (list_map f nil) n H' = f (nth' nil n H)
A, B: Type
f: A -> B
a: A
l: list A
n: nat
H: n < length (a :: l)
H': n < length (list_map f (a :: l))
IHl: forall (n0 : nat) (H0 : n0 < length l) (H'0 : n0 < length (list_map f l)),
nth' (list_map f l) n0 H'0 = f (nth' l n0 H0)
nth' (list_map f (a :: l)) n H' = f (nth' (a :: l) n H)
  1: destruct (not_lt_zero_r _ H).
A, B: Type
f: A -> B
a: A
l: list A
n: nat
H: n < length (a :: l)
H': n < length (list_map f (a :: l))
IHl: forall (n0 : nat) (H0 : n0 < length l) (H'0 : n0 < length (list_map f l)),
nth' (list_map f l) n0 H'0 = f (nth' l n0 H0)
nth' (list_map f (a :: l)) n H' = f (nth' (a :: l) n H)
  destruct n.
A, B: Type
f: A -> B
a: A
l: list A
H: 0 < length (a :: l)
H': 0 < length (list_map f (a :: l))
IHl: forall (n : nat) (H0 : n < length l) (H'0 : n < length (list_map f l)),
nth' (list_map f l) n H'0 = f (nth' l n H0)
nth' (list_map f (a :: l)) 0 H' = f (nth' (a :: l) 0 H)
A, B: Type
f: A -> B
a: A
l: list A
n: nat
H: n.+1 < length (a :: l)
H': n.+1 < length (list_map f (a :: l))
IHl: forall (n0 : nat) (H0 : n0 < length l) (H'0 : n0 < length (list_map f l)),
nth' (list_map f l) n0 H'0 = f (nth' l n0 H0)
nth' (list_map f (a :: l)) n.+1 H' = f (nth' (a :: l) n.+1 H)
  1: reflexivity.
A, B: Type
f: A -> B
a: A
l: list A
n: nat
H: n.+1 < length (a :: l)
H': n.+1 < length (list_map f (a :: l))
IHl: forall (n0 : nat) (H0 : n0 < length l) (H'0 : n0 < length (list_map f l)),
nth' (list_map f l) n0 H'0 = f (nth' l n0 H0)
nth' (list_map f (a :: l)) n.+1 H' = f (nth' (a :: l) n.+1 H)
  apply IHl.
Defined.

(** The [nth'] element of a [list_map2] is the function applied to the [nth'] elements of the original lists. The length of the two lists is required to be the same. *)
Definition nth'_list_map2 {A B C : Type}
  (f : A -> B -> C) (l1 : list A) (l2 : list B)
  (n : nat) defl defr (H : n < length l1) (H' : n < length l2)
  (H'' : n < length (list_map2 f defl defr l1 l2))
  (p : length l1 = length l2)
  : f (nth' l1 n H) (nth' l2 n H') = nth' (list_map2 f defl defr l1 l2) n H''.
A, B, C: Type
f: A -> B -> C
l1: list A
l2: list B
n: nat
defl: list A -> list C
defr: list B -> list C
H: n < length l1
H': n < length l2
H'': n < length (list_map2 f defl defr l1 l2)
p: length l1 = length l2
f (nth' l1 n H) (nth' l2 n H') = nth' (list_map2 f defl defr l1 l2) n H''
Proof.
A, B, C: Type
f: A -> B -> C
l1: list A
l2: list B
n: nat
defl: list A -> list C
defr: list B -> list C
H: n < length l1
H': n < length l2
H'': n < length (list_map2 f defl defr l1 l2)
p: length l1 = length l2
f (nth' l1 n H) (nth' l2 n H') = nth' (list_map2 f defl defr l1 l2) n H''
  revert l2 n defl defr H H' H'' p;
    simple_list_induction l1 a l1 IHl1;
    intros l2 n defl defr H H' H'' p.
A, B, C: Type
f: A -> B -> C
l2: list B
n: nat
defl: list A -> list C
defr: list B -> list C
H: n < length nil
H': n < length l2
H'': n < length (list_map2 f defl defr nil l2)
p: length nil = length l2
f (nth' nil n H) (nth' l2 n H') = nth' (list_map2 f defl defr nil l2) n H''
A, B, C: Type
f: A -> B -> C
l1: list A
IHl1: forall (l0 : list B) (n0 : nat) (defl0 : list A -> list C)
(defr0 : list B -> list C) (H0 : n0 < length l1) (H'0 : n0 < length l0)
(H''0 : n0 < length (list_map2 f defl0 defr0 l1 l0)),
length l1 = length l0 ->
f (nth' l1 n0 H0) (nth' l0 n0 H'0) =
nth' (list_map2 f defl0 defr0 l1 l0) n0 H''0
a: A
l2: list B
n: nat
defl: list A -> list C
defr: list B -> list C
H: n < length (a :: l1)
H': n < length l2
H'': n < length (list_map2 f defl defr (a :: l1) l2)
p: length (a :: l1) = length l2
f (nth' (a :: l1) n H) (nth' l2 n H') =
nth' (list_map2 f defl defr (a :: l1) l2) n H''
  -
A, B, C: Type
f: A -> B -> C
l2: list B
n: nat
defl: list A -> list C
defr: list B -> list C
H: n < length nil
H': n < length l2
H'': n < length (list_map2 f defl defr nil l2)
p: length nil = length l2
f (nth' nil n H) (nth' l2 n H') = nth' (list_map2 f defl defr nil l2) n H'' destruct l2 as [|b l2].
A, B, C: Type
f: A -> B -> C
n: nat
defl: list A -> list C
defr: list B -> list C
H, H': n < length nil
H'': n < length (list_map2 f defl defr nil nil)
p: length nil = length nil
f (nth' nil n H) (nth' nil n H') = nth' (list_map2 f defl defr nil nil) n H''
A, B, C: Type
f: A -> B -> C
b: B
l2: list B
n: nat
defl: list A -> list C
defr: list B -> list C
H: n < length nil
H': n < length (b :: l2)
H'': n < length (list_map2 f defl defr nil (b :: l2))
p: length nil = length (b :: l2)
f (nth' nil n H) (nth' (b :: l2) n H') =
nth' (list_map2 f defl defr nil (b :: l2)) n H''
    +
A, B, C: Type
f: A -> B -> C
n: nat
defl: list A -> list C
defr: list B -> list C
H, H': n < length nil
H'': n < length (list_map2 f defl defr nil nil)
p: length nil = length nil
f (nth' nil n H) (nth' nil n H') = nth' (list_map2 f defl defr nil nil) n H'' destruct (not_lt_zero_r _ H).
    +
A, B, C: Type
f: A -> B -> C
b: B
l2: list B
n: nat
defl: list A -> list C
defr: list B -> list C
H: n < length nil
H': n < length (b :: l2)
H'': n < length (list_map2 f defl defr nil (b :: l2))
p: length nil = length (b :: l2)
f (nth' nil n H) (nth' (b :: l2) n H') =
nth' (list_map2 f defl defr nil (b :: l2)) n H'' inversion p.
  -
A, B, C: Type
f: A -> B -> C
l1: list A
IHl1: forall (l0 : list B) (n0 : nat) (defl0 : list A -> list C)
(defr0 : list B -> list C) (H0 : n0 < length l1) (H'0 : n0 < length l0)
(H''0 : n0 < length (list_map2 f defl0 defr0 l1 l0)),
length l1 = length l0 ->
f (nth' l1 n0 H0) (nth' l0 n0 H'0) =
nth' (list_map2 f defl0 defr0 l1 l0) n0 H''0
a: A
l2: list B
n: nat
defl: list A -> list C
defr: list B -> list C
H: n < length (a :: l1)
H': n < length l2
H'': n < length (list_map2 f defl defr (a :: l1) l2)
p: length (a :: l1) = length l2
f (nth' (a :: l1) n H) (nth' l2 n H') =
nth' (list_map2 f defl defr (a :: l1) l2) n H'' destruct l2 as [|b l2].
A, B, C: Type
f: A -> B -> C
l1: list A
IHl1: forall (l2 : list B) (n0 : nat) (defl0 : list A -> list C)
(defr0 : list B -> list C) (H0 : n0 < length l1) (H'0 : n0 < length l2)
(H''0 : n0 < length (list_map2 f defl0 defr0 l1 l2)),
length l1 = length l2 ->
f (nth' l1 n0 H0) (nth' l2 n0 H'0) =
nth' (list_map2 f defl0 defr0 l1 l2) n0 H''0
a: A
n: nat
defl: list A -> list C
defr: list B -> list C
H: n < length (a :: l1)
H': n < length nil
H'': n < length (list_map2 f defl defr (a :: l1) nil)
p: length (a :: l1) = length nil
f (nth' (a :: l1) n H) (nth' nil n H') =
nth' (list_map2 f defl defr (a :: l1) nil) n H''
A, B, C: Type
f: A -> B -> C
l1: list A
IHl1: forall (l0 : list B) (n0 : nat) (defl0 : list A -> list C)
(defr0 : list B -> list C) (H0 : n0 < length l1) (H'0 : n0 < length l0)
(H''0 : n0 < length (list_map2 f defl0 defr0 l1 l0)),
length l1 = length l0 ->
f (nth' l1 n0 H0) (nth' l0 n0 H'0) =
nth' (list_map2 f defl0 defr0 l1 l0) n0 H''0
a: A
b: B
l2: list B
n: nat
defl: list A -> list C
defr: list B -> list C
H: n < length (a :: l1)
H': n < length (b :: l2)
H'': n < length (list_map2 f defl defr (a :: l1) (b :: l2))
p: length (a :: l1) = length (b :: l2)
f (nth' (a :: l1) n H) (nth' (b :: l2) n H') =
nth' (list_map2 f defl defr (a :: l1) (b :: l2)) n H''
    +
A, B, C: Type
f: A -> B -> C
l1: list A
IHl1: forall (l2 : list B) (n0 : nat) (defl0 : list A -> list C)
(defr0 : list B -> list C) (H0 : n0 < length l1) (H'0 : n0 < length l2)
(H''0 : n0 < length (list_map2 f defl0 defr0 l1 l2)),
length l1 = length l2 ->
f (nth' l1 n0 H0) (nth' l2 n0 H'0) =
nth' (list_map2 f defl0 defr0 l1 l2) n0 H''0
a: A
n: nat
defl: list A -> list C
defr: list B -> list C
H: n < length (a :: l1)
H': n < length nil
H'': n < length (list_map2 f defl defr (a :: l1) nil)
p: length (a :: l1) = length nil
f (nth' (a :: l1) n H) (nth' nil n H') =
nth' (list_map2 f defl defr (a :: l1) nil) n H'' inversion p.
    +
A, B, C: Type
f: A -> B -> C
l1: list A
IHl1: forall (l0 : list B) (n0 : nat) (defl0 : list A -> list C)
(defr0 : list B -> list C) (H0 : n0 < length l1) (H'0 : n0 < length l0)
(H''0 : n0 < length (list_map2 f defl0 defr0 l1 l0)),
length l1 = length l0 ->
f (nth' l1 n0 H0) (nth' l0 n0 H'0) =
nth' (list_map2 f defl0 defr0 l1 l0) n0 H''0
a: A
b: B
l2: list B
n: nat
defl: list A -> list C
defr: list B -> list C
H: n < length (a :: l1)
H': n < length (b :: l2)
H'': n < length (list_map2 f defl defr (a :: l1) (b :: l2))
p: length (a :: l1) = length (b :: l2)
f (nth' (a :: l1) n H) (nth' (b :: l2) n H') =
nth' (list_map2 f defl defr (a :: l1) (b :: l2)) n H'' destruct n.
A, B, C: Type
f: A -> B -> C
l1: list A
IHl1: forall (l0 : list B) (n : nat) (defl0 : list A -> list C)
(defr0 : list B -> list C) (H0 : n < length l1) (H'0 : n < length l0)
(H''0 : n < length (list_map2 f defl0 defr0 l1 l0)),
length l1 = length l0 ->
f (nth' l1 n H0) (nth' l0 n H'0) =
nth' (list_map2 f defl0 defr0 l1 l0) n H''0
a: A
b: B
l2: list B
defl: list A -> list C
defr: list B -> list C
H: 0 < length (a :: l1)
H': 0 < length (b :: l2)
H'': 0 < length (list_map2 f defl defr (a :: l1) (b :: l2))
p: length (a :: l1) = length (b :: l2)
f (nth' (a :: l1) 0 H) (nth' (b :: l2) 0 H') =
nth' (list_map2 f defl defr (a :: l1) (b :: l2)) 0 H''
A, B, C: Type
f: A -> B -> C
l1: list A
IHl1: forall (l0 : list B) (n0 : nat) (defl0 : list A -> list C)
(defr0 : list B -> list C) (H0 : n0 < length l1) (H'0 : n0 < length l0)
(H''0 : n0 < length (list_map2 f defl0 defr0 l1 l0)),
length l1 = length l0 ->
f (nth' l1 n0 H0) (nth' l0 n0 H'0) =
nth' (list_map2 f defl0 defr0 l1 l0) n0 H''0
a: A
b: B
l2: list B
n: nat
defl: list A -> list C
defr: list B -> list C
H: n.+1 < length (a :: l1)
H': n.+1 < length (b :: l2)
H'': n.+1 < length (list_map2 f defl defr (a :: l1) (b :: l2))
p: length (a :: l1) = length (b :: l2)
f (nth' (a :: l1) n.+1 H) (nth' (b :: l2) n.+1 H') =
nth' (list_map2 f defl defr (a :: l1) (b :: l2)) n.+1 H''
      *
A, B, C: Type
f: A -> B -> C
l1: list A
IHl1: forall (l0 : list B) (n : nat) (defl0 : list A -> list C)
(defr0 : list B -> list C) (H0 : n < length l1) (H'0 : n < length l0)
(H''0 : n < length (list_map2 f defl0 defr0 l1 l0)),
length l1 = length l0 ->
f (nth' l1 n H0) (nth' l0 n H'0) =
nth' (list_map2 f defl0 defr0 l1 l0) n H''0
a: A
b: B
l2: list B
defl: list A -> list C
defr: list B -> list C
H: 0 < length (a :: l1)
H': 0 < length (b :: l2)
H'': 0 < length (list_map2 f defl defr (a :: l1) (b :: l2))
p: length (a :: l1) = length (b :: l2)
f (nth' (a :: l1) 0 H) (nth' (b :: l2) 0 H') =
nth' (list_map2 f defl defr (a :: l1) (b :: l2)) 0 H'' reflexivity.
      *
A, B, C: Type
f: A -> B -> C
l1: list A
IHl1: forall (l0 : list B) (n0 : nat) (defl0 : list A -> list C)
(defr0 : list B -> list C) (H0 : n0 < length l1) (H'0 : n0 < length l0)
(H''0 : n0 < length (list_map2 f defl0 defr0 l1 l0)),
length l1 = length l0 ->
f (nth' l1 n0 H0) (nth' l0 n0 H'0) =
nth' (list_map2 f defl0 defr0 l1 l0) n0 H''0
a: A
b: B
l2: list B
n: nat
defl: list A -> list C
defr: list B -> list C
H: n.+1 < length (a :: l1)
H': n.+1 < length (b :: l2)
H'': n.+1 < length (list_map2 f defl defr (a :: l1) (b :: l2))
p: length (a :: l1) = length (b :: l2)
f (nth' (a :: l1) n.+1 H) (nth' (b :: l2) n.+1 H') =
nth' (list_map2 f defl defr (a :: l1) (b :: l2)) n.+1 H'' erewrite 3 nth'_cons.
A, B, C: Type
f: A -> B -> C
l1: list A
IHl1: forall (l0 : list B) (n0 : nat) (defl0 : list A -> list C)
(defr0 : list B -> list C) (H0 : n0 < length l1) (H'0 : n0 < length l0)
(H''0 : n0 < length (list_map2 f defl0 defr0 l1 l0)),
length l1 = length l0 ->
f (nth' l1 n0 H0) (nth' l0 n0 H'0) =
nth' (list_map2 f defl0 defr0 l1 l0) n0 H''0
a: A
b: B
l2: list B
n: nat
defl: list A -> list C
defr: list B -> list C
H: n.+1 < length (a :: l1)
H': n.+1 < length (b :: l2)
H'': n.+1 < length (list_map2 f defl defr (a :: l1) (b :: l2))
p: length (a :: l1) = length (b :: l2)
f (nth' l1 n (leq_pred' H)) (nth' l2 n (leq_pred' H')) =
nth'
  ((fix list_map2
      (A0 B0 C0 : Type) (f0 : A0 -> B0 -> C0) (def_l : list A0 -> list C0)
      (def_r : list B0 -> list C0) (l0 : list A0) 
      (l3 : list B0) {struct l0} : list C0 :=
      match l0 with
      | nil => match l3 with
               | nil => nil
               | _ :: _ => def_r l3
               end
      | x :: l4 =>
          match l3 with
          | nil => def_l l0
          | y :: l5 => f0 x y :: list_map2 A0 B0 C0 f0 def_l def_r l4 l5
          end
      end)
     A B C f defl defr l1 l2)
  n (leq_pred' H'')
        apply IHl1.
A, B, C: Type
f: A -> B -> C
l1: list A
IHl1: forall (l0 : list B) (n0 : nat) (defl0 : list A -> list C)
(defr0 : list B -> list C) (H0 : n0 < length l1) (H'0 : n0 < length l0)
(H''0 : n0 < length (list_map2 f defl0 defr0 l1 l0)),
length l1 = length l0 ->
f (nth' l1 n0 H0) (nth' l0 n0 H'0) =
nth' (list_map2 f defl0 defr0 l1 l0) n0 H''0
a: A
b: B
l2: list B
n: nat
defl: list A -> list C
defr: list B -> list C
H: n.+1 < length (a :: l1)
H': n.+1 < length (b :: l2)
H'': n.+1 < length (list_map2 f defl defr (a :: l1) (b :: l2))
p: length (a :: l1) = length (b :: l2)
length l1 = length l2
        by apply path_nat_succ.
Defined.

(** The [nth'] element of a [repeat] is the repeated value. *)
Definition nth'_repeat@{i|} {A : Type@{i}} (x : A) (i n : nat)
  (H : i < length (repeat x n))
  : nth' (repeat x n) i H = x.
A: Type
x: A
i, n: nat
H: i < length (repeat x n)
nth' (repeat x n) i H = x
Proof.
A: Type
x: A
i, n: nat
H: i < length (repeat x n)
nth' (repeat x n) i H = x
  induction n as [|n IHn] in i, H |- * using nat_ind@{i}.
A: Type
x: A
i: nat
H: i < length (repeat x 0)
nth' (repeat x 0) i H = x
A: Type
x: A
i, n: nat
H: i < length (repeat x n.+1)
IHn: forall (i0 : nat) (H0 : i0 < length (repeat x n)),
nth' (repeat x n) i0 H0 = x
nth' (repeat x n.+1) i H = x
  1: destruct (not_lt_zero_r _ H).
A: Type
x: A
i, n: nat
H: i < length (repeat x n.+1)
IHn: forall (i0 : nat) (H0 : i0 < length (repeat x n)),
nth' (repeat x n) i0 H0 = x
nth' (repeat x n.+1) i H = x
  destruct i.
A: Type
x: A
n: nat
H: 0 < length (repeat x n.+1)
IHn: forall (i : nat) (H0 : i < length (repeat x n)), nth' (repeat x n) i H0 = x
nth' (repeat x n.+1) 0 H = x
A: Type
x: A
i, n: nat
H: i.+1 < length (repeat x n.+1)
IHn: forall (i0 : nat) (H0 : i0 < length (repeat x n)),
nth' (repeat x n) i0 H0 = x
nth' (repeat x n.+1) i.+1 H = x
  1: reflexivity.
A: Type
x: A
i, n: nat
H: i.+1 < length (repeat x n.+1)
IHn: forall (i0 : nat) (H0 : i0 < length (repeat x n)),
nth' (repeat x n) i0 H0 = x
nth' (repeat x n.+1) i.+1 H = x
  apply IHn.
Defined.

(** Two lists are equal if their [nth'] elements are equal. *)
Definition path_list_nth'@{i|} {A : Type@{i}} (l l' : list A)
  (p : length l = length l')
  : (forall n (H : n < length l), nth' l n H = nth' l' n (p # H))
    -> l = l'.
A: Type
l, l': list A
p: length l = length l'
(forall (n : nat) (H : n < length l),
 nth' l n H = nth' l' n (transport (lt n) p H)) ->
l = l'
Proof.
A: Type
l, l': list A
p: length l = length l'
(forall (n : nat) (H : n < length l),
 nth' l n H = nth' l' n (transport (lt n) p H)) ->
l = l'
  intros H.
A: Type
l, l': list A
p: length l = length l'
H: forall (n : nat) (H0 : n < length l),
nth' l n H0 = nth' l' n (transport (lt n) p H0)
l = l'
  induction l as [|a l IHl] in l', p, H |- * using list_ind@{i i}.
A: Type
l': list A
p: length nil = length l'
H: forall (n : nat) (H0 : n < length nil),
nth' nil n H0 = nth' l' n (transport (lt n) p H0)
nil = l'
A: Type
a: A
l, l': list A
p: length (a :: l) = length l'
H: forall (n : nat) (H0 : n < length (a :: l)),
nth' (a :: l) n H0 = nth' l' n (transport (lt n) p H0)
IHl: forall (l'0 : list A) (p0 : length l = length l'0),
(forall (n : nat) (H0 : n < length l),
 nth' l n H0 = nth' l'0 n (transport (lt n) p0 H0)) ->
l = l'0
a :: l = l'
  {
A: Type
l': list A
p: length nil = length l'
H: forall (n : nat) (H0 : n < length nil),
nth' nil n H0 = nth' l' n (transport (lt n) p H0)
nil = l' destruct l'.
A: Type
p: length nil = length nil
H: forall (n : nat) (H0 : n < length nil),
nth' nil n H0 = nth' nil n (transport (lt n) p H0)
nil = nil
A: Type
a: A
l': list A
p: length nil = length (a :: l')
H: forall (n : nat) (H0 : n < length nil),
nth' nil n H0 = nth' (a :: l') n (transport (lt n) p H0)
nil = a :: l'
    -
A: Type
p: length nil = length nil
H: forall (n : nat) (H0 : n < length nil),
nth' nil n H0 = nth' nil n (transport (lt n) p H0)
nil = nil reflexivity.
    -
A: Type
a: A
l': list A
p: length nil = length (a :: l')
H: forall (n : nat) (H0 : n < length nil),
nth' nil n H0 = nth' (a :: l') n (transport (lt n) p H0)
nil = a :: l' discriminate. }
A: Type
a: A
l, l': list A
p: length (a :: l) = length l'
H: forall (n : nat) (H0 : n < length (a :: l)),
nth' (a :: l) n H0 = nth' l' n (transport (lt n) p H0)
IHl: forall (l'0 : list A) (p0 : length l = length l'0),
(forall (n : nat) (H0 : n < length l),
 nth' l n H0 = nth' l'0 n (transport (lt n) p0 H0)) ->
l = l'0
a :: l = l'
  destruct l' as [|a' l'].
A: Type
a: A
l: list A
p: length (a :: l) = length nil
H: forall (n : nat) (H0 : n < length (a :: l)),
nth' (a :: l) n H0 = nth' nil n (transport (lt n) p H0)
IHl: forall (l' : list A) (p0 : length l = length l'),
(forall (n : nat) (H0 : n < length l),
 nth' l n H0 = nth' l' n (transport (lt n) p0 H0)) ->
l = l'
a :: l = nil
A: Type
a: A
l: list A
a': A
l': list A
p: length (a :: l) = length (a' :: l')
H: forall (n : nat) (H0 : n < length (a :: l)),
nth' (a :: l) n H0 = nth' (a' :: l') n (transport (lt n) p H0)
IHl: forall (l'0 : list A) (p0 : length l = length l'0),
(forall (n : nat) (H0 : n < length l),
 nth' l n H0 = nth' l'0 n (transport (lt n) p0 H0)) ->
l = l'0
a :: l = a' :: l'
  1: discriminate.
A: Type
a: A
l: list A
a': A
l': list A
p: length (a :: l) = length (a' :: l')
H: forall (n : nat) (H0 : n < length (a :: l)),
nth' (a :: l) n H0 = nth' (a' :: l') n (transport (lt n) p H0)
IHl: forall (l'0 : list A) (p0 : length l = length l'0),
(forall (n : nat) (H0 : n < length l),
 nth' l n H0 = nth' l'0 n (transport (lt n) p0 H0)) ->
l = l'0
a :: l = a' :: l'
  f_ap.
A: Type
a: A
l: list A
a': A
l': list A
p: length (a :: l) = length (a' :: l')
H: forall (n : nat) (H0 : n < length (a :: l)),
nth' (a :: l) n H0 = nth' (a' :: l') n (transport (lt n) p H0)
IHl: forall (l'0 : list A) (p0 : length l = length l'0),
(forall (n : nat) (H0 : n < length l),
 nth' l n H0 = nth' l'0 n (transport (lt n) p0 H0)) ->
l = l'0
a = a'
A: Type
a: A
l: list A
a': A
l': list A
p: length (a :: l) = length (a' :: l')
H: forall (n : nat) (H0 : n < length (a :: l)),
nth' (a :: l) n H0 = nth' (a' :: l') n (transport (lt n) p H0)
IHl: forall (l'0 : list A) (p0 : length l = length l'0),
(forall (n : nat) (H0 : n < length l),
 nth' l n H0 = nth' l'0 n (transport (lt n) p0 H0)) ->
l = l'0
l = l'
  -
A: Type
a: A
l: list A
a': A
l': list A
p: length (a :: l) = length (a' :: l')
H: forall (n : nat) (H0 : n < length (a :: l)),
nth' (a :: l) n H0 = nth' (a' :: l') n (transport (lt n) p H0)
IHl: forall (l'0 : list A) (p0 : length l = length l'0),
(forall (n : nat) (H0 : n < length l),
 nth' l n H0 = nth' l'0 n (transport (lt n) p0 H0)) ->
l = l'0
a = a' exact (H 0 _).
  -
A: Type
a: A
l: list A
a': A
l': list A
p: length (a :: l) = length (a' :: l')
H: forall (n : nat) (H0 : n < length (a :: l)),
nth' (a :: l) n H0 = nth' (a' :: l') n (transport (lt n) p H0)
IHl: forall (l'0 : list A) (p0 : length l = length l'0),
(forall (n : nat) (H0 : n < length l),
 nth' l n H0 = nth' l'0 n (transport (lt n) p0 H0)) ->
l = l'0
l = l' snapply IHl.
A: Type
a: A
l: list A
a': A
l': list A
p: length (a :: l) = length (a' :: l')
H: forall (n : nat) (H0 : n < length (a :: l)),
nth' (a :: l) n H0 = nth' (a' :: l') n (transport (lt n) p H0)
IHl: forall (l'0 : list A) (p0 : length l = length l'0),
(forall (n : nat) (H0 : n < length l),
 nth' l n H0 = nth' l'0 n (transport (lt n) p0 H0)) ->
l = l'0
length l = length l'
A: Type
a: A
l: list A
a': A
l': list A
p: length (a :: l) = length (a' :: l')
H: forall (n : nat) (H0 : n < length (a :: l)),
nth' (a :: l) n H0 = nth' (a' :: l') n (transport (lt n) p H0)
IHl: forall (l'0 : list A) (p0 : length l = length l'0),
(forall (n : nat) (H0 : n < length l),
 nth' l n H0 = nth' l'0 n (transport (lt n) p0 H0)) ->
l = l'0
forall (n : nat) (H0 : n < length l),
nth' l n H0 = nth' l' n (transport (lt n) ?p H0)
    1: by apply path_nat_succ.
A: Type
a: A
l: list A
a': A
l': list A
p: length (a :: l) = length (a' :: l')
H: forall (n : nat) (H0 : n < length (a :: l)),
nth' (a :: l) n H0 = nth' (a' :: l') n (transport (lt n) p H0)
IHl: forall (l'0 : list A) (p0 : length l = length l'0),
(forall (n : nat) (H0 : n < length l),
 nth' l n H0 = nth' l'0 n (transport (lt n) p0 H0)) ->
l = l'0
forall (n : nat) (H0 : n < length l),
nth' l n H0 =
nth' l' n (transport (lt n) (path_nat_succ (length l) (length l') p) H0)
    intros n Hn.
A: Type
a: A
l: list A
a': A
l': list A
p: length (a :: l) = length (a' :: l')
H: forall (n0 : nat) (H0 : n0 < length (a :: l)),
nth' (a :: l) n0 H0 = nth' (a' :: l') n0 (transport (lt n0) p H0)
IHl: forall (l'0 : list A) (p0 : length l = length l'0),
(forall (n0 : nat) (H0 : n0 < length l),
 nth' l n0 H0 = nth' l'0 n0 (transport (lt n0) p0 H0)) ->
l = l'0
n: nat
Hn: n < length l
nth' l n Hn =
nth' l' n (transport (lt n) (path_nat_succ (length l) (length l') p) Hn)
    snrefine ((nth'_cons l n a Hn _)^ @ _).
A: Type
a: A
l: list A
a': A
l': list A
p: length (a :: l) = length (a' :: l')
H: forall (n0 : nat) (H0 : n0 < length (a :: l)),
nth' (a :: l) n0 H0 = nth' (a' :: l') n0 (transport (lt n0) p H0)
IHl: forall (l'0 : list A) (p0 : length l = length l'0),
(forall (n0 : nat) (H0 : n0 < length l),
 nth' l n0 H0 = nth' l'0 n0 (transport (lt n0) p0 H0)) ->
l = l'0
n: nat
Hn: n < length l
n.+1 < length (a :: l)
A: Type
a: A
l: list A
a': A
l': list A
p: length (a :: l) = length (a' :: l')
H: forall (n0 : nat) (H0 : n0 < length (a :: l)),
nth' (a :: l) n0 H0 = nth' (a' :: l') n0 (transport (lt n0) p H0)
IHl: forall (l'0 : list A) (p0 : length l = length l'0),
(forall (n0 : nat) (H0 : n0 < length l),
 nth' l n0 H0 = nth' l'0 n0 (transport (lt n0) p0 H0)) ->
l = l'0
n: nat
Hn: n < length l
nth' (a :: l) n.+1 ?H' =
nth' l' n (transport (lt n) (path_nat_succ (length l) (length l') p) Hn)
    1: apply leq_succ, Hn.
A: Type
a: A
l: list A
a': A
l': list A
p: length (a :: l) = length (a' :: l')
H: forall (n0 : nat) (H0 : n0 < length (a :: l)),
nth' (a :: l) n0 H0 = nth' (a' :: l') n0 (transport (lt n0) p H0)
IHl: forall (l'0 : list A) (p0 : length l = length l'0),
(forall (n0 : nat) (H0 : n0 < length l),
 nth' l n0 H0 = nth' l'0 n0 (transport (lt n0) p0 H0)) ->
l = l'0
n: nat
Hn: n < length l
nth' (a :: l) n.+1 (leq_succ Hn) =
nth' l' n (transport (lt n) (path_nat_succ (length l) (length l') p) Hn)
    lhs napply H.
A: Type
a: A
l: list A
a': A
l': list A
p: length (a :: l) = length (a' :: l')
H: forall (n0 : nat) (H0 : n0 < length (a :: l)),
nth' (a :: l) n0 H0 = nth' (a' :: l') n0 (transport (lt n0) p H0)
IHl: forall (l'0 : list A) (p0 : length l = length l'0),
(forall (n0 : nat) (H0 : n0 < length l),
 nth' l n0 H0 = nth' l'0 n0 (transport (lt n0) p0 H0)) ->
l = l'0
n: nat
Hn: n < length l
nth' (a' :: l') n.+1 (transport (lt n.+1) p (leq_succ Hn)) =
nth' l' n (transport (lt n) (path_nat_succ (length l) (length l') p) Hn)
    napply nth'_cons.
Defined.

(** The [nth n] element of a concatenated list [l ++ l'] where [n < length l] is the [nth] element of [l]. *)
Definition nth_app@{i|} {A : Type@{i}} (l l' : list A) (n : nat)
  (H : n < length l)
  : nth (l ++ l') n = nth l n.
A: Type
l, l': list A
n: nat
H: n < length l
nth (l ++ l') n = nth l n
Proof.
A: Type
l, l': list A
n: nat
H: n < length l
nth (l ++ l') n = nth l n
  induction l as [|a l IHl] in l', n, H |- * using list_ind@{i i}.
A: Type
l': list A
n: nat
H: n < length nil
nth (nil ++ l') n = nth nil n
A: Type
a: A
l, l': list A
n: nat
H: n < length (a :: l)
IHl: forall (l'0 : list A) (n0 : nat),
n0 < length l -> nth (l ++ l'0) n0 = nth l n0
nth ((a :: l) ++ l') n = nth (a :: l) n
  1: destruct (not_lt_zero_r _ H).
A: Type
a: A
l, l': list A
n: nat
H: n < length (a :: l)
IHl: forall (l'0 : list A) (n0 : nat),
n0 < length l -> nth (l ++ l'0) n0 = nth l n0
nth ((a :: l) ++ l') n = nth (a :: l) n
  destruct n.
A: Type
a: A
l, l': list A
H: 0 < length (a :: l)
IHl: forall (l'0 : list A) (n : nat), n < length l -> nth (l ++ l'0) n = nth l n
nth ((a :: l) ++ l') 0 = nth (a :: l) 0
A: Type
a: A
l, l': list A
n: nat
H: n.+1 < length (a :: l)
IHl: forall (l'0 : list A) (n0 : nat),
n0 < length l -> nth (l ++ l'0) n0 = nth l n0
nth ((a :: l) ++ l') n.+1 = nth (a :: l) n.+1
  1: reflexivity.
A: Type
a: A
l, l': list A
n: nat
H: n.+1 < length (a :: l)
IHl: forall (l'0 : list A) (n0 : nat),
n0 < length l -> nth (l ++ l'0) n0 = nth l n0
nth ((a :: l) ++ l') n.+1 = nth (a :: l) n.+1
  by apply IHl, leq_pred'.
Defined.

(** The [nth i] element where [pred (length l) = i] is the last element of the list. *)
Definition nth_last {A : Type} (l : list A) (i : nat) (p : nat_pred (length l) = i)
  : nth l i = last l.
A: Type
l: list A
i: nat
p: nat_pred (length l) = i
nth l i = last l
Proof.
A: Type
l: list A
i: nat
p: nat_pred (length l) = i
nth l i = last l
  destruct p.
A: Type
l: list A
nth l (nat_pred (length l)) = last l
  induction l as [|a l IHl].
A: Type
nth nil (nat_pred (length nil)) = last nil
A: Type
a: A
l: list A
IHl: nth l (nat_pred (length l)) = last l
nth (a :: l) (nat_pred (length (a :: l))) = last (a :: l)
  1: reflexivity.
A: Type
a: A
l: list A
IHl: nth l (nat_pred (length l)) = last l
nth (a :: l) (nat_pred (length (a :: l))) = last (a :: l)
  destruct l as [|b l].
A: Type
a: A
IHl: nth nil (nat_pred (length nil)) = last nil
nth [a] (nat_pred (length [a])) = last [a]
A: Type
a, b: A
l: list A
IHl: nth (b :: l) (nat_pred (length (b :: l))) = last (b :: l)
nth (a :: b :: l) (nat_pred (length (a :: b :: l))) = last (a :: b :: l)
  1: reflexivity.
A: Type
a, b: A
l: list A
IHl: nth (b :: l) (nat_pred (length (b :: l))) = last (b :: l)
nth (a :: b :: l) (nat_pred (length (a :: b :: l))) = last (a :: b :: l)
  cbn; exact IHl.
Defined.

(** The last element of a list with an element appended is the appended element. *)
Definition last_app {A : Type} (l : list A) (x : A)
  : last (l ++ [x]) = Some x.
A: Type
l: list A
x: A
last (l ++ [x]) = Some x
Proof.
A: Type
l: list A
x: A
last (l ++ [x]) = Some x
  induction l as [|a l IHl] in x |- *.
A: Type
x: A
last (nil ++ [x]) = Some x
A: Type
a: A
l: list A
x: A
IHl: forall x0 : A, last (l ++ [x0]) = Some x0
last ((a :: l) ++ [x]) = Some x
  1: reflexivity.
A: Type
a: A
l: list A
x: A
IHl: forall x0 : A, last (l ++ [x0]) = Some x0
last ((a :: l) ++ [x]) = Some x
  destruct l.
A: Type
a, x: A
IHl: forall x0 : A, last (nil ++ [x0]) = Some x0
last ([a] ++ [x]) = Some x
A: Type
a, a0: A
l: list A
x: A
IHl: forall x0 : A, last ((a0 :: l) ++ [x0]) = Some x0
last ((a :: a0 :: l) ++ [x]) = Some x
  1: reflexivity.
A: Type
a, a0: A
l: list A
x: A
IHl: forall x0 : A, last ((a0 :: l) ++ [x0]) = Some x0
last ((a :: a0 :: l) ++ [x]) = Some x
  cbn; apply IHl.
Defined.

Definition nth'_last_app@{i|} {A : Type@{i}} (l : list A) (a : A)
  (H : length l < length (l ++ [a]))
  : nth' (l ++ [a]) (length l) H = a.
A: Type
l: list A
a: A
H: length l < length (l ++ [a])
nth' (l ++ [a]) (length l) H = a
Proof.
A: Type
l: list A
a: A
H: length l < length (l ++ [a])
nth' (l ++ [a]) (length l) H = a
  revert a H; simple_list_induction l a' l IHl; intros a H.
A: Type
a: A
H: length nil < length (nil ++ [a])
nth' (nil ++ [a]) (length nil) H = a
A: Type
l: list A
IHl: forall (a0 : A) (H0 : length l < length (l ++ [a0])),
nth' (l ++ [a0]) (length l) H0 = a0
a', a: A
H: length (a' :: l) < length ((a' :: l) ++ [a])
nth' ((a' :: l) ++ [a]) (length (a' :: l)) H = a
  1: reflexivity.
A: Type
l: list A
IHl: forall (a0 : A) (H0 : length l < length (l ++ [a0])),
nth' (l ++ [a0]) (length l) H0 = a0
a', a: A
H: length (a' :: l) < length ((a' :: l) ++ [a])
nth' ((a' :: l) ++ [a]) (length (a' :: l)) H = a
  apply IHl.
Defined.

(** ** Removing elements *)

(** These functions allow surgery to be performed on a given list. *)

(** *** Drop *)

(** [drop n l] removes the first [n] elements of [l]. *)
Fixpoint drop {A : Type} (n : nat) (l : list A) : list A :=
  match n with
  | 0 => l
  | n.+1 => drop n (tail l)
  end.

(** A [drop] of zero elements is the identity, by definition. *)
Definition drop_0 {A : Type} (l : list A) : drop 0 l = l := idpath.

(** A [drop] of one element is the tail of the list, by definition. *)
Definition drop_1 {A : Type} (l : list A) : drop 1 l = tail l := idpath.

(** A [drop] of the empty list is the empty list. *)
Definition drop_nil {A : Type} (n : nat)
  : drop n (@nil A) = nil.
A: Type
n: nat
drop n nil = nil
Proof.
A: Type
n: nat
drop n nil = nil
  by induction n.
Defined.

(** A [drop] of [n] elements with [length l <= n] is the empty list. *)
Definition drop_length_leq@{i|} {A : Type@{i}} (n : nat) (l : list A)
  (H : length l <= n)
  : drop n l = nil.
A: Type
n: nat
l: list A
H: length l <= n
drop n l = nil
Proof.
A: Type
n: nat
l: list A
H: length l <= n
drop n l = nil
  induction l as [|a l IHl] in H, n |- * using list_ind@{i i}.
A: Type
n: nat
H: length nil <= n
drop n nil = nil
A: Type
n: nat
a: A
l: list A
H: length (a :: l) <= n
IHl: forall n0 : nat, length l <= n0 -> drop n0 l = nil
drop n (a :: l) = nil
  1: apply drop_nil.
A: Type
n: nat
a: A
l: list A
H: length (a :: l) <= n
IHl: forall n0 : nat, length l <= n0 -> drop n0 l = nil
drop n (a :: l) = nil
  destruct n.
A: Type
a: A
l: list A
H: length (a :: l) <= 0
IHl: forall n : nat, length l <= n -> drop n l = nil
drop 0 (a :: l) = nil
A: Type
n: nat
a: A
l: list A
H: length (a :: l) <= n.+1
IHl: forall n0 : nat, length l <= n0 -> drop n0 l = nil
drop n.+1 (a :: l) = nil
  1: destruct (not_lt_zero_r _ H).
A: Type
n: nat
a: A
l: list A
H: length (a :: l) <= n.+1
IHl: forall n0 : nat, length l <= n0 -> drop n0 l = nil
drop n.+1 (a :: l) = nil
  cbn; apply IHl.
A: Type
n: nat
a: A
l: list A
H: length (a :: l) <= n.+1
IHl: forall n0 : nat, length l <= n0 -> drop n0 l = nil
length l <= n
  apply leq_pred'.
A: Type
n: nat
a: A
l: list A
H: length (a :: l) <= n.+1
IHl: forall n0 : nat, length l <= n0 -> drop n0 l = nil
(length l).+1 <= n.+1
  exact H.
Defined.

(** The length of a [drop n] is the length of the original list minus [n]. *)
Definition length_drop@{i|} {A : Type@{i}} (n : nat) (l : list A)
  : length (drop n l) = length l - n.
A: Type
n: nat
l: list A
length (drop n l) = length l - n
Proof.
A: Type
n: nat
l: list A
length (drop n l) = length l - n
  induction l as [|a l IHl] in n |- * using list_ind@{i i}.
A: Type
n: nat
length (drop n nil) = length nil - n
A: Type
n: nat
a: A
l: list A
IHl: forall n0 : nat, length (drop n0 l) = length l - n0
length (drop n (a :: l)) = length (a :: l) - n
  1: by rewrite drop_nil.
A: Type
n: nat
a: A
l: list A
IHl: forall n0 : nat, length (drop n0 l) = length l - n0
length (drop n (a :: l)) = length (a :: l) - n
  destruct n.
A: Type
a: A
l: list A
IHl: forall n : nat, length (drop n l) = length l - n
length (drop 0 (a :: l)) = length (a :: l) - 0
A: Type
n: nat
a: A
l: list A
IHl: forall n0 : nat, length (drop n0 l) = length l - n0
length (drop n.+1 (a :: l)) = length (a :: l) - n.+1
  1: reflexivity.
A: Type
n: nat
a: A
l: list A
IHl: forall n0 : nat, length (drop n0 l) = length l - n0
length (drop n.+1 (a :: l)) = length (a :: l) - n.+1
  exact (IHl n).
Defined.

(** An element of a [drop] is an element of the original list. *)
Definition drop_inlist@{i|} {A : Type@{i}} (n : nat) (l : list A) (x : A)
  : InList x (drop n l) -> InList x l.
A: Type
n: nat
l: list A
x: A
InList x (drop n l) -> InList x l
Proof.
A: Type
n: nat
l: list A
x: A
InList x (drop n l) -> InList x l
  intros H.
A: Type
n: nat
l: list A
x: A
H: InList x (drop n l)
InList x l
  induction l as [|a l IHl] in n, H, x |- * using list_ind@{i i}.
A: Type
n: nat
x: A
H: InList x (drop n nil)
InList x nil
A: Type
n: nat
a: A
l: list A
x: A
H: InList x (drop n (a :: l))
IHl: forall (n0 : nat) (x0 : A), InList x0 (drop n0 l) -> InList x0 l
InList x (a :: l)
  1: rewrite drop_nil in H; contradiction.
A: Type
n: nat
a: A
l: list A
x: A
H: InList x (drop n (a :: l))
IHl: forall (n0 : nat) (x0 : A), InList x0 (drop n0 l) -> InList x0 l
InList x (a :: l)
  destruct n.
A: Type
a: A
l: list A
x: A
H: InList x (drop 0 (a :: l))
IHl: forall (n : nat) (x0 : A), InList x0 (drop n l) -> InList x0 l
InList x (a :: l)
A: Type
n: nat
a: A
l: list A
x: A
H: InList x (drop n.+1 (a :: l))
IHl: forall (n0 : nat) (x0 : A), InList x0 (drop n0 l) -> InList x0 l
InList x (a :: l)
  1: exact H.
A: Type
n: nat
a: A
l: list A
x: A
H: InList x (drop n.+1 (a :: l))
IHl: forall (n0 : nat) (x0 : A), InList x0 (drop n0 l) -> InList x0 l
InList x (a :: l)
  right; exact (IHl _ _ H).
Defined.

(** *** Take *)

(** [take n l] keeps the first [n] elements of [l] and returns [l] if [n >= length l]. *)
Fixpoint take {A : Type} (n : nat) (l : list A) : list A :=
  match n, l with
  | n.+1, x :: l => x :: take n l
  | _, _ => nil
  end.

(** A [take] of zero elements is the empty list, by definition. *)
Definition take_0 {A : Type} (l : list A) : take 0 l = nil := idpath.

(** A [take] of the empty list is the empty list. *)
Definition take_nil {A : Type} (n : nat) : take n (@nil A) = nil.
A: Type
n: nat
take n nil = nil
Proof.
A: Type
n: nat
take n nil = nil
  by destruct n.
Defined.

(** A [take] of [n] elements with [length l <= n] is the original list. *)
Definition take_length_leq@{i|} {A : Type@{i}} (n : nat) (l : list A)
  (H : length l <= n)
  : take n l = l.
A: Type
n: nat
l: list A
H: length l <= n
take n l = l
Proof.
A: Type
n: nat
l: list A
H: length l <= n
take n l = l
  induction l as [|a l IHl] in H, n |- * using list_ind@{i i}.
A: Type
n: nat
H: length nil <= n
take n nil = nil
A: Type
n: nat
a: A
l: list A
H: length (a :: l) <= n
IHl: forall n0 : nat, length l <= n0 -> take n0 l = l
take n (a :: l) = a :: l
  1: apply take_nil.
A: Type
n: nat
a: A
l: list A
H: length (a :: l) <= n
IHl: forall n0 : nat, length l <= n0 -> take n0 l = l
take n (a :: l) = a :: l
  destruct n.
A: Type
a: A
l: list A
H: length (a :: l) <= 0
IHl: forall n : nat, length l <= n -> take n l = l
take 0 (a :: l) = a :: l
A: Type
n: nat
a: A
l: list A
H: length (a :: l) <= n.+1
IHl: forall n0 : nat, length l <= n0 -> take n0 l = l
take n.+1 (a :: l) = a :: l
  1: destruct (not_lt_zero_r _ H).
A: Type
n: nat
a: A
l: list A
H: length (a :: l) <= n.+1
IHl: forall n0 : nat, length l <= n0 -> take n0 l = l
take n.+1 (a :: l) = a :: l
  cbn; f_ap.
A: Type
n: nat
a: A
l: list A
H: length (a :: l) <= n.+1
IHl: forall n0 : nat, length l <= n0 -> take n0 l = l
take n l = l
  by apply IHl, leq_pred'.
Defined.

(** The length of a [take n] is the minimum of [n] and the length of the original list. *)
Definition length_take@{i|} {A : Type@{i}} (n : nat) (l : list A)
  : length (take n l) = nat_min n (length l).
A: Type
n: nat
l: list A
length (take n l) = nat_min n (length l)
Proof.
A: Type
n: nat
l: list A
length (take n l) = nat_min n (length l)
  induction l as [|a l IHl] in n |- * using list_ind@{i i}.
A: Type
n: nat
length (take n nil) = nat_min n (length nil)
A: Type
n: nat
a: A
l: list A
IHl: forall n0 : nat, length (take n0 l) = nat_min n0 (length l)
length (take n (a :: l)) = nat_min n (length (a :: l))
  {
A: Type
n: nat
length (take n nil) = nat_min n (length nil) rewrite take_nil.
A: Type
n: nat
length nil = nat_min n (length nil)
    rewrite nat_min_r.
A: Type
n: nat
length nil = length nil
A: Type
n: nat
length nil <= n
    1: reflexivity.
A: Type
n: nat
length nil <= n
    cbn; exact _. }
A: Type
n: nat
a: A
l: list A
IHl: forall n0 : nat, length (take n0 l) = nat_min n0 (length l)
length (take n (a :: l)) = nat_min n (length (a :: l))
  destruct n.
A: Type
a: A
l: list A
IHl: forall n : nat, length (take n l) = nat_min n (length l)
length (take 0 (a :: l)) = nat_min 0 (length (a :: l))
A: Type
n: nat
a: A
l: list A
IHl: forall n0 : nat, length (take n0 l) = nat_min n0 (length l)
length (take n.+1 (a :: l)) = nat_min n.+1 (length (a :: l))
  1: reflexivity.
A: Type
n: nat
a: A
l: list A
IHl: forall n0 : nat, length (take n0 l) = nat_min n0 (length l)
length (take n.+1 (a :: l)) = nat_min n.+1 (length (a :: l))
  cbn; f_ap.
Defined.

(** The length of a [take] is less than or equal to the length of the list. *)
Definition length_take_leq {A : Type} {n : nat} (l : list A)
  : length (take n l) <= length l
  := transport (fun x => x <= length l) (length_take n l)^ (leq_nat_min_r _ _).

(** An element of a [take] is an element of the original list. *)
Definition take_inlist@{i|} {A : Type@{i}} (n : nat) (l : list A) (x : A)
  : InList x (take n l) -> InList x l.
A: Type
n: nat
l: list A
x: A
InList x (take n l) -> InList x l
Proof.
A: Type
n: nat
l: list A
x: A
InList x (take n l) -> InList x l
  intros H.
A: Type
n: nat
l: list A
x: A
H: InList x (take n l)
InList x l
  induction l as [|a l IHl] in n, H, x |- * using list_ind@{i i}.
A: Type
n: nat
x: A
H: InList x (take n nil)
InList x nil
A: Type
n: nat
a: A
l: list A
x: A
H: InList x (take n (a :: l))
IHl: forall (n0 : nat) (x0 : A), InList x0 (take n0 l) -> InList x0 l
InList x (a :: l)
  1: rewrite take_nil in H; contradiction.
A: Type
n: nat
a: A
l: list A
x: A
H: InList x (take n (a :: l))
IHl: forall (n0 : nat) (x0 : A), InList x0 (take n0 l) -> InList x0 l
InList x (a :: l)
  destruct n.
A: Type
a: A
l: list A
x: A
H: InList x (take 0 (a :: l))
IHl: forall (n : nat) (x0 : A), InList x0 (take n l) -> InList x0 l
InList x (a :: l)
A: Type
n: nat
a: A
l: list A
x: A
H: InList x (take n.+1 (a :: l))
IHl: forall (n0 : nat) (x0 : A), InList x0 (take n0 l) -> InList x0 l
InList x (a :: l)
  {
A: Type
a: A
l: list A
x: A
H: InList x (take 0 (a :: l))
IHl: forall (n : nat) (x0 : A), InList x0 (take n l) -> InList x0 l
InList x (a :: l) cbn in H.
A: Type
a: A
l: list A
x: A
H: Empty
IHl: forall (n : nat) (x0 : A), InList x0 (take n l) -> InList x0 l
InList x (a :: l) contradiction. }
A: Type
n: nat
a: A
l: list A
x: A
H: InList x (take n.+1 (a :: l))
IHl: forall (n0 : nat) (x0 : A), InList x0 (take n0 l) -> InList x0 l
InList x (a :: l)
  destruct H as [-> | H].
A: Type
n: nat
l: list A
x: A
IHl: forall (n0 : nat) (x0 : A), InList x0 (take n0 l) -> InList x0 l
InList x (x :: l)
A: Type
n: nat
a: A
l: list A
x: A
H: InList x (take n l)
IHl: forall (n0 : nat) (x0 : A), InList x0 (take n0 l) -> InList x0 l
InList x (a :: l)
  -
A: Type
n: nat
l: list A
x: A
IHl: forall (n0 : nat) (x0 : A), InList x0 (take n0 l) -> InList x0 l
InList x (x :: l) left; reflexivity.
  -
A: Type
n: nat
a: A
l: list A
x: A
H: InList x (take n l)
IHl: forall (n0 : nat) (x0 : A), InList x0 (take n0 l) -> InList x0 l
InList x (a :: l) right; exact (IHl _ _ H).
Defined.

(** Applying a [take] twice with [m] and [n] is the same as applying it once with [nat_min m n]. *)
Definition take_take_min {A : Type} {m n : nat} (l : list A)
  : take n (take m l) = take (nat_min n m) l.
A: Type
m, n: nat
l: list A
take n (take m l) = take (nat_min n m) l
Proof.
A: Type
m, n: nat
l: list A
take n (take m l) = take (nat_min n m) l
  induction n in m, l |- *.
A: Type
m: nat
l: list A
take 0 (take m l) = take (nat_min 0 m) l
A: Type
m, n: nat
l: list A
IHn: forall (m0 : nat) (l0 : list A), take n (take m0 l0) = take (nat_min n m0) l0
take n.+1 (take m l) = take (nat_min n.+1 m) l
  1: reflexivity.
A: Type
m, n: nat
l: list A
IHn: forall (m0 : nat) (l0 : list A), take n (take m0 l0) = take (nat_min n m0) l0
take n.+1 (take m l) = take (nat_min n.+1 m) l
  destruct m.
A: Type
n: nat
l: list A
IHn: forall (m : nat) (l0 : list A), take n (take m l0) = take (nat_min n m) l0
take n.+1 (take 0 l) = take (nat_min n.+1 0) l
A: Type
m, n: nat
l: list A
IHn: forall (m0 : nat) (l0 : list A), take n (take m0 l0) = take (nat_min n m0) l0
take n.+1 (take m.+1 l) = take (nat_min n.+1 m.+1) l
  1: reflexivity.
A: Type
m, n: nat
l: list A
IHn: forall (m0 : nat) (l0 : list A), take n (take m0 l0) = take (nat_min n m0) l0
take n.+1 (take m.+1 l) = take (nat_min n.+1 m.+1) l
  destruct l as [|a l'].
A: Type
m, n: nat
IHn: forall (m0 : nat) (l : list A), take n (take m0 l) = take (nat_min n m0) l
take n.+1 (take m.+1 nil) = take (nat_min n.+1 m.+1) nil
A: Type
m, n: nat
a: A
l': list A
IHn: forall (m0 : nat) (l : list A), take n (take m0 l) = take (nat_min n m0) l
take n.+1 (take m.+1 (a :: l')) = take (nat_min n.+1 m.+1) (a :: l')
  1: by rewrite !take_nil.
A: Type
m, n: nat
a: A
l': list A
IHn: forall (m0 : nat) (l : list A), take n (take m0 l) = take (nat_min n m0) l
take n.+1 (take m.+1 (a :: l')) = take (nat_min n.+1 m.+1) (a :: l')
  cbn.
A: Type
m, n: nat
a: A
l': list A
IHn: forall (m0 : nat) (l : list A), take n (take m0 l) = take (nat_min n m0) l
a :: take n (take m l') = a :: take (nat_min n m) l' apply ap, IHn.
Defined.

(** [take] is commutative in [n]. *)
Definition take_comm {A : Type} {m n : nat} (l : list A)
  : take n (take m l) = take m (take n l).
A: Type
m, n: nat
l: list A
take n (take m l) = take m (take n l)
Proof.
A: Type
m, n: nat
l: list A
take n (take m l) = take m (take n l)
  by rewrite !take_take_min, nat_min_comm.
Defined.

(** A [take n] does not change under concatenation if [n] is less than or equal to the length of the first list. *)
Definition take_app {A : Type} {n : nat} (l1 l2 : list A) (hn : n <= length l1)
  : take n l1 = take n (l1 ++ l2).
A: Type
n: nat
l1, l2: list A
hn: n <= length l1
take n l1 = take n (l1 ++ l2)
Proof.
A: Type
n: nat
l1, l2: list A
hn: n <= length l1
take n l1 = take n (l1 ++ l2)
  induction n in l1, l2, hn |- *.
A: Type
l1, l2: list A
hn: 0 <= length l1
take 0 l1 = take 0 (l1 ++ l2)
A: Type
n: nat
l1, l2: list A
hn: n.+1 <= length l1
IHn: forall l0 l3 : list A, n <= length l0 -> take n l0 = take n (l0 ++ l3)
take n.+1 l1 = take n.+1 (l1 ++ l2)
  -
A: Type
l1, l2: list A
hn: 0 <= length l1
take 0 l1 = take 0 (l1 ++ l2) reflexivity.
  -
A: Type
n: nat
l1, l2: list A
hn: n.+1 <= length l1
IHn: forall l0 l3 : list A, n <= length l0 -> take n l0 = take n (l0 ++ l3)
take n.+1 l1 = take n.+1 (l1 ++ l2) destruct l1 as [|a l1].
A: Type
n: nat
l2: list A
hn: n.+1 <= length nil
IHn: forall l1 l0 : list A, n <= length l1 -> take n l1 = take n (l1 ++ l0)
take n.+1 nil = take n.+1 (nil ++ l2)
A: Type
n: nat
a: A
l1, l2: list A
hn: n.+1 <= length (a :: l1)
IHn: forall l0 l3 : list A, n <= length l0 -> take n l0 = take n (l0 ++ l3)
take n.+1 (a :: l1) = take n.+1 ((a :: l1) ++ l2)
    +
A: Type
n: nat
l2: list A
hn: n.+1 <= length nil
IHn: forall l1 l0 : list A, n <= length l1 -> take n l1 = take n (l1 ++ l0)
take n.+1 nil = take n.+1 (nil ++ l2) contradiction (not_lt_zero_r _ hn).
    +
A: Type
n: nat
a: A
l1, l2: list A
hn: n.+1 <= length (a :: l1)
IHn: forall l0 l3 : list A, n <= length l0 -> take n l0 = take n (l0 ++ l3)
take n.+1 (a :: l1) = take n.+1 ((a :: l1) ++ l2) cbn.
A: Type
n: nat
a: A
l1, l2: list A
hn: n.+1 <= length (a :: l1)
IHn: forall l0 l3 : list A, n <= length l0 -> take n l0 = take n (l0 ++ l3)
a :: take n l1 = a :: take n (l1 ++ l2)
      apply ap, IHn, leq_pred', hn.
Defined.

(** *** Remove *)

(** [remove n l] removes the [n]-th element of [l]. *)
Definition remove {A : Type} (n : nat) (l : list A) : list A
  := take n l ++ drop n.+1 l.

(** Removing the first element of a list is the tail of the list. *)
Definition remove_0 {A : Type} (l : list A) : remove 0 l = tail l := idpath.

(** Removing the [n]-th element of a list with [length l <= n] is the original list. *)
Definition remove_length_leq {A : Type} (n : nat) (l : list A)
  (H : length l <= n)
  : remove n l = l.
A: Type
n: nat
l: list A
H: length l <= n
remove n l = l
Proof.
A: Type
n: nat
l: list A
H: length l <= n
remove n l = l
  unfold remove.
A: Type
n: nat
l: list A
H: length l <= n
take n l ++ drop n.+1 l = l
  rewrite take_length_leq.
A: Type
n: nat
l: list A
H: length l <= n
l ++ drop n.+1 l = l
A: Type
n: nat
l: list A
H: length l <= n
length l <= n
  2: exact _.
A: Type
n: nat
l: list A
H: length l <= n
l ++ drop n.+1 l = l
  rewrite drop_length_leq.
A: Type
n: nat
l: list A
H: length l <= n
l ++ nil = l
A: Type
n: nat
l: list A
H: length l <= n
length l <= n.+1
  2: exact _.
A: Type
n: nat
l: list A
H: length l <= n
l ++ nil = l
  apply app_nil.
Defined.

(** The length of a [remove n] is the length of the original list minus one. *)
Definition length_remove@{i|} {A : Type@{i}} (n : nat) (l : list A)
  (H : n < length l)
  : length (remove n l) = nat_pred (length l).
A: Type
n: nat
l: list A
H: n < length l
length (remove n l) = nat_pred (length l)
Proof.
A: Type
n: nat
l: list A
H: n < length l
length (remove n l) = nat_pred (length l)
  unfold remove.
A: Type
n: nat
l: list A
H: n < length l
length (take n l ++ drop n.+1 l) = nat_pred (length l)
  rewrite length_app@{i}.
A: Type
n: nat
l: list A
H: n < length l
length (take n l) + length (drop n.+1 l) = nat_pred (length l)
  rewrite length_take.
A: Type
n: nat
l: list A
H: n < length l
nat_min n (length l) + length (drop n.+1 l) = nat_pred (length l)
  rewrite length_drop.
A: Type
n: nat
l: list A
H: n < length l
nat_min n (length l) + (length l - n.+1) = nat_pred (length l)
  rewrite nat_min_l.
A: Type
n: nat
l: list A
H: n < length l
n + (length l - n.+1) = nat_pred (length l)
A: Type
n: nat
l: list A
H: n < length l
n <= length l
  2: exact (leq_trans _ H).
A: Type
n: nat
l: list A
H: n < length l
n + (length l - n.+1) = nat_pred (length l)
  rewrite <- nat_sub_l_add_r.
A: Type
n: nat
l: list A
H: n < length l
n + length l - n.+1 = nat_pred (length l)
A: Type
n: nat
l: list A
H: n < length l
n.+1 <= length l
  2: exact _.
A: Type
n: nat
l: list A
H: n < length l
n + length l - n.+1 = nat_pred (length l)
  lhs napply nat_sub_succ_r.
A: Type
n: nat
l: list A
H: n < length l
nat_pred (n + length l - n) = nat_pred (length l)
  apply ap.
A: Type
n: nat
l: list A
H: n < length l
n + length l - n = length l
  apply nat_add_sub_cancel_l.
Defined.

(** An element of a [remove] is an element of the original list. *)
Definition remove_inlist {A : Type} (n : nat) (l : list A) (x : A)
  : InList x (remove n l) -> InList x l.
A: Type
n: nat
l: list A
x: A
InList x (remove n l) -> InList x l
Proof.
A: Type
n: nat
l: list A
x: A
InList x (remove n l) -> InList x l
  unfold remove.
A: Type
n: nat
l: list A
x: A
InList x (take n l ++ drop n.+1 l) -> InList x l
  intros p.
A: Type
n: nat
l: list A
x: A
p: InList x (take n l ++ drop n.+1 l)
InList x l
  apply equiv_inlist_app in p.
A: Type
n: nat
l: list A
x: A
p: InList x (take n l) + InList x (drop n.+1 l)
InList x l
  revert p.
A: Type
n: nat
l: list A
x: A
InList x (take n l) + InList x (drop n.+1 l) -> InList x l
  snapply sum_rec.
A: Type
n: nat
l: list A
x: A
InList x (take n l) -> InList x l
A: Type
n: nat
l: list A
x: A
InList x (drop n.+1 l) -> InList x l
  -
A: Type
n: nat
l: list A
x: A
InList x (take n l) -> InList x l apply take_inlist.
  -
A: Type
n: nat
l: list A
x: A
InList x (drop n.+1 l) -> InList x l apply drop_inlist.
Defined.

(** *** Filter *)

(** Produce the list of elements of a list that satisfy a decidable predicate. *)
Fixpoint list_filter@{u v|} {A : Type@{u}} (l : list A) (P : A -> Type@{v})
  (dec : forall x, Decidable (P x))
  : list A
  := match l with
    | nil => nil
    | x :: l =>
      if dec x then x :: list_filter l P dec
        else list_filter l P dec
    end.

Definition inlist_filter@{u v k | u <= k, v <= k} {A : Type@{u}} (l : list A)
  (P : A -> Type@{v}) (dec : forall x, Decidable (P x)) (x : A)
  : iff@{u k k} (InList x (list_filter l P dec)) (InList x l /\ P x).
A: Type
l: list A
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
InList x (list_filter l P dec) <-> InList x l * P x
Proof.
A: Type
l: list A
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
InList x (list_filter l P dec) <-> InList x l * P x
  simple_list_induction l a l IHl.
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
InList x (list_filter nil P dec) <-> InList x nil * P x
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
l: list A
IHl: InList x (list_filter l P dec) <-> InList x l * P x
a: A
InList x (list_filter (a :: l) P dec) <-> InList x (a :: l) * P x
  -
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
InList x (list_filter nil P dec) <-> InList x nil * P x simpl.
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
Empty <-> Empty * P x
    apply iff_inverse.
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
Empty * P x <-> Empty
    apply iff_equiv.
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
Empty * P x <~> Empty
    snapply prod_empty_l@{v}.
  -
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
l: list A
IHl: InList x (list_filter l P dec) <-> InList x l * P x
a: A
InList x (list_filter (a :: l) P dec) <-> InList x (a :: l) * P x simpl.
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
l: list A
IHl: InList x (list_filter l P dec) <-> InList x l * P x
a: A
InList x (if dec a then a :: list_filter l P dec else list_filter l P dec) <->
((a = x) + InList x l) * P x
    napply iff_compose.
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
l: list A
IHl: InList x (list_filter l P dec) <-> InList x l * P x
a: A
InList x (if dec a then a :: list_filter l P dec else list_filter l P dec) <->
?Goal
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
l: list A
IHl: InList x (list_filter l P dec) <-> InList x l * P x
a: A
?Goal <-> ((a = x) + InList x l) * P x
    2: {
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
l: list A
IHl: InList x (list_filter l P dec) <-> InList x l * P x
a: A
?Goal <-> ((a = x) + InList x l) * P x apply iff_inverse.
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
l: list A
IHl: InList x (list_filter l P dec) <-> InList x l * P x
a: A
((a = x) + InList x l) * P x <-> ?Goal
         apply iff_equiv.
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
l: list A
IHl: InList x (list_filter l P dec) <-> InList x l * P x
a: A
((a = x) + InList x l) * P x <~> ?Goal
         exact (sum_distrib_r@{k k k _ _ _ k k} _ _ _). }
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
l: list A
IHl: InList x (list_filter l P dec) <-> InList x l * P x
a: A
InList x (if dec a then a :: list_filter l P dec else list_filter l P dec) <->
(a = x) * P x + InList x l * P x
    destruct (dec a) as [p|p].
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
l: list A
IHl: InList x (list_filter l P dec) <-> InList x l * P x
a: A
p: P a
InList x (a :: list_filter l P dec) <-> (a = x) * P x + InList x l * P x
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
l: list A
IHl: InList x (list_filter l P dec) <-> InList x l * P x
a: A
p: ~ P a
InList x (list_filter l P dec) <-> (a = x) * P x + InList x l * P x
    +
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
l: list A
IHl: InList x (list_filter l P dec) <-> InList x l * P x
a: A
p: P a
InList x (a :: list_filter l P dec) <-> (a = x) * P x + InList x l * P x simpl.
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
l: list A
IHl: InList x (list_filter l P dec) <-> InList x l * P x
a: A
p: P a
(a = x) + InList x (list_filter l P dec) <-> (a = x) * P x + InList x l * P x
      snapply iff_compose.
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
l: list A
IHl: InList x (list_filter l P dec) <-> InList x l * P x
a: A
p: P a
Type
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
l: list A
IHl: InList x (list_filter l P dec) <-> InList x l * P x
a: A
p: P a
(a = x) + InList x (list_filter l P dec) <-> ?B
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
l: list A
IHl: InList x (list_filter l P dec) <-> InList x l * P x
a: A
p: P a
?B <-> (a = x) * P x + InList x l * P x
      1: exact (sum (a = x) (prod (InList@{u} x l) (P x))).
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
l: list A
IHl: InList x (list_filter l P dec) <-> InList x l * P x
a: A
p: P a
(a = x) + InList x (list_filter l P dec) <-> (a = x) + InList x l * P x
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
l: list A
IHl: InList x (list_filter l P dec) <-> InList x l * P x
a: A
p: P a
(a = x) + InList x l * P x <-> (a = x) * P x + InList x l * P x
      1: split; apply functor_sum; only 1,3: exact idmap; apply IHl.
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
l: list A
IHl: InList x (list_filter l P dec) <-> InList x l * P x
a: A
p: P a
(a = x) + InList x l * P x <-> (a = x) * P x + InList x l * P x
      split; apply functor_sum@{k k k k}; only 2,4: exact idmap.
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
l: list A
IHl: InList x (list_filter l P dec) <-> InList x l * P x
a: A
p: P a
a = x -> (a = x) * P x
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
l: list A
IHl: InList x (list_filter l P dec) <-> InList x l * P x
a: A
p: P a
(a = x) * P x -> a = x
      *
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
l: list A
IHl: InList x (list_filter l P dec) <-> InList x l * P x
a: A
p: P a
a = x -> (a = x) * P x intros [].
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
l: list A
IHl: InList x (list_filter l P dec) <-> InList x l * P x
a: A
p: P a
(a = a) * P a
        exact (idpath, p).
      *
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
l: list A
IHl: InList x (list_filter l P dec) <-> InList x l * P x
a: A
p: P a
(a = x) * P x -> a = x exact fst.
    +
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
l: list A
IHl: InList x (list_filter l P dec) <-> InList x l * P x
a: A
p: ~ P a
InList x (list_filter l P dec) <-> (a = x) * P x + InList x l * P x napply iff_compose.
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
l: list A
IHl: InList x (list_filter l P dec) <-> InList x l * P x
a: A
p: ~ P a
InList x (list_filter l P dec) <-> ?Goal
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
l: list A
IHl: InList x (list_filter l P dec) <-> InList x l * P x
a: A
p: ~ P a
?Goal <-> (a = x) * P x + InList x l * P x
      1: exact IHl.
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
l: list A
IHl: InList x (list_filter l P dec) <-> InList x l * P x
a: A
p: ~ P a
InList x l * P x <-> (a = x) * P x + InList x l * P x
      apply iff_inverse.
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
l: list A
IHl: InList x (list_filter l P dec) <-> InList x l * P x
a: A
p: ~ P a
(a = x) * P x + InList x l * P x <-> InList x l * P x
      apply iff_equiv.
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
l: list A
IHl: InList x (list_filter l P dec) <-> InList x l * P x
a: A
p: ~ P a
(a = x) * P x + InList x l * P x <~> InList x l * P x
      nrefine (equiv_compose'@{k k k} (sum_empty_l@{k} _) _).
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
l: list A
IHl: InList x (list_filter l P dec) <-> InList x l * P x
a: A
p: ~ P a
(a = x) * P x + InList x l * P x <~> Empty + InList x l * P x
      snapply equiv_functor_sum'@{k k k k k k}.
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
l: list A
IHl: InList x (list_filter l P dec) <-> InList x l * P x
a: A
p: ~ P a
(a = x) * P x <~> Empty
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
l: list A
IHl: InList x (list_filter l P dec) <-> InList x l * P x
a: A
p: ~ P a
InList x l * P x <~> InList x l * P x
      2: exact equiv_idmap.
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
l: list A
IHl: InList x (list_filter l P dec) <-> InList x l * P x
a: A
p: ~ P a
(a = x) * P x <~> Empty
      apply equiv_to_empty.
A: Type
P: A -> Type
dec: forall x0 : A, Decidable (P x0)
x: A
l: list A
IHl: InList x (list_filter l P dec) <-> InList x l * P x
a: A
p: ~ P a
(a = x) * P x -> Empty
      by intros [[] r].
Defined.

Definition list_filter_app {A : Type} (l l' : list A) (P : A -> Type)
  (dec : forall x, Decidable (P x))
  : list_filter (l ++ l') P dec = list_filter l P dec ++ list_filter l' P dec.
A: Type
l, l': list A
P: A -> Type
dec: forall x : A, Decidable (P x)
list_filter (l ++ l') P dec = list_filter l P dec ++ list_filter l' P dec
Proof.
A: Type
l, l': list A
P: A -> Type
dec: forall x : A, Decidable (P x)
list_filter (l ++ l') P dec = list_filter l P dec ++ list_filter l' P dec
  simple_list_induction l a l IHl.
A: Type
l': list A
P: A -> Type
dec: forall x : A, Decidable (P x)
list_filter (nil ++ l') P dec = list_filter nil P dec ++ list_filter l' P dec
A: Type
l': list A
P: A -> Type
dec: forall x : A, Decidable (P x)
l: list A
IHl: list_filter (l ++ l') P dec = list_filter l P dec ++ list_filter l' P dec
a: A
list_filter ((a :: l) ++ l') P dec =
list_filter (a :: l) P dec ++ list_filter l' P dec
  -
A: Type
l': list A
P: A -> Type
dec: forall x : A, Decidable (P x)
list_filter (nil ++ l') P dec = list_filter nil P dec ++ list_filter l' P dec reflexivity.
  -
A: Type
l': list A
P: A -> Type
dec: forall x : A, Decidable (P x)
l: list A
IHl: list_filter (l ++ l') P dec = list_filter l P dec ++ list_filter l' P dec
a: A
list_filter ((a :: l) ++ l') P dec =
list_filter (a :: l) P dec ++ list_filter l' P dec simpl; destruct (dec a); trivial.
A: Type
l': list A
P: A -> Type
dec: forall x : A, Decidable (P x)
l: list A
IHl: list_filter (l ++ l') P dec = list_filter l P dec ++ list_filter l' P dec
a: A
p: P a
a :: list_filter (l ++ l') P dec =
(a :: list_filter l P dec) ++ list_filter l' P dec
    simpl; f_ap.
Defined.

(** ** Sequences *)

(** The length of a reverse sequence of [n] numbers is [n]. *)
Definition length_seq_rev@{} (n : nat)
  : length (seq_rev n) = n.
n: nat
length (seq_rev n) = n
Proof.
n: nat
length (seq_rev n) = n
  induction n as [|n IHn].
length (seq_rev 0) = 0
n: nat
IHn: length (seq_rev n) = n
length (seq_rev n.+1) = n.+1
  1: reflexivity.
n: nat
IHn: length (seq_rev n) = n
length (seq_rev n.+1) = n.+1
  cbn; f_ap.
Defined.

(** The length of a sequence of [n] numbers is [n]. *)
Definition length_seq@{} (n : nat)
  : length (seq n) = n.
n: nat
length (seq n) = n
Proof.
n: nat
length (seq n) = n
  lhs napply length_reverse.
n: nat
length (seq_rev n) = n
  apply length_seq_rev.
Defined.

(** The reversed sequence of [n.+1] numbers is the [n] followed by the rest of the reversed sequence. *)
Definition seq_rev_cons@{} (n : nat)
  : seq_rev n.+1 = n :: seq_rev n
  := idpath.

(** The sequence of [n.+1] numbers is the sequence of [n] numbers concatenated with [[n]]. *)
Definition seq_succ@{} (n : nat)
  : seq n.+1 = seq n ++ [n].
n: nat
seq n.+1 = seq n ++ [n]
Proof.
n: nat
seq n.+1 = seq n ++ [n]
  apply reverse_cons.
Defined.

(** Alternate definition of [seq_rev] that keeps the proofs of the entries being [< n]. *)
Definition seq_rev'@{} (n : nat) : list {k : nat & k < n}.
n: nat
list {k : nat & k < n}
Proof.
n: nat
list {k : nat & k < n}
  transparent assert (f : (forall n, {k : nat & k < n}
    -> {k : nat & k < n.+1})).
n: nat
forall n0 : nat, {k : nat & k < n0} -> {k : nat & k < n0.+1}
n: nat
f:= ?Goal: forall n0 : nat, {k : nat & k < n0} -> {k : nat & k < n0.+1}
list {k : nat & k < n}
  {
n: nat
forall n0 : nat, {k : nat & k < n0} -> {k : nat & k < n0.+1} intros m.
n, m: nat
{k : nat & k < m} -> {k : nat & k < m.+1}
    snapply (functor_sigma idmap).
n, m: nat
forall a : nat,
(fun k : nat => k < m) a -> (fun k : nat => k < m.+1) (idmap a)
    intros k H.
n, m, k: nat
H: (fun k0 : nat => k0 < m) k
(fun k0 : nat => k0 < m.+1) (idmap k)
    exact (leq_succ_r H). }
n: nat
f:= fun m : nat =>
functor_sigma idmap
  (fun (k : nat) (H : (fun k0 : nat => k0 < m) k) => leq_succ_r H): forall n0 : nat, {k : nat & k < n0} -> {k : nat & k < n0.+1}
list {k : nat & k < n}
  induction n as [|n IHn].
f:= fun m : nat =>
functor_sigma idmap
  (fun (k : nat) (H : (fun k0 : nat => k0 < m) k) => leq_succ_r H): forall n : nat, {k : nat & k < n} -> {k : nat & k < n.+1}
list {k : nat & k < 0}
n: nat
f:= fun m : nat =>
functor_sigma idmap
  (fun (k : nat) (H : (fun k0 : nat => k0 < m) k) => leq_succ_r H): forall n0 : nat, {k : nat & k < n0} -> {k : nat & k < n0.+1}
IHn: list {k : nat & k < n}
list {k : nat & k < n.+1}
  1: exact nil.
n: nat
f:= fun m : nat =>
functor_sigma idmap
  (fun (k : nat) (H : (fun k0 : nat => k0 < m) k) => leq_succ_r H): forall n0 : nat, {k : nat & k < n0} -> {k : nat & k < n0.+1}
IHn: list {k : nat & k < n}
list {k : nat & k < n.+1}
  nrefine ((n; _) :: list_map (f n) IHn).
n: nat
f:= fun m : nat =>
functor_sigma idmap
  (fun (k : nat) (H : (fun k0 : nat => k0 < m) k) => leq_succ_r H): forall n0 : nat, {k : nat & k < n0} -> {k : nat & k < n0.+1}
IHn: list {k : nat & k < n}
n < n.+1
  exact _.
Defined.

(** Alternate definition of [seq] that keeps the proofs of the entries being [< n]. *)
Definition seq'@{} (n : nat) : list {k : nat & k < n}
  := reverse (seq_rev' n).

(** The length of [seq_rev' n] is [n]. *)
Definition length_seq_rev'@{} (n : nat)
  : length (seq_rev' n) = n.
n: nat
length (seq_rev' n) = n
Proof.
n: nat
length (seq_rev' n) = n
  induction n as [|n IHn].
length (seq_rev' 0) = 0
n: nat
IHn: length (seq_rev' n) = n
length (seq_rev' n.+1) = n.+1
  1: reflexivity.
n: nat
IHn: length (seq_rev' n) = n
length (seq_rev' n.+1) = n.+1
  cbn; f_ap.
n: nat
IHn: length (seq_rev' n) = n
length
  (list_map (functor_sigma idmap (fun (k : nat) (H : k < n) => leq_succ_r H))
     (nat_rec (fun n0 : nat => list {k : nat & k < n0}) nil
        (fun (n0 : nat) (IHn0 : list {k : nat & k < n0}) =>
         (n0; leq_refl n0.+1)
         :: list_map
              (functor_sigma idmap
                 (fun (k : nat) (H : k < n0) => leq_succ_r H))
              IHn0)
        n)) =
n
  lhs napply length_list_map.
n: nat
IHn: length (seq_rev' n) = n
length
  (nat_rec (fun n0 : nat => list {k : nat & k < n0}) nil
     (fun (n0 : nat) (IHn0 : list {k : nat & k < n0}) =>
      (n0; leq_refl n0.+1)
      :: list_map
           (functor_sigma idmap (fun (k : nat) (H : k < n0) => leq_succ_r H))
           IHn0)
     n) =
n
  exact IHn.
Defined.

(** The length of [seq' n] is [n]. *)
Definition length_seq'@{} (n : nat)
  : length (seq' n) = n.
n: nat
length (seq' n) = n
Proof.
n: nat
length (seq' n) = n
  lhs napply length_reverse.
n: nat
length (seq_rev' n) = n
  apply length_seq_rev'.
Defined.

(** The [list_map] of first projections on [seq_rev' n] is [seq_rev n]. *)
Definition seq_rev_seq_rev'@{} (n : nat)
  : list_map pr1 (seq_rev' n) = seq_rev n.
n: nat
list_map pr1 (seq_rev' n) = seq_rev n
Proof.
n: nat
list_map pr1 (seq_rev' n) = seq_rev n
  induction n as [|n IHn].
list_map pr1 (seq_rev' 0) = seq_rev 0
n: nat
IHn: list_map pr1 (seq_rev' n) = seq_rev n
list_map pr1 (seq_rev' n.+1) = seq_rev n.+1
  1: reflexivity.
n: nat
IHn: list_map pr1 (seq_rev' n) = seq_rev n
list_map pr1 (seq_rev' n.+1) = seq_rev n.+1
  simpl; f_ap.
n: nat
IHn: list_map pr1 (seq_rev' n) = seq_rev n
list_map pr1
  (list_map (functor_sigma idmap (fun (k : nat) (H : k < n) => leq_succ_r H))
     (seq_rev' n)) =
seq_rev n
  lhs_V napply list_map_compose.
n: nat
IHn: list_map pr1 (seq_rev' n) = seq_rev n
list_map
  (fun x : {k : nat & k < n} =>
   (functor_sigma idmap (fun (k : nat) (H : k < n) => leq_succ_r H) x).1)
  (seq_rev' n) =
seq_rev n
  exact IHn.
Defined.

(** The [list_map] of first projections on [seq' n] is [seq n]. *)
Definition seq_seq'@{} (n : nat)
  : list_map pr1 (seq' n) = seq n.
n: nat
list_map pr1 (seq' n) = seq n
Proof.
n: nat
list_map pr1 (seq' n) = seq n
  lhs napply list_map_reverse_acc.
n: nat
reverse_acc (list_map pr1 nil) (list_map pr1 (seq_rev' n)) = seq n
  apply (ap reverse).
n: nat
list_map pr1 (seq_rev' n) = seq_rev n
  apply seq_rev_seq_rev'.
Defined.

(** The [nth] element of a [seq_rev] is [n - i.+1]. *)
Definition nth_seq_rev@{} {n i} (H : i < n)
  : nth (seq_rev n) i = Some (n - i.+1).
n, i: nat
H: i < n
nth (seq_rev n) i = Some (n - i.+1)
Proof.
n, i: nat
H: i < n
nth (seq_rev n) i = Some (n - i.+1)
  induction i as [|i IHi] in n, H |- *.
n: nat
H: 0 < n
nth (seq_rev n) 0 = Some (n - 1)
n, i: nat
H: i.+1 < n
IHi: forall n0 : nat, i < n0 -> nth (seq_rev n0) i = Some (n0 - i.+1)
nth (seq_rev n) i.+1 = Some (n - i.+2)
  -
n: nat
H: 0 < n
nth (seq_rev n) 0 = Some (n - 1) induction n.
H: 0 < 0
nth (seq_rev 0) 0 = Some (0 - 1)
n: nat
H: 0 < n.+1
IHn: 0 < n -> nth (seq_rev n) 0 = Some (n - 1)
nth (seq_rev n.+1) 0 = Some (n.+1 - 1)
    1: destruct (not_lt_zero_r _ H).
n: nat
H: 0 < n.+1
IHn: 0 < n -> nth (seq_rev n) 0 = Some (n - 1)
nth (seq_rev n.+1) 0 = Some (n.+1 - 1)
    cbn; by rewrite nat_sub_zero_r.
  -
n, i: nat
H: i.+1 < n
IHi: forall n0 : nat, i < n0 -> nth (seq_rev n0) i = Some (n0 - i.+1)
nth (seq_rev n) i.+1 = Some (n - i.+2) induction n as [|n IHn].
i: nat
H: i.+1 < 0
IHi: forall n : nat, i < n -> nth (seq_rev n) i = Some (n - i.+1)
nth (seq_rev 0) i.+1 = Some (0 - i.+2)
n, i: nat
H: i.+1 < n.+1
IHi: forall n0 : nat, i < n0 -> nth (seq_rev n0) i = Some (n0 - i.+1)
IHn: i.+1 < n -> nth (seq_rev n) i.+1 = Some (n - i.+2)
nth (seq_rev n.+1) i.+1 = Some (n.+1 - i.+2)
    1: destruct (not_lt_zero_r _ H).
n, i: nat
H: i.+1 < n.+1
IHi: forall n0 : nat, i < n0 -> nth (seq_rev n0) i = Some (n0 - i.+1)
IHn: i.+1 < n -> nth (seq_rev n) i.+1 = Some (n - i.+2)
nth (seq_rev n.+1) i.+1 = Some (n.+1 - i.+2)
    by apply IHi, leq_pred'.
Defined.

(** The [nth] element of a [seq] is [i]. *)
Definition nth_seq@{} {n i} (H : i < n)
  : nth (seq n) i = Some i.
n, i: nat
H: i < n
nth (seq n) i = Some i
Proof.
n, i: nat
H: i < n
nth (seq n) i = Some i
  induction n.
i: nat
H: i < 0
nth (seq 0) i = Some i
n, i: nat
H: i < n.+1
IHn: i < n -> nth (seq n) i = Some i
nth (seq n.+1) i = Some i
  1: destruct (not_lt_zero_r _ H).
n, i: nat
H: i < n.+1
IHn: i < n -> nth (seq n) i = Some i
nth (seq n.+1) i = Some i
  rewrite seq_succ.
n, i: nat
H: i < n.+1
IHn: i < n -> nth (seq n) i = Some i
nth (seq n ++ [n]) i = Some i
  destruct (dec (i < n)) as [H'|H'].
n, i: nat
H: i < n.+1
IHn: i < n -> nth (seq n) i = Some i
H': i < n
nth (seq n ++ [n]) i = Some i
n, i: nat
H: i < n.+1
IHn: i < n -> nth (seq n) i = Some i
H': ~ (i < n)
nth (seq n ++ [n]) i = Some i
  -
n, i: nat
H: i < n.+1
IHn: i < n -> nth (seq n) i = Some i
H': i < n
nth (seq n ++ [n]) i = Some i lhs napply nth_app.
n, i: nat
H: i < n.+1
IHn: i < n -> nth (seq n) i = Some i
H': i < n
i < length (seq n)
n, i: nat
H: i < n.+1
IHn: i < n -> nth (seq n) i = Some i
H': i < n
nth (seq n) i = Some i
    1: by rewrite length_seq.
n, i: nat
H: i < n.+1
IHn: i < n -> nth (seq n) i = Some i
H': i < n
nth (seq n) i = Some i
    by apply IHn.
  -
n, i: nat
H: i < n.+1
IHn: i < n -> nth (seq n) i = Some i
H': ~ (i < n)
nth (seq n ++ [n]) i = Some i apply geq_iff_not_lt in H'.
n, i: nat
H: i < n.+1
IHn: i < n -> nth (seq n) i = Some i
H': i >= n
nth (seq n ++ [n]) i = Some i
    apply leq_pred' in H.
n, i: nat
H: i <= n
IHn: i < n -> nth (seq n) i = Some i
H': i >= n
nth (seq n ++ [n]) i = Some i
    destruct (leq_antisym H H').
i: nat
H: i <= i
IHn: i < i -> nth (seq i) i = Some i
H': i >= i
nth (seq i ++ [i]) i = Some i
    lhs napply nth_last.
i: nat
H: i <= i
IHn: i < i -> nth (seq i) i = Some i
H': i >= i
nat_pred (length (seq i ++ [i])) = i
i: nat
H: i <= i
IHn: i < i -> nth (seq i) i = Some i
H': i >= i
last (seq i ++ [i]) = Some i
    {
i: nat
H: i <= i
IHn: i < i -> nth (seq i) i = Some i
H': i >= i
nat_pred (length (seq i ++ [i])) = i rewrite length_app.
i: nat
H: i <= i
IHn: i < i -> nth (seq i) i = Some i
H': i >= i
nat_pred (length (seq i) + length [i]) = i
      rewrite nat_add_comm.
i: nat
H: i <= i
IHn: i < i -> nth (seq i) i = Some i
H': i >= i
nat_pred (length [i] + length (seq i)) = i
      apply length_seq. }
i: nat
H: i <= i
IHn: i < i -> nth (seq i) i = Some i
H': i >= i
last (seq i ++ [i]) = Some i
    napply last_app.
Defined.

(** The [nth'] element of a [seq'] is [i]. *)
Definition nth'_seq'@{} (n i : nat) (H : i < length (seq' n))
  : (nth' (seq' n) i H).1 = i.
n, i: nat
H: i < length (seq' n)
(nth' (seq' n) i H).1 = i
Proof.
n, i: nat
H: i < length (seq' n)
(nth' (seq' n) i H).1 = i
  unshelve lhs_V napply nth'_list_map.
n, i: nat
H: i < length (seq' n)
i < length (list_map pr1 (seq' n))
n, i: nat
H: i < length (seq' n)
nth' (list_map pr1 (seq' n)) i ?Goal = i
  1: by rewrite length_list_map.
n, i: nat
H: i < length (seq' n)
nth' (list_map pr1 (seq' n)) i
  (internal_paths_rew_r (fun n0 : nat => i < n0) H
     (length_list_map pr1 (seq' n))) =
i
  unshelve lhs napply (ap011D (fun x y => nth' x _ y) _ idpath).
n, i: nat
H: i < length (seq' n)
list nat
n, i: nat
H: i < length (seq' n)
list_map pr1 (seq' n) = ?Goal
n, i: nat
H: i < length (seq' n)
nth' ?Goal i
  (transport (fun x : list nat => i < length x) ?Goal0
     (internal_paths_rew_r (fun n0 : nat => i < n0) H
        (length_list_map pr1 (seq' n)))) =
i
  2: apply seq_seq'.
n, i: nat
H: i < length (seq' n)
nth' (seq n) i
  (transport (fun x : list nat => i < length x) (seq_seq' n)
     (internal_paths_rew_r (fun n0 : nat => i < n0) H
        (length_list_map pr1 (seq' n)))) =
i
  apply isinj_some.
n, i: nat
H: i < length (seq' n)
Some
  (nth' (seq n) i
     (transport (fun x : list nat => i < length x) 
        (seq_seq' n)
        (internal_paths_rew_r (fun n0 : nat => i < n0) H
           (length_list_map pr1 (seq' n))))) =
Some i
  lhs_V napply nth_nth'.
n, i: nat
H: i < length (seq' n)
nth (seq n) i = Some i
  apply nth_seq.
n, i: nat
H: i < length (seq' n)
i < n
  by rewrite length_seq' in H.
Defined.

Definition inlist_seq@{} (n : nat) x
  : InList x (seq n) <~> (x < n).
n, x: nat
InList x (seq n) <~> x < n
Proof.
n, x: nat
InList x (seq n) <~> x < n
  simple_induction n n IHn.
x: nat
InList x (seq 0) <~> x < 0
x, n: nat
IHn: InList x (seq n) <~> x < n
InList x (seq n.+1) <~> x < n.+1
  {
x: nat
InList x (seq 0) <~> x < 0 symmetry; apply equiv_to_empty.
x: nat
x < 0 -> Empty
    apply not_lt_zero_r. }
x, n: nat
IHn: InList x (seq n) <~> x < n
InList x (seq n.+1) <~> x < n.+1
  refine (_ oE equiv_transport _ (seq_succ _)).
x, n: nat
IHn: InList x (seq n) <~> x < n
InList x (seq n ++ [n]) <~> x < n.+1
  nrefine (_ oE (equiv_inlist_app _ _ _)^-1).
x, n: nat
IHn: InList x (seq n) <~> x < n
InList x (seq n) + InList x [n] <~> x < n.+1
  nrefine (_ oE equiv_functor_sum' (B':=x = n) IHn _).
x, n: nat
IHn: InList x (seq n) <~> x < n
(x < n) + (x = n) <~> x < n.+1
x, n: nat
IHn: InList x (seq n) <~> x < n
InList x [n] <~> x = n
  2: {
x, n: nat
IHn: InList x (seq n) <~> x < n
InList x [n] <~> x = n simpl.
x, n: nat
IHn: InList x (seq n) <~> x < n
(n = x) + Empty <~> x = n
       exact (equiv_path_inverse _ _ oE sum_empty_r@{Set} _). }
x, n: nat
IHn: InList x (seq n) <~> x < n
(x < n) + (x = n) <~> x < n.+1
  nrefine (_ oE equiv_leq_lt_or_eq^-1).
x, n: nat
IHn: InList x (seq n) <~> x < n
x <= n <~> x < n.+1
  rapply equiv_iff_hprop.
Defined.

(** Turning a finite sequence into a list. *)
Definition Build_list {A : Type} (n : nat)
  (f : forall (i : nat), (i < n) -> A)
  : list A
  := list_map (fun '(i; Hi) => f i Hi) (seq' n).

Definition length_Build_list {A : Type} (n : nat)
  (f : forall (i : nat), (i < n) -> A)
  : length (Build_list n f) = n.
A: Type
n: nat
f: forall i : nat, i < n -> A
length (Build_list n f) = n
Proof.
A: Type
n: nat
f: forall i : nat, i < n -> A
length (Build_list n f) = n
  lhs napply length_list_map.
A: Type
n: nat
f: forall i : nat, i < n -> A
length (seq' n) = n
  apply length_seq'.
Defined.

Definition nth'_Build_list {A : Type} {n : nat}
  (f : forall (i : nat), (i < n) -> A) {i : nat} (Hi : i < n)
  (Hi' : i < length (Build_list n f))
  : nth' (Build_list n f) i Hi' = f i Hi.
A: Type
n: nat
f: forall i0 : nat, i0 < n -> A
i: nat
Hi: i < n
Hi': i < length (Build_list n f)
nth' (Build_list n f) i Hi' = f i Hi
Proof.
A: Type
n: nat
f: forall i0 : nat, i0 < n -> A
i: nat
Hi: i < n
Hi': i < length (Build_list n f)
nth' (Build_list n f) i Hi' = f i Hi
  unshelve lhs snrefine (nth'_list_map _ _ _ (_^ # Hi) _).
A: Type
n: nat
f: forall i0 : nat, i0 < n -> A
i: nat
Hi: i < n
Hi': i < length (Build_list n f)
length (seq' n) = n
A: Type
n: nat
f: forall i0 : nat, i0 < n -> A
i: nat
Hi: i < n
Hi': i < length (Build_list n f)
(let x := nth' (seq' n) i (transport (lt i) ?Goal^ Hi) in
 let i0 := x.1 in let Hi0 := x.2 in f i0 Hi0) =
f i Hi
  1: napply length_seq'.
A: Type
n: nat
f: forall i0 : nat, i0 < n -> A
i: nat
Hi: i < n
Hi': i < length (Build_list n f)
(let x := nth' (seq' n) i (transport (lt i) (length_seq' n)^ Hi) in
 let i0 := x.1 in let Hi0 := x.2 in f i0 Hi0) =
f i Hi
  snapply ap011D.
A: Type
n: nat
f: forall i0 : nat, i0 < n -> A
i: nat
Hi: i < n
Hi': i < length (Build_list n f)
(nth' (seq' n) i (transport (lt i) (length_seq' n)^ Hi)).1 = i
A: Type
n: nat
f: forall i0 : nat, i0 < n -> A
i: nat
Hi: i < n
Hi': i < length (Build_list n f)
transport (fun i0 : nat => i0 < n) ?p
  (nth' (seq' n) i (transport (lt i) (length_seq' n)^ Hi)).2 =
Hi
  1: napply nth'_seq'.
A: Type
n: nat
f: forall i0 : nat, i0 < n -> A
i: nat
Hi: i < n
Hi': i < length (Build_list n f)
transport (fun i0 : nat => i0 < n)
  (nth'_seq' n i (transport (lt i) (length_seq' n)^ Hi))
  (nth' (seq' n) i (transport (lt i) (length_seq' n)^ Hi)).2 =
Hi
  rapply path_ishprop.
Defined.

(** Restriction of an infinite sequence to a list of specified length. *)
Definition list_restrict {A : Type} (s : nat -> A) (n : nat) : list A
  := Build_list n (fun m _ => s m).

Definition length_list_restrict {A : Type} (s : nat -> A) (n : nat)
  : length (list_restrict s n) = n
  := length_Build_list _ _.

(** [nth'] of the restriction of a sequence is the corresponding term of the sequence. *)
Definition nth'_list_restrict {A : Type} (s : nat -> A) {n : nat}
  {i : nat} (Hi : i < length (list_restrict s n))
  : nth' (list_restrict s n) i Hi = s i.
A: Type
s: nat -> A
n, i: nat
Hi: i < length (list_restrict s n)
nth' (list_restrict s n) i Hi = s i
Proof.
A: Type
s: nat -> A
n, i: nat
Hi: i < length (list_restrict s n)
nth' (list_restrict s n) i Hi = s i
  unshelve lhs snapply nth'_list_map.
A: Type
s: nat -> A
n, i: nat
Hi: i < length (list_restrict s n)
i < length (seq' n)
A: Type
s: nat -> A
n, i: nat
Hi: i < length (list_restrict s n)
(let x := nth' (seq' n) i ?Goal in let i0 := x.1 in let Hi0 := x.2 in s i0) =
s i
  -
A: Type
s: nat -> A
n, i: nat
Hi: i < length (list_restrict s n)
i < length (seq' n) exact ((length_list_restrict _ _ @ (length_seq' n)^) # Hi).
  -
A: Type
s: nat -> A
n, i: nat
Hi: i < length (list_restrict s n)
(let x :=
   nth' (seq' n) i
     (transport (lt i) (length_list_restrict s n @ (length_seq' n)^) Hi)
   in
 let i0 := x.1 in let Hi0 := x.2 in s i0) =
s i exact (ap s (nth'_seq' _ _ _)).
Defined.

(** ** Repeat *)

(** The length of a repeated list is the number of repetitions. *)
Definition length_repeat@{i|} {A : Type@{i}} (n : nat) (x : A)
  : length (repeat x n) = n.
A: Type
n: nat
x: A
length (repeat x n) = n
Proof.
A: Type
n: nat
x: A
length (repeat x n) = n
  induction n using nat_ind@{i}.
A: Type
x: A
length (repeat x 0) = 0
A: Type
n: nat
x: A
IHn: length (repeat x n) = n
length (repeat x n.+1) = n.+1
  -
A: Type
x: A
length (repeat x 0) = 0 reflexivity.
  -
A: Type
n: nat
x: A
IHn: length (repeat x n) = n
length (repeat x n.+1) = n.+1 exact (ap S IHn).
Defined.

(** An element of a repeated list is equal to the repeated element. *)
Definition inlist_repeat@{i|} {A : Type@{i}} (n : nat) (x y : A)
  : InList y (repeat x n) -> y = x.
A: Type
n: nat
x, y: A
InList y (repeat x n) -> y = x
Proof.
A: Type
n: nat
x, y: A
InList y (repeat x n) -> y = x
  induction n as [|n IHn].
A: Type
x, y: A
InList y (repeat x 0) -> y = x
A: Type
n: nat
x, y: A
IHn: InList y (repeat x n) -> y = x
InList y (repeat x n.+1) -> y = x
  1:contradiction.
A: Type
n: nat
x, y: A
IHn: InList y (repeat x n) -> y = x
InList y (repeat x n.+1) -> y = x
  intros [p | i].
A: Type
n: nat
x, y: A
IHn: InList y (repeat x n) -> y = x
p: x = y
y = x
A: Type
n: nat
x, y: A
IHn: InList y (repeat x n) -> y = x
i: InList y (repeat x n)
y = x
  -
A: Type
n: nat
x, y: A
IHn: InList y (repeat x n) -> y = x
p: x = y
y = x by symmetry.
  -
A: Type
n: nat
x, y: A
IHn: InList y (repeat x n) -> y = x
i: InList y (repeat x n)
y = x by apply IHn.
Defined.

(** Restricting a sequence to [n.+1] terms has a computation rule. *)
Definition list_restrict_succ {A : Type} (s : nat -> A) (n : nat)
  : list_restrict s n.+1 = list_restrict s n ++ [s n].
A: Type
s: nat -> A
n: nat
list_restrict s n.+1 = list_restrict s n ++ [s n]
Proof.
A: Type
s: nat -> A
n: nat
list_restrict s n.+1 = list_restrict s n ++ [s n]
  unfold list_restrict, Build_list.
A: Type
s: nat -> A
n: nat
list_map (fun pat : {i : nat & i < n.+1} => s pat.1) (seq' n.+1) =
list_map (fun pat : {i : nat & i < n} => s pat.1) (seq' n) ++ [s n]
  lhs napply list_map_compose.
A: Type
s: nat -> A
n: nat
list_map s (list_map (fun x : {i : nat & i < n.+1} => x.1) (seq' n.+1)) =
list_map (fun pat : {i : nat & i < n} => s pat.1) (seq' n) ++ [s n]
  rewrite seq_seq'.
A: Type
s: nat -> A
n: nat
list_map s (seq n.+1) =
list_map (fun pat : {i : nat & i < n} => s pat.1) (seq' n) ++ [s n]
  rewrite seq_succ.
A: Type
s: nat -> A
n: nat
list_map s (seq n ++ [n]) =
list_map (fun pat : {i : nat & i < n} => s pat.1) (seq' n) ++ [s n]
  lhs napply list_map_app.
A: Type
s: nat -> A
n: nat
list_map s (seq n) ++ list_map s [n] =
list_map (fun pat : {i : nat & i < n} => s pat.1) (seq' n) ++ [s n]
  simpl.
A: Type
s: nat -> A
n: nat
list_map s (seq n) ++ [s n] =
list_map (fun pat : {i : nat & i < n} => s pat.1) (seq' n) ++ [s n]
  apply (ap (fun z => z ++ [s n])).
A: Type
s: nat -> A
n: nat
list_map s (seq n) =
list_map (fun pat : {i : nat & i < n} => s pat.1) (seq' n)
  symmetry.
A: Type
s: nat -> A
n: nat
list_map (fun pat : {i : nat & i < n} => s pat.1) (seq' n) =
list_map s (seq n)
  lhs napply list_map_compose.
A: Type
s: nat -> A
n: nat
list_map s (list_map (fun x : {i : nat & i < n} => x.1) (seq' n)) =
list_map s (seq n)
  apply ap, seq_seq'.
Defined.

(** ** Forall *)

(** If a predicate holds for all elements of a list, then the [for_all] predicate holds for the list. *)
Definition for_all_inlist {A : Type} (P : A -> Type) l
  : (forall x, InList x l -> P x) -> for_all P l.
A: Type
P: A -> Type
l: list A
(forall x : A, InList x l -> P x) -> for_all P l
Proof.
A: Type
P: A -> Type
l: list A
(forall x : A, InList x l -> P x) -> for_all P l
  simple_list_induction l h t IHl; intros H; cbn; trivial; split.
A: Type
P: A -> Type
t: list A
IHl: (forall x : A, InList x t -> P x) -> for_all P t
h: A
H: forall x : A, InList x (h :: t) -> P x
P h
A: Type
P: A -> Type
t: list A
IHl: (forall x : A, InList x t -> P x) -> for_all P t
h: A
H: forall x : A, InList x (h :: t) -> P x
for_all P t
  -
A: Type
P: A -> Type
t: list A
IHl: (forall x : A, InList x t -> P x) -> for_all P t
h: A
H: forall x : A, InList x (h :: t) -> P x
P h apply H.
A: Type
P: A -> Type
t: list A
IHl: (forall x : A, InList x t -> P x) -> for_all P t
h: A
H: forall x : A, InList x (h :: t) -> P x
InList h (h :: t)
    by left.
  -
A: Type
P: A -> Type
t: list A
IHl: (forall x : A, InList x t -> P x) -> for_all P t
h: A
H: forall x : A, InList x (h :: t) -> P x
for_all P t apply IHl.
A: Type
P: A -> Type
t: list A
IHl: (forall x : A, InList x t -> P x) -> for_all P t
h: A
H: forall x : A, InList x (h :: t) -> P x
forall x : A, InList x t -> P x
    intros y i.
A: Type
P: A -> Type
t: list A
IHl: (forall x : A, InList x t -> P x) -> for_all P t
h: A
H: forall x : A, InList x (h :: t) -> P x
y: A
i: InList y t
P y
    apply H.
A: Type
P: A -> Type
t: list A
IHl: (forall x : A, InList x t -> P x) -> for_all P t
h: A
H: forall x : A, InList x (h :: t) -> P x
y: A
i: InList y t
InList y (h :: t)
    by right.
Defined.

(** Conversely, if [for_all P l] then each element of the list satisfies [P]. *)
Definition inlist_for_all {A : Type} {P : A -> Type}
  (l : list A)
  : for_all P l -> forall x, InList x l -> P x.
A: Type
P: A -> Type
l: list A
for_all P l -> forall x : A, InList x l -> P x
Proof.
A: Type
P: A -> Type
l: list A
for_all P l -> forall x : A, InList x l -> P x
  simple_list_induction l x l IHl.
A: Type
P: A -> Type
for_all P nil -> forall x : A, InList x nil -> P x
A: Type
P: A -> Type
l: list A
IHl: for_all P l -> forall x0 : A, InList x0 l -> P x0
x: A
for_all P (x :: l) -> forall x0 : A, InList x0 (x :: l) -> P x0
  -
A: Type
P: A -> Type
for_all P nil -> forall x : A, InList x nil -> P x contradiction.
  -
A: Type
P: A -> Type
l: list A
IHl: for_all P l -> forall x0 : A, InList x0 l -> P x0
x: A
for_all P (x :: l) -> forall x0 : A, InList x0 (x :: l) -> P x0 intros [Hx Hl] y [-> | i].
A: Type
P: A -> Type
l: list A
IHl: for_all P l -> forall x : A, InList x l -> P x
y: A
Hx: P y
Hl: for_all P l
P y
A: Type
P: A -> Type
l: list A
IHl: for_all P l -> forall x0 : A, InList x0 l -> P x0
x: A
Hx: P x
Hl: for_all P l
y: A
i: InList y l
P y
    +
A: Type
P: A -> Type
l: list A
IHl: for_all P l -> forall x : A, InList x l -> P x
y: A
Hx: P y
Hl: for_all P l
P y exact Hx.
    +
A: Type
P: A -> Type
l: list A
IHl: for_all P l -> forall x0 : A, InList x0 l -> P x0
x: A
Hx: P x
Hl: for_all P l
y: A
i: InList y l
P y apply IHl.
A: Type
P: A -> Type
l: list A
IHl: for_all P l -> forall x0 : A, InList x0 l -> P x0
x: A
Hx: P x
Hl: for_all P l
y: A
i: InList y l
for_all P l
A: Type
P: A -> Type
l: list A
IHl: for_all P l -> forall x0 : A, InList x0 l -> P x0
x: A
Hx: P x
Hl: for_all P l
y: A
i: InList y l
InList y l
      1: exact Hl.
A: Type
P: A -> Type
l: list A
IHl: for_all P l -> forall x0 : A, InList x0 l -> P x0
x: A
Hx: P x
Hl: for_all P l
y: A
i: InList y l
InList y l
      exact i.
Defined.

(** If a predicate [P] implies a predicate [Q] composed with a function [f], then [for_all P l] implies [for_all Q (list_map f l)]. *)
Definition for_all_list_map {A B : Type} (P : A -> Type) (Q : B -> Type)
  (f : A -> B) (Hf : forall x, P x -> Q (f x))
  : forall l, for_all P l -> for_all Q (list_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 (list_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 (list_map f l)
  simple_list_induction l x l IHl; simpl; trivial.
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
Hf: forall x0 : A, P x0 -> Q (f x0)
l: list A
IHl: for_all P l -> for_all Q (list_map f l)
x: A
P x * for_all P l -> Q (f x) * for_all Q (list_map f l)
  intros [Hx Hl].
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
Hf: forall x0 : A, P x0 -> Q (f x0)
l: list A
IHl: for_all P l -> for_all Q (list_map f l)
x: A
Hx: P x
Hl: for_all P l
Q (f x) * for_all Q (list_map f l)
  split; auto.
Defined.

(** A variant of [for_all_map P Q f] where [Q] is [P o f]. *)
Definition for_all_list_map' {A B : Type} (P : B -> Type) (f : A -> B)
  : forall l, for_all (P o f) l -> for_all P (list_map f l).
A, B: Type
P: B -> Type
f: A -> B
forall l : list A, for_all (P o f) l -> for_all P (list_map f l)
Proof.
A, B: Type
P: B -> Type
f: A -> B
forall l : list A, for_all (P o f) l -> for_all P (list_map f l)
  by apply for_all_list_map.
Defined.

(** If a predicate [P] and a predicate [Q] together imply a predicate [R], then [for_all P l] and [for_all Q l] together imply [for_all R l]. There are also some side conditions for the default elements. *)
Lemma for_all_list_map2 {A B C : Type}
  (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 (list_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 l0 : list A, for_all P l0 -> for_all R (def_l l0)
def_r: list B -> list C
Hdefr: forall l0 : list B, for_all Q l0 -> for_all R (def_r l0)
l1: list A
l2: list B
for_all P l1 -> for_all Q l2 -> for_all R (list_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 l0 : list A, for_all P l0 -> for_all R (def_l l0)
def_r: list B -> list C
Hdefr: forall l0 : list B, for_all Q l0 -> for_all R (def_r l0)
l1: list A
l2: list B
for_all P l1 -> for_all Q l2 -> for_all R (list_map2 f def_l def_r l1 l2)
  revert l2;
    simple_list_induction l1 x l1 IHl1;
    intro 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 l0 : list B, for_all Q l0 -> for_all R (def_r l0)
l2: list B
for_all P nil -> for_all Q l2 -> for_all R (list_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 (x0 : A) (y : B), P x0 -> Q y -> R (f x0 y)
def_l: list A -> list C
Hdefl: forall l0 : list A, for_all P l0 -> for_all R (def_l l0)
def_r: list B -> list C
Hdefr: forall l0 : list B, for_all Q l0 -> for_all R (def_r l0)
l1: list A
IHl1: forall l0 : list B,
for_all P l1 -> for_all Q l0 -> for_all R (list_map2 f def_l def_r l1 l0)
x: A
l2: list B
for_all P (x :: l1) ->
for_all Q l2 -> for_all R (list_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 l0 : list B, for_all Q l0 -> for_all R (def_r l0)
l2: list B
for_all P nil -> for_all Q l2 -> for_all R (list_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 (x0 : A) (y : B), P x0 -> Q y -> R (f x0 y)
def_l: list A -> list C
Hdefl: forall l0 : list A, for_all P l0 -> for_all R (def_l l0)
def_r: list B -> list C
Hdefr: forall l0 : list B, for_all Q l0 -> for_all R (def_r l0)
l1: list A
IHl1: forall l0 : list B,
for_all P l1 -> for_all Q l0 -> for_all R (list_map2 f def_l def_r l1 l0)
x: A
l2: list B
for_all P (x :: l1) ->
for_all Q l2 -> for_all R (list_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 (x0 : A) (y : B), P x0 -> Q y -> R (f x0 y)
def_l: list A -> list C
Hdefl: forall l0 : list A, for_all P l0 -> for_all R (def_l l0)
def_r: list B -> list C
Hdefr: forall l0 : list B, for_all Q l0 -> for_all R (def_r l0)
l1: list A
IHl1: forall l0 : list B,
for_all P l1 -> for_all Q l0 -> for_all R (list_map2 f def_l def_r l1 l0)
x: A
l2: list B
P x * for_all P l1 ->
for_all Q l2 ->
for_all R
  match l2 with
  | nil => def_l (x :: l1)
  | y :: l0 => f x y :: list_map2 f def_l def_r l1 l0
  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 (x0 : A) (y : B), P x0 -> Q y -> R (f x0 y)
def_l: list A -> list C
Hdefl: forall l0 : list A, for_all P l0 -> for_all R (def_l l0)
def_r: list B -> list C
Hdefr: forall l2 : list B, for_all Q l2 -> for_all R (def_r l2)
l1: list A
IHl1: forall l2 : list B,
for_all P l1 -> for_all Q l2 -> for_all R (list_map2 f def_l def_r l1 l2)
x: A
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 (x0 : A) (y : B), P x0 -> Q y -> R (f x0 y)
def_l: list A -> list C
Hdefl: forall l0 : list A, for_all P l0 -> for_all R (def_l l0)
def_r: list B -> list C
Hdefr: forall l2 : list B, for_all Q l2 -> for_all R (def_r l2)
l1: list A
IHl1: forall l2 : list B,
for_all P l1 -> for_all Q l2 -> for_all R (list_map2 f def_l def_r l1 l2)
x: A
Hx: P x
Hl1: for_all P l1
for_all P (x :: l1)
    simpl; auto.
Defined.

(** A simpler variant of [for_all_map2] where both lists have the same length and the side conditions on the default elements can be avoided. *)
Definition for_all_list_map2' {A B C : Type}
  (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 def_r} {l1 : list A} {l2 : list B}
  (p : length l1 = length l2)
  : for_all P l1 -> for_all Q l2
    -> for_all R (list_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
def_r: list B -> list C
l1: list A
l2: list B
p: length l1 = length l2
for_all P l1 -> for_all Q l2 -> for_all R (list_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
def_r: list B -> list C
l1: list A
l2: list B
p: length l1 = length l2
for_all P l1 -> for_all Q l2 -> for_all R (list_map2 f def_l def_r l1 l2)
  revert l2 p;
    simple_list_induction l1 x l1 IHl1;
    intros l2 p.
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
def_r: list B -> list C
l2: list B
p: length nil = length l2
for_all P nil -> for_all Q l2 -> for_all R (list_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 (x0 : A) (y : B), P x0 -> Q y -> R (f x0 y)
def_l: list A -> list C
def_r: list B -> list C
l1: list A
IHl1: forall l0 : list B,
length l1 = length l0 ->
for_all P l1 -> for_all Q l0 -> for_all R (list_map2 f def_l def_r l1 l0)
x: A
l2: list B
p: length (x :: l1) = length l2
for_all P (x :: l1) ->
for_all Q l2 -> for_all R (list_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
def_r: list B -> list C
l2: list B
p: length nil = length l2
for_all P nil -> for_all Q l2 -> for_all R (list_map2 f def_l def_r nil l2) destruct 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
def_r: list B -> list C
p: length nil = length nil
for_all P nil -> for_all Q nil -> for_all R (list_map2 f def_l def_r nil nil)
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
def_r: list B -> list C
b: B
l2: list B
p: length nil = length (b :: l2)
for_all P nil ->
for_all Q (b :: l2) -> for_all R (list_map2 f def_l def_r nil (b :: 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
def_r: list B -> list C
p: length nil = length nil
for_all P nil -> for_all Q nil -> for_all R (list_map2 f def_l def_r nil nil) reflexivity.
    +
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
def_r: list B -> list C
b: B
l2: list B
p: length nil = length (b :: l2)
for_all P nil ->
for_all Q (b :: l2) -> for_all R (list_map2 f def_l def_r nil (b :: l2)) discriminate.
  -
A, B, C: Type
P: A -> Type
Q: B -> Type
R: C -> Type
f: A -> B -> C
Hf: forall (x0 : A) (y : B), P x0 -> Q y -> R (f x0 y)
def_l: list A -> list C
def_r: list B -> list C
l1: list A
IHl1: forall l0 : list B,
length l1 = length l0 ->
for_all P l1 -> for_all Q l0 -> for_all R (list_map2 f def_l def_r l1 l0)
x: A
l2: list B
p: length (x :: l1) = length l2
for_all P (x :: l1) ->
for_all Q l2 -> for_all R (list_map2 f def_l def_r (x :: l1) l2) destruct l2 as [|y l2].
A, B, C: Type
P: A -> Type
Q: B -> Type
R: C -> Type
f: A -> B -> C
Hf: forall (x0 : A) (y : B), P x0 -> Q y -> R (f x0 y)
def_l: list A -> list C
def_r: list B -> list C
l1: list A
IHl1: forall l2 : list B,
length l1 = length l2 ->
for_all P l1 -> for_all Q l2 -> for_all R (list_map2 f def_l def_r l1 l2)
x: A
p: length (x :: l1) = length nil
for_all P (x :: l1) ->
for_all Q nil -> for_all R (list_map2 f def_l def_r (x :: l1) nil)
A, B, C: Type
P: A -> Type
Q: B -> Type
R: C -> Type
f: A -> B -> C
Hf: forall (x0 : A) (y0 : B), P x0 -> Q y0 -> R (f x0 y0)
def_l: list A -> list C
def_r: list B -> list C
l1: list A
IHl1: forall l0 : list B,
length l1 = length l0 ->
for_all P l1 -> for_all Q l0 -> for_all R (list_map2 f def_l def_r l1 l0)
x: A
y: B
l2: list B
p: length (x :: l1) = length (y :: l2)
for_all P (x :: l1) ->
for_all Q (y :: l2) ->
for_all R (list_map2 f def_l def_r (x :: l1) (y :: l2))
    +
A, B, C: Type
P: A -> Type
Q: B -> Type
R: C -> Type
f: A -> B -> C
Hf: forall (x0 : A) (y : B), P x0 -> Q y -> R (f x0 y)
def_l: list A -> list C
def_r: list B -> list C
l1: list A
IHl1: forall l2 : list B,
length l1 = length l2 ->
for_all P l1 -> for_all Q l2 -> for_all R (list_map2 f def_l def_r l1 l2)
x: A
p: length (x :: l1) = length nil
for_all P (x :: l1) ->
for_all Q nil -> for_all R (list_map2 f def_l def_r (x :: l1) nil) discriminate.
    +
A, B, C: Type
P: A -> Type
Q: B -> Type
R: C -> Type
f: A -> B -> C
Hf: forall (x0 : A) (y0 : B), P x0 -> Q y0 -> R (f x0 y0)
def_l: list A -> list C
def_r: list B -> list C
l1: list A
IHl1: forall l0 : list B,
length l1 = length l0 ->
for_all P l1 -> for_all Q l0 -> for_all R (list_map2 f def_l def_r l1 l0)
x: A
y: B
l2: list B
p: length (x :: l1) = length (y :: l2)
for_all P (x :: l1) ->
for_all Q (y :: l2) ->
for_all R (list_map2 f def_l def_r (x :: l1) (y :: l2)) intros [Hx Hl1] [Hy Hl2].
A, B, C: Type
P: A -> Type
Q: B -> Type
R: C -> Type
f: A -> B -> C
Hf: forall (x0 : A) (y0 : B), P x0 -> Q y0 -> R (f x0 y0)
def_l: list A -> list C
def_r: list B -> list C
l1: list A
IHl1: forall l0 : list B,
length l1 = length l0 ->
for_all P l1 -> for_all Q l0 -> for_all R (list_map2 f def_l def_r l1 l0)
x: A
y: B
l2: list B
p: length (x :: l1) = length (y :: l2)
Hx: P x
Hl1: for_all P l1
Hy: Q y
Hl2: for_all Q l2
for_all R (list_map2 f def_l def_r (x :: l1) (y :: l2))
      split.
A, B, C: Type
P: A -> Type
Q: B -> Type
R: C -> Type
f: A -> B -> C
Hf: forall (x0 : A) (y0 : B), P x0 -> Q y0 -> R (f x0 y0)
def_l: list A -> list C
def_r: list B -> list C
l1: list A
IHl1: forall l0 : list B,
length l1 = length l0 ->
for_all P l1 -> for_all Q l0 -> for_all R (list_map2 f def_l def_r l1 l0)
x: A
y: B
l2: list B
p: length (x :: l1) = length (y :: l2)
Hx: P x
Hl1: for_all P l1
Hy: Q y
Hl2: for_all Q l2
R (f x y)
A, B, C: Type
P: A -> Type
Q: B -> Type
R: C -> Type
f: A -> B -> C
Hf: forall (x0 : A) (y0 : B), P x0 -> Q y0 -> R (f x0 y0)
def_l: list A -> list C
def_r: list B -> list C
l1: list A
IHl1: forall l0 : list B,
length l1 = length l0 ->
for_all P l1 -> for_all Q l0 -> for_all R (list_map2 f def_l def_r l1 l0)
x: A
y: B
l2: list B
p: length (x :: l1) = length (y :: l2)
Hx: P x
Hl1: for_all P l1
Hy: Q y
Hl2: for_all Q l2
for_all R (list_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 (x0 : A) (y0 : B), P x0 -> Q y0 -> R (f x0 y0)
def_l: list A -> list C
def_r: list B -> list C
l1: list A
IHl1: forall l0 : list B,
length l1 = length l0 ->
for_all P l1 -> for_all Q l0 -> for_all R (list_map2 f def_l def_r l1 l0)
x: A
y: B
l2: list B
p: length (x :: l1) = length (y :: l2)
Hx: P x
Hl1: for_all P l1
Hy: Q y
Hl2: for_all Q l2
R (f x y) by apply Hf.
      *
A, B, C: Type
P: A -> Type
Q: B -> Type
R: C -> Type
f: A -> B -> C
Hf: forall (x0 : A) (y0 : B), P x0 -> Q y0 -> R (f x0 y0)
def_l: list A -> list C
def_r: list B -> list C
l1: list A
IHl1: forall l0 : list B,
length l1 = length l0 ->
for_all P l1 -> for_all Q l0 -> for_all R (list_map2 f def_l def_r l1 l0)
x: A
y: B
l2: list B
p: length (x :: l1) = length (y :: l2)
Hx: P x
Hl1: for_all P l1
Hy: Q y
Hl2: for_all Q l2
for_all R (list_map2 f def_l def_r l1 l2) apply IHl1; trivial.
A, B, C: Type
P: A -> Type
Q: B -> Type
R: C -> Type
f: A -> B -> C
Hf: forall (x0 : A) (y0 : B), P x0 -> Q y0 -> R (f x0 y0)
def_l: list A -> list C
def_r: list B -> list C
l1: list A
IHl1: forall l0 : list B,
length l1 = length l0 ->
for_all P l1 -> for_all Q l0 -> for_all R (list_map2 f def_l def_r l1 l0)
x: A
y: B
l2: list B
p: length (x :: l1) = length (y :: l2)
Hx: P x
Hl1: for_all P l1
Hy: Q y
Hl2: for_all Q l2
length l1 = length l2
        apply path_nat_succ.
A, B, C: Type
P: A -> Type
Q: B -> Type
R: C -> Type
f: A -> B -> C
Hf: forall (x0 : A) (y0 : B), P x0 -> Q y0 -> R (f x0 y0)
def_l: list A -> list C
def_r: list B -> list C
l1: list A
IHl1: forall l0 : list B,
length l1 = length l0 ->
for_all P l1 -> for_all Q l0 -> for_all R (list_map2 f def_l def_r l1 l0)
x: A
y: B
l2: list B
p: length (x :: l1) = length (y :: l2)
Hx: P x
Hl1: for_all P l1
Hy: Q y
Hl2: for_all Q l2
(length l1).+1 = (length l2).+1
        exact p.
Defined.

(** The left fold of [f] on a list [l] for which [for_all Q l] satisfies [P] if [P] and [Q] imply [P] composed with [f]. *)
Lemma fold_left_preserves {A B : Type}
  (P : A -> Type) (Q : B -> Type) (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)
  revert acc Ha Hl;
    simple_list_induction l x l IHl;
    intros 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 (x0 : A) (y : B), P x0 -> Q y -> P (f x0 y)
l: list B
IHl: forall acc0 : A, P acc0 -> for_all Q l -> P (fold_left f l acc0)
x: B
acc: A
Ha: P acc
Hl: for_all Q (x :: l)
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 (x0 : A) (y : B), P x0 -> Q y -> P (f x0 y)
l: list B
IHl: forall acc0 : A, P acc0 -> for_all Q l -> P (fold_left f l acc0)
x: B
acc: A
Ha: P acc
Hl: for_all Q (x :: l)
P (fold_left f (x :: l) acc) simpl.
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B -> A
Hf: forall (x0 : A) (y : B), P x0 -> Q y -> P (f x0 y)
l: list B
IHl: forall acc0 : A, P acc0 -> for_all Q l -> P (fold_left f l acc0)
x: B
acc: A
Ha: P acc
Hl: for_all Q (x :: l)
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 (x0 : A) (y : B), P x0 -> Q y -> P (f x0 y)
l: list B
IHl: forall acc0 : A, P acc0 -> for_all Q l -> P (fold_left f l acc0)
x: B
acc: A
Ha: P acc
Qx: Q x
Hl: for_all Q l
P (fold_left f l (f acc x))
    apply IHl; auto.
Defined.

(** [for_all] preserves the truncation predicate. *)
Definition istrunc_for_all {A : Type}
  {n : trunc_index} (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 x0 : A => IsTrunc n (P x0)) l -> IsTrunc n (for_all P l)
IsTrunc n (P x) * for_all (fun x0 : A => IsTrunc n (P x0)) 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 x0 : A => IsTrunc n (P x0)) l -> IsTrunc n (for_all P l)
IsTrunc n (P x) * for_all (fun x0 : A => IsTrunc n (P x0)) 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 x0 : A => IsTrunc n (P x0)) l -> IsTrunc n (for_all P l)
Hx: IsTrunc n (P x)
Hl: for_all (fun x0 : A => IsTrunc n (P x0)) 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 x0 : A => IsTrunc n (P x0)) 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.

Instance istrunc_for_all' {A : Type} {n : trunc_index}
  (P : A -> Type) (l : list A)
  `{forall x, IsTrunc n (P x)}
  : IsTrunc n (for_all P l).
A: Type
n: trunc_index
P: A -> Type
l: list A
H: forall x : A, IsTrunc n (P x)
IsTrunc n (for_all P l)
Proof.
A: Type
n: trunc_index
P: A -> Type
l: list A
H: forall x : A, IsTrunc n (P x)
IsTrunc n (for_all P l)
  by apply istrunc_for_all, for_all_inlist.
Defined.

(** If a predicate holds for an element, then it holds [for_all] the elements of the repeated list. *)
Definition for_all_repeat {A : Type} {n : nat}
  (P : A -> Type) (x : A)
  : P x -> for_all P (repeat x n).
A: Type
n: nat
P: A -> Type
x: A
P x -> for_all P (repeat x n)
Proof.
A: Type
n: nat
P: A -> Type
x: A
P x -> for_all P (repeat x n)
  intros H.
A: Type
n: nat
P: A -> Type
x: A
H: P x
for_all P (repeat x n)
  induction n as [|n IHn].
A: Type
P: A -> Type
x: A
H: P x
for_all P (repeat x 0)
A: Type
n: nat
P: A -> Type
x: A
H: P x
IHn: for_all P (repeat x n)
for_all P (repeat x n.+1)
  1: exact tt.
A: Type
n: nat
P: A -> Type
x: A
H: P x
IHn: for_all P (repeat x n)
for_all P (repeat x n.+1)
  exact (H, IHn).
Defined.

(** We can form a list of pairs of a sigma type given a list and a for_all predicate over it. *)
Definition list_sigma {A : Type} (P : A -> Type) (l : list A) (p : for_all P l)
  : list {x : A & P x}.
A: Type
P: A -> Type
l: list A
p: for_all P l
list {x : A & P x}
Proof.
A: Type
P: A -> Type
l: list A
p: for_all P l
list {x : A & P x}
  induction l as [|x l IHl] in p |- *.
A: Type
P: A -> Type
p: for_all P nil
list {x : A & P x}
A: Type
P: A -> Type
x: A
l: list A
p: for_all P (x :: l)
IHl: for_all P l -> list {x0 : A & P x0}
list {x0 : A & P x0}
  1: exact nil.
A: Type
P: A -> Type
x: A
l: list A
p: for_all P (x :: l)
IHl: for_all P l -> list {x0 : A & P x0}
list {x0 : A & P x0}
  destruct p as [Hx Hl].
A: Type
P: A -> Type
x: A
l: list A
Hx: P x
Hl: for_all P l
IHl: for_all P l -> list {x0 : A & P x0}
list {x0 : A & P x0}
  exact ((x; Hx) :: IHl Hl).
Defined.

(** The length of a list of sigma types is the same as the original list. *)
Definition length_list_sigma {A : Type} {P : A -> Type} {l : list A} {p : for_all P l}
  : length (list_sigma P l p) = length l.
A: Type
P: A -> Type
l: list A
p: for_all P l
length (list_sigma P l p) = length l
Proof.
A: Type
P: A -> Type
l: list A
p: for_all P l
length (list_sigma P l p) = length l
  revert p; simple_list_induction l x l IHl; intro p.
A: Type
P: A -> Type
p: for_all P nil
length (list_sigma P nil p) = length nil
A: Type
P: A -> Type
l: list A
IHl: forall p0 : for_all P l, length (list_sigma P l p0) = length l
x: A
p: for_all P (x :: l)
length (list_sigma P (x :: l) p) = length (x :: l)
  1: reflexivity.
A: Type
P: A -> Type
l: list A
IHl: forall p0 : for_all P l, length (list_sigma P l p0) = length l
x: A
p: for_all P (x :: l)
length (list_sigma P (x :: l) p) = length (x :: l)
  destruct p as [Hx Hl].
A: Type
P: A -> Type
l: list A
IHl: forall p : for_all P l, length (list_sigma P l p) = length l
x: A
Hx: P x
Hl: for_all P l
length (list_sigma P (x :: l) (Hx, Hl)) = length (x :: l)
  cbn; f_ap.
A: Type
P: A -> Type
l: list A
IHl: forall p : for_all P l, length (list_sigma P l p) = length l
x: A
Hx: P x
Hl: for_all P l
length
  (list_rect A (fun l0 : list A => for_all P l0 -> list {x0 : A & P x0})
     (unit_name nil)
     (fun (x0 : A) (l0 : list A)
        (IHl0 : for_all P l0 -> list {x1 : A & P x1})
        (p : P x0 * for_all P l0) =>
      (x0; fst p) :: IHl0 (snd p))
     l Hl) =
length l
  apply IHl.
Defined.

(** If a predicate [P] is decidable then so is [for_all P]. *)
Instance decidable_for_all {A : Type} (P : A -> Type)
  `{forall x, Decidable (P x)} (l : list A)
  : Decidable (for_all P l).
A: Type
P: A -> Type
H: forall x : A, Decidable (P x)
l: list A
Decidable (for_all P l)
Proof.
A: Type
P: A -> Type
H: forall x : A, Decidable (P x)
l: list A
Decidable (for_all P l)
  simple_list_induction l x l IHl; exact _.
Defined.

(** If a predicate [P] is decidable then so is [list_exists P]. *)
Instance decidable_list_exists {A : Type} (P : A -> Type)
  `{forall x, Decidable (P x)} (l : list A)
  : Decidable (list_exists P l).
A: Type
P: A -> Type
H: forall x : A, Decidable (P x)
l: list A
Decidable (list_exists P l)
Proof.
A: Type
P: A -> Type
H: forall x : A, Decidable (P x)
l: list A
Decidable (list_exists P l)
  simple_list_induction l x l IHl; exact _.
Defined.

Definition inlist_list_exists {A : Type} (P : A -> Type) (l : list A)
  : list_exists P l -> exists (x : A), InList x l /\ P x.
A: Type
P: A -> Type
l: list A
list_exists P l -> {x : A & (InList x l * P x)%type}
Proof.
A: Type
P: A -> Type
l: list A
list_exists P l -> {x : A & (InList x l * P x)%type}
  simple_list_induction l x l IHl.
A: Type
P: A -> Type
list_exists P nil -> {x : A & (InList x nil * P x)%type}
A: Type
P: A -> Type
l: list A
IHl: list_exists P l -> {x0 : A & (InList x0 l * P x0)%type}
x: A
list_exists P (x :: l) -> {x0 : A & (InList x0 (x :: l) * P x0)%type}
  1: done.
A: Type
P: A -> Type
l: list A
IHl: list_exists P l -> {x0 : A & (InList x0 l * P x0)%type}
x: A
list_exists P (x :: l) -> {x0 : A & (InList x0 (x :: l) * P x0)%type}
  simpl.
A: Type
P: A -> Type
l: list A
IHl: list_exists P l -> {x0 : A & (InList x0 l * P x0)%type}
x: A
P x + list_exists P l -> {x0 : A & (((x = x0) + InList x0 l) * P x0)%type}
  intros [Px | ex].
A: Type
P: A -> Type
l: list A
IHl: list_exists P l -> {x0 : A & (InList x0 l * P x0)%type}
x: A
Px: P x
{x0 : A & (((x = x0) + InList x0 l) * P x0)%type}
A: Type
P: A -> Type
l: list A
IHl: list_exists P l -> {x0 : A & (InList x0 l * P x0)%type}
x: A
ex: list_exists P l
{x0 : A & (((x = x0) + InList x0 l) * P x0)%type}
  -
A: Type
P: A -> Type
l: list A
IHl: list_exists P l -> {x0 : A & (InList x0 l * P x0)%type}
x: A
Px: P x
{x0 : A & (((x = x0) + InList x0 l) * P x0)%type} exists x.
A: Type
P: A -> Type
l: list A
IHl: list_exists P l -> {x0 : A & (InList x0 l * P x0)%type}
x: A
Px: P x
((x = x) + InList x l) * P x
    by split; [left|].
  -
A: Type
P: A -> Type
l: list A
IHl: list_exists P l -> {x0 : A & (InList x0 l * P x0)%type}
x: A
ex: list_exists P l
{x0 : A & (((x = x0) + InList x0 l) * P x0)%type} destruct (IHl ex) as [x' [H Px']].
A: Type
P: A -> Type
l: list A
IHl: list_exists P l -> {x0 : A & (InList x0 l * P x0)%type}
x: A
ex: list_exists P l
x': A
H: InList x' l
Px': P x'
{x0 : A & (((x = x0) + InList x0 l) * P x0)%type}
    exists x'.
A: Type
P: A -> Type
l: list A
IHl: list_exists P l -> {x0 : A & (InList x0 l * P x0)%type}
x: A
ex: list_exists P l
x': A
H: InList x' l
Px': P x'
((x = x') + InList x' l) * P x'
    by split; [right|].
Defined.

Definition list_exists_inlist {A : Type} (P : A -> Type) (l : list A)
  : forall (x : A), InList x l -> P x -> list_exists P l.
A: Type
P: A -> Type
l: list A
forall x : A, InList x l -> P x -> list_exists P l
Proof.
A: Type
P: A -> Type
l: list A
forall x : A, InList x l -> P x -> list_exists P l
  simple_list_induction l x l IHl.
A: Type
P: A -> Type
forall x : A, InList x nil -> P x -> list_exists P nil
A: Type
P: A -> Type
l: list A
IHl: forall x0 : A, InList x0 l -> P x0 -> list_exists P l
x: A
forall x0 : A, InList x0 (x :: l) -> P x0 -> list_exists P (x :: l)
  1: trivial.
A: Type
P: A -> Type
l: list A
IHl: forall x0 : A, InList x0 l -> P x0 -> list_exists P l
x: A
forall x0 : A, InList x0 (x :: l) -> P x0 -> list_exists P (x :: l)
  simpl; intros y H p; revert H.
A: Type
P: A -> Type
l: list A
IHl: forall x0 : A, InList x0 l -> P x0 -> list_exists P l
x, y: A
p: P y
(x = y) + InList y l -> P x + list_exists P l
  apply functor_sum.
A: Type
P: A -> Type
l: list A
IHl: forall x0 : A, InList x0 l -> P x0 -> list_exists P l
x, y: A
p: P y
x = y -> P x
A: Type
P: A -> Type
l: list A
IHl: forall x0 : A, InList x0 l -> P x0 -> list_exists P l
x, y: A
p: P y
InList y l -> list_exists P l
  -
A: Type
P: A -> Type
l: list A
IHl: forall x0 : A, InList x0 l -> P x0 -> list_exists P l
x, y: A
p: P y
x = y -> P x exact (fun r => r^ # p).
  -
A: Type
P: A -> Type
l: list A
IHl: forall x0 : A, InList x0 l -> P x0 -> list_exists P l
x, y: A
p: P y
InList y l -> list_exists P l intros H.
A: Type
P: A -> Type
l: list A
IHl: forall x0 : A, InList x0 l -> P x0 -> list_exists P l
x, y: A
p: P y
H: InList y l
list_exists P l
    by apply (IHl y).
Defined.

Definition list_exists_seq {n : nat} (P : nat -> Type)
  (H : forall k, P k -> k < n)
  : (exists k, P k) <-> list_exists P (seq n).
n: nat
P: nat -> Type
H: forall k : nat, P k -> k < n
{k : nat & P k} <-> list_exists P (seq n)
Proof.
n: nat
P: nat -> Type
H: forall k : nat, P k -> k < n
{k : nat & P k} <-> list_exists P (seq n)
  split.
n: nat
P: nat -> Type
H: forall k : nat, P k -> k < n
{k : nat & P k} -> list_exists P (seq n)
n: nat
P: nat -> Type
H: forall k : nat, P k -> k < n
list_exists P (seq n) -> {k : nat & P k}
  -
n: nat
P: nat -> Type
H: forall k : nat, P k -> k < n
{k : nat & P k} -> list_exists P (seq n) intros [k p].
n: nat
P: nat -> Type
H: forall k0 : nat, P k0 -> k0 < n
k: nat
p: P k
list_exists P (seq n)
    snapply (list_exists_inlist P _ k _ p).
n: nat
P: nat -> Type
H: forall k0 : nat, P k0 -> k0 < n
k: nat
p: P k
InList k (seq n)
    apply inlist_seq, H.
n: nat
P: nat -> Type
H: forall k0 : nat, P k0 -> k0 < n
k: nat
p: P k
P k
    exact p.
  -
n: nat
P: nat -> Type
H: forall k : nat, P k -> k < n
list_exists P (seq n) -> {k : nat & P k} intros H1.
n: nat
P: nat -> Type
H: forall k : nat, P k -> k < n
H1: list_exists P (seq n)
{k : nat & P k}
    apply inlist_list_exists in H1.
n: nat
P: nat -> Type
H: forall k : nat, P k -> k < n
H1: {x : nat & (InList x (seq n) * P x)%type}
{k : nat & P k}
    destruct H1 as [k [Hk p]].
n: nat
P: nat -> Type
H: forall k0 : nat, P k0 -> k0 < n
k: nat
Hk: InList k (seq n)
p: P k
{k0 : nat & P k0}
    exists k.
n: nat
P: nat -> Type
H: forall k0 : nat, P k0 -> k0 < n
k: nat
Hk: InList k (seq n)
p: P k
P k
    exact p.
Defined.

(** An upper bound on witnesses of a decidable predicate makes the sigma type decidable. *)
Definition decidable_exists_nat (n : nat) (P : nat -> Type)
  (H1 : forall k, P k -> k < n)
  (H2 : forall k, Decidable (P k))
  : Decidable (exists k, P k).
n: nat
P: nat -> Type
H1: forall k : nat, P k -> k < n
H2: forall k : nat, Decidable (P k)
Decidable {k : nat & P k}
Proof.
n: nat
P: nat -> Type
H1: forall k : nat, P k -> k < n
H2: forall k : nat, Decidable (P k)
Decidable {k : nat & P k}
  napply decidable_iff.
n: nat
P: nat -> Type
H1: forall k : nat, P k -> k < n
H2: forall k : nat, Decidable (P k)
?Goal <-> {k : nat & P k}
n: nat
P: nat -> Type
H1: forall k : nat, P k -> k < n
H2: forall k : nat, Decidable (P k)
Decidable ?Goal
  1: apply iff_inverse; napply list_exists_seq.
n: nat
P: nat -> Type
H1: forall k : nat, P k -> k < n
H2: forall k : nat, Decidable (P k)
forall k : nat, P k -> k < ?Goal0
n: nat
P: nat -> Type
H1: forall k : nat, P k -> k < n
H2: forall k : nat, Decidable (P k)
Decidable (list_exists P (seq ?Goal0))
  1: exact H1.
n: nat
P: nat -> Type
H1: forall k : nat, P k -> k < n
H2: forall k : nat, Decidable (P k)
Decidable (list_exists P (seq n))
  exact _.
Defined.

(** A common special case.  See also [decidable_search] in Misc/BoundedSearch.v for a similar result with different dependencies. *)
Definition decidable_exists_bounded_nat (n : nat) (P : nat -> Type)
  (H2 : forall k, Decidable (P k))
  : Decidable { k : nat & prod (k < n) (P k) }
  := decidable_exists_nat n _ (fun k => fst) _.