All sub-proofs about "update" closed.

[helm.git] / helm / software / matita / library / assembly / vm.ma

diff --git a/helm/software/matita/library/assembly/vm.ma b/helm/software/matita/library/assembly/vm.ma
index dac755c82c54484fb506596c11a7435a5e0eb857..239146a07526445c12d662592117e32c26358b2e 100644 (file)
--- a/helm/software/matita/library/assembly/vm.ma
+++ b/helm/software/matita/library/assembly/vm.ma
@@ -139,6 +139,38 @@ lemma update_update_a_b:
  ].
 qed.
 
+lemma eq_update_s_a_sa: ∀s,a,b. update s a (s a) b = s b.
+ intros;
+ unfold update;
+ apply (bool_elim ? (eqb b a) ? ?); simplify; intros;
+  [ rewrite > (eqb_true_to_eq ? ? H);
+    reflexivity
+  | reflexivity
+  ]
+qed.
+
+lemma inj_update:
+ ∀s,s',a,v,b. (a ≠ b → s b = s' b) → update s a v b = update s' a v b.
+ intros;
+ unfold update;
+ apply (bool_elim ? (eqb b a) ? ?); simplify; intros;
+  [ reflexivity
+  | apply H;
+    intro;
+    autobatch
+  ]
+qed.
+
+lemma not_eq_a_b_to_eq_update_a_b: ∀s,a,b,v. a ≠ b → update s a v b = s b.
+ intros;
+ unfold update;
+ rewrite > not_eq_to_eqb_false; simplify;
+  [ reflexivity
+  | intro;
+    autobatch
+  ]
+qed.
+
 definition mmod16 ≝ λn. nat_of_byte (byte_of_nat n).
 
 definition tick ≝