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