Changeset 891 for src/utilities/binary

Timestamp:

Jun 7, 2011, 4:53:53 PM (10 years ago)

Author:

campbell

Message:

Revise proofs affected by recent matita change.

Location:

src/utilities/binary

Files:

• Z.ma (modified) (8 diffs)
• positive.ma (modified) (1 diff)

src/utilities/binary/Z.ma

@@ -333 +333 @@
 |#n cases y;
    [@nmk #H elim (not_eq_OZ_pos n);#H2 /2/;
-   |#m @eqb_elim
+   |#m normalize @eqb_elim
       [//
       | * #H % #H' @H @(match H' return λx.λ_.n=match x with [pos m ⇒ m | neg m ⇒ m | OZ ⇒ one ] with [refl ⇒ ?]) //
@@ -341 +341 @@
    [@nmk #H elim (not_eq_OZ_neg n);#H /2/;
    |#m @nmk #H destruct
-   |#m @eqb_elim
+   |#m normalize @eqb_elim
       [//
       | * #H % #H' @H @(match H' return λx.λ_.n=match x with [pos m ⇒ m | neg m ⇒ m | OZ ⇒ one ] with [refl ⇒ ?]) //
@@ -458 +458 @@
 
 theorem sym_Zplus : ∀x,y:Z. x+y = y+x.
-#x #y cases x;
-[>(Zplus_z_OZ ?) (*XXX*) //
+#x #y cases x
+[>Zplus_z_OZ //
 |#p cases y
    [//
-   |normalize;//
-   |#q normalize;>(pos_compare_n_m_m_n ??) (*XXX*)
+   |//
+   |#q whd in ⊢ (??%%) >pos_compare_n_m_m_n
       cases (pos_compare q p);//]
 |#p cases y
    [//;
-   |#q normalize;>(pos_compare_n_m_m_n ??) (*XXX*)
+   |#q whd in ⊢ (??%%) >pos_compare_n_m_m_n
       cases (pos_compare q p);//
    |normalize;//]
@@ -503 +503 @@
   ∀n,m. (pos n)+(neg m) = (Zsucc (pos n))+(Zpred (neg m)).
 #n #m
-normalize;
+whd in ⊢ (??%%) 
 <(pos_compare_S_S …)
->(partialminus_S_S …)
->(partialminus_S_S …) //;
+>(minus_S_S …)
+>(minus_S_S …) //;
 qed.
 
@@ -521 +521 @@
 #n #m @(pos_cases … n) @(pos_cases … m)
 [ //;
-| #m' >(Zpred_pos_succ …)
-    >(?:pos (succ m') = Zsucc (pos m')) //;
-| #m' normalize; >(pos_compare_S_one …) normalize;
-    >(partial_minus_S_one …) normalize; >(pos_nonzero …)
-    <(pred_succ_n …) //;
-| #m' #n' normalize; <(pos_compare_S_S …)
-    >(partialminus_S_S …)
-    >(partialminus_S_S …)
-    >(pos_nonzero …)
-    >(pos_nonzero …)
-    <(pred_succ_n …)
-    <(pred_succ_n …)
+| #m' >Zpred_pos_succ
+    change in ⊢ (??(??%)?) with (Zsucc (pos m'))
+    <Zpred_Zplus_neg_O >Zpred_Zsucc @refl
+| #m' whd in ⊢ (??%%) >pos_compare_S_one normalize;
+    >partial_minus_S_one normalize; >pos_nonzero
+    <pred_succ_n //
+| #m' #n' whd in ⊢ (??%%) <pos_compare_S_S
+    >minus_S_S
+    >minus_S_S normalize
+    >pos_nonzero
+    >pos_nonzero
+    <pred_succ_n
+    <pred_succ_n
     normalize; //;
 ] qed. 
@@ -600 +601 @@
 
 lemma neg_pos_succ: ∀n,m:Pos. neg (succ n) + pos (succ m) = neg n + pos m.
-#n #m normalize; <(pos_compare_S_S …)
->(partialminus_S_S …)
->(partialminus_S_S …)
+#n #m whd in ⊢ (??%%) <pos_compare_S_S
+>minus_S_S >minus_S_S
  //; qed.
 
@@ -676 +676 @@
 #x #y cases x
 [cases y;//
-|*:#n cases y;//;#m normalize;@pos_compare_elim normalize;//]
+|*:#n cases y;//;#m whd in ⊢ (??(?%)%) @pos_compare_elim normalize;//]
 qed.
 
@@ -686 +686 @@
 #x cases x
 [//
-|*:#n normalize;>(pos_compare_n_n ?) //]
+|*:#n whd in ⊢ (??%?) >pos_compare_n_n //]
 qed.
 

src/utilities/binary/positive.ma

@@ -1095 +1095 @@
   [ LT ⇒ n < m
   | EQ ⇒ n = m
-  | GT ⇒ m < n ]) ?????) (* FIXME: don't want to put all these ?, especially when … does not work! *)
+  | GT ⇒ m < n ]))
 [1,2:@pos_cases
   [ 1,3: /2/;
   | 2,4: #m' cases m'; //;
   ]
-|#n1 #m1 normalize;<(pos_compare_S_S …) cases (pos_compare n1 m1);
-   [1,3:normalize;#IH @le_succ_succ //;
-   |normalize;#IH >IH //]
+|#n1 #m1 <pos_compare_S_S cases (pos_compare n1 m1)
+   [1,3: #IH @le_succ_succ //
+   | #IH >IH //
+   ]
+]
 qed.