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.