First snapshot at trying to clean up the Q library.

[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 b5871dc94fb0397adf4c20872db631c859763bec..334f1c868162802fc40b414f2c27aeaba22de525 100644 (file)
--- a/helm/software/matita/library/Q/frac.ma
+++ b/helm/software/matita/library/Q/frac.ma
@@ -17,146 +17,16 @@ set "baseuri" "cic:/matita/Q/frac".
 include "nat/factorization.ma".
 include "Q/q.ma".
 
-(* transformation from nat_fact to fracion *)
-let rec nat_fact_to_fraction l \def
-  match l with
-  [nf_last a \Rightarrow pp a
-  |nf_cons a p \Rightarrow 
-    cons (Z_of_nat a) (nat_fact_to_fraction p)
-  ]
-.
-
-(* returns the numerator of a fraction in the form of a nat_fact_all *)
-let rec numerator f \def
-  match f with
-  [pp a \Rightarrow nfa_proper (nf_last a)
-  |nn a \Rightarrow nfa_one
-  |cons a l \Rightarrow
-    let n \def numerator l in
-    match n with
-    [nfa_zero \Rightarrow (* this case is vacuous *) nfa_zero
-    |nfa_one  \Rightarrow
-      match a with 
-      [OZ \Rightarrow nfa_one
-      |pos x \Rightarrow nfa_proper (nf_last x)
-      |neg x \Rightarrow nfa_one
-      ]
-    |nfa_proper g \Rightarrow
-      match a with 
-      [OZ \Rightarrow nfa_proper (nf_cons O g)
-      |pos x \Rightarrow nfa_proper (nf_cons (S x) g)
-      |neg x \Rightarrow nfa_proper (nf_cons O g)
-      ]
-    ]
-  ]
-.
-
-theorem not_eq_numerator_nfa_zero: 
-\forall f.numerator f \neq nfa_zero.
-intro.elim f
-  [simplify.intro.destruct H
-  |simplify.intro.destruct H
-  |simplify.generalize in match H.
-   cases (numerator f1)
-    [intro.elim H1.reflexivity
-    |simplify.intro.
-     cases z;simplify;intro;destruct H2
-    |simplify.intro.
-     cases z;simplify;intro;destruct H2
-    ]
-  ]
-qed.
-  
-theorem or_numerator_nfa_one_nfa_proper: 
-\forall f.(numerator f = nfa_one \land \exists g.numerator (finv f) =
-nfa_proper g) \lor \exists g.numerator f = nfa_proper g.
-intro.elim f
-  [simplify.right.
-   apply (ex_intro ? ? (nf_last n)).reflexivity
-  |simplify.left.split
-    [reflexivity
-    |apply (ex_intro ? ? (nf_last n)).reflexivity
-    ]
-  |elim H;clear H
-    [elim H1.clear H1.
-     elim H2.clear H2.
-     elim z
-      [simplify.
-       rewrite > H.rewrite > H1.simplify.
-       left.split
-        [reflexivity
-        |apply (ex_intro ? ? (nf_cons O a)).reflexivity
-        ]
-      |simplify.
-       rewrite > H.rewrite > H1.simplify.
-       right.apply (ex_intro ? ? (nf_last n)).reflexivity
-      |simplify.
-       rewrite > H.rewrite > H1.simplify.
-       left.split
-        [reflexivity
-        |apply (ex_intro ? ? (nf_cons (S n) a)).reflexivity
-        ]
-      ]
-    |elim H1.clear H1.
-      elim z
-      [simplify.
-       rewrite > H.simplify.
-       right.
-       apply (ex_intro ? ? (nf_cons O a)).reflexivity
-      |simplify.
-       rewrite > H.simplify.
-       right.apply (ex_intro ? ? (nf_cons (S n) a)).reflexivity
-      |simplify.
-       rewrite > H.simplify.
-       right.
-       apply (ex_intro ? ? (nf_cons O a)).reflexivity
-      ]
-    ]
-  ]
-qed.
-  
-theorem eq_nfa_one_to_eq_finv_nfa_proper: 
-\forall f.numerator f = nfa_one \to 
-\exist h.numerator (finv f) = nfa_proper h.
-intro.elim f
-  [simplify in H.destruct H
-  |simplify.apply (ex_intro ? ? (nf_last n)).reflexivity
-  |generalize in match H1.clear H1.
-   generalize in match H.clear H.
-   simplify.
-   cases (numerator f1);simplify
-    [intros;destruct H1
-    |intros;elim (H (refl_eq ? ?)).
-     rewrite > H2.simplify.
-     elim z;simplify
-      [apply (ex_intro ? ? (nf_cons O a)).reflexivity
-      |apply (ex_intro ? ? (nf_cons O a)).reflexivity
-      |apply (ex_intro ? ? (nf_cons (S n) a)).reflexivity
-      ]
-    |elim z;destruct H1
-    ]
-  ]
-qed.
-
-theorem numerator_nat_fact_to_fraction: \forall g:nat_fact. 
-numerator (nat_fact_to_fraction g) = nfa_proper g.
-intro.
-elim g
-  [simplify.reflexivity.
-  |simplify.rewrite > H.simplify.
-   cases n;reflexivity
-  ]
-qed.
 
 definition numeratorQ \def
 \lambda q.match q with
   [OQ \Rightarrow nfa_zero
-  |pos r \Rightarrow 
+  |Qpos r \Rightarrow 
     match r with 
     [one \Rightarrow nfa_one
     |frac x \Rightarrow numerator x
     ]
-  |neg r \Rightarrow 
+  |Qneg r \Rightarrow 
     match r with 
     [one \Rightarrow nfa_one
     |frac x \Rightarrow numerator x
@@ -193,6 +63,7 @@ let rec nat_fact_to_fraction_inv l \def
   ]
 .
 
+
 (*
 definition nat_fact_all_to_Q_inv \def
 \lambda n.
@@ -488,7 +359,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.
@@ -874,7 +745,8 @@ cases x
   [simplify in ⊢ (? ? % ?).rewrite > Qtimes_OQ.reflexivity
   |elim y
     [reflexivity
-    |simplify.rewrite > symmetric_rtimes.reflexivity
+    |simplify.alias id "symmetric_rtimes" = "cic:/matita/Q/times/symmetric_rtimes.con".
+rewrite > symmetric_rtimes.reflexivity
     |simplify.rewrite > symmetric_rtimes.reflexivity
     ]
   |elim y
@@ -889,7 +761,8 @@ theorem Qtimes_Qinv: \forall q. q \neq OQ \to Qtimes q (Qinv q) = Qone.
 intro.
 cases q;intro
   [elim H.reflexivity
-  |simplify.rewrite > rtimes_rinv.reflexivity
+  |simplify.alias id "rtimes_rinv" = "cic:/matita/Q/times/rtimes_rinv.con".
+rewrite > rtimes_rinv.reflexivity
   |simplify.rewrite > rtimes_rinv.reflexivity
   ]
 qed.
@@ -975,7 +848,7 @@ qed.
 
 
 (* la prova seguente e' tutta una ripetizione. Sistemare. *)
-
+(*CSC
 theorem Qtimes1: \forall f:fraction.
 Qtimes (nat_fact_all_to_Q (numerator f))
 (Qinv (nat_fact_all_to_Q (numerator (finv f))))
@@ -1079,7 +952,7 @@ intro.elim f
     ]
   ]
 qed.
-
+*)
 (*     
 definition numQ:Q \to Z \def
 \lambda q. 
@@ -1102,7 +975,7 @@ match q with
 |Qpos q \Rightarrow Qneg q
 |Qneg q \Rightarrow Qpos q
 ].
-
+(*CSC
 theorem frac_numQ_denomQ1: \forall r:ratio. 
 frac (numQ (Qpos r)) (denomQ (Qpos r)) = (Qpos r).
 intro.
@@ -1118,8 +991,9 @@ elim r
     |apply Qtimes1.
     ]
   ]
-qed.
+qed.*)
 
+(*CSC
 theorem frac_numQ_denomQ2: \forall r:ratio. 
 frac (numQ (Qneg r)) (denomQ (Qneg r)) = (Qpos r).
 intro.
@@ -1135,7 +1009,7 @@ elim r
     |apply Qtimes1.
     ]
   ]
-qed.
+qed.*)
 
 definition Qabs:Q \to Q \def \lambda q.
 match q with
@@ -1143,7 +1017,7 @@ match q with
 |Qpos q \Rightarrow Qpos q
 |Qneg q \Rightarrow Qpos q
 ].
-
+(*CSC
 theorem frac_numQ_denomQ: \forall q. 
 frac (numQ q) (denomQ q) = (Qabs q).
 intros.
@@ -1152,8 +1026,8 @@ cases q
   |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ1
   |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ2
   ]
-qed.
-
+qed.*)
+(*CSC
 definition Qfrac: Z \to nat \to Q \def
 \lambda z,n.match z with
 [OZ \Rightarrow OQ
@@ -1190,4 +1064,4 @@ cases q
   |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ2
   ]
 qed.
-
+*)