# Library compilation

``` Require Import vector. Require Import recursive. Require Import minski_ops. Section Max.   Definition max(x y: nat) := match le_lt_dec x y with left _ => y | right _ => x end.   Lemma le_max_l: forall x y, x<=max x y.   Lemma le_max_r: forall x y, y<=max x y.   Lemma le_max_l': forall x x' y, x<=x' -> x<=max x' y.   Lemma le_max_r': forall x y y', y<=y' -> y<=max x y'.   Lemma minus_mSn_n: forall m n, m+S n-n = S m.   Lemma minus_Sn_n: forall n, S n-n = 1. End Max. Section Constant.   Definition Constant(n: nat): MinskiS :=     [ ! (fix f (n: nat) :=           match n with           | 0 => { Clear (lt_O_Sn _) }           | S n => { Concat (! f n) (Incr _ 1 0 (lt_O_Sn _) 1 (le_n _) :: nnil _) }           end) n ].   Theorem ConstantSem: forall n k (x: vector nat k), MinskiSem (Constant n) x n. End Constant. Section Zero.   Definition Zero: MinskiS := [Clear (lt_O_Sn 0)].   Theorem ZeroSem: forall k (x: vector nat k), MinskiSem Zero x 0. End Zero. Section Succ.   Definition Succ: MinskiS := [ Incr 1 1 0 (lt_O_Sn _) 1 (le_n _) :: nnil _ ].   Theorem SuccSem: forall k (x: vector nat (S k)), MinskiSem Succ x (S (head x)). End Succ. Section Pik.   Variable i: nat.   Definition Pik: MinskiS :=     match eq_nat_dec i 0 with     | left _ => [ Nil 0 ]     | right h => [ Move (lt_n_Sn i) (lt_O_Sn i) ]     end.   Theorem PikSem: forall k (x: vector nat k) (h: i<k), MinskiSem Pik x (get x i h).   Lemma PikSem': forall k (x: vector nat k) y (h: i<k), y=get x i h -> MinskiSem Pik x y. End Pik. Section Compose.   Variable i: nat.   Variable k: nat.   Variable F: MinskiS.   Variable G: forall j, j<k -> MinskiS.   Fixpoint vmax(s: nat): s<S k -> nat :=     match s return s<S k -> nat with     | 0 => fun _ => 0     | S s => fun h => max (ns (G (lt_S_n _ _ h))) (vmax (lt_S _ _ (lt_S_n _ _ h)))     end.   Let n := max i (vmax (lt_n_Sn k)).   Let n' := max k (ns F).   Let k_n': k<=n'.   Let nsF_n': ns F<=n'.   Let i_n: i<=n.   Let nsGj_n: forall j (h: j<k), ns (G h) <= n.   Let Sn_SnSn: S n < S n+S n.   Let n'_nSnSn': n' <= n+S n+ S n'.   Let wG (j: nat) (h: j<k): MinskiM n := { Widen (#G h) (nsGj_n h) }.   Let wF : MinskiM n' := { Widen (#F) nsF_n'}.   Let swF : MinskiM (n+S n+S n') := { Shift (!wF) n'_nSnSn'}.   Let Move_Sn_SnSnj j (h: j<k): Minski 3 (n+S n+S n').   Let Move_SnSn_O : Minski 3 (n+S n+S n').   Let Gj (j: nat) (h: j<k): MinskiM (n+S n+S n') :=     {Concat (Widen (MultipleCopy n (S n)) (le_plus_l _ _))     (Concat (Widen (Shift (!wG h) (le_plus_l n (S n))) (le_plus_l (n+S n) (S n')))             (Move_Sn_SnSnj h))     }.   Fixpoint AllGj (j: nat): j<S k -> MinskiM (n+S n+S n') :=     match j return j<S k -> MinskiM (n+S n+S n') with     | 0 => fun h => { Nil _ }     | S j => fun h => { Concat (!AllGj (lt_S _ _ (lt_S_n _ _ h))) (!Gj (lt_S_n _ _ h)) }     end.   Definition Compose: MinskiS :=      [ Concat (!AllGj (lt_n_Sn k)) (Concat (!swF) Move_SnSn_O) ].   Section Sem.     Variable x: vector nat i.     Variable gx: vector nat k.     Variable y: nat.     Hypothesis HG: forall j (h: j<k), MinskiSem (G h) x (get gx j h).     Hypothesis HF: MinskiSem F gx y.     Let mcopy_n_Sn: forall (x01 x02: vector nat (S n)) (x03: vector nat (S n')),       mcopy         (truncate (S n + S n) (overwrite x x01 @ x02 @ x03)           (le_n_S _ _ (le_plus_l _ _)))         (truncate (S n + S n) (overwrite x x01 @ change (overwrite x x01) n 0 @ x03)           (le_n_S _ _ (le_plus_l _ _))).     Let HwG: forall j (h: j<k), MinskiSem [!wG h] x (get gx j h).     Let wGSemR: forall j (h: j<k) (x0: vector nat (S n)), exists r: vector nat (S n),       MinskiSemR [!wG h] (overwrite x x0) r /\ get r 0 (lt_O_Sn _) = get gx j h.     Lemma AllGjSem: forall k' (hk': k'<S k) (x0: vector nat (S n+S n+S n')),       exists rG: vector nat (S n), forall (r': vector nat (S n+S n+S n')),       r' = (overwrite x (split1 _ _ (split1 _ _ x0))) @ rG @ (overwrite (truncate k' gx (lt_n_Sm_le _ _ hk')) (split2 _ _ x0)) ->       MinskiSemR [!AllGj hk'] (overwrite x x0) r'.       Opaque MultipleCopy wG.     Let HwF: MinskiSem [!wF] gx y.     Let wFSemR: forall (x0: vector nat (S n')), exists r: vector nat (S n'),       MinskiSemR [!wF] (overwrite gx x0) r /\ get r 0 (lt_O_Sn _) = y.     Let swFSemR: forall (x0: vector nat (S n')), exists r: vector nat (S n'),       get r O (lt_O_Sn _) = y /\       forall a: vector nat (S n+S n), MinskiSemR [!swF] (a @ overwrite gx x0) (a @ r).     Theorem ComposeSem: MinskiSem Compose x y.       Opaque swF.   End Sem. End Compose. Section Prim.   Variable k: nat.   Variable F: MinskiS.   Variable G: MinskiS.   Let m := ms G.   Let n := max (ns G) (S (S (S k))).   Let SSSk_n: S(S(S k))<= n.   Let SSk_n: S(S k)<= n.   Let O_n: 0<n.   Let O_SnSSn: 0<S n+S (S n).   Let SO_SnSSn: 1<S n+S (S n).   Let SSO_SnSSn: 2<S n+S (S n).   Let n_SnSSn: n<S n+S (S n).   Let Sn_SnSSn: S n<S n+S (S n).   Let nSn_nSSn: n+S n<=n+S (S n).   Let SSn_SnSSn: S (S n)<S n+S (S n).   Section PrimIter.     Let wG: Minski m n := Widen (#G) (le_max_l _ _).     Let sG: Minski m (n+S (S n)) := Shift wG (le_plus_l n (S (S n))).     Definition PrimIter: MinskiS :=       [Loop 0 (Concat (Widen (MultipleCopy n (S n)) nSn_nSSn) (Concat sG (Concat (Move SSn_SnSSn SSO_SnSSn) (Inkr SO_SnSSn)))) O_SnSSn].     Section Sem.       Variable y e: nat.       Variable x: vector nat k.       Lemma PrimIterSemRO: forall x0: vector nat (S n+S (S n)), get x0 0 O_SnSSn = 0 -> MinskiSemR PrimIter x0 x0.       Variables z t h h': nat.       Hypothesis HG: MinskiSem G (t::h::x) h'.       Hypothesis HR: forall x0: vector nat (S n+S (S n)),         exists x0': vector nat (S n+S (S n)),         get x0' 2 SSO_SnSSn = y /\ MinskiSemR PrimIter (overwrite (z::S t::h'::x) x0) x0'.       Let HwG: MinskiSem [wG] (t::h::x) h'.       Let sGSemR: forall (x0: vector nat (S n)), exists r: vector nat (S n),         get r 0 (lt_O_Sn n) = h' /\         forall (a: vector nat (S n)) b,         MinskiSemR [sG] (a @ b :: overwrite (t::h::x) x0) (a @ b :: r).       Let mcopy_n_Sn: forall x0: vector nat (S n+S (S n)),         mcopy (truncate (S n+S n) (overwrite (z::t::h::x) x0) (le_n_S (n + S n) (n + S (S n)) nSn_nSSn))               (truncate (S n+S n)                  (split1 (S n) (S (S n)) (overwrite (z::t::h::x) x0) @                  overwrite (change (split1 (S n) (S (S n)) (overwrite (z::t::h::x) x0)) n 0) (split2 _ _ x0))                  (le_n_S (n + S n) (n + S (S n)) nSn_nSSn)).       Lemma PrimIterSemRS: forall x0: vector nat (S n+S (S n)), exists x0': vector nat (S n+S (S n)),         get x0' 2 SSO_SnSSn = y /\ MinskiSemR PrimIter (overwrite (S z::t::h::x) x0) x0'.     End Sem.   End PrimIter.   Let sF: MinskiS := Compose (S k) F (fun j (h: j<k) => Pik (S j)).   Definition Prim: MinskiS :=     Compose (S k)       [Concat (#PrimIter) (Move SSO_SnSSn O_SnSSn)]       (fun j (h: j<S (S (S k))) =>         match j with         | 0 => Pik 0         | 1 => Zero         | 2 => sF         | (S (S j)) => Pik j         end).   Section Sem.     Variable y : nat.     Variable x : vector nat (S k).     Variable SemF: vector nat k -> nat -> Prop.     Variable SemG: vector nat (S (S k)) -> nat -> Prop.     Hypothesis HSemF: Injective SemF.     Hypothesis HSemG: Injective SemG.     Hypothesis HF: forall x y, SemF x y -> MinskiSem F x y.     Hypothesis HG: forall x y, SemG x y -> MinskiSem G x y.     Hypothesis HIter: IterSem SemF SemG (head x) (tail x) y.     Let PrimIterSemR: forall z t h (x0: vector nat (S n+S (S n))),       IterSem SemF SemG (t+z) (tail x) y ->       IterSem SemF SemG t (tail x) h ->       exists r': vector nat (S n+S (S n)),         get r' 2 SSO_SnSSn = y /\ MinskiSemR PrimIter (overwrite (z :: t :: h :: tail x) x0) r'.     Theorem PrimSem: MinskiSem Prim x y.   End Sem. End Prim. Section Min.   Variable k: nat.   Variable F: MinskiS.   Let n := max (S (ns F)) k.   Let k_n: k<= n.   Let nsF_Sn: ns F<=S n.   Let neq_O_n: 0<>n.   Let O_SnSSn: O<S n+S (S n).   Let n_SnSSn: n<S n+S (S n).   Let Sn_SnSSn: S n<S n+S (S n).   Let Sn_nSSn: S n<=n+S (S n).   Let n_nSSn': n<>n+S (S n).   Let Sn_nSSn': S n<>n+S (S n).   Let wF: MinskiM (S n) := {Widen (#F) nsF_Sn}.   Let swF: MinskiM (n+S (S n)) := {Shift (!wF) Sn_nSSn}.   Let MinIter: MinskiM (n+S (S n)) :=     {Concat (Copy n_SnSSn Sn_SnSSn (lt_n_Sn _))     (Concat (MultipleCopy n (S (S n)))     (Concat (!swF)             (Inkr n_SnSSn)))}.   Definition Min: MinskiS :=     [Concat (Clear n_SnSSn) (Concat (Inkr Sn_SnSSn) (Concat (Loop (S n) (!MinIter) Sn_SnSSn) (Concat (Decr n_SnSSn) (Move n_SnSSn O_SnSSn))))].   Section Sem.     Variable y: nat.     Variable x: vector nat k.     Hypothesis H0: MinskiSem F (y::x) 0.     Hypothesis Hm: forall y', y'<y -> exists x', MinskiSem F (y'::x) (S x').     Section SWF.       Variables z t: nat.       Hypothesis HF: MinskiSem F (z::x) t.       Let HwF: MinskiSem [!wF] (z::x) t.       Let wFSemR: forall (x0: vector nat (S (S n))), exists r: vector nat (S (S n)),         MinskiSemR [!wF] (overwrite (z::x) x0) r /\ get r 0 (lt_O_Sn _) = t.       Lemma swFSemR: forall (x0: vector nat (S n)), exists r: vector nat (S (S n)),         get r O (lt_O_Sn _) = t /\         forall a: vector nat (S n), MinskiSemR [!swF] (a @ z::overwrite x x0) (a @ r).     End SWF.     Let mcopy_n_SSn: forall (x1: vector nat (S n)) (x2: vector nat (S (S n))),       mcopy (x1 @ x2) (x1 @ (get x2 0 (lt_O_Sn _)) :: (change x1 n 0)).     Let MinIterStep: forall w (x1: vector nat (S n)) (r r': vector nat (S (S n))),       w<=y ->       (forall a : vector nat (S n), MinskiSemR [!swF] (a @ (y-w) :: overwrite x (change x1 n 0)) (a @ r)) ->       MinskiSemR [Loop (S n) (!MinIter) Sn_SnSSn]         (overwrite x (change x1 n (S (y - w))) @ r)         (overwrite x (change x1 n (S y)) @ r') ->       forall x2 p,       MinskiSemR [Loop (S n) (!MinIter) Sn_SnSSn]         (change (overwrite x x1) n (y - w) @ change x2 0 (S p))         (change (overwrite x x1) n (S y) @ r').     Let MinIterSemR: forall (x0: vector nat (S n+S (S n))) p w,       w<=y ->       exists r: vector nat (S (S n)),       MinskiSemR [Loop (S n) (!MinIter) Sn_SnSSn]         (change (change (overwrite x x0) n (y-w)) (S n) (S p))         (change (overwrite x (split1 _ _ x0)) n (S y) @ r).     Theorem MinSem: MinskiSem Min x y.   End Sem. End Min. Section Compilation.   Let force k (f: forall i, i<k -> MinskiS): forall i, i<k -> MinskiS :=     get (init k (fun i => match le_lt_dec k i with left _ => Zero | right h => f i h end)).   Let get_force: forall k (f: forall i, i<k -> MinskiS) i (h: i<k), force f h = f i h.   Fixpoint compile(k: nat)(f: Recfun k) {struct f}: MinskiS :=     match f with       | recursive.Constant n => Constant n       | recursive.Zero => Zero       | recursive.Succ => Succ       | recursive.Pik i _ _ => Pik i       | recursive.Compose _ i f g => Compose i (compile f) (force (fun j h => compile (g j h)))       | recursive.Prim k f g => Prim k (compile f) (compile g)       | recursive.Min _ f => Min k (compile f)     end.   Theorem CompileCorrect: forall (k: nat) (f: Recfun k) (x: vector nat k) (y: nat),     RecSem f x y -> MinskiSem (compile f) x y. End Compilation. ```