# 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. ```