Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc
  Basics.Equivalences Basics.Decidable Basics.Iff.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
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 x y z : list A,
(ap (fun l : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (fun l : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
(ap (fun l : list A => (a :: w) ++ l)
   (app_assoc x y z) @ app_assoc (a :: w) (x ++ y) z) @
ap (fun l : list A => l ++ z) (app_assoc (a :: w) x y) =
app_assoc (a :: w) x (y ++ z) @
app_assoc ((a :: w) ++ x) y z
  -
A: Type
x, y, z: list A
(ap (fun l : list A => nil ++ l) (app_assoc x y z) @
 app_assoc nil (x ++ y) z) @
ap (fun l : list A => l ++ z) (app_assoc nil x y) =
app_assoc nil x (y ++ z) @ app_assoc (nil ++ x) y z simpl.
A: Type
x, y, z: list A
(ap idmap (app_assoc x y z) @ 1) @ 1 =
1 @ app_assoc x y z
    apply equiv_p1_1q.
A: Type
x, y, z: list A
ap idmap (app_assoc x y z) @ 1 = app_assoc x y z
    lhs 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 x y z : list A,
(ap (fun l : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (fun l : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
(ap (fun l : list A => (a :: w) ++ l)
   (app_assoc x y z) @ app_assoc (a :: w) (x ++ y) z) @
ap (fun l : list A => l ++ z) (app_assoc (a :: w) x y) =
app_assoc (a :: w) x (y ++ z) @
app_assoc ((a :: w) ++ x) y z simpl.
A: Type
a: A
w, x, y, z: list A
IHw: forall x y z : list A,
(ap (fun l : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (fun l : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
(ap (fun l : list A => a :: w ++ l) (app_assoc x y z) @
 ap (cons a) (app_assoc w (x ++ y) z)) @
ap (fun l : list A => l ++ z)
  (ap (cons a) (app_assoc w x y)) =
ap (cons a) (app_assoc w x (y ++ z)) @
ap (cons a) (app_assoc (w ++ x) y z)
    rhs_V napply ap_pp.
A: Type
a: A
w, x, y, z: list A
IHw: forall x y z : list A,
(ap (fun l : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (fun l : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
(ap (fun l : list A => a :: w ++ l) (app_assoc x y z) @
 ap (cons a) (app_assoc w (x ++ y) z)) @
ap (fun l : list A => l ++ z)
  (ap (cons a) (app_assoc w x y)) =
ap (cons a)
  (app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z)
    rhs_V exact (ap (ap (cons a)) (IHw x y z)).
A: Type
a: A
w, x, y, z: list A
IHw: forall x y z : list A,
(ap (fun l : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (fun l : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
(ap (fun l : list A => a :: w ++ l) (app_assoc x y z) @
 ap (cons a) (app_assoc w (x ++ y) z)) @
ap (fun l : list A => l ++ z)
  (ap (cons a) (app_assoc w x y)) =
ap (cons a)
  ((ap (fun l : list A => w ++ l) (app_assoc x y z) @
    app_assoc w (x ++ y) z) @
   ap (fun l : list A => l ++ z) (app_assoc w x y))
    rhs napply ap_pp.
A: Type
a: A
w, x, y, z: list A
IHw: forall x y z : list A,
(ap (fun l : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (fun l : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
(ap (fun l : list A => a :: w ++ l) (app_assoc x y z) @
 ap (cons a) (app_assoc w (x ++ y) z)) @
ap (fun l : list A => l ++ z)
  (ap (cons a) (app_assoc w x y)) =
ap (cons a)
  (ap (fun l : list A => w ++ l) (app_assoc x y z) @
   app_assoc w (x ++ y) z) @
ap (cons a)
  (ap (fun l : list A => l ++ z) (app_assoc w x y))
    f_ap.
A: Type
a: A
w, x, y, z: list A
IHw: forall x y z : list A,
(ap (fun l : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (fun l : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
ap (fun l : list A => a :: w ++ l) (app_assoc x y z) @
ap (cons a) (app_assoc w (x ++ y) z) =
ap (cons a)
  (ap (fun l : list A => w ++ l) (app_assoc x y z) @
   app_assoc w (x ++ y) z)
A: Type
a: A
w, x, y, z: list A
IHw: forall x y z : list A,
(ap (fun l : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (fun l : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
ap (fun l : list A => l ++ z)
  (ap (cons a) (app_assoc w x y)) =
ap (cons a)
  (ap (fun l : list A => l ++ z) (app_assoc w x y))
    {
A: Type
a: A
w, x, y, z: list A
IHw: forall x y z : list A,
(ap (fun l : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (fun l : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
ap (fun l : list A => a :: w ++ l) (app_assoc x y z) @
ap (cons a) (app_assoc w (x ++ y) z) =
ap (cons a)
  (ap (fun l : list A => w ++ l) (app_assoc x y z) @
   app_assoc w (x ++ y) z) rhs napply ap_pp.
A: Type
a: A
w, x, y, z: list A
IHw: forall x y z : list A,
(ap (fun l : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (fun l : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
ap (fun l : list A => a :: w ++ l) (app_assoc x y z) @
ap (cons a) (app_assoc w (x ++ y) z) =
ap (cons a)
  (ap (fun l : list A => w ++ l) (app_assoc x y z)) @
ap (cons a) (app_assoc w (x ++ y) z)
      f_ap.
A: Type
a: A
w, x, y, z: list A
IHw: forall x y z : list A,
(ap (fun l : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (fun l : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
ap (fun l : list A => a :: w ++ l) (app_assoc x y z) =
ap (cons a)
  (ap (fun l : list A => w ++ l) (app_assoc x y z))
      apply ap_compose. }
A: Type
a: A
w, x, y, z: list A
IHw: forall x y z : list A,
(ap (fun l : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (fun l : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
ap (fun l : list A => l ++ z)
  (ap (cons a) (app_assoc w x y)) =
ap (cons a)
  (ap (fun l : list A => l ++ z) (app_assoc w x y))
    lhs_V napply ap_compose.
A: Type
a: A
w, x, y, z: list A
IHw: forall x y z : list A,
(ap (fun l : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (fun l : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
ap (fun x : list A => (a :: x) ++ z) (app_assoc w x y) =
ap (cons a)
  (ap (fun l : list A => l ++ z) (app_assoc w x y))
    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 i : A, fold_left f (l ++ l') i = fold_left f l' (fold_left f l i)
fold_left f ((a :: l) ++ l') i =
fold_left f l' (fold_left f (a :: l) i)
  1: reflexivity.
A, B: Type
f: A -> B -> A
a: B
l, l': list B
i: A
IHl: forall i : A, fold_left f (l ++ l') i = fold_left f l' (fold_left f l i)
fold_left f ((a :: l) ++ l') i =
fold_left f l' (fold_left f (a :: l) i)
  apply IHl.
Defined.

(** 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 i : A, fold_right f i (l ++ l') = fold_right f (fold_right f i l') l
fold_right f i ((a :: l) ++ l') =
fold_right f (fold_right f i l') (a :: l)
  1: reflexivity.
A, B: Type
f: B -> A -> A
i: A
a: B
l, l': list B
IHl: forall i : A, fold_right f i (l ++ l') = fold_right f (fold_right f i l') l
fold_right f i ((a :: l) ++ l') =
fold_right f (fold_right f i l') (a :: l)
  exact (ap (f a) (IHl _)).
Defined.

(** ** Maps *)

(** 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) -> {y : A & ((f y = x) * InList y 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) -> {y : A & ((f y = x) * InList y 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) -> {y : A & ((f y = x) * InList y 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) -> {y : A & ((f y = x) * InList y 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) -> {y : A & ((f y = x) * InList y 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) -> {y : A & ((f y = x) * InList y 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) -> {y : A & ((f y = x) * InList y 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 x : A, InList x l -> f x = x) -> 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 x : A, InList x l -> f x = x) -> 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 x : A, InList x l -> f x = x) -> 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 x : A, InList x l -> f x = x) -> 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 x : A, InList x l -> f x = x) -> 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 x : A, InList x l -> f x = x) -> 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 x : A, InList x l -> f x = x) -> 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 x : A, InList x l -> f x = x) -> list_map f l = l
forall x : A, InList x l -> f x = x
      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 x : A, InList x l -> f x = x) -> 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 x : A, InList x l -> f x = x) -> 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 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) 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 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) 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 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) (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 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) (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 l2 : list B,
length l1 = length l2 ->
length (list_map2 f defl defr l1 l2) =
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 (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}}
{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 (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}}
{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) (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}}
{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 (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}}
{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 (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}}
{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 (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}}
{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 (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}}
{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 (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}}
{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 (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}}
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 (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}}
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 (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}}
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 x : A => f x y) l
list_map2 f defl defr (x :: l)
  (repeat y (length (x :: l))) =
list_map (fun x : A => f x 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 x : A => f x y) l
list_map2 f defl defr (x :: l)
  (repeat y (length (x :: l))) =
list_map (fun x : A => f x 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 acc : list A, length acc + length l = length (reverse_acc acc 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 acc : list A, length acc + length l = length (reverse_acc acc 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 acc : list A, length acc + length l = length (reverse_acc acc 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' : list A,
list_map f (reverse_acc l' l) = reverse_acc (list_map f l') (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' : list A,
list_map f (reverse_acc l' l) = reverse_acc (list_map f l') (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' : list A, reverse_acc l' l = reverse l ++ l'
reverse_acc l' (a :: l) = reverse (a :: l) ++ l'
  1: reflexivity.
A: Type
a: A
l, l': list A
IHl: forall l' : list A, reverse_acc l' l = reverse l ++ l'
reverse_acc l' (a :: l) = reverse (a :: l) ++ l'
  lhs napply IHl.
A: Type
a: A
l, l': list A
IHl: forall l' : list A, reverse_acc l' l = reverse l ++ l'
reverse l ++ a :: l' = reverse (a :: l) ++ l'
  lhs napply (app_assoc _ [a]).
A: Type
a: A
l, l': list A
IHl: forall l' : list A, reverse_acc l' l = reverse l ++ l'
(reverse l ++ [a]) ++ l' = reverse (a :: l) ++ l'
  f_ap; symmetry.
A: Type
a: A
l, l': list A
IHl: forall l' : list A, reverse_acc l' l = reverse l ++ l'
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 a : A, reverse (a :: l) = reverse l ++ [a]
reverse (a :: b :: l) = reverse (b :: l) ++ [a]
  1: reflexivity.
A: Type
a, b: A
l: list A
IHl: forall a : A, reverse (a :: l) = reverse l ++ [a]
reverse (a :: b :: l) = reverse (b :: l) ++ [a]
  rewrite IHl.
A: Type
a, b: A
l: list A
IHl: forall a : A, reverse (a :: l) = reverse l ++ [a]
reverse (a :: b :: l) = (reverse l ++ [b]) ++ [a]
  rewrite <- app_assoc.
A: Type
a, b: A
l: list A
IHl: forall a : A, reverse (a :: l) = reverse l ++ [a]
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' : list A, reverse (l ++ l') = reverse l' ++ 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' : list A, reverse (l ++ l') = reverse l' ++ reverse l
reverse ((a :: l) ++ l') =
reverse l' ++ reverse (a :: l)
  simpl.
A: Type
a: A
l, l': list A
IHl: forall l' : list A, reverse (l ++ l') = reverse l' ++ 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' : list A, reverse (l ++ l') = reverse l' ++ 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' : list A, reverse (l ++ l') = reverse l' ++ reverse l
reverse (l ++ l') ++ [a] = reverse l' ++ ?Goal
A: Type
a: A
l, l': list A
IHl: forall l' : list A, reverse (l ++ l') = reverse l' ++ reverse l
reverse (a :: l) = ?Goal
  2: napply reverse_cons.
A: Type
a: A
l, l': list A
IHl: forall l' : list A, reverse (l ++ l') = reverse l' ++ 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' : list A, reverse (l ++ l') = reverse l' ++ 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' : list A, reverse (l ++ l') = reverse l' ++ 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 n : nat, n < length l -> {x : A & nth l n = 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 n : nat, n < length l -> {x : A & nth l n = 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 n : nat, n < length l -> {x : A & nth l n = 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 n : nat, n < length l -> {x : A & nth l n = 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 n : nat, n < length l -> {x : A & nth l n = 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 n : nat, n < length l -> {x : A & nth l n = 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 (n : nat) (H : n < length l), InList (nth' l n H) 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 (n : nat) (H : n < length l), InList (nth' l n H) 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) (H : n < length l), InList (nth' l n H) 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 (n : nat) (H : n < length l), InList (nth' l n H) 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 (n : nat) (H : n < length l), InList (nth' l n H) 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 (n : nat) (H : n < length l), InList (nth' l n H) 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' : list A) (n : nat) (H : n < length l)
(H' : n < length (l ++ l')), nth' (l ++ l') n H' = nth' l n H
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' : list A) (n : nat) (H : n < length l)
(H' : n < length (l ++ l')), nth' (l ++ l') n H' = nth' l n H
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' : list A) (n : nat) (H : n < length l)
(H' : n < length (l ++ l')), nth' (l ++ l') n H' = nth' l n H
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' : list A) (n : nat) (H : n < length l)
(H' : n < length (l ++ l')), nth' (l ++ l') n H' = nth' l n H
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' : list A) (n : nat) (H : n < length l)
(H' : n < length (l ++ l')), nth' (l ++ l') n H' = nth' l n H
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 (A : Type) (l : list A) {struct l} :
     nat :=
   match l with
   | nil => 0
   | _ :: l0 => (length A l0).+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 -> {n : nat & {H : n < length l & nth' l n H = x}}
i: InList x l
n: nat
H: n < length l
H': nth' l n H = x
{n : nat &
{H : n < length (a :: l) & nth' (a :: l) n H = x}}
    snrefine (exist@{i i} _ n.+1 _).
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 l
H': nth' l n H = x
(fun n : nat =>
 {H : n < length (a :: l) & nth' (a :: l) n H = x})
  n.+1
    snrefine (_; _); cbn.
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 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 -> {n : nat & {H : n < length l & nth' l n H = 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 -> {n : nat & {H : n < length l & nth' l n H = 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 -> {n : nat & {H : n < length l & nth' l n H = 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 n : nat, nth (list_map f l) n = functor_option f (nth l n)
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 n : nat, nth (list_map f l) n = functor_option f (nth l n)
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 n : nat, nth (list_map f l) n = functor_option f (nth l n)
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 n : nat, nth (list_map f l) n = functor_option f (nth l n)
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 (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)
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 (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)
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) (H : n < length l) (H' : n < length (list_map f l)),
nth' (list_map f l) n H' = f (nth' l n H)
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 (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)
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 (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)
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 (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)),
length l1 = length l2 ->
f (nth' l1 n H) (nth' l2 n H') =
nth' (list_map2 f defl defr l1 l2) n H''
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 (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)),
length l1 = length l2 ->
f (nth' l1 n H) (nth' l2 n H') =
nth' (list_map2 f defl defr l1 l2) n H''
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) (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)),
length l1 = length l2 ->
f (nth' l1 n H) (nth' l2 n H') =
nth' (list_map2 f defl defr l1 l2) n H''
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 (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)),
length l1 = length l2 ->
f (nth' l1 n H) (nth' l2 n H') =
nth' (list_map2 f defl defr l1 l2) n H''
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) (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)),
length l1 = length l2 ->
f (nth' l1 n H) (nth' l2 n H') =
nth' (list_map2 f defl defr l1 l2) n H''
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 (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)),
length l1 = length l2 ->
f (nth' l1 n H) (nth' l2 n H') =
nth' (list_map2 f defl defr l1 l2) n H''
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 (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)),
length l1 = length l2 ->
f (nth' l1 n H) (nth' l2 n H') =
nth' (list_map2 f defl defr l1 l2) n H''
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 (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)),
length l1 = length l2 ->
f (nth' l1 n H) (nth' l2 n H') =
nth' (list_map2 f defl defr l1 l2) n H''
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 (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)),
length l1 = length l2 ->
f (nth' l1 n H) (nth' l2 n H') =
nth' (list_map2 f defl defr l1 l2) n H''
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 (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)),
length l1 = length l2 ->
f (nth' l1 n H) (nth' l2 n H') =
nth' (list_map2 f defl defr l1 l2) n H''
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 (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)),
length l1 = length l2 ->
f (nth' l1 n H) (nth' l2 n H') =
nth' (list_map2 f defl defr l1 l2) n H''
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
      (A B C : Type) (f : A -> B -> C)
      (def_l : list A -> list C)
      (def_r : list B -> list C) 
      (l1 : list A) (l2 : list B) {struct l1} :
        list C :=
      match l1 with
      | nil =>
          match l2 with
          | nil => nil
          | _ :: _ => def_r l2
          end
      | x :: l3 =>
          match l2 with
          | nil => def_l l1
          | y :: l4 =>
              f x y
              :: list_map2 A B C f def_l def_r l3 l4
          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 (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)),
length l1 = length l2 ->
f (nth' l1 n H) (nth' l2 n H') =
nth' (list_map2 f defl defr l1 l2) n H''
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 (i : nat) (H : i < length (repeat x n)), nth' (repeat x n) i H = 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 (i : nat) (H : i < length (repeat x n)), nth' (repeat x n) i H = 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) (H : i < length (repeat x n)), nth' (repeat x n) i H = 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 (i : nat) (H : i < length (repeat x n)), nth' (repeat x n) i H = 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 (i : nat) (H : i < length (repeat x n)), nth' (repeat x n) i H = 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) (H : n < length l),
nth' l n H = nth' l' n (transport (lt n) p H)
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) (H : n < length nil),
nth' nil n H = nth' l' n (transport (lt n) p H)
nil = l'
A: Type
a: A
l, l': list A
p: length (a :: l) = length l'
H: forall (n : nat) (H : n < length (a :: l)),
nth' (a :: l) n H =
nth' l' n (transport (lt n) p H)
IHl: forall (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'
a :: l = l'
  {
A: Type
l': list A
p: length nil = length l'
H: forall (n : nat) (H : n < length nil),
nth' nil n H = nth' l' n (transport (lt n) p H)
nil = l' destruct l'.
A: Type
p: length nil = length nil
H: forall (n : nat) (H : n < length nil),
nth' nil n H = nth' nil n (transport (lt n) p H)
nil = nil
A: Type
a: A
l': list A
p: length nil = length (a :: l')
H: forall (n : nat) (H : n < length nil),
nth' nil n H =
nth' (a :: l') n (transport (lt n) p H)
nil = a :: l'
    -
A: Type
p: length nil = length nil
H: forall (n : nat) (H : n < length nil),
nth' nil n H = nth' nil n (transport (lt n) p H)
nil = nil reflexivity.
    -
A: Type
a: A
l': list A
p: length nil = length (a :: l')
H: forall (n : nat) (H : n < length nil),
nth' nil n H =
nth' (a :: l') n (transport (lt n) p H)
nil = a :: l' discriminate. }
A: Type
a: A
l, l': list A
p: length (a :: l) = length l'
H: forall (n : nat) (H : n < length (a :: l)),
nth' (a :: l) n H =
nth' l' n (transport (lt n) p H)
IHl: forall (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'
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) (H : n < length (a :: l)),
nth' (a :: l) n H =
nth' nil n (transport (lt n) p H)
IHl: forall (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'
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) (H : n < length (a :: l)),
nth' (a :: l) n H =
nth' (a' :: l') n (transport (lt n) p H)
IHl: forall (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'
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) (H : n < length (a :: l)),
nth' (a :: l) n H =
nth' (a' :: l') n (transport (lt n) p H)
IHl: forall (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'
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) (H : n < length (a :: l)),
nth' (a :: l) n H =
nth' (a' :: l') n (transport (lt n) p H)
IHl: forall (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'
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) (H : n < length (a :: l)),
nth' (a :: l) n H =
nth' (a' :: l') n (transport (lt n) p H)
IHl: forall (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'
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) (H : n < length (a :: l)),
nth' (a :: l) n H =
nth' (a' :: l') n (transport (lt n) p H)
IHl: forall (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'
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) (H : n < length (a :: l)),
nth' (a :: l) n H =
nth' (a' :: l') n (transport (lt n) p H)
IHl: forall (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'
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) (H : n < length (a :: l)),
nth' (a :: l) n H =
nth' (a' :: l') n (transport (lt n) p H)
IHl: forall (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'
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) (H : n < length (a :: l)),
nth' (a :: l) n H =
nth' (a' :: l') n (transport (lt n) p H)
IHl: forall (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'
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) (H : n < length (a :: l)),
nth' (a :: l) n H =
nth' (a' :: l') n (transport (lt n) p H)
IHl: forall (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'
forall (n : nat) (H : n < length l),
nth' l n H =
nth' l' n
  (transport (lt n)
     (path_nat_succ (length l) (length l') p) H)
    intros n Hn.
A: Type
a: A
l: list A
a': A
l': list A
p: length (a :: l) = length (a' :: l')
H: forall (n : nat) (H : n < length (a :: l)),
nth' (a :: l) n H =
nth' (a' :: l') n (transport (lt n) p H)
IHl: forall (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'
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 (n : nat) (H : n < length (a :: l)),
nth' (a :: l) n H =
nth' (a' :: l') n (transport (lt n) p H)
IHl: forall (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'
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 (n : nat) (H : n < length (a :: l)),
nth' (a :: l) n H =
nth' (a' :: l') n (transport (lt n) p H)
IHl: forall (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'
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 (n : nat) (H : n < length (a :: l)),
nth' (a :: l) n H =
nth' (a' :: l') n (transport (lt n) p H)
IHl: forall (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'
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 (n : nat) (H : n < length (a :: l)),
nth' (a :: l) n H =
nth' (a' :: l') n (transport (lt n) p H)
IHl: forall (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'
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' : list A) (n : nat), n < length l -> nth (l ++ l') n = nth l n
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' : list A) (n : nat), n < length l -> nth (l ++ l') n = nth l n
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' : list A) (n : nat), n < length l -> nth (l ++ l') 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' : list A) (n : nat), n < length l -> nth (l ++ l') n = nth l n
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' : list A) (n : nat), n < length l -> nth (l ++ l') n = nth l n
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 x : A, last (l ++ [x]) = Some x
last ((a :: l) ++ [x]) = Some x
  1: reflexivity.
A: Type
a: A
l: list A
x: A
IHl: forall x : A, last (l ++ [x]) = Some x
last ((a :: l) ++ [x]) = Some x
  destruct l.
A: Type
a, x: A
IHl: forall x : A, last (nil ++ [x]) = Some x
last ([a] ++ [x]) = Some x
A: Type
a, a0: A
l: list A
x: A
IHl: forall x : A, last ((a0 :: l) ++ [x]) = Some x
last ((a :: a0 :: l) ++ [x]) = Some x
  1: reflexivity.
A: Type
a, a0: A
l: list A
x: A
IHl: forall x : A, last ((a0 :: l) ++ [x]) = Some x
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 (a : A) (H : length l < length (l ++ [a])),
nth' (l ++ [a]) (length l) H = a
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 (a : A) (H : length l < length (l ++ [a])),
nth' (l ++ [a]) (length l) H = a
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 n : nat, length l <= n -> drop n 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 n : nat, length l <= n -> drop n 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 n : nat, length l <= n -> drop n 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 n : nat, length l <= n -> drop n 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 n : nat, length l <= n -> drop n 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 n : nat, length l <= n -> drop n 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 n : nat, length (drop n l) = length l - n
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 n : nat, length (drop n l) = length l - n
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 n : nat, length (drop n l) = length l - n
length (drop n.+1 (a :: l)) = length (a :: l) - n.+1
  1: reflexivity.
A: Type
n: nat
a: A
l: list A
IHl: forall n : nat, length (drop n l) = length l - n
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 (n : nat) (x : A), InList x (drop n l) -> InList x 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 (n : nat) (x : A), InList x (drop n l) -> InList x 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) (x : A), InList x (drop n l) -> InList x 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 (n : nat) (x : A), InList x (drop n l) -> InList x 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 (n : nat) (x : A), InList x (drop n l) -> InList x 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 n : nat, length l <= n -> take n 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 n : nat, length l <= n -> take n 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 n : nat, length l <= n -> take n 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 n : nat, length l <= n -> take n 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 n : nat, length l <= n -> take n 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 n : nat, length (take n l) = nat_min n (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 n : nat, length (take n l) = nat_min n (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 n : nat, length (take n l) = nat_min n (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 n : nat, length (take n l) = nat_min n (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 (n : nat) (x : A), InList x (take n l) -> InList x 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 (n : nat) (x : A), InList x (take n l) -> InList x 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) (x : A), InList x (take n l) -> InList x 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 (n : nat) (x : A), InList x (take n l) -> InList x 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) (x : A), InList x (take n l) -> InList x l
InList x (a :: l) cbn in H.
A: Type
a: A
l: list A
x: A
H: Empty
IHl: forall (n : nat) (x : A), InList x (take n l) -> InList x 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 (n : nat) (x : A), InList x (take n l) -> InList x l
InList x (a :: l)
  destruct H as [-> | H].
A: Type
n: nat
l: list A
x: A
IHl: forall (n : nat) (x : A), InList x (take n l) -> InList x l
InList x (x :: l)
A: Type
n: nat
a: A
l: list A
x: A
H: InList x (take n l)
IHl: forall (n : nat) (x : A), InList x (take n l) -> InList x l
InList x (a :: l)
  -
A: Type
n: nat
l: list A
x: A
IHl: forall (n : nat) (x : A), InList x (take n l) -> InList x 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 (n : nat) (x : A), InList x (take n l) -> InList x 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 (m : nat) (l : list A), take n (take m l) = take (nat_min n m) l
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 (m : nat) (l : list A), take n (take m l) = take (nat_min n m) l
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) (l : list A), take n (take m l) = take (nat_min n m) l
take n.+1 (take 0 l) = take (nat_min n.+1 0) l
A: Type
m, n: nat
l: list A
IHn: forall (m : nat) (l : list A), take n (take m l) = take (nat_min n m) l
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 (m : nat) (l : list A), take n (take m l) = take (nat_min n m) l
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 (m : nat) (l : list A), take n (take m l) = take (nat_min n m) 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 (m : nat) (l : list A), take n (take m l) = take (nat_min n m) 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 (m : nat) (l : list A), take n (take m l) = take (nat_min n m) 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 (m : nat) (l : list A), take n (take m l) = take (nat_min n m) 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 l1 l2 : list A, n <= length l1 -> take n l1 = take n (l1 ++ l2)
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 l1 l2 : list A, n <= length l1 -> take n l1 = take n (l1 ++ l2)
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 l2 : list A, n <= length l1 -> take n l1 = take n (l1 ++ l2)
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 l1 l2 : list A, n <= length l1 -> take n l1 = take n (l1 ++ l2)
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 l2 : list A, n <= length l1 -> take n l1 = take n (l1 ++ l2)
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 l1 l2 : list A, n <= length l1 -> take n l1 = take n (l1 ++ l2)
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 l1 l2 : list A, n <= length l1 -> take n l1 = take n (l1 ++ l2)
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))%type
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 x : A, Decidable (P x)
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 x : A, Decidable (P x)
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 x : A, Decidable (P x)
x: A
InList x (list_filter nil P dec) <->
InList x nil * P x
A: Type
P: A -> Type
dec: forall x : A, Decidable (P x)
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 x : A, Decidable (P x)
x: A
InList x (list_filter nil P dec) <->
InList x nil * P x simpl.
A: Type
P: A -> Type
dec: forall x : A, Decidable (P x)
x: A
Empty <-> Empty * P x
    apply iff_inverse.
A: Type
P: A -> Type
dec: forall x : A, Decidable (P x)
x: A
Empty * P x <-> Empty
    apply iff_equiv.
A: Type
P: A -> Type
dec: forall x : A, Decidable (P x)
x: A
Empty * P x <~> Empty
    snapply prod_empty_l@{v}.
  -
A: Type
P: A -> Type
dec: forall x : A, Decidable (P x)
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 x : A, Decidable (P x)
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 x : A, Decidable (P x)
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 x : A, Decidable (P x)
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 x : A, Decidable (P x)
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 x : A, Decidable (P x)
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 x : A, Decidable (P x)
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 x : A, Decidable (P x)
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 x : A, Decidable (P x)
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 x : A, Decidable (P x)
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 x : A, Decidable (P x)
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 x : A, Decidable (P x)
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 x : A, Decidable (P x)
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 x : A, Decidable (P x)
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 x : A, Decidable (P x)
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 x : A, Decidable (P x)
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 x : A, Decidable (P x)
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 x : A, Decidable (P x)
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 x : A, Decidable (P x)
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 x : A, Decidable (P x)
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 x : A, Decidable (P x)
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 x : A, Decidable (P x)
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)%type
        exact (idpath, p).
      *
A: Type
P: A -> Type
dec: forall x : A, Decidable (P x)
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 x : A, Decidable (P x)
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 x : A, Decidable (P x)
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 x : A, Decidable (P x)
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 x : A, Decidable (P x)
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 x : A, Decidable (P x)
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 x : A, Decidable (P x)
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 x : A, Decidable (P x)
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 x : A, Decidable (P x)
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 x : A, Decidable (P x)
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 x : A, Decidable (P x)
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 x : A, Decidable (P x)
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 n : nat,
{k : nat & k < n} -> {k : nat & k < n.+1}
n: nat
f:= ?Goal: forall n : nat,
{k : nat & k < n} -> {k : nat & k < n.+1}
list {k : nat & k < n}
  {
n: nat
forall n : nat,
{k : nat & k < n} -> {k : nat & k < n.+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 k : nat => k < m) k
(fun k : nat => k < 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 n : nat,
{k : nat & k < n} -> {k : nat & k < n.+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 n : nat,
{k : nat & k < n} -> {k : nat & k < n.+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 n : nat,
{k : nat & k < n} -> {k : nat & k < n.+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 n : nat,
{k : nat & k < n} -> {k : nat & k < n.+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 n : nat => list {k : nat & k < n})
        nil
        (fun (n : nat) (IHn : list {k : nat & k < n})
         =>
         (n; leq_refl n.+1)
         :: list_map
              (functor_sigma idmap
                 (fun (k : nat) (H : k < n) =>
                  leq_succ_r H)) IHn) n)) = n
  lhs napply length_list_map.
n: nat
IHn: length (seq_rev' n) = n
length
  (nat_rec (fun n : nat => list {k : nat & k < n}) nil
     (fun (n : nat) (IHn : list {k : nat & k < n}) =>
      (n; leq_refl n.+1)
      :: list_map
           (functor_sigma idmap
              (fun (k : nat) (H : k < n) =>
               leq_succ_r H)) IHn) 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 n : nat, i < n -> nth (seq_rev n) i = Some (n - 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 n : nat, i < n -> nth (seq_rev n) i = Some (n - 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 n : nat, i < n -> nth (seq_rev n) i = Some (n - 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 n : nat, i < n -> nth (seq_rev n) i = Some (n - 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 n : nat => i < n) 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 n : nat => i < n) 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 n : nat => i < n) 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 n : nat => i < n) 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 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
Proof.
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
  unshelve lhs snrefine (nth'_list_map _ _ _ (_^ # Hi) _).
A: Type
n: nat
f: forall i : nat, i < n -> A
i: nat
Hi: i < n
Hi': i < length (Build_list n f)
length (seq' n) = n
A: Type
n: nat
f: forall i : nat, i < 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 i := x.1 in let Hi := x.2 in f i Hi) = f i Hi
  1: napply length_seq'.
A: Type
n: nat
f: forall i : nat, i < 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 i := x.1 in let Hi := x.2 in f i Hi) = f i Hi
  snapply ap011D.
A: Type
n: nat
f: forall i : nat, i < 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 i : nat, i < n -> A
i: nat
Hi: i < n
Hi': i < length (Build_list n f)
transport (fun i : nat => i < 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 i : nat, i < n -> A
i: nat
Hi: i < n
Hi': i < length (Build_list n f)
transport (fun i : nat => i < 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 i := x.1 in let Hi := x.2 in s i) = 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 i := x.1 in let Hi := x.2 in s i) = 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 x : A, InList x l -> P x
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 x : A, InList x l -> P x
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 x : A, InList x l -> P x
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 x : A, InList x l -> P x
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 x : A, InList x l -> P x
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 x : A, InList x l -> P x
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 x : A, InList x l -> P x
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 x : A, P x -> Q (f x)
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 x : A, P x -> Q (f x)
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))%type
  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 l1 : list A,
for_all P l1 -> for_all R (def_l l1)
def_r: list B -> list C
Hdefr: forall l2 : list B,
for_all Q l2 -> for_all R (def_r l2)
l1: list A
l2: list B
for_all P l1 ->
for_all Q l2 ->
for_all R (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 l1 : list A,
for_all P l1 -> for_all R (def_l l1)
def_r: list B -> list C
Hdefr: forall l2 : list B,
for_all Q l2 -> for_all R (def_r l2)
l1: list A
l2: list B
for_all P l1 ->
for_all Q l2 ->
for_all R (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 l2 : list B,
for_all Q l2 -> for_all R (def_r l2)
l2: list B
for_all P nil ->
for_all Q l2 ->
for_all R (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 (x : A) (y : B), P x -> Q y -> R (f x y)
def_l: list A -> list C
Hdefl: forall l1 : list A,
for_all P l1 -> for_all R (def_l l1)
def_r: list B -> list C
Hdefr: forall l2 : list B,
for_all Q l2 -> for_all R (def_r l2)
l1: list A
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
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 l2 : list B,
for_all Q l2 -> for_all R (def_r l2)
l2: list B
for_all P nil ->
for_all Q l2 ->
for_all R (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 (x : A) (y : B), P x -> Q y -> R (f x y)
def_l: list A -> list C
Hdefl: forall l1 : list A,
for_all P l1 -> for_all R (def_l l1)
def_r: list B -> list C
Hdefr: forall l2 : list B,
for_all Q l2 -> for_all R (def_r l2)
l1: list A
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
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 (x : A) (y : B), P x -> Q y -> R (f x y)
def_l: list A -> list C
Hdefl: forall l1 : list A,
for_all P l1 -> for_all R (def_l l1)
def_r: list B -> list C
Hdefr: forall l2 : list B,
for_all Q l2 -> for_all R (def_r l2)
l1: list A
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
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 :: l2 => f x y :: list_map2 f def_l def_r l1 l2
  end destruct l2 as [|y l2]; intros [Hx Hl1];
      [intros _ | intros [Hy Hl2] ]; simpl; auto.
A, B, C: Type
P: A -> Type
Q: B -> Type
R: C -> Type
f: A -> B -> C
Hf: forall (x : A) (y : B), P x -> Q y -> R (f x y)
def_l: list A -> list C
Hdefl: forall l1 : list A,
for_all P l1 -> for_all R (def_l l1)
def_r: list B -> list C
Hdefr: forall l2 : list B,
for_all Q l2 -> for_all R (def_r l2)
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 (x : A) (y : B), P x -> Q y -> R (f x y)
def_l: list A -> list C
Hdefl: forall l1 : list A,
for_all P l1 -> for_all R (def_l l1)
def_r: list B -> list C
Hdefr: forall l2 : list B,
for_all Q l2 -> for_all R (def_r l2)
l1: list A
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 (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
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
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 (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
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
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 (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
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 (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
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
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 (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
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 (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
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
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 (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
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
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 (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
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
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 (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
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
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 (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
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
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 (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
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
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 (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
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
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 (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
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
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 (x : A) (y : B), P x -> Q y -> P (f x y)
l: list B
IHl: forall acc : A, P acc -> for_all Q l -> P (fold_left f l acc)
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 (x : A) (y : B), P x -> Q y -> P (f x y)
l: list B
IHl: forall acc : A, P acc -> for_all Q l -> P (fold_left f l acc)
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 (x : A) (y : B), P x -> Q y -> P (f x y)
l: list B
IHl: forall acc : A, P acc -> for_all Q l -> P (fold_left f l acc)
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 (x : A) (y : B), P x -> Q y -> P (f x y)
l: list B
IHl: forall acc : A, P acc -> for_all Q l -> P (fold_left f l acc)
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 x : A => IsTrunc n (P x)) l -> IsTrunc n (for_all P l)
IsTrunc n (P x) *
for_all (fun x : A => IsTrunc n (P x)) l ->
IsTrunc n (P x * for_all P l)
  -
A: Type
n: trunc_index
P: A -> Type
Unit -> IsTrunc n Unit destruct n; exact _.
  -
A: Type
n: trunc_index
P: A -> Type
x: A
l: list A
IHl: for_all (fun x : A => IsTrunc n (P x)) l -> IsTrunc n (for_all P l)
IsTrunc n (P x) *
for_all (fun x : A => IsTrunc n (P x)) l ->
IsTrunc n (P x * for_all P l) intros [Hx Hl].
A: Type
n: trunc_index
P: A -> Type
x: A
l: list A
IHl: for_all (fun x : A => IsTrunc n (P x)) l -> IsTrunc n (for_all P l)
Hx: IsTrunc n (P x)
Hl: for_all (fun x : A => IsTrunc n (P x)) l
IsTrunc n (P x * for_all P l)
    apply IHl in Hl.
A: Type
n: trunc_index
P: A -> Type
x: A
l: list A
IHl: for_all (fun x : A => IsTrunc n (P x)) l -> IsTrunc n (for_all P l)
Hx: IsTrunc n (P x)
Hl: IsTrunc n (for_all P l)
IsTrunc n (P x * for_all P l)
    exact _.
Defined.

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 {x : A & P x}
list {x : A & P x}
  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 {x : A & P x}
list {x : A & P x}
  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 {x : A & P x}
list {x : A & P x}
  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 p : for_all P l, length (list_sigma P l p) = 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 p : for_all P l, length (list_sigma P l p) = 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 l : list A =>
      for_all P l -> list {x : A & P x})
     (unit_name nil)
     (fun (x : A) (l : list A)
        (IHl : for_all P l -> list {x0 : A & P x0})
        (p : P x * for_all P l) =>
      (x; fst p) :: IHl (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 -> {x : A & (InList x l * P x)%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 -> {x : A & (InList x l * P x)%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 -> {x : A & (InList x l * P x)%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 -> {x : A & (InList x l * P x)%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 -> {x : A & (InList x l * P x)%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 -> {x : A & (InList x l * P x)%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 -> {x : A & (InList x l * P x)%type}
x: A
Px: P x
(((x = x) + InList x l) * P x)%type
    by split; [left|].
  -
A: Type
P: A -> Type
l: list A
IHl: list_exists P l -> {x : A & (InList x l * P x)%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 -> {x : A & (InList x l * P x)%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 -> {x : A & (InList x l * P x)%type}
x: A
ex: list_exists P l
x': A
H: InList x' l
Px': P x'
(((x = x') + InList x' l) * P x')%type
    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 x : A, InList x l -> P x -> 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 x : A, InList x l -> P x -> 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 x : A, InList x l -> P x -> 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 x : A, InList x l -> P x -> list_exists P l
x, y: A
p: P y
x = y -> P x
A: Type
P: A -> Type
l: list A
IHl: forall x : A, InList x l -> P x -> 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 x : A, InList x l -> P x -> 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 x : A, InList x l -> P x -> 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 x : A, InList x l -> P x -> 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 k : nat, P k -> k < 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 k : nat, P k -> k < n
k: nat
p: P k
InList k (seq n)
    apply inlist_seq, H.
n: nat
P: nat -> Type
H: forall k : nat, P k -> k < 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 k : nat, P k -> k < n
k: nat
Hk: InList k (seq n)
p: P k
{k : nat & P k}
    exists k.
n: nat
P: nat -> Type
H: forall k : nat, P k -> k < 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) _.