All sub-proofs about "update" closed.

diff --git a/matita/library/assembly/test.ma b/matita/library/assembly/test.ma
index 98eb48d91604c360b43608a17a72ebb27e1be075..b2494615be6dc7444ac87f04c156f780dba2ca1a 100644 (file)
--- a/matita/library/assembly/test.ma
+++ b/matita/library/assembly/test.ma
@@ -118,7 +118,21 @@ lemma loop_invariant':
       normalize;
       reflexivity 
     | intro;
-      elim daemon
+      rewrite < minus_n_O;
+      normalize in ⊢ (? ? (? (? ? %) ?) ?);
+      whd in ⊢ (? ? % ?);
+      change in ⊢ (? ? % ?) with (update (mult_memory x y) 32 (mk_byte x0 x0) a);
+      change in ⊢ (? ? ? %) with (update (update (update (mult_memory x y) 30 x) 31
+        (byte_of_nat y)) 32 (byte_of_nat 0) a);
+      change in ⊢ (? ? ? (? (? (? ? ? %) ? ?) ? ? ?)) with (mult_memory x y 30);
+      rewrite > byte_of_nat_nat_of_byte;
+      change in ⊢ (? ? ? (? (? ? ? %) ? ? ?)) with (mult_memory x y 31);
+      apply inj_update;
+      intro;
+      rewrite > (eq_update_s_a_sa (update (mult_memory x y) 30 (mult_memory x y 30))
+       31 a) in ⊢ (? ? ? %);
+      rewrite > eq_update_s_a_sa;
+      reflexivity
     ]
   | cut (5 + 23 * S n = 5 + 23 * n + 23);
     [ letin K ≝ (breakpoint (mult_status x y) (5 + 23 * n) 23); clearbody K;
@@ -249,7 +263,31 @@ lemma loop_invariant':
                              plusbytec (byte_of_nat (x*n)) x);
               reflexivity
             |6: intro;
-              elim daemon
+              simplify in ⊢ (? ? ? %);
+              change in ⊢ (? ? % ?) with
+               (update
+                (update
+                 (update
+                  (update (update (mult_memory x y) 30 x) 31
+                   (byte_of_nat (S (nat_of_byte y-S n)))) 32 (byte_of_nat (nat_of_byte x*n))) 31
+                    (byte_of_nat (nat_of_byte y-S n)))
+                   (nat_of_byte
+                    (update
+                     (update
+                      (update (update (mult_memory x y) 30 x) 31
+                       (byte_of_nat (S (nat_of_byte y-S n)))) 32 (byte_of_nat (nat_of_byte x*n))) 31
+                      (byte_of_nat (nat_of_byte y-S n)) 15))
+                     (byte_of_nat (nat_of_byte x*S n)) a);
+              normalize in ⊢ (? ? (? ? % ? ?) ?);
+              apply inj_update;
+              intro;
+              apply inj_update;
+              intro;
+              rewrite > not_eq_a_b_to_eq_update_a_b in ⊢ (? ? % ?); [2: apply H | ];
+              rewrite > not_eq_a_b_to_eq_update_a_b in ⊢ (? ? % ?);
+               [ reflexivity
+               | assumption
+               ]
             ]
          | exists;
             [ apply (y - S n)
@@ -264,7 +302,9 @@ lemma loop_invariant':
          ]
       ]
     | rewrite > associative_plus;
-      autobatch paramodulation
+      rewrite < times_n_Sm;
+      rewrite > sym_plus in ⊢ (? ? ? (? ? %));
+      reflexivity
     ] 
   ]   
 qed.

diff --git a/matita/library/assembly/vm.ma b/matita/library/assembly/vm.ma
index dac755c82c54484fb506596c11a7435a5e0eb857..239146a07526445c12d662592117e32c26358b2e 100644 (file)
--- a/matita/library/assembly/vm.ma
+++ b/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 ≝