(** * Types of Sequences [nat -> X] *)

Require Import Basics Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Spaces.Nat.Core.

Local Open Scope nat_scope.
Local Open Scope type_scope.

(** ** Operations on sequences *)

(** Shift of a sequence by 1 to the left. *)
Definition seq_tail {X : Type} (u : nat -> X) : (nat -> X) := u o S.

(** Add a term to the start of a sequence. *)
Definition seq_cons {X : Type} : X -> (nat -> X) -> (nat -> X).
X: Type
X -> (nat -> X) -> nat -> X
Proof.
X: Type
X -> (nat -> X) -> nat -> X
  intros x u [|n].
X: Type
x: X
u: nat -> X
X
X: Type
x: X
u: nat -> X
n: nat
X
  -
X: Type
x: X
u: nat -> X
X exact x.
  -
X: Type
x: X
u: nat -> X
n: nat
X exact (u n).
Defined.

Definition seq_cons_head_tail {X : Type} (u : nat -> X)
  : seq_cons (u 0) (seq_tail u) == u.
X: Type
u: nat -> X
seq_cons (u 0) (seq_tail u) == u
Proof.
X: Type
u: nat -> X
seq_cons (u 0) (seq_tail u) == u
  by intros [|n].
Defined.

Definition tail_cons {X : Type} (u : nat -> X) {x : X} : seq_tail (seq_cons x u) == u
  := fun _ => idpath.

(** ** Equivalence relations on sequences.  *)

(** For every [n : nat], we define a relation between two sequences that holds if and only if their first [n] terms are equal. *)
Definition seq_agree_lt {X : Type} (n : nat) (s t : nat -> X) : Type
  := forall (m : nat), m < n -> s m = t m.

(** [seq_agree_lt] has an equivalent inductive definition. We don't use this equivalence, but include it in case it is useful in future work. *)
Definition seq_agree_inductive {X : Type} (n : nat) (s t : nat -> X) : Type.
X: Type
n: nat
s, t: nat -> X
Type
Proof.
X: Type
n: nat
s, t: nat -> X
Type
  induction n in s, t |- *.
X: Type
s, t: nat -> X
Type
X: Type
n: nat
s, t: nat -> X
IHn: (nat -> X) -> (nat -> X) -> Type
Type
  -
X: Type
s, t: nat -> X
Type exact Unit.
  -
X: Type
n: nat
s, t: nat -> X
IHn: (nat -> X) -> (nat -> X) -> Type
Type exact ((s 0 = t 0) * (IHn (seq_tail s) (seq_tail t))).
Defined.

Definition seq_agree_inductive_seq_agree_lt {X : Type} {n : nat}
  {s t : nat -> X} (h : seq_agree_lt n s t)
  : seq_agree_inductive n s t.
X: Type
n: nat
s, t: nat -> X
h: seq_agree_lt n s t
seq_agree_inductive n s t
Proof.
X: Type
n: nat
s, t: nat -> X
h: seq_agree_lt n s t
seq_agree_inductive n s t
  induction n in s, t, h |- *.
X: Type
s, t: nat -> X
h: seq_agree_lt 0 s t
seq_agree_inductive 0 s t
X: Type
n: nat
s, t: nat -> X
h: seq_agree_lt n.+1 s t
IHn: forall s t : nat -> X, seq_agree_lt n s t -> seq_agree_inductive n s t
seq_agree_inductive n.+1 s t
  -
X: Type
s, t: nat -> X
h: seq_agree_lt 0 s t
seq_agree_inductive 0 s t exact tt.
  -
X: Type
n: nat
s, t: nat -> X
h: seq_agree_lt n.+1 s t
IHn: forall s t : nat -> X, seq_agree_lt n s t -> seq_agree_inductive n s t
seq_agree_inductive n.+1 s t simpl.
X: Type
n: nat
s, t: nat -> X
h: seq_agree_lt n.+1 s t
IHn: forall s t : nat -> X, seq_agree_lt n s t -> seq_agree_inductive n s t
(s 0 = t 0) *
seq_agree_inductive n (seq_tail s) (seq_tail t)
    exact (h 0 _, IHn _ _ (fun m hm => h m.+1 (_ hm))).
Defined.

Definition seq_agree_lt_seq_agree_inductive {X : Type} {n : nat}
  {s t : nat -> X} (h : seq_agree_inductive n s t)
  : seq_agree_lt n s t.
X: Type
n: nat
s, t: nat -> X
h: seq_agree_inductive n s t
seq_agree_lt n s t
Proof.
X: Type
n: nat
s, t: nat -> X
h: seq_agree_inductive n s t
seq_agree_lt n s t
  intros m hm.
X: Type
n: nat
s, t: nat -> X
h: seq_agree_inductive n s t
m: nat
hm: m < n
s m = t m
  induction m in n, s, t, h, hm |- *.
X: Type
n: nat
s, t: nat -> X
h: seq_agree_inductive n s t
hm: 0 < n
s 0 = t 0
X: Type
n: nat
s, t: nat -> X
h: seq_agree_inductive n s t
m: nat
hm: m.+1 < n
IHm: forall (n : nat) (s t : nat -> X),
seq_agree_inductive n s t -> m < n -> s m = t m
s m.+1 = t m.+1
  -
X: Type
n: nat
s, t: nat -> X
h: seq_agree_inductive n s t
hm: 0 < n
s 0 = t 0 revert n hm h; napply gt_zero_ind; intros n h.
X: Type
s, t: nat -> X
n: nat
h: seq_agree_inductive n.+1 s t
s 0 = t 0
    exact (fst h).
  -
X: Type
n: nat
s, t: nat -> X
h: seq_agree_inductive n s t
m: nat
hm: m.+1 < n
IHm: forall (n : nat) (s t : nat -> X),
seq_agree_inductive n s t -> m < n -> s m = t m
s m.+1 = t m.+1 induction n.
X: Type
s, t: nat -> X
h: seq_agree_inductive 0 s t
m: nat
hm: m.+1 < 0
IHm: forall (n : nat) (s t : nat -> X),
seq_agree_inductive n s t -> m < n -> s m = t m
s m.+1 = t m.+1
X: Type
n: nat
s, t: nat -> X
h: seq_agree_inductive n.+1 s t
m: nat
hm: m.+1 < n.+1
IHm: forall (n : nat) (s t : nat -> X),
seq_agree_inductive n s t -> m < n -> s m = t m
IHn: seq_agree_inductive n s t -> m.+1 < n -> s m.+1 = t m.+1
s m.+1 = t m.+1
    +
X: Type
s, t: nat -> X
h: seq_agree_inductive 0 s t
m: nat
hm: m.+1 < 0
IHm: forall (n : nat) (s t : nat -> X),
seq_agree_inductive n s t -> m < n -> s m = t m
s m.+1 = t m.+1 contradiction (not_lt_zero_r _ hm).
    +
X: Type
n: nat
s, t: nat -> X
h: seq_agree_inductive n.+1 s t
m: nat
hm: m.+1 < n.+1
IHm: forall (n : nat) (s t : nat -> X),
seq_agree_inductive n s t -> m < n -> s m = t m
IHn: seq_agree_inductive n s t -> m.+1 < n -> s m.+1 = t m.+1
s m.+1 = t m.+1 exact (IHm _ (seq_tail s) (seq_tail t) (snd h) _).
Defined.

Definition seq_agree_lt_iff_seq_agree_inductive
  {X : Type} {n : nat} {s t : nat -> X}
  : seq_agree_lt n s t <-> seq_agree_inductive n s t
  := (fun h => seq_agree_inductive_seq_agree_lt h,
      fun h => seq_agree_lt_seq_agree_inductive h).