More daemons closed. A couple left in byte and many in extras.

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

diff --git a/helm/software/matita/library/assembly/test.ma b/helm/software/matita/library/assembly/test.ma
index 98eb48d91604c360b43608a17a72ebb27e1be075..1fd030efb1bb998c0302fdb3bab8c8f7695ef905 100644 (file)
--- a/helm/software/matita/library/assembly/test.ma
+++ b/helm/software/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;
@@ -200,7 +214,9 @@ lemma loop_invariant':
            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
            normalize in ⊢ (? ? (? (? ? ? ? ? ? (? ? % ?) ?) ?) ?);
            cut (y - S n = a);
-            [2: elim daemon | ];
+            [2: rewrite > eq_minus_S_pred;
+                rewrite > H2;
+                reflexivity | ];
            rewrite < Hcut; clear Hcut; clear H3; clear H2; clear a;          
            (* instruction ADDd *)
            letin K ≝
@@ -249,7 +265,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 +304,9 @@ lemma loop_invariant':
          ]
       ]
     | rewrite > associative_plus;
-      autobatch paramodulation
+      rewrite < times_n_Sm;
+      rewrite > sym_plus in ⊢ (? ? ? (? ? %));
+      reflexivity
     ] 
   ]   
 qed.
@@ -290,7 +332,15 @@ theorem test_x_y:
      | rewrite < minus_n_n;
        apply status_eq;
         [1,2,3,4,5,7: normalize; reflexivity
-        | elim daemon
+        | intro;
+          change with (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat O)) 32
+(byte_of_nat (nat_of_byte x*nat_of_byte y)) a =
+           update (update (mult_memory x y) 31 (mk_byte x0 x0)) 32
+(byte_of_nat (nat_of_byte x*nat_of_byte y)) a);
+          apply inj_update; intro;
+          apply inj_update; intro;
+          change in ⊢ (? ? (? ? ? % ?) ?) with (mult_memory x y 30);
+          apply eq_update_s_a_sa
         ]
      ]
   ].