- transcript: bugfix

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

diff --git a/helm/software/matita/library/Q/q/q.ma b/helm/software/matita/library/Q/q/q.ma
index 86f6d1dcfa96281e678523cd9e7d692471168d0b..f16851f016bfcc983478224574171e2f792fc0a5 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 
@@ -20,10 +21,56 @@ inductive Q : Set \def
   | Qpos : ratio  \to Q
   | Qneg : ratio  \to Q.
 
-definition Q_of_nat ≝
- λn.
-  match factorize n with
-   [ nfa_zero ⇒ OQ
-   | nfa_one ⇒ Qpos one
-   | nfa_proper l ⇒ Qpos (frac (nat_fact_to_fraction l))
+interpretation "Rationals" 'Q = Q.
+
+definition Qone ≝ Qpos one.
+
+definition Qopp ≝
+ λq.
+  match q with
+   [ OQ ⇒ OQ
+   | Qpos r ⇒ Qneg r
+   | Qneg r ⇒ Qpos r
+   ].
+
+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))
+  ].
+
+definition nat_to_Q ≝ λn.nat_fact_all_to_Q (factorize n).
+
+definition Z_to_Q ≝
+ λz.
+  match z with
+   [ OZ ⇒ OQ
+   | pos n ⇒ nat_to_Q (S n)
+   | neg n ⇒ Qopp (nat_to_Q (S n))
    ].
+
+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
+    ]
+  ].
+
+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.