FinSeq.v

Require Import
  HoTT.Basics
  HoTT.Types
  HoTT.Universes.HSet
  HoTT.Spaces.Finite.Fin
  HoTT.Spaces.Finite.FinInduction
  HoTT.Spaces.Nat.Core.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Local Open Scope nat_scope.

(** Finite-dimensional sequence. It is often referred to as vector,
    but we call it finite sequence [FinSeq] to avoid confusion with
    vector from linear algebra.

    Note that the induction principle [finseq_]*)

Definition FinSeq@{u} (n : nat) (A : Type@{u}) : Type@{u} := Fin n -> A.

(** The empty finite sequence. *)

Definition fsnil {A : Type} : FinSeq 0 A := Empty_rec.

Definition path_fsnil `{Funext} {A : Type} (v : FinSeq 0 A) : fsnil = v.H: Funext
A: Type
v: FinSeq 0 A
fsnil = v
Proof.H: Funext
A: Type
v: FinSeq 0 A
fsnil = v
  apply path_contr.
Defined.

(** Add an element in the end of a finite sequence, [fscons'] and [fscons]. *)

Definition fscons' {A : Type} (n : nat) (a : A) (v : FinSeq (nat_pred n) A)
  : FinSeq n A
  := fun i =>  fin_rec (fun n => FinSeq (nat_pred n) A -> A)
                       (fun _ _ => a) (fun n' i _ v => v i) i v.

Definition fscons {A : Type} {n : nat} : A -> FinSeq n A -> FinSeq n.+1 A
  := fscons' n.+1.

(** Take the first element of a non-empty finite sequence,
    [fshead'] and [fshead]. *)

Definition fshead' {A} (n : nat) : 0 < n -> FinSeq n A -> A
  := match n with
     | 0 => fun N _ => Empty_rec (not_lt_zero_r _ N)
     | n'.+1 => fun _ v => v fin_zero
     end.

Definition fshead {A} {n : nat} : FinSeq n.+1 A -> A := fshead' n.+1 _.

Definition fshead'_beta_fscons' {A} n (N : n > 0) (a : A) (v : FinSeq (nat_pred n) A)
  : fshead' n N (fscons' n a v) = a.A: Type
n: nat
N: n > 0
a: A
v: FinSeq (nat_pred n) A
fshead' n N (fscons' n a v) = a
Proof.A: Type
n: nat
N: n > 0
a: A
v: FinSeq (nat_pred n) A
fshead' n N (fscons' n a v) = a
  destruct n; [elim (lt_irrefl _ N)|].A: Type
n: nat
N: n.+1 > 0
a: A
v: FinSeq (nat_pred n.+1) A
fshead' n.+1 N (fscons' n.+1 a v) = a
  exact (apD10 (fin_rec_beta_zero _ _ _ _) v).
Defined.

Definition fshead_beta_fscons {A} {n} (a : A) (v : FinSeq n A)
  : fshead (fscons a v) = a.A: Type
n: nat
a: A
v: FinSeq n A
fshead (fscons a v) = a
Proof.A: Type
n: nat
a: A
v: FinSeq n A
fshead (fscons a v) = a
  apply fshead'_beta_fscons'.
Defined.

(** If the sequence is non-empty, then remove the first element. *)

Definition fstail' {A} (n : nat) : FinSeq n A -> FinSeq (nat_pred n) A
  := match n with
     | 0 => fun _ => Empty_rec
     | n'.+1 => fun v i => v (fsucc i)
     end.

(** Remove the first element from a non-empty sequence. *)

Definition fstail {A} {n : nat} : FinSeq n.+1 A -> FinSeq n A := fstail' n.+1.

Definition fstail'_beta_fscons' {A} n (a : A) (v : FinSeq (nat_pred n) A)
  : fstail' n (fscons' n a v) == v.A: Type
n: nat
a: A
v: FinSeq (nat_pred n) A
fstail' n (fscons' n a v) == v
Proof.A: Type
n: nat
a: A
v: FinSeq (nat_pred n) A
fstail' n (fscons' n a v) == v
  intro i.A: Type
n: nat
a: A
v: FinSeq (nat_pred n) A
i: Fin (nat_pred n)
fstail' n (fscons' n a v) i = v i
  destruct n; [elim i|].A: Type
n: nat
a: A
v: FinSeq (nat_pred n.+1) A
i: Fin (nat_pred n.+1)
fstail' n.+1 (fscons' n.+1 a v) i = v i
  exact (apD10 (fin_rec_beta_fsucc _ _ _ _) v).
Defined.

Definition fstail_beta_fscons `{Funext} {A} {n} (a : A) (v : FinSeq n A)
  : fstail (fscons a v) = v.H: Funext
A: Type
n: nat
a: A
v: FinSeq n A
fstail (fscons a v) = v
Proof.H: Funext
A: Type
n: nat
a: A
v: FinSeq n A
fstail (fscons a v) = v
  funext i.H: Funext
A: Type
n: nat
a: A
v: FinSeq n A
i: Fin n
fstail (fscons a v) i = v i
  apply fstail'_beta_fscons'.
Defined.

(** A non-empty finite sequence is equal to [fscons] of head and tail,
    [path_expand_fscons'] and [path_expand_fscons]. *)

Lemma path_expand_fscons' {A : Type} (n : nat)
  (i : Fin n) (N : n > 0) (v : FinSeq n A)
  : fscons' n (fshead' n N v) (fstail' n v) i = v i.A: Type
n: nat
i: Fin n
N: n > 0
v: FinSeq n A
fscons' n (fshead' n N v) (fstail' n v) i = v i
Proof.A: Type
n: nat
i: Fin n
N: n > 0
v: FinSeq n A
fscons' n (fshead' n N v) (fstail' n v) i = v i
  induction i using fin_ind.A: Type
n: nat
N: n.+1 > 0
v: FinSeq n.+1 A
fscons' n.+1 (fshead' n.+1 N v) (fstail' n.+1 v)
  fin_zero = v fin_zero
A: Type
n: nat
i: Fin n
N: n.+1 > 0
v: FinSeq n.+1 A
IHi: forall (N : n > 0) (v : FinSeq n A),
fscons' n (fshead' n N v) (fstail' n v) i = v i
fscons' n.+1 (fshead' n.+1 N v) (fstail' n.+1 v)
  (fsucc i) = v (fsucc i)
  -A: Type
n: nat
N: n.+1 > 0
v: FinSeq n.+1 A
fscons' n.+1 (fshead' n.+1 N v) (fstail' n.+1 v)
  fin_zero = v fin_zero apply fshead_beta_fscons.
  -A: Type
n: nat
i: Fin n
N: n.+1 > 0
v: FinSeq n.+1 A
IHi: forall (N : n > 0) (v : FinSeq n A),
fscons' n (fshead' n N v) (fstail' n v) i = v i
fscons' n.+1 (fshead' n.+1 N v) (fstail' n.+1 v)
  (fsucc i) = v (fsucc i) apply (fstail'_beta_fscons' n.+1 (fshead v) (fstail v)).
Defined.

Lemma path_expand_fscons `{Funext} {A} {n} (v : FinSeq n.+1 A)
  : fscons (fshead v) (fstail v) = v.H: Funext
A: Type
n: nat
v: FinSeq n.+1 A
fscons (fshead v) (fstail v) = v
Proof.H: Funext
A: Type
n: nat
v: FinSeq n.+1 A
fscons (fshead v) (fstail v) = v
  funext i.H: Funext
A: Type
n: nat
v: FinSeq n.+1 A
i: Fin n.+1
fscons (fshead v) (fstail v) i = v i
  apply path_expand_fscons'.
Defined.

(** The following [path_fscons'] and [path_fscons] gives a way to construct
    a path between [fscons] finite sequences. They cooperate nicely with
    [path_expand_fscons'] and [path_expand_fscons]. *)

Definition path_fscons' {A} n {a1 a2 : A} {v1 v2 : FinSeq (nat_pred n) A}
  (p : a1 = a2) (q : forall i, v1 i = v2 i) (i : Fin n)
  : fscons' n a1 v1 i = fscons' n a2 v2 i.A: Type
n: nat
a1, a2: A
v1, v2: FinSeq (nat_pred n) A
p: a1 = a2
q: forall i : Fin (nat_pred n), v1 i = v2 i
i: Fin n
fscons' n a1 v1 i = fscons' n a2 v2 i
Proof.A: Type
n: nat
a1, a2: A
v1, v2: FinSeq (nat_pred n) A
p: a1 = a2
q: forall i : Fin (nat_pred n), v1 i = v2 i
i: Fin n
fscons' n a1 v1 i = fscons' n a2 v2 i
  induction i using fin_ind.A: Type
a1, a2: A
n: nat
v1, v2: FinSeq (nat_pred n.+1) A
p: a1 = a2
q: forall i : Fin (nat_pred n.+1), v1 i = v2 i
fscons' n.+1 a1 v1 fin_zero =
fscons' n.+1 a2 v2 fin_zero
A: Type
a1, a2: A
n: nat
v1, v2: FinSeq (nat_pred n.+1) A
p: a1 = a2
q: forall i : Fin (nat_pred n.+1), v1 i = v2 i
i: Fin n
IHi: forall v1 v2 : FinSeq (nat_pred n) A,
(forall i : Fin (nat_pred n), v1 i = v2 i) ->
fscons' n a1 v1 i = fscons' n a2 v2 i
fscons' n.+1 a1 v1 (fsucc i) =
fscons' n.+1 a2 v2 (fsucc i)
  -A: Type
a1, a2: A
n: nat
v1, v2: FinSeq (nat_pred n.+1) A
p: a1 = a2
q: forall i : Fin (nat_pred n.+1), v1 i = v2 i
fscons' n.+1 a1 v1 fin_zero =
fscons' n.+1 a2 v2 fin_zero exact (fshead_beta_fscons _ _ @ p @ (fshead_beta_fscons _ _)^).
  -A: Type
a1, a2: A
n: nat
v1, v2: FinSeq (nat_pred n.+1) A
p: a1 = a2
q: forall i : Fin (nat_pred n.+1), v1 i = v2 i
i: Fin n
IHi: forall v1 v2 : FinSeq (nat_pred n) A,
(forall i : Fin (nat_pred n), v1 i = v2 i) ->
fscons' n a1 v1 i = fscons' n a2 v2 i
fscons' n.+1 a1 v1 (fsucc i) =
fscons' n.+1 a2 v2 (fsucc i) refine (_ @ (fstail'_beta_fscons' n.+1 a2 v2 i)^).A: Type
a1, a2: A
n: nat
v1, v2: FinSeq (nat_pred n.+1) A
p: a1 = a2
q: forall i : Fin (nat_pred n.+1), v1 i = v2 i
i: Fin n
IHi: forall v1 v2 : FinSeq (nat_pred n) A,
(forall i : Fin (nat_pred n), v1 i = v2 i) ->
fscons' n a1 v1 i = fscons' n a2 v2 i
fscons' n.+1 a1 v1 (fsucc i) = v2 i
    exact (fstail'_beta_fscons' n.+1 a1 v1 i @ q i).
Defined.

Definition path_fscons'_beta {A} (n : nat)
    (a : A) (v : FinSeq (nat_pred n) A) (i : Fin n)
    : path_fscons' n (idpath a) (fun j => idpath (v j)) i = idpath.A: Type
n: nat
a: A
v: FinSeq (nat_pred n) A
i: Fin n
path_fscons' n 1 (fun j : Fin (nat_pred n) => 1) i = 1
Proof.A: Type
n: nat
a: A
v: FinSeq (nat_pred n) A
i: Fin n
path_fscons' n 1 (fun j : Fin (nat_pred n) => 1) i = 1
  induction i using fin_ind; unfold path_fscons'.A: Type
a: A
n: nat
v: FinSeq (nat_pred n.+1) A
fin_ind
  (fun (n : nat) (i : Fin n) =>
   forall v1 v2 : FinSeq (nat_pred n) A,
   (forall i0 : Fin (nat_pred n), v1 i0 = v2 i0) ->
   fscons' n a v1 i = fscons' n a v2 i)
  (fun (n : nat) (v1 v2 : FinSeq (nat_pred n.+1) A)
     (_ : forall i : Fin (nat_pred n.+1), v1 i = v2 i)
   =>
   (fshead_beta_fscons a v1 @ 1) @
   (fshead_beta_fscons a v2)^)
  (fun (n : nat) (i : Fin n)
     (_ : forall v1 v2 : FinSeq (nat_pred n) A,
          (forall i0 : Fin (nat_pred n), v1 i0 = v2 i0) ->
          fscons' n a v1 i = fscons' n a v2 i)
     (v1 v2 : FinSeq (nat_pred n.+1) A)
     (q : forall i0 : Fin (nat_pred n.+1),
          v1 i0 = v2 i0) =>
   (fstail'_beta_fscons' n.+1 a v1 i @ q i) @
   (fstail'_beta_fscons' n.+1 a v2 i)^) fin_zero v v
  (fun j : Fin (nat_pred n.+1) => 1) = 1
A: Type
a: A
n: nat
v: FinSeq (nat_pred n.+1) A
i: Fin n
IHi: forall v : FinSeq (nat_pred n) A,
path_fscons' n 1 (fun j : Fin (nat_pred n) => 1) i = 1
fin_ind
  (fun (n : nat) (i : Fin n) =>
   forall v1 v2 : FinSeq (nat_pred n) A,
   (forall i0 : Fin (nat_pred n), v1 i0 = v2 i0) ->
   fscons' n a v1 i = fscons' n a v2 i)
  (fun (n : nat) (v1 v2 : FinSeq (nat_pred n.+1) A)
     (_ : forall i : Fin (nat_pred n.+1), v1 i = v2 i)
   =>
   (fshead_beta_fscons a v1 @ 1) @
   (fshead_beta_fscons a v2)^)
  (fun (n : nat) (i : Fin n)
     (_ : forall v1 v2 : FinSeq (nat_pred n) A,
          (forall i0 : Fin (nat_pred n), v1 i0 = v2 i0) ->
          fscons' n a v1 i = fscons' n a v2 i)
     (v1 v2 : FinSeq (nat_pred n.+1) A)
     (q : forall i0 : Fin (nat_pred n.+1),
          v1 i0 = v2 i0) =>
   (fstail'_beta_fscons' n.+1 a v1 i @ q i) @
   (fstail'_beta_fscons' n.+1 a v2 i)^) (fsucc i) v v
  (fun j : Fin (nat_pred n.+1) => 1) = 1
  -A: Type
a: A
n: nat
v: FinSeq (nat_pred n.+1) A
fin_ind
  (fun (n : nat) (i : Fin n) =>
   forall v1 v2 : FinSeq (nat_pred n) A,
   (forall i0 : Fin (nat_pred n), v1 i0 = v2 i0) ->
   fscons' n a v1 i = fscons' n a v2 i)
  (fun (n : nat) (v1 v2 : FinSeq (nat_pred n.+1) A)
     (_ : forall i : Fin (nat_pred n.+1), v1 i = v2 i)
   =>
   (fshead_beta_fscons a v1 @ 1) @
   (fshead_beta_fscons a v2)^)
  (fun (n : nat) (i : Fin n)
     (_ : forall v1 v2 : FinSeq (nat_pred n) A,
          (forall i0 : Fin (nat_pred n), v1 i0 = v2 i0) ->
          fscons' n a v1 i = fscons' n a v2 i)
     (v1 v2 : FinSeq (nat_pred n.+1) A)
     (q : forall i0 : Fin (nat_pred n.+1),
          v1 i0 = v2 i0) =>
   (fstail'_beta_fscons' n.+1 a v1 i @ q i) @
   (fstail'_beta_fscons' n.+1 a v2 i)^) fin_zero v v
  (fun j : Fin (nat_pred n.+1) => 1) = 1 rewrite fin_ind_beta_zero.A: Type
a: A
n: nat
v: FinSeq (nat_pred n.+1) A
(fshead_beta_fscons a v @ 1) @
(fshead_beta_fscons a v)^ = 1
    refine (ap (fun p => p @ _) (concat_p1 _) @ _).A: Type
a: A
n: nat
v: FinSeq (nat_pred n.+1) A
fshead_beta_fscons a v @ (fshead_beta_fscons a v)^ = 1
    apply concat_pV.
  -A: Type
a: A
n: nat
v: FinSeq (nat_pred n.+1) A
i: Fin n
IHi: forall v : FinSeq (nat_pred n) A,
path_fscons' n 1 (fun j : Fin (nat_pred n) => 1) i = 1
fin_ind
  (fun (n : nat) (i : Fin n) =>
   forall v1 v2 : FinSeq (nat_pred n) A,
   (forall i0 : Fin (nat_pred n), v1 i0 = v2 i0) ->
   fscons' n a v1 i = fscons' n a v2 i)
  (fun (n : nat) (v1 v2 : FinSeq (nat_pred n.+1) A)
     (_ : forall i : Fin (nat_pred n.+1), v1 i = v2 i)
   =>
   (fshead_beta_fscons a v1 @ 1) @
   (fshead_beta_fscons a v2)^)
  (fun (n : nat) (i : Fin n)
     (_ : forall v1 v2 : FinSeq (nat_pred n) A,
          (forall i0 : Fin (nat_pred n), v1 i0 = v2 i0) ->
          fscons' n a v1 i = fscons' n a v2 i)
     (v1 v2 : FinSeq (nat_pred n.+1) A)
     (q : forall i0 : Fin (nat_pred n.+1),
          v1 i0 = v2 i0) =>
   (fstail'_beta_fscons' n.+1 a v1 i @ q i) @
   (fstail'_beta_fscons' n.+1 a v2 i)^) (fsucc i) v v
  (fun j : Fin (nat_pred n.+1) => 1) = 1 rewrite fin_ind_beta_fsucc.A: Type
a: A
n: nat
v: FinSeq (nat_pred n.+1) A
i: Fin n
IHi: forall v : FinSeq (nat_pred n) A,
path_fscons' n 1 (fun j : Fin (nat_pred n) => 1) i = 1
(fstail'_beta_fscons' n.+1 a v i @ 1) @
(fstail'_beta_fscons' n.+1 a v i)^ = 1
    refine (ap (fun p => p @ _) (concat_p1 _) @ _).A: Type
a: A
n: nat
v: FinSeq (nat_pred n.+1) A
i: Fin n
IHi: forall v : FinSeq (nat_pred n) A,
path_fscons' n 1 (fun j : Fin (nat_pred n) => 1) i = 1
fstail'_beta_fscons' n.+1 a v i @
(fstail'_beta_fscons' n.+1 a v i)^ = 1
    apply concat_pV.
Qed.

Definition path_fscons `{Funext} {A} {n} {a1 a2 : A} (p : a1 = a2)
  {v1 v2 : FinSeq n A} (q : v1 = v2)
  : fscons a1 v1 = fscons a2 v2.H: Funext
A: Type
n: nat
a1, a2: A
p: a1 = a2
v1, v2: FinSeq n A
q: v1 = v2
fscons a1 v1 = fscons a2 v2
Proof.H: Funext
A: Type
n: nat
a1, a2: A
p: a1 = a2
v1, v2: FinSeq n A
q: v1 = v2
fscons a1 v1 = fscons a2 v2
  funext i.H: Funext
A: Type
n: nat
a1, a2: A
p: a1 = a2
v1, v2: FinSeq n A
q: v1 = v2
i: Fin n.+1
fscons a1 v1 i = fscons a2 v2 i apply path_fscons'.H: Funext
A: Type
n: nat
a1, a2: A
p: a1 = a2
v1, v2: FinSeq n A
q: v1 = v2
i: Fin n.+1
a1 = a2
H: Funext
A: Type
n: nat
a1, a2: A
p: a1 = a2
v1, v2: FinSeq n A
q: v1 = v2
i: Fin n.+1
forall i : Fin (nat_pred n.+1), v1 i = v2 i
  -H: Funext
A: Type
n: nat
a1, a2: A
p: a1 = a2
v1, v2: FinSeq n A
q: v1 = v2
i: Fin n.+1
a1 = a2 assumption.
  -H: Funext
A: Type
n: nat
a1, a2: A
p: a1 = a2
v1, v2: FinSeq n A
q: v1 = v2
i: Fin n.+1
forall i : Fin (nat_pred n.+1), v1 i = v2 i intro j.H: Funext
A: Type
n: nat
a1, a2: A
p: a1 = a2
v1, v2: FinSeq n A
q: v1 = v2
i: Fin n.+1
j: Fin (nat_pred n.+1)
v1 j = v2 j exact (apD10 q j).
Defined.

Lemma path_fscons_beta `{Funext} {A} {n} (a : A) (v : FinSeq n A)
  : path_fscons (idpath a) (idpath v) = idpath.H: Funext
A: Type
n: nat
a: A
v: FinSeq n A
path_fscons 1 1 = 1
Proof.H: Funext
A: Type
n: nat
a: A
v: FinSeq n A
path_fscons 1 1 = 1
  refine (ap (path_forall _ _) _ @ eta_path_forall _ _ _).H: Funext
A: Type
n: nat
a: A
v: FinSeq n A
(fun i : Fin n.+1 =>
 path_fscons' n.+1 1
   (fun j : Fin (nat_pred n.+1) => apD10 1 j) i) =
apD10 1
  funext i.H: Funext
A: Type
n: nat
a: A
v: FinSeq n A
i: Fin n.+1
path_fscons' n.+1 1
  (fun j : Fin (nat_pred n.+1) => apD10 1 j) i =
apD10 1 i exact (path_fscons'_beta n.+1 a v i).
Defined.

(** The lemmas [path_expand_fscons_fscons'] and [path_expand_fscons_fscons]
    identify [path_expand_fscons'] with [path_fscons'] and
    [path_expand_fscons] with [path_fscons]. *)

Lemma path_expand_fscons_fscons' {A : Type} (n : nat)
  (N : n > 0) (a : A) (v : FinSeq (nat_pred n) A) (i : Fin n)
  : path_expand_fscons' n i N (fscons' n a v) =
    path_fscons' n (fshead'_beta_fscons' n N a v) (fstail'_beta_fscons' n a v) i.A: Type
n: nat
N: n > 0
a: A
v: FinSeq (nat_pred n) A
i: Fin n
path_expand_fscons' n i N (fscons' n a v) =
path_fscons' n (fshead'_beta_fscons' n N a v)
  (fstail'_beta_fscons' n a v) i
Proof.A: Type
n: nat
N: n > 0
a: A
v: FinSeq (nat_pred n) A
i: Fin n
path_expand_fscons' n i N (fscons' n a v) =
path_fscons' n (fshead'_beta_fscons' n N a v)
  (fstail'_beta_fscons' n a v) i
  induction i using fin_ind; unfold path_fscons', path_expand_fscons'.A: Type
n: nat
N: n.+1 > 0
a: A
v: FinSeq (nat_pred n.+1) A
fin_ind
  (fun (n : nat) (i : Fin n) =>
   forall (N : n > 0) (v : FinSeq n A),
   fscons' n (fshead' n N v) (fstail' n v) i = v i)
  (fun (n : nat) (_ : n.+1 > 0) (v : FinSeq n.+1 A) =>
   fshead_beta_fscons (v fin_zero) (fstail' n.+1 v))
  (fun (n : nat) (i : Fin n)
     (_ : forall (N : n > 0) (v : FinSeq n A),
          fscons' n (fshead' n N v) (fstail' n v) i =
          v i) (_ : n.+1 > 0) (v : FinSeq n.+1 A) =>
   fstail'_beta_fscons' n.+1 (fshead v) (fstail v) i)
  fin_zero N (fscons' n.+1 a v) =
fin_ind
  (fun (n0 : nat) (i : Fin n0) =>
   forall v1 v2 : FinSeq (nat_pred n0) A,
   (forall i0 : Fin (nat_pred n0), v1 i0 = v2 i0) ->
   fscons' n0 (fshead' n.+1 N (fscons' n.+1 a v)) v1 i =
   fscons' n0 a v2 i)
  (fun (n0 : nat) (v1 v2 : FinSeq (nat_pred n0.+1) A)
     (_ : forall i : Fin (nat_pred n0.+1), v1 i = v2 i)
   =>
   (fshead_beta_fscons
      (fshead' n.+1 N (fscons' n.+1 a v)) v1 @
    fshead'_beta_fscons' n.+1 N a v) @
   (fshead_beta_fscons a v2)^)
  (fun (n0 : nat) (i : Fin n0)
     (_ : forall v1 v2 : FinSeq (nat_pred n0) A,
          (forall i0 : Fin (nat_pred n0),
           v1 i0 = v2 i0) ->
          fscons' n0
            (fshead' n.+1 N (fscons' n.+1 a v)) v1 i =
          fscons' n0 a v2 i)
     (v1 v2 : FinSeq (nat_pred n0.+1) A)
     (q : forall i0 : Fin (nat_pred n0.+1),
          v1 i0 = v2 i0) =>
   (fstail'_beta_fscons' n0.+1
      (fshead' n.+1 N (fscons' n.+1 a v)) v1 i @ q i) @
   (fstail'_beta_fscons' n0.+1 a v2 i)^) fin_zero
  (fstail' n.+1 (fscons' n.+1 a v)) v
  (fstail'_beta_fscons' n.+1 a v)
A: Type
n: nat
N: n.+1 > 0
a: A
v: FinSeq (nat_pred n.+1) A
i: Fin n
IHi: forall (N : n > 0) (v : FinSeq (nat_pred n) A),
path_expand_fscons' n i N (fscons' n a v) =
path_fscons' n (fshead'_beta_fscons' n N a v) (fstail'_beta_fscons' n a v) i
fin_ind
  (fun (n : nat) (i : Fin n) =>
   forall (N : n > 0) (v : FinSeq n A),
   fscons' n (fshead' n N v) (fstail' n v) i = v i)
  (fun (n : nat) (_ : n.+1 > 0) (v : FinSeq n.+1 A) =>
   fshead_beta_fscons (v fin_zero) (fstail' n.+1 v))
  (fun (n : nat) (i : Fin n)
     (_ : forall (N : n > 0) (v : FinSeq n A),
          fscons' n (fshead' n N v) (fstail' n v) i =
          v i) (_ : n.+1 > 0) (v : FinSeq n.+1 A) =>
   fstail'_beta_fscons' n.+1 (fshead v) (fstail v) i)
  (fsucc i) N (fscons' n.+1 a v) =
fin_ind
  (fun (n0 : nat) (i : Fin n0) =>
   forall v1 v2 : FinSeq (nat_pred n0) A,
   (forall i0 : Fin (nat_pred n0), v1 i0 = v2 i0) ->
   fscons' n0 (fshead' n.+1 N (fscons' n.+1 a v)) v1 i =
   fscons' n0 a v2 i)
  (fun (n0 : nat) (v1 v2 : FinSeq (nat_pred n0.+1) A)
     (_ : forall i : Fin (nat_pred n0.+1), v1 i = v2 i)
   =>
   (fshead_beta_fscons
      (fshead' n.+1 N (fscons' n.+1 a v)) v1 @
    fshead'_beta_fscons' n.+1 N a v) @
   (fshead_beta_fscons a v2)^)
  (fun (n0 : nat) (i : Fin n0)
     (_ : forall v1 v2 : FinSeq (nat_pred n0) A,
          (forall i0 : Fin (nat_pred n0),
           v1 i0 = v2 i0) ->
          fscons' n0
            (fshead' n.+1 N (fscons' n.+1 a v)) v1 i =
          fscons' n0 a v2 i)
     (v1 v2 : FinSeq (nat_pred n0.+1) A)
     (q : forall i0 : Fin (nat_pred n0.+1),
          v1 i0 = v2 i0) =>
   (fstail'_beta_fscons' n0.+1
      (fshead' n.+1 N (fscons' n.+1 a v)) v1 i @ q i) @
   (fstail'_beta_fscons' n0.+1 a v2 i)^) (fsucc i)
  (fstail' n.+1 (fscons' n.+1 a v)) v
  (fstail'_beta_fscons' n.+1 a v)
  -A: Type
n: nat
N: n.+1 > 0
a: A
v: FinSeq (nat_pred n.+1) A
fin_ind
  (fun (n : nat) (i : Fin n) =>
   forall (N : n > 0) (v : FinSeq n A),
   fscons' n (fshead' n N v) (fstail' n v) i = v i)
  (fun (n : nat) (_ : n.+1 > 0) (v : FinSeq n.+1 A) =>
   fshead_beta_fscons (v fin_zero) (fstail' n.+1 v))
  (fun (n : nat) (i : Fin n)
     (_ : forall (N : n > 0) (v : FinSeq n A),
          fscons' n (fshead' n N v) (fstail' n v) i =
          v i) (_ : n.+1 > 0) (v : FinSeq n.+1 A) =>
   fstail'_beta_fscons' n.+1 (fshead v) (fstail v) i)
  fin_zero N (fscons' n.+1 a v) =
fin_ind
  (fun (n0 : nat) (i : Fin n0) =>
   forall v1 v2 : FinSeq (nat_pred n0) A,
   (forall i0 : Fin (nat_pred n0), v1 i0 = v2 i0) ->
   fscons' n0 (fshead' n.+1 N (fscons' n.+1 a v)) v1 i =
   fscons' n0 a v2 i)
  (fun (n0 : nat) (v1 v2 : FinSeq (nat_pred n0.+1) A)
     (_ : forall i : Fin (nat_pred n0.+1), v1 i = v2 i)
   =>
   (fshead_beta_fscons
      (fshead' n.+1 N (fscons' n.+1 a v)) v1 @
    fshead'_beta_fscons' n.+1 N a v) @
   (fshead_beta_fscons a v2)^)
  (fun (n0 : nat) (i : Fin n0)
     (_ : forall v1 v2 : FinSeq (nat_pred n0) A,
          (forall i0 : Fin (nat_pred n0),
           v1 i0 = v2 i0) ->
          fscons' n0
            (fshead' n.+1 N (fscons' n.+1 a v)) v1 i =
          fscons' n0 a v2 i)
     (v1 v2 : FinSeq (nat_pred n0.+1) A)
     (q : forall i0 : Fin (nat_pred n0.+1),
          v1 i0 = v2 i0) =>
   (fstail'_beta_fscons' n0.+1
      (fshead' n.+1 N (fscons' n.+1 a v)) v1 i @ q i) @
   (fstail'_beta_fscons' n0.+1 a v2 i)^) fin_zero
  (fstail' n.+1 (fscons' n.+1 a v)) v
  (fstail'_beta_fscons' n.+1 a v) do 2 rewrite fin_ind_beta_zero.A: Type
n: nat
N: n.+1 > 0
a: A
v: FinSeq (nat_pred n.+1) A
fshead_beta_fscons (fscons' n.+1 a v fin_zero)
  (fstail' n.+1 (fscons' n.+1 a v)) =
(fshead_beta_fscons
   (fshead' n.+1 N (fscons' n.+1 a v))
   (fstail' n.+1 (fscons' n.+1 a v)) @
 fshead'_beta_fscons' n.+1 N a v) @
(fshead_beta_fscons a v)^
    refine (_ @ concat_p_pp _ _ _).A: Type
n: nat
N: n.+1 > 0
a: A
v: FinSeq (nat_pred n.+1) A
fshead_beta_fscons (fscons' n.+1 a v fin_zero)
  (fstail' n.+1 (fscons' n.+1 a v)) =
fshead_beta_fscons (fshead' n.+1 N (fscons' n.+1 a v))
  (fstail' n.+1 (fscons' n.+1 a v)) @
(fshead'_beta_fscons' n.+1 N a v @
 (fshead_beta_fscons a v)^)
    refine (_ @ (ap (fun p => _ @ p) (concat_pV _))^).A: Type
n: nat
N: n.+1 > 0
a: A
v: FinSeq (nat_pred n.+1) A
fshead_beta_fscons (fscons' n.+1 a v fin_zero)
  (fstail' n.+1 (fscons' n.+1 a v)) =
fshead_beta_fscons (fshead' n.+1 N (fscons' n.+1 a v))
  (fstail' n.+1 (fscons' n.+1 a v)) @ 1
    exact (concat_p1 _)^.
  -A: Type
n: nat
N: n.+1 > 0
a: A
v: FinSeq (nat_pred n.+1) A
i: Fin n
IHi: forall (N : n > 0) (v : FinSeq (nat_pred n) A),
path_expand_fscons' n i N (fscons' n a v) =
path_fscons' n (fshead'_beta_fscons' n N a v) (fstail'_beta_fscons' n a v) i
fin_ind
  (fun (n : nat) (i : Fin n) =>
   forall (N : n > 0) (v : FinSeq n A),
   fscons' n (fshead' n N v) (fstail' n v) i = v i)
  (fun (n : nat) (_ : n.+1 > 0) (v : FinSeq n.+1 A) =>
   fshead_beta_fscons (v fin_zero) (fstail' n.+1 v))
  (fun (n : nat) (i : Fin n)
     (_ : forall (N : n > 0) (v : FinSeq n A),
          fscons' n (fshead' n N v) (fstail' n v) i =
          v i) (_ : n.+1 > 0) (v : FinSeq n.+1 A) =>
   fstail'_beta_fscons' n.+1 (fshead v) (fstail v) i)
  (fsucc i) N (fscons' n.+1 a v) =
fin_ind
  (fun (n0 : nat) (i : Fin n0) =>
   forall v1 v2 : FinSeq (nat_pred n0) A,
   (forall i0 : Fin (nat_pred n0), v1 i0 = v2 i0) ->
   fscons' n0 (fshead' n.+1 N (fscons' n.+1 a v)) v1 i =
   fscons' n0 a v2 i)
  (fun (n0 : nat) (v1 v2 : FinSeq (nat_pred n0.+1) A)
     (_ : forall i : Fin (nat_pred n0.+1), v1 i = v2 i)
   =>
   (fshead_beta_fscons
      (fshead' n.+1 N (fscons' n.+1 a v)) v1 @
    fshead'_beta_fscons' n.+1 N a v) @
   (fshead_beta_fscons a v2)^)
  (fun (n0 : nat) (i : Fin n0)
     (_ : forall v1 v2 : FinSeq (nat_pred n0) A,
          (forall i0 : Fin (nat_pred n0),
           v1 i0 = v2 i0) ->
          fscons' n0
            (fshead' n.+1 N (fscons' n.+1 a v)) v1 i =
          fscons' n0 a v2 i)
     (v1 v2 : FinSeq (nat_pred n0.+1) A)
     (q : forall i0 : Fin (nat_pred n0.+1),
          v1 i0 = v2 i0) =>
   (fstail'_beta_fscons' n0.+1
      (fshead' n.+1 N (fscons' n.+1 a v)) v1 i @ q i) @
   (fstail'_beta_fscons' n0.+1 a v2 i)^) (fsucc i)
  (fstail' n.+1 (fscons' n.+1 a v)) v
  (fstail'_beta_fscons' n.+1 a v) do 2 rewrite fin_ind_beta_fsucc.A: Type
n: nat
N: n.+1 > 0
a: A
v: FinSeq (nat_pred n.+1) A
i: Fin n
IHi: forall (N : n > 0) (v : FinSeq (nat_pred n) A),
path_expand_fscons' n i N (fscons' n a v) =
path_fscons' n (fshead'_beta_fscons' n N a v) (fstail'_beta_fscons' n a v) i
fstail'_beta_fscons' n.+1 (fshead (fscons' n.+1 a v))
  (fstail (fscons' n.+1 a v)) i =
(fstail'_beta_fscons' n.+1
   (fshead' n.+1 N (fscons' n.+1 a v))
   (fstail' n.+1 (fscons' n.+1 a v)) i @
 fstail'_beta_fscons' n.+1 a v i) @
(fstail'_beta_fscons' n.+1 a v i)^
    refine (_ @ concat_p_pp _ _ _).A: Type
n: nat
N: n.+1 > 0
a: A
v: FinSeq (nat_pred n.+1) A
i: Fin n
IHi: forall (N : n > 0) (v : FinSeq (nat_pred n) A),
path_expand_fscons' n i N (fscons' n a v) =
path_fscons' n (fshead'_beta_fscons' n N a v) (fstail'_beta_fscons' n a v) i
fstail'_beta_fscons' n.+1 (fshead (fscons' n.+1 a v))
  (fstail (fscons' n.+1 a v)) i =
fstail'_beta_fscons' n.+1
  (fshead' n.+1 N (fscons' n.+1 a v))
  (fstail' n.+1 (fscons' n.+1 a v)) i @
(fstail'_beta_fscons' n.+1 a v i @
 (fstail'_beta_fscons' n.+1 a v i)^)
    refine (_ @ (ap (fun p => _ @ p) (concat_pV _))^).A: Type
n: nat
N: n.+1 > 0
a: A
v: FinSeq (nat_pred n.+1) A
i: Fin n
IHi: forall (N : n > 0) (v : FinSeq (nat_pred n) A),
path_expand_fscons' n i N (fscons' n a v) =
path_fscons' n (fshead'_beta_fscons' n N a v) (fstail'_beta_fscons' n a v) i
fstail'_beta_fscons' n.+1 (fshead (fscons' n.+1 a v))
  (fstail (fscons' n.+1 a v)) i =
fstail'_beta_fscons' n.+1
  (fshead' n.+1 N (fscons' n.+1 a v))
  (fstail' n.+1 (fscons' n.+1 a v)) i @ 1
    exact (concat_p1 _)^.
Qed.

Lemma path_expand_fscons_fscons `{Funext}
  {A : Type} {n : nat} (a : A) (v : FinSeq n A)
  : path_expand_fscons (fscons a v) =
    path_fscons (fshead_beta_fscons a v) (fstail_beta_fscons a v).H: Funext
A: Type
n: nat
a: A
v: FinSeq n A
path_expand_fscons (fscons a v) =
path_fscons (fshead_beta_fscons a v)
  (fstail_beta_fscons a v)
Proof.H: Funext
A: Type
n: nat
a: A
v: FinSeq n A
path_expand_fscons (fscons a v) =
path_fscons (fshead_beta_fscons a v)
  (fstail_beta_fscons a v)
  refine (ap (path_forall _ _) _).H: Funext
A: Type
n: nat
a: A
v: FinSeq n A
(fun i : Fin n.+1 =>
 path_expand_fscons' n.+1 i (leq_add_r 1 n)
   (fscons a v)) =
(fun i : Fin n.+1 =>
 path_fscons' n.+1 (fshead_beta_fscons a v)
   (fun j : Fin (nat_pred n.+1) =>
    apD10 (fstail_beta_fscons a v) j) i)
  funext i.H: Funext
A: Type
n: nat
a: A
v: FinSeq n A
i: Fin n.+1
path_expand_fscons' n.+1 i (leq_add_r 1 n)
  (fscons a v) =
path_fscons' n.+1 (fshead_beta_fscons a v)
  (fun j : Fin (nat_pred n.+1) =>
   apD10 (fstail_beta_fscons a v) j) i
  pose (p := eisretr apD10 (fstail'_beta_fscons' n.+1 a v)).H: Funext
A: Type
n: nat
a: A
v: FinSeq n A
i: Fin n.+1
p:= eisretr apD10 (fstail'_beta_fscons' n.+1 a v): (apD10 o apD10^-1) (fstail'_beta_fscons' n.+1 a v) =
idmap (fstail'_beta_fscons' n.+1 a v)
path_expand_fscons' n.+1 i (leq_add_r 1 n)
  (fscons a v) =
path_fscons' n.+1 (fshead_beta_fscons a v)
  (fun j : Fin (nat_pred n.+1) =>
   apD10 (fstail_beta_fscons a v) j) i
  refine (_ @ (ap (fun f => _ f i) p)^).H: Funext
A: Type
n: nat
a: A
v: FinSeq n A
i: Fin n.+1
p:= eisretr apD10 (fstail'_beta_fscons' n.+1 a v): (apD10 o apD10^-1) (fstail'_beta_fscons' n.+1 a v) =
idmap (fstail'_beta_fscons' n.+1 a v)
path_expand_fscons' n.+1 i (leq_add_r 1 n)
  (fscons a v) =
path_fscons' n.+1 (fshead_beta_fscons a v)
  (fstail'_beta_fscons' n.+1 a v) i
  exact (path_expand_fscons_fscons' n.+1 _ a v i).
Defined.

(** The induction principle for finite sequence, [finseq_ind].
    Note that it uses funext and does not compute. *)

Lemma finseq_ind `{Funext} {A : Type} (P : forall n, FinSeq n A -> Type)
  (z : P 0 fsnil) (s : forall n a (v : FinSeq n A), P n v -> P n.+1 (fscons a v))
  {n : nat} (v : FinSeq n A)
  : P n v.H: Funext
A: Type
P: forall n : nat, FinSeq n A -> Type
z: P 0 fsnil
s: forall (n : nat) (a : A) (v : FinSeq n A),
P n v -> P n.+1 (fscons a v)
n: nat
v: FinSeq n A
P n v
Proof.H: Funext
A: Type
P: forall n : nat, FinSeq n A -> Type
z: P 0 fsnil
s: forall (n : nat) (a : A) (v : FinSeq n A),
P n v -> P n.+1 (fscons a v)
n: nat
v: FinSeq n A
P n v
  induction n.H: Funext
A: Type
P: forall n : nat, FinSeq n A -> Type
z: P 0 fsnil
s: forall (n : nat) (a : A) (v : FinSeq n A),
P n v -> P n.+1 (fscons a v)
v: FinSeq 0 A
P 0 v
H: Funext
A: Type
P: forall n : nat, FinSeq n A -> Type
z: P 0 fsnil
s: forall (n : nat) (a : A) (v : FinSeq n A),
P n v -> P n.+1 (fscons a v)
n: nat
v: FinSeq n.+1 A
IHn: forall v : FinSeq n A, P n v
P n.+1 v
  -H: Funext
A: Type
P: forall n : nat, FinSeq n A -> Type
z: P 0 fsnil
s: forall (n : nat) (a : A) (v : FinSeq n A),
P n v -> P n.+1 (fscons a v)
v: FinSeq 0 A
P 0 v exact (transport (P 0) (path_fsnil v) z).
  -H: Funext
A: Type
P: forall n : nat, FinSeq n A -> Type
z: P 0 fsnil
s: forall (n : nat) (a : A) (v : FinSeq n A),
P n v -> P n.+1 (fscons a v)
n: nat
v: FinSeq n.+1 A
IHn: forall v : FinSeq n A, P n v
P n.+1 v refine (transport (P n.+1) (path_expand_fscons v) _).H: Funext
A: Type
P: forall n : nat, FinSeq n A -> Type
z: P 0 fsnil
s: forall (n : nat) (a : A) (v : FinSeq n A),
P n v -> P n.+1 (fscons a v)
n: nat
v: FinSeq n.+1 A
IHn: forall v : FinSeq n A, P n v
P n.+1 (fscons (fshead v) (fstail v))
    apply s.H: Funext
A: Type
P: forall n : nat, FinSeq n A -> Type
z: P 0 fsnil
s: forall (n : nat) (a : A) (v : FinSeq n A),
P n v -> P n.+1 (fscons a v)
n: nat
v: FinSeq n.+1 A
IHn: forall v : FinSeq n A, P n v
P n (fstail v) apply IHn.
Defined.

Lemma finseq_ind_beta_fsnil `{Funext} {A : Type}
  (P : forall n, FinSeq n A -> Type) (z : P 0 fsnil)
  (s : forall (n : nat) (a : A) (v : FinSeq n A), P n v -> P n.+1 (fscons a v))
  : finseq_ind P z s fsnil = z.H: Funext
A: Type
P: forall n : nat, FinSeq n A -> Type
z: P 0 fsnil
s: forall (n : nat) (a : A) (v : FinSeq n A),
P n v -> P n.+1 (fscons a v)
finseq_ind P z s fsnil = z
Proof.H: Funext
A: Type
P: forall n : nat, FinSeq n A -> Type
z: P 0 fsnil
s: forall (n : nat) (a : A) (v : FinSeq n A),
P n v -> P n.+1 (fscons a v)
finseq_ind P z s fsnil = z
  exact (ap (fun x => _ x z) (hset_path2 1 (path_fsnil fsnil)))^.
Defined.

Lemma finseq_ind_beta_fscons `{Funext} {A : Type}
  (P : forall n, FinSeq n A -> Type) (z : P 0 fsnil)
  (s : forall (n : nat) (a : A) (v : FinSeq n A), P n v -> P n.+1 (fscons a v))
  {n : nat} (a : A) (v : FinSeq n A)
  : finseq_ind P z s (fscons a v) = s n a v (finseq_ind P z s v).H: Funext
A: Type
P: forall n : nat, FinSeq n A -> Type
z: P 0 fsnil
s: forall (n : nat) (a : A) (v : FinSeq n A),
P n v -> P n.+1 (fscons a v)
n: nat
a: A
v: FinSeq n A
finseq_ind P z s (fscons a v) =
s n a v (finseq_ind P z s v)
Proof.H: Funext
A: Type
P: forall n : nat, FinSeq n A -> Type
z: P 0 fsnil
s: forall (n : nat) (a : A) (v : FinSeq n A),
P n v -> P n.+1 (fscons a v)
n: nat
a: A
v: FinSeq n A
finseq_ind P z s (fscons a v) =
s n a v (finseq_ind P z s v)
  simpl.H: Funext
A: Type
P: forall n : nat, FinSeq n A -> Type
z: P 0 fsnil
s: forall (n : nat) (a : A) (v : FinSeq n A),
P n v -> P n.+1 (fscons a v)
n: nat
a: A
v: FinSeq n A
transport (P n.+1) (path_expand_fscons (fscons a v))
  (s n (fshead (fscons a v)) (fstail (fscons a v))
     (finseq_ind P z s (fstail (fscons a v)))) =
s n a v (finseq_ind P z s v)
  induction (path_expand_fscons_fscons a v)^.H: Funext
A: Type
P: forall n : nat, FinSeq n A -> Type
z: P 0 fsnil
s: forall (n : nat) (a : A) (v : FinSeq n A),
P n v -> P n.+1 (fscons a v)
n: nat
a: A
v: FinSeq n A
transport (P n.+1)
  (path_fscons (fshead_beta_fscons a v)
     (fstail_beta_fscons a v))
  (s n (fshead (fscons a v)) (fstail (fscons a v))
     (finseq_ind P z s (fstail (fscons a v)))) =
s n a v (finseq_ind P z s v)
  set (p1 := fshead_beta_fscons a v).H: Funext
A: Type
P: forall n : nat, FinSeq n A -> Type
z: P 0 fsnil
s: forall (n : nat) (a : A) (v : FinSeq n A),
P n v -> P n.+1 (fscons a v)
n: nat
a: A
v: FinSeq n A
p1:= fshead_beta_fscons a v: fshead (fscons a v) = a
transport (P n.+1)
  (path_fscons p1 (fstail_beta_fscons a v))
  (s n (fshead (fscons a v)) (fstail (fscons a v))
     (finseq_ind P z s (fstail (fscons a v)))) =
s n a v (finseq_ind P z s v)
  set (p2 := fstail_beta_fscons a v).H: Funext
A: Type
P: forall n : nat, FinSeq n A -> Type
z: P 0 fsnil
s: forall (n : nat) (a : A) (v : FinSeq n A),
P n v -> P n.+1 (fscons a v)
n: nat
a: A
v: FinSeq n A
p1:= fshead_beta_fscons a v: fshead (fscons a v) = a
p2:= fstail_beta_fscons a v: fstail (fscons a v) = v
transport (P n.+1) (path_fscons p1 p2)
  (s n (fshead (fscons a v)) (fstail (fscons a v))
     (finseq_ind P z s (fstail (fscons a v)))) =
s n a v (finseq_ind P z s v)
  induction p1, p2.H: Funext
A: Type
P: forall n : nat, FinSeq n A -> Type
z: P 0 fsnil
s: forall (n : nat) (a : A) (v : FinSeq n A),
P n v -> P n.+1 (fscons a v)
n: nat
a: A
v: FinSeq n A
transport (P n.+1) (path_fscons 1 1)
  (s n (fshead (fscons a (fstail (fscons a v))))
     (fstail (fscons a v))
     (finseq_ind P z s (fstail (fscons a v)))) =
s n (fshead (fscons a (fstail (fscons a v))))
  (fstail (fscons a v))
  (finseq_ind P z s (fstail (fscons a v)))
  exact (ap (fun p => transport _ p _) (path_fscons_beta _ _)).
Defined.