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

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

diff --git a/helm/software/matita/library/assembly/byte.ma b/helm/software/matita/library/assembly/byte.ma
index d0f1ada88783e3c5af799e126cd4c70764595eb9..4d050e0cda93fadd1d08b10b07b5268cbde01e48 100644 (file)
--- a/helm/software/matita/library/assembly/byte.ma
+++ b/helm/software/matita/library/assembly/byte.ma
@@ -87,8 +87,23 @@ lemma nat_of_byte_byte_of_nat: ∀n. nat_of_byte (byte_of_nat n) = n \mod 256.
   ].
 qed.
 
-axiom eq_nat_of_byte_n_nat_of_byte_mod_n_256:
+lemma eq_nat_of_byte_n_nat_of_byte_mod_n_256:
  ∀n. byte_of_nat n = byte_of_nat (n \mod 256).
+ intro;
+ unfold byte_of_nat;
+ apply eq_f2;
+  [ rewrite > exadecimal_of_nat_mod in ⊢ (? ? % ?);
+    rewrite > exadecimal_of_nat_mod in ⊢ (? ? ? %);
+    apply eq_f;
+    elim daemon
+  | rewrite > exadecimal_of_nat_mod;
+    rewrite > exadecimal_of_nat_mod in ⊢ (? ? ? %);
+    rewrite > divides_to_eq_mod_mod_mod;
+     [ reflexivity
+     | autobatch
+     ]
+  ]
+qed.
 
 lemma plusbyte_ok:
  ∀b1,b2,c.
@@ -163,7 +178,12 @@ lemma plusbytenc_O_x:
  reflexivity.
 qed.
 
-axiom eq_nat_of_byte_mod: ∀b. nat_of_byte b = nat_of_byte b \mod 256.
+lemma eq_nat_of_byte_mod: ∀b. nat_of_byte b = nat_of_byte b \mod 256.
+ intro;
+ lapply (lt_nat_of_byte_256 b);
+ rewrite > (lt_to_eq_mod ? ? Hletin) in ⊢ (? ? ? %);
+ reflexivity.
+qed.
 
 theorem plusbytenc_ok:
  ∀b1,b2:byte. nat_of_byte (plusbytenc b1 b2) = (b1 + b2) \mod 256.
@@ -237,6 +257,25 @@ qed.
 
 lemma eq_bpred_S_a_a:
  ∀a. a < 255 → bpred (byte_of_nat (S a)) = byte_of_nat a.
+(*
+ intros;
+ unfold bpred;
+ apply (bool_elim ? (eqex (bl (byte_of_nat (S a))) x0)); intros;
+  [ change with (mk_byte (xpred (bh (byte_of_nat (S a)))) (xpred (bl (byte_of_nat (S a))))
+     = byte_of_nat a);
+    rewrite > (eqex_true_to_eq ? ? H1);
+    normalize in ⊢ (? ? (? ? %) ?);
+    unfold byte_of_nat;
+    change with (mk_byte (xpred (exadecimal_of_nat (S a/16))) xF =
+                 mk_byte (exadecimal_of_nat (a/16)) (exadecimal_of_nat a));
+    
+    
+  |
+ change in ⊢ (? ? match ? % ? in bool return ? with [true\rArr ?|false\rArr ?] ?);
+ unfold byte_of_nat;
+ unfold bpred;
+ simplify;
+*)
 elim daemon. (*
  intros;
  unfold byte_of_nat;
@@ -255,11 +294,13 @@ lemma plusbytenc_S:
  rewrite < byte_of_nat_nat_of_byte;
  rewrite > (plusbytenc_ok (byte_of_nat (x*n)) x);
  rewrite < times_n_Sm;
- rewrite > mod_plus;
- rewrite < eq_nat_of_byte_mod in ⊢ (? ? (? (? (? ? %) ?)) ?);
- rewrite > nat_of_byte_byte_of_nat;
- rewrite < mod_mod in ⊢ (? ? (? (? (? % ?) ?)) ?);
-elim daemon.
+ rewrite > nat_of_byte_byte_of_nat in ⊢ (? ? (? (? (? % ?) ?)) ?);
+ rewrite > eq_nat_of_byte_n_nat_of_byte_mod_n_256 in ⊢ (? ? ? %);
+ rewrite > mod_plus in ⊢ (? ? (? %) ?);
+ rewrite > mod_plus in ⊢ (? ? ? (? %));
+ rewrite < mod_mod in ⊢ (? ? (? (? (? % ?) ?)) ?); [2: autobatch | ];
+ rewrite > sym_plus in ⊢ (? ? (? (? % ?)) ?);
+ reflexivity.
 qed. 
 
 lemma eq_plusbytec_x0_x0_x_false: