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.