X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2FQ%2Fq.ma;h=6e3639f6e726b27ad9dfb37b0004c8abbaa18748;hb=7deb67bf075a845f84d51ac4757a5c69b779487d;hp=1ff2adcd8dfa0bf99462486ce3641519849e0df7;hpb=b8c6dd0220fba9ebed2d51d5808790b5949177ea;p=helm.git

diff --git a/helm/matita/library/Q/q.ma b/helm/matita/library/Q/q.ma
index 1ff2adcd8..6e3639f6e 100644
--- a/helm/matita/library/Q/q.ma
+++ b/helm/matita/library/Q/q.ma
@@ -117,7 +117,7 @@ change with (ftl (cons x f)) = (ftl (cons y g)).
 apply eq_f.assumption.
 qed.
 
-theorem not_eq_pp_nn: \forall n,m:nat. \lnot (pp n) = (nn m).
+theorem not_eq_pp_nn: \forall n,m:nat. pp n \neq nn m.
 intros.simplify. intro.
 change with match (pp n) with
 [ (pp n) \Rightarrow False
@@ -129,7 +129,7 @@ qed.
 
 theorem not_eq_pp_cons: 
 \forall n:nat.\forall x:Z. \forall f:fraction. 
-\lnot (pp n) = (cons x f).
+pp n \neq cons x f.
 intros.simplify. intro.
 change with match (pp n) with
 [ (pp n) \Rightarrow False
@@ -141,7 +141,7 @@ qed.
 
 theorem not_eq_nn_cons: 
 \forall n:nat.\forall x:Z. \forall f:fraction. 
-\lnot (nn n) = (cons x f).
+nn n \neq cons x f.
 intros.simplify. intro.
 change with match (nn n) with
 [ (pp n) \Rightarrow True
@@ -154,23 +154,23 @@ qed.
 theorem decidable_eq_fraction: \forall f,g:fraction.
 decidable (f = g).
 intros.simplify.
-apply fraction_elim2 (\lambda f,g. Or (f=g) (f=g \to False)).
+apply fraction_elim2 (\lambda f,g. f=g \lor (f=g \to False)).
   intros.elim g1.
-    elim ((decidable_eq_nat n n1) : Or (n=n1) (n=n1 \to False)).
+    elim ((decidable_eq_nat n n1) : n=n1 \lor (n=n1 \to False)).
       left.apply eq_f. assumption.
       right.intro.apply H.apply injective_pp.assumption.
     right.apply not_eq_pp_nn.
     right.apply not_eq_pp_cons.
   intros. elim g1.
       right.intro.apply not_eq_pp_nn n1 n.apply sym_eq. assumption.
-      elim ((decidable_eq_nat n n1) : Or (n=n1) (n=n1 \to False)).
+      elim ((decidable_eq_nat n n1) : n=n1 \lor (n=n1 \to False)).
         left. apply eq_f. assumption.
         right.intro.apply H.apply injective_nn.assumption.
       right.apply not_eq_nn_cons.
   intros.right.intro.apply not_eq_pp_cons m x f1.apply sym_eq.assumption.
   intros.right.intro.apply not_eq_nn_cons m x f1.apply sym_eq.assumption.
   intros.elim H.
-    elim ((decidable_eq_Z x y) : Or (x=y) (x=y \to False)).
+    elim ((decidable_eq_Z x y) : x=y \lor (x=y \to False)).
       left.apply eq_f2.assumption.
       assumption.
     right.intro.apply H2.apply eq_cons_to_eq1 f1 g1.assumption.
@@ -180,11 +180,11 @@ qed.
 theorem eqfb_to_Prop: \forall f,g:fraction.
 match (eqfb f g) with
 [true \Rightarrow f=g
-|false \Rightarrow \lnot f=g].
+|false \Rightarrow f \neq g].
 intros.apply fraction_elim2 
 (\lambda f,g.match (eqfb f g) with
 [true \Rightarrow f=g
-|false \Rightarrow \lnot f=g]).
+|false \Rightarrow f \neq g]).
   intros.elim g1.
     simplify.apply eqb_elim.
       intro.simplify.apply eq_f.assumption.
@@ -225,65 +225,65 @@ let rec ftimes f g \def
   match f with
   [ (pp n) \Rightarrow 
     match g with
-    [(pp m) \Rightarrow Z_to_ratio (Zplus (pos n) (pos m))
-    | (nn m) \Rightarrow Z_to_ratio (Zplus (pos n) (neg m))
-    | (cons y g1) \Rightarrow frac (cons (Zplus (pos n) y) g1)]
+    [(pp m) \Rightarrow Z_to_ratio (pos n + pos m)
+    | (nn m) \Rightarrow Z_to_ratio (pos n + neg m)
+    | (cons y g1) \Rightarrow frac (cons (pos n + y) g1)]
   | (nn n) \Rightarrow 
     match g with
-    [(pp m) \Rightarrow Z_to_ratio (Zplus (neg n) (pos m))
-    | (nn m) \Rightarrow Z_to_ratio (Zplus (neg n) (neg m))
-    | (cons y g1) \Rightarrow frac (cons (Zplus (neg n) y) g1)]
+    [(pp m) \Rightarrow Z_to_ratio (neg n + pos m)
+    | (nn m) \Rightarrow Z_to_ratio (neg n + neg m)
+    | (cons y g1) \Rightarrow frac (cons (neg n + y) g1)]
   | (cons x f1) \Rightarrow
     match g with
-    [ (pp m) \Rightarrow frac (cons (Zplus x (pos m)) f1)
-    | (nn m) \Rightarrow frac (cons (Zplus x (neg m)) f1)
+    [ (pp m) \Rightarrow frac (cons (x + pos m) f1)
+    | (nn m) \Rightarrow frac (cons (x + neg m) f1)
     | (cons y g1) \Rightarrow 
       match ftimes f1 g1 with
-        [ one \Rightarrow Z_to_ratio (Zplus x y)
-        | (frac h) \Rightarrow frac (cons (Zplus x y) h)]]].
+        [ one \Rightarrow Z_to_ratio (x + y)
+        | (frac h) \Rightarrow frac (cons (x + y) h)]]].
         
 theorem symmetric2_ftimes: symmetric2 fraction ratio ftimes.
 simplify. intros.apply fraction_elim2 (\lambda f,g.ftimes f g = ftimes g f).
   intros.elim g.
-    change with Z_to_ratio (Zplus (pos n) (pos n1)) = Z_to_ratio (Zplus (pos n1) (pos n)).
+    change with Z_to_ratio (pos n + pos n1) = Z_to_ratio (pos n1 + pos n).
      apply eq_f.apply sym_Zplus.
-    change with Z_to_ratio (Zplus (pos n) (neg n1)) = Z_to_ratio (Zplus (neg n1) (pos n)).
+    change with Z_to_ratio (pos n + neg n1) = Z_to_ratio (neg n1 + pos n).
      apply eq_f.apply sym_Zplus.
-    change with frac (cons (Zplus (pos n) z) f) = frac (cons (Zplus z (pos n)) f).
+    change with frac (cons (pos n + z) f) = frac (cons (z + pos n) f).
      rewrite < sym_Zplus.reflexivity.
   intros.elim g.
-    change with Z_to_ratio (Zplus (neg n) (pos n1)) = Z_to_ratio (Zplus (pos n1) (neg n)).
+    change with Z_to_ratio (neg n + pos n1) = Z_to_ratio (pos n1 + neg n).
      apply eq_f.apply sym_Zplus.
-    change with Z_to_ratio (Zplus (neg n) (neg n1)) = Z_to_ratio (Zplus (neg n1) (neg n)).
+    change with Z_to_ratio (neg n + neg n1) = Z_to_ratio (neg n1 + neg n).
      apply eq_f.apply sym_Zplus.
-    change with frac (cons (Zplus (neg n) z) f) = frac (cons (Zplus z (neg n)) f).
+    change with frac (cons (neg n + z) f) = frac (cons (z + neg n) f).
      rewrite < sym_Zplus.reflexivity.
-  intros.change with frac (cons (Zplus x1 (pos m)) f) = frac (cons (Zplus (pos m) x1) f).
+  intros.change with frac (cons (x1 + pos m) f) = frac (cons (pos m + x1) f).
    rewrite < sym_Zplus.reflexivity.
-  intros.change with frac (cons (Zplus x1 (neg m)) f) = frac (cons (Zplus (neg m) x1) f).
+  intros.change with frac (cons (x1 + neg m) f) = frac (cons (neg m + x1) f).
    rewrite < sym_Zplus.reflexivity.
   intros.
    change with 
    match ftimes f g with
-   [ one \Rightarrow Z_to_ratio (Zplus x1 y1)
-   | (frac h) \Rightarrow frac (cons (Zplus x1 y1) h)] =
+   [ one \Rightarrow Z_to_ratio (x1 + y1)
+   | (frac h) \Rightarrow frac (cons (x1 + y1) h)] =
    match ftimes g f with
-   [ one \Rightarrow Z_to_ratio (Zplus y1 x1)
-   | (frac h) \Rightarrow frac (cons (Zplus y1 x1) h)].
+   [ one \Rightarrow Z_to_ratio (y1 + x1)
+   | (frac h) \Rightarrow frac (cons (y1 + x1) h)].
     rewrite < H.rewrite < sym_Zplus.reflexivity.
 qed.
 
 theorem ftimes_finv : \forall f:fraction. ftimes f (finv f) = one.
 intro.elim f.
-  change with Z_to_ratio (Zplus (pos n) (Zopp (pos n))) = one.
+  change with Z_to_ratio (pos n + - (pos n)) = one.
    rewrite > Zplus_Zopp.reflexivity.
-  change with Z_to_ratio (Zplus (neg n) (Zopp (neg n))) = one.
+  change with Z_to_ratio (neg n + - (neg n)) = one.
    rewrite > Zplus_Zopp.reflexivity.
 (* again: we would need something to help finding the right change *)
   change with 
   match ftimes f1 (finv f1) with
-  [ one \Rightarrow Z_to_ratio (Zplus z (Zopp z))
-  | (frac h) \Rightarrow frac (cons (Zplus z (Zopp z)) h)] = one.
+  [ one \Rightarrow Z_to_ratio (z + - z)
+  | (frac h) \Rightarrow frac (cons (z + - z) h)] = one.
   rewrite > H.rewrite > Zplus_Zopp.reflexivity.
 qed.