From Coq Require Import Arith Lists.List Lia.
From hydras Require Import extEqualNat primRec.
From hydras Require Export Compat815 ssrnat_extracts.
Import PRNotations.
Import Nat.

Fixpoint sumToN (n : nat): nat :=
  match n with
    0 ⇒ 0
  | S p ⇒ S p + sumToN p
  end.

Lemma sumToN1 n : n ≤ sumToN n.

Lemma sumToN2 b a : a ≤ b → sumToN a ≤ sumToN b.

#[export] Instance sumToNIsPR : isPR 1 sumToN.

Definition cPair (a b : nat) := a + sumToN (a + b).

 Definition xPair a b := b + sumToN ( b + a).

 Lemma xPairDef a b : xPair a b = cPair b a.

#[export] Instance cPairIsPR : isPR 2 cPair.

Section CPair_Injectivity.

  Remark cPairInjHelp :
    ∀ a b c d : nat, cPair a b = cPair c d → a + b = c + d.

  Lemma cPairInj1 a b c d: cPair a b = cPair c d → a = c.

  Lemma cPairInj2 a b c d : cPair a b = cPair c d → b = d.

End CPair_Injectivity.

Section CPair_projections.


  Let searchXY (a : nat) :=
        boundedSearch (fun a y : nat ⇒ ltBool a (sumToN y.+1)) a.

  Definition cPairPi1 (a : nat) := a - sumToN (searchXY a).
  Definition cPairPi2 (a : nat) := searchXY a - cPairPi1 a.

Lemma cPairProjectionsHelp (a b: nat):
  b < sumToN a.+1 → sumToN a ≤ b → searchXY b = a.

Lemma cPairProjections a: cPair (cPairPi1 a) (cPairPi2 a) = a.

#[local] Instance searchXYIsPR : isPR 1 searchXY.

#[export] Instance cPairPi1IsPR : isPR 1 cPairPi1.

Lemma cPairProjections1 (a b : nat): cPairPi1 (cPair a b) = a.

Lemma cPairProjections2 (a b : nat): cPairPi2 (cPair a b) = b.

#[export] Instance cPairPi2IsPR : isPR 1 cPairPi2.

End CPair_projections.

Section CPair_Order.

  Lemma cPairLe1 (a b : nat) : a ≤ cPair a b.

  Lemma cPairLe1A (a : nat) : cPairPi1 a ≤ a.

  Lemma cPairLe2 (a b : nat) : b ≤ cPair a b.

  Lemma cPairLe2A (a: nat): cPairPi2 a ≤ a.

  Lemma cPairLe3 (a b c d : nat): a ≤ b → c ≤ d → cPair a c ≤ cPair b d.

  Lemma cPairLt1 (a b : nat): a < cPair a (S b).

  Lemma cPairLt2 (a b : nat): b < cPair (S a) b.

End CPair_Order.

Require Import Extraction.
Section code_nat_list.

Fixpoint codeList (l : list nat) : nat :=
  match l with
  | nil ⇒ 0
  | n :: l' ⇒ S (cPair n (codeList l'))
  end.

Lemma codeListInj (l m : list nat): codeList l = codeList m → l = m.

Definition codeNth (n m:nat) : nat :=
  let X := nat_rec (fun _ : nat ⇒ nat)
             m
             (fun _ Hrecn : nat ⇒ cPairPi2 (pred Hrecn)) n
  in cPairPi1 (pred X).

Let drop (n : nat) : ∀ (l : list nat), list nat.

Lemma codeNthCorrect :
  ∀ (n : nat) (l : list nat), codeNth n (codeList l) = nth n l 0.

#[export] Instance codeNthIsPR : isPR 2 codeNth.

End code_nat_list.

Extraction codeNth.
Print codeNth.

Section Strong_Recursion.
Definition evalStrongRecHelp (n : nat) (f : naryFunc n.+2) :
  naryFunc n.+1 :=
  evalPrimRecFunc n (evalComposeFunc n 0 (Vector.nil _) (codeList nil))
    (evalComposeFunc n.+2 2
       (Vector.cons _ f _
          (Vector.cons _ (evalProjFunc n.+2 n
                            (Nat.lt_lt_succ_r _ _
                               (Nat.lt_succ_diag_r _))) _
             (Vector.nil _)))
       (fun a b : nat ⇒ S (cPair a b))).

Definition evalStrongRec (n : nat) (f : naryFunc n.+2):
  naryFunc n.+1 :=
  evalComposeFunc n.+1 1
    (Vector.cons _
       (fun z : nat ⇒ evalStrongRecHelp n f z.+1) _ (Vector.nil _))
    (fun z : nat ⇒ cPairPi1 z.-1).

#[export] Instance
 evalStrongRecIsPR (n : nat) (f : naryFunc n.+2):
  isPR _ f → isPR _ (evalStrongRec n f).

Lemma computeEvalStrongRecHelp :
  ∀ (n : nat) (f : naryFunc n.+2) (c : nat),
    evalStrongRecHelp n f c.+1 =
      compose2 n (evalStrongRecHelp n f c)
        (fun a0 : nat ⇒
           evalComposeFunc n 2
             (Vector.cons (naryFunc n) (f c a0) 1
                (Vector.cons (naryFunc n) (evalConstFunc n a0) 0
                   (Vector.nil (naryFunc n))))
             (fun a1 b0 : nat ⇒ S (cPair a1 b0))).

Fixpoint listValues (f : naryFunc 2) (n : nat) : list nat :=
  match n with
    0 ⇒ nil
  | S m ⇒ evalStrongRec _ f m :: listValues f m
  end.

Lemma evalStrongRecHelp1 :
 ∀ (f : naryFunc 2) (n m : nat),
   m < n →
   codeNth (n - m.+1) (evalStrongRecHelp _ f n) = evalStrongRec _ f m.

Lemma evalStrongRecHelpParam :
  ∀ (a n c : nat) (f : naryFunc a.+3),
    extEqual a (evalStrongRecHelp (S a) f n c)
      (evalStrongRecHelp a (fun x y : nat ⇒ f x y c) n).

Lemma evalStrongRecHelp2 :
  ∀ (a : nat) (f : naryFunc a.+2) (n m : nat),
    m < n →
    extEqual _
      (evalComposeFunc _ 1
         (Vector.cons _ (evalStrongRecHelp _ f n) 0 (Vector.nil _))
         (fun b : nat ⇒ codeNth (n - m.+1) b)) (evalStrongRec _ f m).

#[export] Instance callIsPR (g : nat → nat) (H : isPR 1 g) :
   isPR 2 (fun a recs : nat ⇒ codeNth (a - S (g a)) recs).

End Strong_Recursion.

#[export] Instance div2IsPR : isPR 1 div2.

Lemma cPairLemma1 :
  ∀ a b : nat, (a + b) × S (a + b) + 2 × a = 2 × cPair a b.

Module LispAbbreviations.
  #[global] Notation car := cPairPi1.
  #[global] Notation cdr := cPairPi2.
  #[global] Notation caar n := (cPairPi1 (cPairPi1 n)).
  #[global] Notation cadr n := (cPairPi1 (cPairPi2 n)).
  #[global] Notation caddr n := (cPairPi1 (cPairPi2 (cPairPi2 n))).

  #[global] Notation cddr n := (cPairPi2 (cPairPi2 n)).
  #[global] Notation cdddr n := (cPairPi2 (cPairPi2 (cPairPi2 n))).
  #[global] Notation cddddr n :=
    (cPairPi2 (cPairPi2 (cPairPi2 (cPairPi2 n)))).

End LispAbbreviations.

Definition cTriple (a b c : nat) : nat := cPair a (cPair b c).

Definition cTriplePi1 (n : nat) : nat := cPairPi1 n.

Definition cTriplePi2 (n : nat) : nat := cPairPi1 (cPairPi2 n).

Definition cTriplePi3 (n : nat) : nat := cPairPi2 (cPairPi2 n).

#[export] Instance cTripleIsPR : isPR 3 cTriple.

#[export] Instance cTriplePi1IsPR : isPR 1 cTriplePi1.

#[export] Instance cTriplePi2IsPR : isPR 1 cTriplePi2.

#[export] Instance cTriplePi3IsPR : isPR 1 cTriplePi3.

Lemma cTripleProj1 (a b c : nat) : cTriplePi1 (cTriple a b c) = a.

Lemma cTripleProj2 (a b c : nat) : cTriplePi2 (cTriple a b c) = b.

Lemma cTripleProj3 (a b c : nat) : cTriplePi3 (cTriple a b c) = c.

Lemma cTripleProj (a: nat) :
 cTriple (cTriplePi1 a) (cTriplePi2 a) (cTriplePi3 a) = a.