From hydras Require Import primRec Ack MoreVectors.
From Coq Require Import Arith ArithRing List Lia Compare_dec.
Import extEqualNat VectorNotations Vector.

Notation "'v_apply' f v" := (evalList _ v f) (at level 10, f at level 9).

Check [4].
Example Ex2 : ∀ (f: naryFunc 2) x y,
    v_apply f [x;y] = f x y.

Example Ex4 : ∀ (f: naryFunc 4) x y z t,
    v_apply f [x;y;z;t] = f x y z t.

Definition majorized {n} (f: naryFunc n) (A: naryFunc 2) :=
  ∃ (q:nat),
    ∀ (v: t nat n), v_apply f v ≤ A q (max_v v).

Definition majorizedPR {n} (x: PrimRec n) A :=
  majorized (evalPrimRec n x) A.

Definition majorizedS {n m} (fs : Vector.t (naryFunc n) m)
           (A : naryFunc 2):=
  ∃ N, ∀ (v: t nat n),
      max_v (Vector.map (fun f ⇒ v_apply f v) fs) ≤ A N (max_v v).

Definition majorizedSPR {n m} (x : PrimRecs n m) :=
  majorizedS (evalPrimRecs _ _ x).


Section evalList.


  Lemma evalList_Const : ∀ n (v:t nat n) x,
    v_apply (evalConstFunc n x) v = x.

  Lemma proj_le_max : ∀ n, ∀ v : t nat n, ∀ k (H: k < n),
          v_apply (evalProjFunc n k H) v ≤ max_v v.

  Lemma evalListComp : ∀ n (v: t nat n) m (gs: t (naryFunc n) m)
                              (h: naryFunc m),
      v_apply (evalComposeFunc _ _ gs h) v =
      v_apply h (map (fun g ⇒ v_apply g v) gs).
  Lemma evalListCompose2 : ∀ n (v: t nat n) (f: naryFunc n)
                                  (g : naryFunc (S n)),
      v_apply (compose2 n f g) v =
      v_apply g ((evalList n v f) :: v).

  Lemma evalListPrimrec_0 : ∀ n (v: t nat n) (f : naryFunc n)
                                   (g : naryFunc (S (S n))),
      v_apply (evalPrimRecFunc _ f g) (cons 0 v)
      = v_apply f v.

  Lemma evalListPrimrec_S : ∀ n (v: t nat n) (f : naryFunc n)
                                   (g : naryFunc (S (S n))) a,
      v_apply (evalPrimRecFunc _ f g) (cons (S a) v)
      = v_apply g
                (a :: v_apply (evalPrimRecFunc n f g) (a :: v) :: v).

End evalList.

Lemma majorSucc : majorizedPR succFunc Ack.

Lemma majorZero : majorizedPR zeroFunc Ack.

Lemma majorProjection (n m:nat)(H: m < n): majorizedPR (projFunc n m H) Ack.

Lemma majorAnyPR: ∀ n (x: PrimRec n), majorizedPR x Ack.

Lemma majorPR1 (f: naryFunc 1)(Hf : isPR 1 f)
  : ∃ (n:nat), ∀ x, f x ≤ Ack n x.

Lemma majorPR2 (f: naryFunc 2)(Hf : isPR 2 f)
  : ∃ (n:nat), ∀ x y, f x y ≤ Ack n (max x y).

Lemma majorPR2_strict (f: naryFunc 2)(Hf : isPR 2 f):
    ∃ n:nat,
      ∀ x y, 2 ≤ x → 2 ≤ y → f x y < Ack n (max x y).

Section Impossibility_Proof.

  Context (HAck : isPR 2 Ack).

  Lemma Ack_not_PR : False.
End Impossibility_Proof.

Section dom_AckNotPR.

  Variable f : nat → nat.
  Hypothesis Hf : dominates f (fun n ⇒ Ack n n).

  Lemma dom_AckNotPR: isPR 1 f → False.

End dom_AckNotPR.

Lemma AckSn_as_iterate (n:nat) : extEqual 1 (Ack (S n))
                                          (fun k ⇒ iterate (Ack n) (S k) 1).

Lemma AckSn_as_PRiterate (n:nat):
  extEqual 1 (Ack (S n)) (fun k ⇒ primRec.iterate (Ack n) (S k) 1).

Lemma iterate_nat_rec (g: nat→nat) (n:nat) x :
  iterate g n x = nat_rec (fun _ ⇒ nat) x (fun x y ⇒ g y) n.

Section Proof_of_Ackn_PR.

  Section S_step.
    Variable n:nat.
    Context (IHn: isPR 1 (Ack n)).

    Remark R1 : extEqual 1 (Ack (S n))
                         (fun a : nat ⇒
                            nat_rec (fun _ : nat ⇒ nat) 1
                                    (fun _ y : nat ⇒ Ack n y)
                                    (S a)).

    #[local] Instance R2 : isPR 1
                     (fun a : nat ⇒
                        nat_rec (fun _ : nat ⇒ nat) 1
                                (fun _ y : nat ⇒ Ack n y)
                                (S a)).

    #[export] Instance iSPR_Ack_Sn : isPR 1 (Ack (S n)).

  End S_step.




  #[export] Instance Ackn_IsPR (n: nat) : isPR 1 (Ack n).
  Proof.
    induction n.


    - cbn; apply succIsPR.
    - apply iSPR_Ack_Sn; auto.
  Qed.

End Proof_of_Ackn_PR.