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.