Even more Q stuff moved around.

diff --git a/helm/software/matita/library/Q/frac.ma b/helm/software/matita/library/Q/frac.ma
index d00cd3158956c72f9f59e3a479a9b7850eebfa79..a1f0cd54a2218c868ca5cefbf703a97ebd544190 100644 (file)
--- a/helm/software/matita/library/Q/frac.ma
+++ b/helm/software/matita/library/Q/frac.ma
@@ -52,112 +52,8 @@ reflexivity.
 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))))
-= Qpos (frac f).
-simplify.
-intro.elim f
-  [reflexivity
-  |reflexivity
-  |elim (or_numerator_nfa_one_nfa_proper f1)
-    [elim H1.clear H1.
-     elim H3.clear H3.
-     cut (finv (nat_fact_to_fraction a) = f1)
-      [elim z
-        [simplify.
-         rewrite > H2.rewrite > H1.simplify.
-         rewrite > Hcut.reflexivity
-        |simplify.
-         rewrite > H2.rewrite > H1.simplify.
-         rewrite > Hcut.reflexivity
-        |simplify.
-         rewrite > H2.rewrite > H1.simplify.
-         rewrite > Hcut.reflexivity
-        ]
-      |generalize in match H.
-       rewrite > H2.rewrite > H1.simplify.
-       intro.destruct H3.assumption
-      ]
-    |elim H1.clear H1.
-     elim z
-      [simplify.
-       rewrite > H2.rewrite > H2.simplify.
-       elim (or_numerator_nfa_one_nfa_proper (finv f1))
-        [elim H1.clear H1.
-         rewrite > H3.simplify.
-         cut (nat_fact_to_fraction a = f1)
-          [rewrite > Hcut.reflexivity
-          |generalize in match H.
-           rewrite > H2.
-           rewrite > H3.
-           rewrite > Qtimes_q_Qone.
-           intro.
-           destruct H1.
-           assumption
-          ]
-        |elim H1.clear H1.
-         generalize in match H.
-         rewrite > H2.
-         rewrite > H3.simplify. 
-         intro.
-         destruct H1.
-         rewrite > Hcut.
-         simplify.reflexivity
-        ]
-      |simplify.rewrite > H2.simplify.
-        elim (or_numerator_nfa_one_nfa_proper (finv f1))
-        [elim H1.clear H1.
-         rewrite > H3.simplify.
-         cut (nat_fact_to_fraction a = f1)
-          [rewrite > Hcut.reflexivity
-          |generalize in match H.
-           rewrite > H2.
-           rewrite > H3.
-           rewrite > Qtimes_q_Qone.
-           intro.
-           destruct H1.
-           assumption
-          ]
-        |elim H1.clear H1.
-         generalize in match H.
-         rewrite > H2.
-         rewrite > H3.simplify. 
-         intro.
-         destruct H1.
-         rewrite > Hcut.
-         simplify.reflexivity
-        ]
-      |simplify.rewrite > H2.simplify.
-        elim (or_numerator_nfa_one_nfa_proper (finv f1))
-        [elim H1.clear H1.
-         rewrite > H3.simplify.
-         cut (nat_fact_to_fraction a = f1)
-          [rewrite > Hcut.reflexivity
-          |generalize in match H.
-           rewrite > H2.
-           rewrite > H3.
-           rewrite > Qtimes_q_Qone.
-           intro.
-           destruct H1.
-           assumption
-          ]
-        |elim H1.clear H1.
-         generalize in match H.
-         rewrite > H2.
-         rewrite > H3.simplify. 
-         intro.
-         destruct H1.
-         rewrite > Hcut.
-         simplify.reflexivity
-        ]
-      ]
-    ]
-  ]
-qed.
-*)
+Qtimes1 == Qtimes_numerator_denominator
+
 (*     
 definition numQ:Q \to Z \def
 \lambda q. 

diff --git a/helm/software/matita/library/Q/fraction/finv.ma b/helm/software/matita/library/Q/fraction/finv.ma
index 2868bece0cd85f4d48217abbc0b3b16342cc68d1..ce05b29c7132bae42df04bfd77e196f13890f4aa 100644 (file)
--- a/helm/software/matita/library/Q/fraction/finv.ma
+++ b/helm/software/matita/library/Q/fraction/finv.ma
@@ -15,11 +15,11 @@
 include "Z/plus.ma".
 include "Q/fraction/fraction.ma".
 
-let rec finv f \def                                               
+let rec finv f ≝                                               
   match f with
-  [ (pp n) \Rightarrow (nn n)
-  | (nn n) \Rightarrow (pp n)
-  | (cons x g) \Rightarrow (cons (Zopp x) (finv g))].
+  [ pp n ⇒ nn n
+  | nn n ⇒ pp n
+  | cons x g ⇒ cons (Zopp x) (finv g)].
 
 theorem finv_finv: ∀f. finv (finv f) = f.
  intro; 
@@ -31,62 +31,3 @@ theorem finv_finv: ∀f. finv (finv f) = f.
     reflexivity
   ]
 qed.
-
-theorem or_numerator_nfa_one_nfa_proper: 
-∀f.
- (numerator f = nfa_one ∧ ∃g.numerator (finv f) = nfa_proper g) ∨
- ∃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: 
-∀f.numerator f = nfa_one → ∃h.numerator (finv f) = nfa_proper h.
-  intros;
-  elim (or_numerator_nfa_one_nfa_proper f); cases H1;
-   [ assumption
-   | rewrite > H in H2;
-     destruct
-   ]
-qed.

diff --git a/helm/software/matita/library/Q/fraction/fraction.ma b/helm/software/matita/library/Q/fraction/fraction.ma
index 81b60de91fc924a0e3d10214d920c00fb461b123..ba4b417f6c2b6d067b2e1c331eaa8e87ee60e12f 100644 (file)
--- a/helm/software/matita/library/Q/fraction/fraction.ma
+++ b/helm/software/matita/library/Q/fraction/fraction.ma
@@ -29,56 +29,6 @@ let rec nat_fact_to_fraction n ≝
   | nf_cons m l ⇒ cons (Z_of_nat m) (nat_fact_to_fraction l)
   ].
 
-(* 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 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.
-
 (* double elimination principles *)
 theorem fraction_elim2:
 \forall R:fraction \to fraction \to Prop.

diff --git a/helm/software/matita/library/Q/fraction/numerator_denominator.ma b/helm/software/matita/library/Q/fraction/numerator_denominator.ma
new file mode 100644 (file)
index 0000000..0b51d11
--- /dev/null
+++ b/helm/software/matita/library/Q/fraction/numerator_denominator.ma
@@ -0,0 +1,132 @@
+(**************************************************************************)
+(*       ___                                                               *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "Q/fraction/finv.ma".
+
+(* 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)
+      ]]].
+
+definition denominator ≝ λf.numerator (finv f).
+
+theorem not_eq_numerator_nfa_zero: ∀f.numerator f ≠ 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 not_eq_denominator_nfa_zero: ∀f.denominator f ≠ nfa_zero.
+ unfold denominator; intro; apply not_eq_numerator_nfa_zero.
+qed.
+
+theorem numerator_nat_fact_to_fraction: ∀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.
+
+theorem denominator_nat_fact_to_fraction: ∀g:nat_fact.
+denominator (finv (nat_fact_to_fraction g)) = nfa_proper g.
+ unfold denominator;
+ intro;
+ rewrite > finv_finv;
+ apply numerator_nat_fact_to_fraction.
+qed.
+
+theorem or_numerator_nfa_one_nfa_proper: 
+∀f.
+ (numerator f = nfa_one ∧ ∃g.denominator f = nfa_proper g) ∨
+ ∃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: 
+∀f.numerator f = nfa_one → ∃h.denominator f = nfa_proper h.
+  intros;
+  elim (or_numerator_nfa_one_nfa_proper f); cases H1;
+   [ assumption
+   | rewrite > H in H2;
+     destruct]
+qed.
\ No newline at end of file

diff --git a/helm/software/matita/library/Q/q/q.ma b/helm/software/matita/library/Q/q/q.ma
index 43b090fef3f3f30139460c85521e46d8d032d72f..960756abe8ba41573efc4b0c3ca8de782e3af516 100644 (file)
--- a/helm/software/matita/library/Q/q/q.ma
+++ b/helm/software/matita/library/Q/q/q.ma
@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 include "Q/ratio/ratio.ma".
+include "Q/fraction/numerator_denominator.ma".
 
 (* a rational number is either O or a ratio with a sign *)
 inductive Q : Set \def 

diff --git a/helm/software/matita/library/Q/q/qtimes.ma b/helm/software/matita/library/Q/q/qtimes.ma
index 52246e5a57794a159c34d7445c3f0cd6c9c114b8..3b4b24b7971179f25ca96747d2bef57cc6a7bfad 100644 (file)
--- a/helm/software/matita/library/Q/q/qtimes.ma
+++ b/helm/software/matita/library/Q/q/qtimes.ma
@@ -189,3 +189,53 @@ cases p
     |apply Qinv_Qtimes;intro;destruct H
     |apply Qinv_Qtimes;intro;destruct H]]
 qed.
+
+theorem Qtimes_numerator_denominator: ∀f:fraction.
+  Qtimes (nat_fact_all_to_Q (numerator f)) (Qinv (nat_fact_all_to_Q (denominator f)))
+  = Qpos (frac f).
+simplify.
+intro.elim f
+  [reflexivity
+  |reflexivity
+  |elim (or_numerator_nfa_one_nfa_proper f1)
+    [elim H1.clear H1.
+     elim H3.clear H3.
+     cut (finv (nat_fact_to_fraction a) = f1)
+      [elim z;
+       simplify;
+       rewrite > H2;rewrite > H1;simplify;
+       rewrite > Hcut;reflexivity
+      |generalize in match H.
+       rewrite > H2.rewrite > H1.simplify.
+       intro.destruct H3.reflexivity
+      ]
+    |elim H1;clear H1;
+     elim z
+      [*:simplify;
+       rewrite > H2;simplify;
+       elim (or_numerator_nfa_one_nfa_proper (finv f1))
+        [1,3,5:elim H1;clear H1;
+         rewrite > H3;simplify;
+         cut (nat_fact_to_fraction a = f1)
+          [1,3,5:rewrite > Hcut;reflexivity
+          |*:generalize in match H;
+           rewrite > H2;
+           rewrite > H3;
+           rewrite > Qtimes_q_Qone;
+           intro;
+           simplify in H1;
+           destruct H1;
+           reflexivity
+          ]
+        |*:elim H1;clear H1;
+         generalize in match H;
+         rewrite > H2;
+         rewrite > H3;simplify;
+         intro;
+         destruct H1;
+         rewrite > Hcut;
+         simplify;reflexivity
+        ]]]]
+qed.
+
+

diff --git a/helm/software/matita/library/depends b/helm/software/matita/library/depends
index b17029e9226db6deb50c1fc949d3a11dc55bceb6..2ae7107a4c6180b98c74dc463fc8cce3363ec47e 100644 (file)
--- a/helm/software/matita/library/depends
+++ b/helm/software/matita/library/depends
@@ -32,7 +32,8 @@ Q/ratio/rinv.ma Q/fraction/finv.ma Q/ratio/ratio.ma
 Q/ratio/rtimes.ma Q/fraction/ftimes.ma Q/ratio/rinv.ma
 Q/fraction/fraction.ma Z/compare.ma nat/factorization.ma
 Q/fraction/finv.ma Q/fraction/fraction.ma Z/plus.ma
-Q/fraction/ftimes.ma Q/fraction/finv.ma Q/ratio/ratio.ma
+Q/fraction/ftimes.ma Q/fraction/finv.ma Q/nat_fact/times.ma Q/ratio/ratio.ma Z/times.ma
+Q/fraction/numerator_denominator.ma Q/fraction/finv.ma
 Q/nat_fact/times.ma nat/factorization.ma
 datatypes/compare.ma 
 datatypes/constructors.ma logic/equality.ma