X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2FQ%2Fq.ma;h=340154979777529f94387cd1c630c6234cf21ab5;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=f04603f15f0b129423e8bd5a0fe289f2495b7cbc;hpb=373b88228a8f9a6b4b4dcf781bc166865f89f43d;p=helm.git

diff --git a/helm/matita/library/Q/q.ma b/helm/matita/library/Q/q.ma
index f04603f15..340154979 100644
--- a/helm/matita/library/Q/q.ma
+++ b/helm/matita/library/Q/q.ma
@@ -92,33 +92,33 @@ definition ftl \def
     | (cons x f) \Rightarrow f].
     
 theorem injective_pp : injective nat fraction pp.
-simplify.intros.
-change with (aux (pp x)) = (aux (pp y)).
+unfold injective.intros.
+change with ((aux (pp x)) = (aux (pp y))).
 apply eq_f.assumption.
 qed.
 
 theorem injective_nn : injective nat fraction nn.
-simplify.intros.
-change with (aux (nn x)) = (aux (nn y)).
+unfold injective.intros.
+change with ((aux (nn x)) = (aux (nn y))).
 apply eq_f.assumption.
 qed.
 
 theorem eq_cons_to_eq1: \forall f,g:fraction.\forall x,y:Z. 
 (cons x f) = (cons y g) \to x = y.
 intros.
-change with (fhd (cons x f)) = (fhd (cons y g)).
+change with ((fhd (cons x f)) = (fhd (cons y g))).
 apply eq_f.assumption.
 qed.
 
 theorem eq_cons_to_eq2: \forall x,y:Z.\forall f,g:fraction.
 (cons x f) = (cons y g) \to f = g.
 intros.
-change with (ftl (cons x f)) = (ftl (cons y g)).
+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).
-intros.simplify. intro.
+theorem not_eq_pp_nn: \forall n,m:nat. pp n \neq nn m.
+intros.unfold Not. intro.
 change with match (pp n) with
 [ (pp n) \Rightarrow False
 | (nn n) \Rightarrow True
@@ -129,8 +129,8 @@ qed.
 
 theorem not_eq_pp_cons: 
 \forall n:nat.\forall x:Z. \forall f:fraction. 
-\lnot (pp n) = (cons x f).
-intros.simplify. intro.
+pp n \neq cons x f.
+intros.unfold Not. intro.
 change with match (pp n) with
 [ (pp n) \Rightarrow False
 | (nn n) \Rightarrow True
@@ -141,8 +141,8 @@ qed.
 
 theorem not_eq_nn_cons: 
 \forall n:nat.\forall x:Z. \forall f:fraction. 
-\lnot (nn n) = (cons x f).
-intros.simplify. intro.
+nn n \neq cons x f.
+intros.unfold Not. intro.
 change with match (nn n) with
 [ (pp n) \Rightarrow True
 | (nn n) \Rightarrow False
@@ -153,8 +153,8 @@ qed.
 
 theorem decidable_eq_fraction: \forall f,g:fraction.
 decidable (f = g).
-intros.simplify.
-apply fraction_elim2 (\lambda f,g. f=g \lor (f=g \to False)).
+intros.unfold decidable.
+apply (fraction_elim2 (\lambda f,g. f=g \lor (f=g \to False))).
   intros.elim g1.
     elim ((decidable_eq_nat n n1) : n=n1 \lor (n=n1 \to False)).
       left.apply eq_f. assumption.
@@ -162,42 +162,42 @@ apply fraction_elim2 (\lambda f,g. f=g \lor (f=g \to False)).
     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.
+      right.intro.apply (not_eq_pp_nn n1 n).apply sym_eq. assumption.
       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.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) : 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.
-    right.intro.apply H1.apply eq_cons_to_eq2 x y f1 g1.assumption.
+    right.intro.apply H2.apply (eq_cons_to_eq1 f1 g1).assumption.
+    right.intro.apply H1.apply (eq_cons_to_eq2 x y f1 g1).assumption.
 qed.
 
 theorem eqfb_to_Prop: \forall f,g:fraction.
 match (eqfb f g) with
 [true \Rightarrow f=g
-|false \Rightarrow \lnot f=g].
-intros.apply fraction_elim2 
+|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.
-      intro.simplify.intro.apply H.apply injective_pp.assumption.
+      intro.simplify.unfold Not.intro.apply H.apply injective_pp.assumption.
     simplify.apply not_eq_pp_nn.
     simplify.apply not_eq_pp_cons.
   intros.elim g1.
-    simplify.intro.apply not_eq_pp_nn n1 n.apply sym_eq. assumption.
+    simplify.unfold Not.intro.apply (not_eq_pp_nn n1 n).apply sym_eq. assumption.
     simplify.apply eqb_elim.intro.simplify.apply eq_f.assumption.
-    intro.simplify.intro.apply H.apply injective_nn.assumption.
+    intro.simplify.unfold Not.intro.apply H.apply injective_nn.assumption.
   simplify.apply not_eq_nn_cons.
-  intros.simplify.intro.apply not_eq_pp_cons m x f1.apply sym_eq. assumption.
-  intros.simplify.intro.apply not_eq_nn_cons m x f1.apply sym_eq. assumption.
+  intros.simplify.unfold Not.intro.apply (not_eq_pp_cons m x f1).apply sym_eq. assumption.
+  intros.simplify.unfold Not.intro.apply (not_eq_nn_cons m x f1).apply sym_eq. assumption.
   intros.
    change in match (eqfb (cons x f1) (cons y g1)) 
    with (andb (eqZb x y) (eqfb f1 g1)).
@@ -205,8 +205,8 @@ intros.apply fraction_elim2
       intro.generalize in match H.elim (eqfb f1 g1).
         simplify.apply eq_f2.assumption.
         apply H2.
-      simplify.intro.apply H2.apply eq_cons_to_eq2 x y.assumption.
-      intro.simplify.intro.apply H1.apply eq_cons_to_eq1 f1 g1.assumption.
+      simplify.unfold Not.intro.apply H2.apply (eq_cons_to_eq2 x y).assumption.
+      intro.simplify.unfold Not.intro.apply H1.apply (eq_cons_to_eq1 f1 g1).assumption.
 qed.
 
 let rec finv f \def
@@ -243,47 +243,47 @@ let rec ftimes f g \def
         | (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).
+unfold symmetric2. intros.apply (fraction_elim2 (\lambda f,g.ftimes f g = ftimes g f)).
   intros.elim g.
-    change with Z_to_ratio (pos n + pos n1) = Z_to_ratio (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 (pos n + neg n1) = Z_to_ratio (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 (pos n + z) f) = frac (cons (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 (neg n + pos n1) = Z_to_ratio (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 (neg n + neg n1) = Z_to_ratio (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 (neg n + z) f) = frac (cons (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 (x1 + pos m) f) = frac (cons (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 (x1 + neg m) f) = frac (cons (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
+   (match ftimes f g with
    [ 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 (y1 + x1)
-   | (frac h) \Rightarrow frac (cons (y1 + x1) h)].
+   | (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 (pos n + - (pos n)) = one.
+  change with (Z_to_ratio (pos n + - (pos n)) = one).
    rewrite > Zplus_Zopp.reflexivity.
-  change with Z_to_ratio (neg n + - (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
+  (match ftimes f1 (finv f1) with
   [ one \Rightarrow Z_to_ratio (z + - z)
-  | (frac h) \Rightarrow frac (cons (z + - z) h)] = one.
+  | (frac h) \Rightarrow frac (cons (z + - z) h)] = one).
   rewrite > H.rewrite > Zplus_Zopp.reflexivity.
 qed.
 
@@ -297,7 +297,7 @@ definition rtimes : ratio \to ratio \to ratio \def
       | (frac g) \Rightarrow ftimes f g]].
 
 theorem symmetric_rtimes : symmetric ratio rtimes.
-change with \forall r,s:ratio. rtimes r s = rtimes s r.
+change with (\forall r,s:ratio. rtimes r s = rtimes s r).
 intros.
 elim r. elim s.
 reflexivity.