From Coq Require Import ZArith Rfunctions NaryFunctions Lia.
From mathcomp.ssreflect Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple.

Require Import MathComp.


Set Implicit Arguments.

Ltac flatten := repeat
  first[rewrite Nat.sub_1_r in *| rewrite<-plusE in *|rewrite<-minusE in *].
Ltac iomega := intros; flatten; (lia || apply/leP; lia).
Ltac iomega_le := (repeat move/leP=>?); iomega.

Notation nth_defaults := set_nth_default.
Lemma behead_rcons (T : Type) (s : seq T) (x : T) :
  s ≠ [::] → behead (rcons s x) = rcons (behead s) x.

Lemma behead_rev_take (T : Type) (s : seq T) (n : nat) :
  n ≤ size s → behead (rev (take n s)) = rev (take n.-1 s).

Section Defix1.

Variable T : Type.

Variable F : T → nat → T.

Fixpoint loop1 (n p : nat) (a : T) (s : seq T) {struct n} : seq T :=
  match n with
    | 0 ⇒ s
    | m.+1 ⇒ let c := F a p in loop1 m p.+1 c (c :: s)
  end.

Variable a0 : T.

Definition rec1down n := loop1 n 1 a0 [:: a0].

Definition rec1up n := rev (rec1down n).

Lemma size_loop1 n p a s : size (loop1 n p a s) = n + size s.

Lemma size_rec1down n : size (rec1down n) = n.+1.

Lemma size_rec1up n : size (rec1up n) = n.+1.

Variable d : T.

Lemma head_loop1S n s a p :
  head d s = a →
  head d (loop1 n.+1 p a s) = F (head d (loop1 n p a s)) (n+p).

Theorem head_loop1 (n p : nat) a s :
  head d s = a →
  head d (loop1 n p a s) = iteri n (fun i c ⇒ F c (i + p)) a.

Lemma head_rec1downS n :
  head d (rec1down n.+1) = F (head d (rec1down n)) n.+1.

Lemma nth_rec1up_last k : nth d (rec1up k) k = last d (rec1up k).

Lemma last_rec1up k : last d (rec1up k) = head d (loop1 k 1 a0 [:: a0]).

Lemma nth_rec1upS k :
  nth d (rec1up k.+1) k.+1 = F (nth d (rec1up k) k) k.+1.

Lemma loop1S_ex n p a s :
  ∃ c, loop1 n.+1 p a s = c :: (loop1 n p a s).

Lemma behead_rec1down n : behead (rec1down n.+1) = rec1down n.

Lemma nth_rec1downD d1 p q n :
  nth d1 (rec1down (p+q+n)) (p+q) = nth d1 (rec1down (p+n)) p.

Lemma nth_rec1downD_dflt2 d1 d2 p q n :
  nth d1 (rec1down (p+q+n)) (p+q) = nth d2 (rec1down (p+n)) p.

Lemma nth_rec1down_indep d1 d2 m1 m2 n :
  n ≤ m1 → n ≤ m2 →
  nth d1 (rec1down m1) (m1 - n) = nth d2 (rec1down m2) (m2 - n).

Lemma nth_rec1up_indep d1 d2 m1 m2 n :
  n ≤ m1 → n ≤ m2 →
  nth d1 (rec1up m1) n = nth d2 (rec1up m2) n.

Theorem nth_rec1up n k :
  nth d (rec1up n) k =
  if n < k then d
  else iteri k (fun i c ⇒ F c (i + 1)) a0.

Lemma rec1down_co0 n: nth d (rec1down n) n = a0.

Lemma rec1up_co0 n : nth d (rec1up n) 0 = a0.

End Defix1.

Section GenDefix1.

Variables A T : Type.

Variable F : A → nat → A.

Variable G : A → nat → T.

Fixpoint gloop1 (n p : nat) (a : A) (s : seq T) {struct n} : seq T :=
  match n with
    | 0 ⇒ s
    | m.+1 ⇒ let r := G a p in
              let p1 := p.+1 in
              let c := F a p1 in gloop1 m p1 c (r :: s)
  end.

Variable a0 : A.

Variable init : seq T.

Definition grec1down n :=
  if (n.+1 - size init) is n'.+1
    then gloop1 n'.+1 (size init) a0 (rev init)
    else rev (take n.+1 init).

Lemma grec1downE (n : nat) :
  grec1down n =
  if n ≥ size init
    then gloop1 (n - size init).+1 (size init) a0 (rev init)
    else rev (take n.+1 init).

Definition grec1up n := rev (grec1down n).

Lemma size_gloop1 n p a s : size (gloop1 n p a s) = n + size s.

Lemma size_grec1down n : size (grec1down n) = n.+1.

Lemma size_grec1up n : size (grec1up n) = n.+1.

Theorem grec1up_init n :
  n < size init →
  grec1up n = take n.+1 init.

Theorem last_grec1up (d : T) (n : nat) :
  size init ≤ n →
  last d (grec1up n) =
  head d (gloop1 (n - size init).+1 (size init) a0 (rev init)).

Theorem head_gloop1 (d : T) (n p : nat) (a : A) (s : seq T):
  head d (gloop1 n.+1 p a s) = G (iteri n (fun i c ⇒ F c (i + p).+1) a) (n + p).

Lemma gloop1S_ex n p a s :
  ∃ c, gloop1 n.+1 p a s = c :: (gloop1 n p a s).

Theorem behead_grec1down (n : nat) :
  behead (grec1down n.+1) = grec1down n.

Lemma nth_grec1downD d1 p q n:
  nth d1 (grec1down (p+q+n)) (p+q) = nth d1 (grec1down (p+n)) p.

Lemma nth_grec1downD_dflt2 d1 d2 p q n:
  nth d1 (grec1down (p+q+n)) (p+q) = nth d2 (grec1down (p+n)) p.

Theorem nth_grec1down_indep (d1 d2 : T) (m1 m2 n : nat) :
  n ≤ m1 → n ≤ m2 →
  nth d1 (grec1down m1) (m1 - n) = nth d2 (grec1down m2) (m2 - n).

Theorem nth_grec1up_indep (d1 d2 : T) (m1 m2 n : nat) :
  n ≤ m1 → n ≤ m2 →
  nth d1 (grec1up m1) n = nth d2 (grec1up m2) n.

Arguments nth_grec1up_indep [d1 d2 m1 m2 n] _ _.

Lemma nth_grec1up_last (d : T) k : nth d (grec1up k) k = last d (grec1up k).

Theorem nth_grec1up d n k :
  nth d (grec1up n) k =
  if n < k then d
  else
    if k < size init then nth d init k
    else G (iteri (k - size init) (fun i c ⇒ F c (i + size init).+1) a0) k.

Arguments nth_grec1up [d] n k.

End GenDefix1.

Section Defix2.

Variable T : Type.

Variable F : T → T → nat → T.

Fixpoint loop2 (n p : nat) (a b : T) (s : seq T) {struct n} : seq T :=
  match n with
    | 0 ⇒ s
    | m.+1 ⇒ let c := F a b p in loop2 m p.+1 b c (c :: s)
  end.

Variables a0 a1 : T.

Definition rec2down n :=
  if n is n'.+1 then (loop2 n' 2 a0 a1 [:: a1; a0]) else [:: a0].

Definition rec2up n := rev (rec2down n).

Lemma size_loop2 n p a b s : size (loop2 n p a b s) = n + size s.

Lemma size_rec2down n : size (rec2down n) = n.+1.

Lemma size_rec2up n : size (rec2up n) = n.+1.

Variable d : T.

Lemma head_loop2S n s a b p :
  hb d s = a → head d s = b →
  let s' := (loop2 n p a b s) in
  head d (loop2 n.+1 p a b s) = F (hb d s') (head d s') (n+p).

Lemma head_rec2downSS n :
  head d (rec2down n.+2) =
  F (hb d (rec2down n.+1)) (head d (rec2down n.+1)) n.+2.

Lemma behead_loop2 n s a b p : behead (loop2 n.+1 p a b s) = loop2 n p a b s.

Lemma behead_rec2down n : behead (rec2down n.+1) = rec2down n.


Lemma nth_rec2up_last k : nth d (rec2up k) k = last d (rec2up k).

Theorem last_rec2up k :
  last d (rec2up k.+1) = head d (loop2 k 2 a0 a1 [:: a1; a0]).

Lemma nth_rec2downSS' k :
  nth d (rec2down k.+2) 0 =
  F (nth d (rec2down k) 0) (nth d (rec2down k.+1) 0) k.+2.

Lemma nth_rec2upSS' k :
  nth d (rec2up k.+2) k.+2 =
  F (nth d (rec2up k) k) (nth d (rec2up k.+1) k.+1) k.+2.

Lemma nth_rec2downD d1 p q n :
  nth d1 (rec2down (p+q+n)) (p+q) = nth d1 (rec2down (p+n)) p.

Lemma nth_rec2downD_dflt2 d1 d2 p q n :
  nth d1 (rec2down (p+q+n)) (p+q) = nth d2 (rec2down (p+n)) p.

Lemma nth_rec2down_indep d1 d2 m1 m2 n : n ≤ m1 → n ≤ m2 →
  nth d1 (rec2down m1) (m1 - n) = nth d2 (rec2down m2) (m2 - n).

Lemma nth_rec2up_indep d1 d2 m1 m2 n : n ≤ m1 → n ≤ m2 →
  nth d1 (rec2up m1) n = nth d2 (rec2up m2) n.

End Defix2.

Section RecZ.


Definition fact_rec (a : Z) (n : nat) : Z := Z.mul a (Z.of_nat n).
Definition fact_seq := rec1up fact_rec 1%Z.

Theorem fact_seq_correct (d : Z) (n k : nat) :
  k ≤ n →
  nth d (fact_seq n) k = Z.of_nat (fact k).

Lemma size_fact_seq n : size (fact_seq n) = n.+1.

Definition falling_rec (p : Z) (a : Z) (n : nat) : Z :=
  (a × (p - (Z.of_nat n) + 1))%Z.
Definition falling_seq (p : Z) := rec1up (falling_rec p) 1%Z.

Theorem falling_seq_correct (d : Z) (p : Z) (n k : nat) :
  k ≤ n →
  nth d (falling_seq p n) k =
  \big[Z.mul/1%Z]_(0 ≤ i < k) (p - Z.of_nat i)%Z.

Lemma size_falling_seq p n : size (falling_seq p n) = n.+1.

End RecZ.

Section rec_proofs.
Variables (V T : Type).
Variable Rel : V → T → Prop.
Variables (dv : V) (dt : T).
Hypothesis H0 : Rel dv dt.
Local Notation RelP sv st := (∀ k : nat, Rel (nth dv sv k) (nth dt st k)) (only parsing).

Lemma grec1up_correct (A := seq V) Fi (F : A → nat → A) Gi (G : A → nat → V) ai a si s n :
  (∀ qi q m, RelP q qi → RelP (F q m) (Fi qi m)) →
  (∀ qi q m, RelP q qi → Rel (G q m) (Gi qi m)) →
  RelP a ai →
  RelP s si →
  size s = size si →
  RelP (grec1up F G a s n) (grec1up Fi Gi ai si n).

Lemma rec1up_correct fi f fi0 f0 n :
  (∀ ai a m, Rel a ai → Rel (f a m) (fi ai m)) →
  Rel f0 fi0 →
  RelP (rec1up f f0 n) (rec1up fi fi0 n).

Lemma rec2up_correct fi f fi0 f0 fi1 f1 n :
  (∀ ai bi a b m, Rel a ai → Rel b bi → Rel (f a b m) (fi ai bi m)) →
  Rel f0 fi0 →
  Rel f1 fi1 →
  RelP (rec2up f f0 f1 n) (rec2up fi fi0 fi1 n).

End rec_proofs.