Library minski_ops

``` Require Import vector. Require Export minski_tools. Section Clear.   Variables k n: nat.   Hypothesis k_n: k < S n.   Definition Clear: Minski 1 n := Test 1 n k k_n 1 0 (le_n _) (le_O_n _) :: nnil _.   Theorem ClearSemR: forall r r', r' = change r k 0 -> MinskiSemR [Clear] r r'. End Clear. Section Inkr.   Variables k n: nat.   Hypothesis k_n: k < S n.   Definition Inkr: Minski 1 n := Incr 1 n k k_n 1 (le_n _) :: nnil _.   Theorem InkrSemR: forall r r', r' = change r k (S (get r k k_n)) -> MinskiSemR [Inkr] r r'. End Inkr. Section Decr.   Variables k n: nat.   Hypothesis k_n: k < S n.   Definition Decr: Minski 1 n := Test 1 n k k_n 1 1 (le_n _) (le_n _) :: nnil _.   Theorem DecrSemR: forall r r', r' = change r k (pred (get r k k_n)) -> MinskiSemR [Decr] r r'. End Decr. Section Move.   Variables k k' n: nat.   Hypothesis k_n: k < S n.   Hypothesis k'_n: k'< S n.   Definition MoveAdd: Minski 2 n :=     Test 2 n k k_n 2 1 (le_n _) (le_n_Sn _) ::     Incr 2 n k' k'_n 0 (le_O_n _) ::     nnil _.   Theorem MoveAddSemR: k<>k' -> forall r r', r' = change (change r k 0) k' (get r k k_n + get r k' k'_n) ->     MinskiSemR [MoveAdd] r r'.   Definition Move: Minski 3 n := Concat (Clear k'_n) MoveAdd.   Theorem MoveSemR: forall r r', r' = change (change r k' (get r k k_n)) k 0 ->     MinskiSemR [Move] r r'. End Move. Section Copy.   Variables k k' t n: nat.   Hypothesis kk' : k <> k'.   Hypothesis kt : k <> t.   Hypothesis k't : k'<> t.   Hypothesis kn : k < S n.   Hypothesis k'n : k' < S n.   Hypothesis tn : t < S n.   Let dup_k_k'_t: Minski 3 n.   Let dup_sem: forall v v' V r,      v =get r k kn ->      v'=get r k' k'n ->      V =get r t tn ->        MinskiSemR [dup_k_k'_t] r (change (change (change r k 0) k' (v+v')) t (v+V)).   Definition Copy: Minski 7 n :=      Concat (Clear tn)     (Concat (Clear k'n)     (Concat dup_k_k'_t             (MoveAdd tn kn))).   Theorem CopySemR: forall r r', r' = change (change r k' (get r k kn)) t 0 -> MinskiSemR [Copy] r r'. End Copy. Section MultipleCopy.   Let CopyOmSm m n: Minski 7 (S n + m).   Fixpoint MultipleCopy (n m: nat) {struct n}: Minski (S (n*7)) (n+m) :=     match n return Minski (S (n*7)) (n+m) with     | 0 => Clear (lt_n_Sn _)     | S n => Concat (CopyOmSm m n) (Shift (MultipleCopy n m) (le_n_Sn _))     end.   Definition mcopy n m (r r': vector nat (S n + m)): Prop :=     (forall i, i<m -> forall h, get r' i h = get r i h) /\     (forall i, i<n -> forall h h', get r' (i+m) h = get r i h') /\     ( forall h, get r' (n+m) h = 0).   Let in_i_Si_eq: forall i j, i<j -> j<=S i -> j=S i.   Let lt_neq: forall i j, i<j -> j<>i.   Theorem MultipleCopySemR: forall n m (h: n<=m) r r', mcopy r r' ->     MinskiSemR [MultipleCopy n m] r r'. End MultipleCopy. Ltac MiscSemR :=   match goal with   | |- MinskiSemR [Clear _] _ _ => apply ClearSemR   | |- MinskiSemR [Inkr _] _ _ => apply InkrSemR   | |- MinskiSemR [Decr _] _ _ => apply DecrSemR   | |- MinskiSemR [Copy _ _ _] _ _ => apply CopySemR   | |- MinskiSemR [MultipleCopy _ _] _ _ => apply MultipleCopySemR   | |- MinskiSemR [Move _ _] _ _ => apply MoveSemR   end. ```