Library recursive


Require Import vector.


Inductive Recfun: nat -> Set :=
| Constant: nat -> Recfun 0
| Zero: Recfun 1
| Succ: Recfun 1
| Pik: forall i k, i < k -> Recfun k
| Compose: forall k i, Recfun k -> (forall j, j<k -> Recfun i) -> Recfun i
| Prim: forall k , Recfun k -> Recfun (S (S k)) -> Recfun (S k)
| Min: forall k , Recfun (S k) -> Recfun k.
Implicit Arguments Pik [].


Definition Injective k (P: vector nat k -> nat -> Prop): Prop :=
  forall (x: vector nat k) y y', P x y -> P x y' -> y=y'.


Section IterSem.

  Variable k: nat.
  Variable SemF: vector nat k -> nat -> Prop.
  Variable SemG: vector nat (S (S k)) -> nat -> Prop.


  Fixpoint IterSem (t: nat): vector nat k -> nat -> Prop :=
    match t with
    | 0 => SemF
    | S t => fun x y => exists h, IterSem t x h /\ SemG (t :: h :: x) y
    end.


  Lemma IterSemReverse: forall (x: vector nat k) t z yzt,
    IterSem (t+z) x yzt -> exists yt: nat, IterSem t x yt.





  Lemma IterSemInjective: Injective SemF -> Injective SemG -> forall t, Injective (IterSem t).

End IterSem.


Fixpoint RecSem k (f: Recfun k) {struct f} : vector nat k -> nat -> Prop :=
match f in Recfun k return vector nat k -> nat -> Prop with
| Constant n => fun _ m => m = n
| Zero => fun _ m => m = 0
| Succ => fun l m => m = S (head l)
| Pik i k h => fun l m => m = get l i h
| Compose k i f g => fun l m => exists gl, RecSem f gl m /\ forall j (h: j<k), RecSem (g j h) l (get gl j h)
| Prim k f g => fun l => IterSem (RecSem f) (RecSem g) (head l) (tail l)
| Min k f => fun l m => RecSem f (m::l) 0 /\ forall i, i<m -> exists x, RecSem f (i::l) (S x)
end.


Theorem RecSemInjective: forall k (f: Recfun k), Injective (RecSem f).









Definition Compose0 i (f: Recfun 0) := Compose f (get (nnil (Recfun i))).
Definition Compose1 i (f: Recfun 1) (g: Recfun i) := Compose f (get (g :: nnil _)).
Definition Compose2 i (f: Recfun 2) (g g': Recfun i) := Compose f (get (g :: g' :: nnil _)).

Definition RecSem1 (f: Recfun 1) a n := RecSem f (a :: nnil _) n.
Definition RecSem2 (f: Recfun 2) a b n := RecSem f (a :: b :: nnil _) n.
Definition RecSem3 (f: Recfun 3) a b c n := RecSem f (a :: b :: c :: nnil _) n.


Ltac absurd_lt h := elim (lt_irrefl _ h) || elim (lt_n_O _ h) || absurd_lt (lt_S_n _ _ h).
Ltac sreflexivity := simpl; reflexivity.

Ltac bounded_prop := match goal with | |- forall (j: nat) (h: j<_), _ => intros j h; ( absurd_lt h || bounded_prop' j h ) end
with bounded_prop' j h := destruct j; [ idtac | absurd_lt h || bounded_prop' j h ].

Ltac composition gx := exists gx; split; [ try sreflexivity | bounded_prop; unfold get; try sreflexivity ].
Ltac composition0 := composition (nnil nat).
Ltac composition1 x := composition (x :: nnil _).
Ltac composition2 x x' := composition (x :: x' :: nnil _).

Ltac primitive1 f := match goal with
                     | |- forall m: nat, RecSem _ (m :: nnil nat) _ =>
                       intro m; induction m as [ | m HR ];
                       [ try sreflexivity
                       | exists (f m); split; [ exact HR | try sreflexivity ] ]
                     | |- forall m: nat, RecSem1 _ _ _ => unfold RecSem1; primitive1 f
                    end.
Ltac primitive2 f := match goal with
                     | |- forall m n: nat, RecSem _ (m :: n :: nnil nat) _ =>
                       intro m; induction m as [ | m HR ];
                       [ try sreflexivity
                       | intro n; exists (f m n); split; [ exact (HR n) | try sreflexivity ] ]
                     | |- forall m n: nat, RecSem2 _ _ _ _ => unfold RecSem2; primitive2 f
                    end.

Ltac deCompose H x :=
  elim H; intro x; finite_list x;intro Hx; clear H;
  elim Hx; intros Heq Hg; clear H Hx;
  deCompose_ Hg 0 lt_O_Sn; clear Hg
with
deCompose_ Hg n h := generalize (Hg n (h _)); unfold get; intro; try deCompose_ Hg (S n) (fun x => lt_n_S _ _ (h x)).


Definition Id: Recfun 1 := Pik 0 1 (lt_O_Sn _).
Definition P02: Recfun 2 := Pik 0 2 (lt_O_Sn _).
Definition P12: Recfun 2 := Pik 1 2 (lt_n_Sn _).
Definition P03: Recfun 3 := Pik 0 3 (lt_O_Sn _).
Definition P13: Recfun 3 := Pik 1 3 (lt_trans _ _ _ (lt_n_Sn _) (lt_n_Sn _)).
Definition P23: Recfun 3 := Pik 2 3 (lt_n_Sn _).

Section Addition.

  Definition Add: Recfun 2 := Prim Id (Compose1 Succ P13).

  Theorem AddSem: forall m n: nat, RecSem2 Add m n (m+n).

End Addition.

Section Multiplication.

  Definition Mult: Recfun 2 := Prim Zero (Compose2 Add P13 P23).

  Theorem MultSem: forall m n: nat, RecSem2 Mult m n (m*n).

End Multiplication.

Section SquareRoot.

  Definition Sqr: Recfun 1 := Compose2 Mult Id Id.
  Lemma SqrSem: forall n: nat, RecSem1 Sqr n (n*n).

  Definition null n := match n with 0 => 0 | _ => 1 end.
  Lemma nullS: forall m n, m < n -> null (n-m) = 1.
  Definition Null: Recfun 1 := Prim (Constant 0) (Compose0 _ (Constant 1)).
  Lemma NullSem: forall n: nat, RecSem1 Null n (null n).

  Definition null2 m n := null (m+n).
  Definition Null2: Recfun 2 := Compose1 Null Add.
  Lemma Null2Sem: forall m n: nat, RecSem2 Null2 m n (null2 m n).

  Definition Pred: Recfun 1 := Prim (Constant 0) (Compose1 Id P02).
  Lemma PredSem: forall n: nat, RecSem1 Pred n (pred n).

  Definition SubInv: Recfun 2 := Prim Id (Compose1 Pred P13).
  Lemma SubInvSem: forall m n: nat, RecSem2 SubInv m n (n - m).

  Definition Sub: Recfun 2 := Compose2 SubInv P12 P02.
  Lemma SubSem: forall m n: nat, RecSem2 Sub m n (m - n).

  Definition beq m n := null2 (m-n) (n-m).
  Definition Eq: Recfun 2 := Compose2 Null2 Sub SubInv.
  Lemma EqSem: forall m n: nat, RecSem2 Eq m n (beq m n).
  Lemma EqRefl: forall n: nat, RecSem2 Eq n n 0.
  Lemma EqNRefl: forall m n: nat, m<>n -> RecSem2 Eq m n 1.
  Lemma EqRefl_eq: forall m n: nat, RecSem Eq (m::n::nnil _) 0 -> m=n.

  Definition sqrt(m n: nat): Prop := m=n*n.
  Definition Sqrt: Recfun 1 := Min (Compose2 Eq (Compose1 Id P12) (Compose1 Sqr P02)).

  Lemma sqr_S: forall n: nat, S n*S n = n*n + (n+n + 1).
  Lemma sqr_lt: forall m n: nat, m < n -> m*m < n*n.
  Lemma nsqrt: forall m n, sqrt m n -> forall i, i<n -> ~ sqrt m i.

  Theorem SqrtSem: forall m n: nat, sqrt m n <-> RecSem1 Sqrt m n.



End SquareRoot.