Library minski_tools
Require Import vector.
Require Export minski.
Section Nil.
Variables n: nat.
Definition Nil: Minski 0 n := nnil _.
Theorem NilSemR: forall r r': vector nat (S n), r=r' -> MinskiSemR [Nil] r r'.
End Nil.
Section Widen.
Variables m k n: nat.
Variable M: Minski m k.
Hypothesis k_n: k<=n.
Let Sk_Sn: S k<=S n.
Let Widen_map(s: Step m k): Step m n :=
match s with
| Incr i hi q hq => Incr _ _ i (lt_le_trans _ _ _ hi Sk_Sn) q hq
| Test i hi q q' hq hq' => Test _ _ i (lt_le_trans _ _ _ hi Sk_Sn) q q' hq hq'
end.
Definition Widen: Minski m n := map Widen_map M.
Let unwiden(C: Config m n): Config m k := config m k (state C) (proof C) (truncate (S k) (reg C) Sk_Sn).
Let widen(C: Config m k)(x0: vector nat (S n)): Config m n := config m n (state C) (proof C) (overwrite (reg C) x0).
Let unwiden_widen: forall C x0, unwiden (widen C x0) = C.
Hint Resolve unwiden_widen.
Let Widen_step: forall C H C',
unwiden C' = step [M] (unwiden C) H -> eq_from (S k) (reg C) (reg C') ->
step [Widen] C H = C'.
Let WidenSem': forall (Cu Cu': Config m k), transition [M] Cu Cu' ->
forall C C', Cu=unwiden C -> Cu'=unwiden C' -> eq_from (S k) (reg C) (reg C') -> transition [Widen] C C'.
Theorem WidenSemR: forall r r': vector nat (S n),
MinskiSemR [M] (truncate (S k) r Sk_Sn) (truncate (S k) r' Sk_Sn) ->
eq_from (S k) r r' ->
MinskiSemR [Widen] r r'.
Theorem WidenSem: forall k' (x: vector nat k') y, MinskiSem [M] x y -> MinskiSem [Widen] x y.
End Widen.
Section Shift.
Variables m k n: nat.
Variable M: Minski m k.
Hypothesis k_n: k<=n.
Definition nk := n-k.
Let Sk_Sn: S k<=S n.
Let nki_Sn: forall i, i < S k -> nk+i < S n.
Let nkSk_Sn: S n = n-k+S k.
Let Shift_map(s: Step m k): Step m n :=
match s with
| Incr i hi q hq => Incr m n (n-k+i) (nki_Sn hi) q hq
| Test i hi q q' hq hq' => Test m n (n-k+i) (nki_Sn hi) q q' hq hq'
end.
Definition Shift: Minski m n := map Shift_map M.
Let unshift(C: Config m n): Config m k := config m k (state C) (proof C) (etruncate (S k) (reg C) Sk_Sn).
Let shift(C: Config m k) s: Config m n := config _ _ (state C) (proof C) (coerce _ nkSk_Sn (s @ (reg C))).
Let unshift_shift: forall s C, unshift (shift C s) = C.
Hint Resolve unshift_shift.
Let Shift_step: forall C H C',
unshift C' = step [M] (unshift C) H -> eq_until (n-k) (reg C) (reg C') -> step [Shift] C H = C'.
Let ShiftSem': forall (Cu Cu': Config m k), transition [M] Cu Cu' ->
forall C C', Cu = unshift C -> Cu' = unshift C' -> eq_until (n-k) (reg C) (reg C') -> transition [Shift] C C'.
Theorem ShiftSemR: forall r r': vector nat (S n),
MinskiSemR [M] (etruncate (S k) r Sk_Sn) (etruncate (S k) r' Sk_Sn) ->
eq_until (n-k) r r' ->
MinskiSemR [Shift] r r'.
End Shift.
Section Prepend.
Variables m m' n: nat.
Variable M: vector (Step (m'+m) n) m'.
Variable N: Minski m n.
Definition Prepend_map(s: Step m n): Step (m'+m) n :=
match s with
| Incr i hi q hq => Incr (m'+m) n i hi (m'+q) (plus_le_compat_l _ _ _ hq)
| Test i hi q q' hq hq' => Test (m'+m) n i hi (m'+q) (m'+q') (plus_le_compat_l _ _ _ hq) (plus_le_compat_l _ _ _ hq')
end.
Definition Prepend: Minski (m'+m) n := M @ (map Prepend_map N).
Lemma prepend_proof: forall i (hi: i<=m'+m), i-m'<=m.
Let prepend(C: Config m n) := config (m'+m) n (m' + state C) (plus_le_compat_l _ _ _ (proof C)) (reg C).
Definition unprepend(C: Config (m'+m) n) := config m n (state C - m') (prepend_proof (proof C)) (reg C).
Let prepend_nfinal: forall C, nfinal C -> nfinal (prepend C).
Lemma unprepend_nfinal: forall C, nfinal (unprepend C) -> nfinal C.
Let prepend_step: forall C (hm: state C >= m') (H: nfinal (unprepend C)),
step [N] (unprepend C) H = unprepend (step [Prepend] C (unprepend_nfinal H)).
Let prepend_step_m: forall C (hm: state C >= m') (H: nfinal (unprepend C)), state (step [Prepend] C (unprepend_nfinal H)) - m' <= m.
Let prepend_step_m': forall C (hm: state C >= m') (H: nfinal (unprepend C)), state (step [Prepend] C (unprepend_nfinal H)) >= m'.
Let prepend_step_m'': forall (C C': Config (m'+m) n), transition [Prepend] C C' -> state C >= m' -> state C' >= m'.
Theorem PrependSem: forall (Cu Cu': Config m n),
forall (C: Config (m'+m) n) (hm: state C >= m') (C': Config (m'+m) n) (hm': state C' >= m'),
transition [N] Cu Cu' -> Cu = unprepend C -> Cu' = unprepend C' -> transition [Prepend] C C'.
End Prepend.
Section Append.
Variables m m' n: nat.
Variable M: Minski m n.
Variable N: vector (Step (m+m') n) m'.
Definition Append_map(s: Step m n): Step (m+m') n :=
match s with
| Incr i hi q hq => Incr (m+m') n i hi q (le_plus_trans _ _ _ hq)
| Test i hi q q' hq hq' => Test (m+m') n i hi q q' (le_plus_trans _ _ _ hq) (le_plus_trans _ _ _ hq')
end.
Definition Append: Minski (m+m') n := (map Append_map M) @ N.
Let appent(C: Config m n) := config (m+m') n (state C) (le_plus_trans _ _ _ (proof C)) (reg C).
Definition unappend(C: Config (m+m') n) (hq: state C <= m) := config m n (state C) hq (reg C).
Let h_append: forall C, state (appent C) <= m.
Let unappend_append: forall C, unappend (appent C) (h_append C) = C.
Let append_nfinal: forall C, nfinal C -> nfinal (appent C).
Let unappend_nfinal: forall C h, nfinal (unappend C h) -> nfinal C.
Let append_step: forall C h (H: nfinal (unappend C h)) P, step [M] (unappend C h) H = unappend (step [Append] C (append_nfinal H)) P.
Let append_step_m: forall C h (H: nfinal (unappend C h)), state (step [Append] C (append_nfinal H)) <= m.
Theorem AppendSem: forall (Cu Cu': Config m n),
forall (C: Config (m+m') n) h (C': Config (m+m') n) h',
transition [M] Cu Cu' -> Cu = unappend C h -> Cu' = unappend C' h' -> transition [Append] C C'.
End Append.
Section Concat.
Variables m1 m2 n: nat.
Variable M1: Minski m1 n.
Variable M2: Minski m2 n.
Definition Concat: Minski (m1+m2) n := Prepend (map (Append_map (m:=m1) (n:=n) m2) M1) M2.
Theorem ConcatSemR: forall r' r r'': vector nat (S n),
MinskiSemR [M1] r r' -> MinskiSemR [M2] r' r'' -> MinskiSemR[Concat] r r''.
End Concat.
Ltac MinskiSemR :=
match goal with
| |- MinskiSemR [Nil] _ _ => apply NilSemR
| |- MinskiSemR [Shift ?M ?h] _ _ => apply (ShiftSemR (M:=M) (k_n:=h)); try MinskiSemR
| |- MinskiSemR [Widen ?M ?h] _ _ => apply (WidenSemR (M:=M) h); try MinskiSemR
| |- MinskiSemR [Concat ?M1 ?M2] _ _ => eapply (ConcatSemR (M1:=M1) (M2:=M2)); try MinskiSemR
end.
Section Loop.
Variables m n k: nat.
Variable M: Minski m n.
Hypothesis k_n: k<S n.
Definition Loop: Minski (1+(m+1)) n :=
Prepend (Test _ _ k k_n (1+(m+1)) 1 (le_n _) (le_n_S _ _ (le_O_n _)) :: nnil _)
(Append M
(Test _ _ k k_n (m+1) 0 (le_n _) (le_O_n _) :: nnil _ )).
Theorem LoopSemO: forall r: vector nat (S n), get r k k_n = 0 -> forall r', r=r' -> MinskiSemR [Loop] r r'.
Let mO_m: m-0 <= m.
Theorem LoopSemS: forall (r: vector nat (S n)) x, get r k k_n = S x ->
forall r' r'': vector nat (S n),
MinskiSemR [M] (change r k x) r' -> MinskiSemR [Loop] r' r'' -> MinskiSemR [Loop] r r''.
End Loop.
Implicit Arguments Loop [m n].