More Q stuff organized in a coherent way.

[helm.git] / helm / software / matita / library / Q / frac.ma

diff --git a/helm/software/matita/library/Q/frac.ma b/helm/software/matita/library/Q/frac.ma
index 334f1c868162802fc40b414f2c27aeaba22de525..de156e2db3881836b774e74ee0e26569906ffc45 100644 (file)
--- a/helm/software/matita/library/Q/frac.ma
+++ b/helm/software/matita/library/Q/frac.ma
@@ -12,49 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/Q/frac".
-
-include "nat/factorization.ma".
-include "Q/q.ma".
-
-
-definition numeratorQ \def
-\lambda q.match q with
-  [OQ \Rightarrow nfa_zero
-  |Qpos r \Rightarrow 
-    match r with 
-    [one \Rightarrow nfa_one
-    |frac x \Rightarrow numerator x
-    ]
-  |Qneg r \Rightarrow 
-    match r with 
-    [one \Rightarrow nfa_one
-    |frac x \Rightarrow numerator x
-    ]
-  ]
-.
-
-definition nat_fact_all_to_Q \def
-\lambda n.
-  match n with
-  [nfa_zero \Rightarrow OQ
-  |nfa_one \Rightarrow Qpos one
-  |nfa_proper l \Rightarrow Qpos (frac (nat_fact_to_fraction l))
-  ]
-.
-
-theorem numeratorQ_nat_fact_all_to_Q: \forall g.
-numeratorQ (nat_fact_all_to_Q g) = g.
-intro.cases g
-  [reflexivity
-  |reflexivity
-  |apply numerator_nat_fact_to_fraction
-  ]
-qed.
-
-definition nat_to_Q \def
-\lambda n. nat_fact_all_to_Q (factorize n).
-
+(*
 let rec nat_fact_to_fraction_inv l \def
   match l with
   [nf_last a \Rightarrow nn a
@@ -63,8 +21,6 @@ let rec nat_fact_to_fraction_inv l \def
   ]
 .
 
-
-(*
 definition nat_fact_all_to_Q_inv \def
 \lambda n.
   match n with
@@ -78,13 +34,6 @@ definition nat_to_Q_inv \def
 \lambda n. nat_fact_all_to_Q_inv (factorize n).
 *)
 
-definition Qinv \def
-\lambda q.match q with
-[OQ \Rightarrow OQ
-|Qpos r \Rightarrow Qpos (rinv r)
-|Qneg r \Rightarrow Qneg (rinv r)
-].
-
 definition frac:nat \to nat \to Q \def
 \lambda p,q. Qtimes (nat_to_Q p) (Qinv (nat_to_Q q)).
 
@@ -96,36 +45,6 @@ theorem rtimes_onel: \forall r.rtimes one r = r.
 intro.cases r;reflexivity.
 qed.
 
-definition Qone \def Qpos one.
-
-theorem Qtimes_Qoner: \forall q.Qtimes q Qone = q.
-intro.cases q
-  [reflexivity
-  |cases r
-    [reflexivity
-    |reflexivity
-    ]
-  |cases r
-    [reflexivity
-    |reflexivity
-    ]
-  ]
-qed.
-
-theorem Qtimes_Qonel: \forall q.Qtimes Qone q = q.
-intros.cases q
-  [reflexivity
-  |cases r
-    [reflexivity
-    |reflexivity
-    ]
-  |cases r
-    [reflexivity
-    |reflexivity
-    ]
-  ]
-qed.
-
 let rec times_f h g \def
   match h with
   [nf_last a \Rightarrow 
@@ -359,7 +278,7 @@ rtimes (rtimes (Z_to_ratio z) (frac f1)) (frac f2)
 =rtimes (Z_to_ratio z) (rtimes (frac f1) (frac f2)).
 intros 2.elim f1
   [elim f2
-    [ change with
+    [change with
      (rtimes (rtimes (Z_to_ratio z) (Z_to_ratio (pos n))) (Z_to_ratio (pos n1))
       =rtimes (Z_to_ratio z) (rtimes (Z_to_ratio (pos n)) (Z_to_ratio (pos n1)))).
      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
@@ -745,8 +664,7 @@ cases x
   [simplify in ⊢ (? ? % ?).rewrite > Qtimes_OQ.reflexivity
   |elim y
     [reflexivity
-    |simplify.alias id "symmetric_rtimes" = "cic:/matita/Q/times/symmetric_rtimes.con".
-rewrite > symmetric_rtimes.reflexivity
+    |simplify.rewrite > symmetric_rtimes.reflexivity
     |simplify.rewrite > symmetric_rtimes.reflexivity
     ]
   |elim y
@@ -761,8 +679,7 @@ theorem Qtimes_Qinv: \forall q. q \neq OQ \to Qtimes q (Qinv q) = Qone.
 intro.
 cases q;intro
   [elim H.reflexivity
-  |simplify.alias id "rtimes_rinv" = "cic:/matita/Q/times/rtimes_rinv.con".
-rewrite > rtimes_rinv.reflexivity
+  |simplify.rewrite > rtimes_rinv.reflexivity
   |simplify.rewrite > rtimes_rinv.reflexivity
   ]
 qed.
@@ -790,7 +707,7 @@ p \neq OQ \to q \neq OQ \to
 Qinv(Qtimes p q) =
 Qtimes (Qinv p) (Qinv q).
 intros.
-rewrite < Qtimes_Qonel in ⊢ (? ? ? %).
+rewrite < Qtimes_Qone_q in ⊢ (? ? ? %).
 rewrite < (Qtimes_Qinv (Qtimes p q))
   [lapply (Qtimes_Qinv ? H).
    lapply (Qtimes_Qinv ? H1). 
@@ -801,9 +718,9 @@ rewrite < (Qtimes_Qinv (Qtimes p q))
    rewrite < symmetric_Qtimes in ⊢ (? ? ? (? ? (? ? (? % ?)))).
    rewrite > associative_Qtimes in ⊢ (? ? ? (? ? (? ? %))).
    rewrite > Hletin1.
-   rewrite > Qtimes_Qoner.
+   rewrite > Qtimes_q_Qone.
    rewrite > Hletin.
-   rewrite > Qtimes_Qoner.
+   rewrite > Qtimes_q_Qone.
    reflexivity
   |intro.
    elim (eq_Qtimes_OQ_to_eq_OQ ? ? H2)
@@ -888,7 +805,7 @@ intro.elim f
           |generalize in match H.
            rewrite > H2.
            rewrite > H3.
-           rewrite > Qtimes_Qoner.
+           rewrite > Qtimes_q_Qone.
            intro.
            destruct H1.
            assumption
@@ -911,7 +828,7 @@ intro.elim f
           |generalize in match H.
            rewrite > H2.
            rewrite > H3.
-           rewrite > Qtimes_Qoner.
+           rewrite > Qtimes_q_Qone.
            intro.
            destruct H1.
            assumption
@@ -934,7 +851,7 @@ intro.elim f
           |generalize in match H.
            rewrite > H2.
            rewrite > H3.
-           rewrite > Qtimes_Qoner.
+           rewrite > Qtimes_q_Qone.
            intro.
            destruct H1.
            assumption