From bdfc19218ead418772ef02a1693e75d7551c8727 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 3 Jun 2008 22:50:48 +0000
Subject: [PATCH] Some proofs on enumerator and denominator.

---
 helm/software/matita/library/Q/inv.ma | 103 ++++++++++++++++++++++++++
 helm/software/matita/library/Q/q.ma   |   2 +-
 2 files changed, 104 insertions(+), 1 deletion(-)

diff --git a/helm/software/matita/library/Q/inv.ma b/helm/software/matita/library/Q/inv.ma
index 6725f5c99..39b9c776e 100644
--- a/helm/software/matita/library/Q/inv.ma
+++ b/helm/software/matita/library/Q/inv.ma
@@ -20,12 +20,32 @@ let rec finv f \def
   | (nn n) \Rightarrow (pp n)
   | (cons x g) \Rightarrow (cons (Zopp x) (finv g))].
 
+theorem finv_finv: ∀f. finv (finv f) = f.
+ intro;
+ elim f;
+  [1,2: reflexivity
+  | simplify;
+    rewrite > H;
+    rewrite > Zopp_Zopp;
+    reflexivity
+  ]
+qed.
+
 definition rinv : ratio \to ratio \def
 \lambda r:ratio.
   match r with
   [one \Rightarrow one
   | (frac f) \Rightarrow frac (finv f)].
 
+theorem rinv_rinv: ∀r. rinv (rinv r) = r.
+ intro;
+ elim r;
+  [ reflexivity
+  | simplify;
+    rewrite > finv_finv;
+    reflexivity]
+qed.
+
 definition Qinv : Q → Q ≝
  λp.
   match p with
@@ -33,3 +53,86 @@ definition Qinv : Q → Q ≝
    | Qpos r ⇒ Qpos (rinv r)
    | Qneg r ⇒ Qneg (rinv r)
    ].
+
+theorem Qinv_Qinv: ∀q. Qinv (Qinv q) = q.
+ intro;
+ elim q;
+  [ reflexivity
+  |*:simplify;
+    rewrite > rinv_rinv;
+    reflexivity]
+qed.
+
+theorem denominator_integral_factor_finv:
+ ∀f. enumerator_integral_fraction f = denominator_integral_fraction (finv f).
+ intro;
+ elim f;
+  [1,2: reflexivity
+  |simplify;
+   rewrite > H;
+   elim z; simplify; reflexivity]
+qed.
+
+definition is_positive ≝
+ λq.
+  match q with
+   [ Qpos _ ⇒ True
+   | _ ⇒ False
+   ].
+
+definition is_negative ≝
+ λq.
+  match q with
+   [ Qneg _ ⇒ True
+   | _ ⇒ False
+   ].
+
+theorem is_positive_denominator_Qinv:
+ ∀q. is_positive q → enumerator q = denominator (Qinv q).
+ intro;
+ elim q;
+  [1,3: elim H;
+  | simplify; clear H;
+    elim r; simplify;
+     [ reflexivity
+     | rewrite > denominator_integral_factor_finv;
+       reflexivity]]
+qed.
+
+theorem is_negative_denominator_Qinv:
+ ∀q. is_negative q → enumerator q = -(denominator (Qinv q)).
+ intro;
+ elim q;
+  [1,2: elim H;
+  | simplify; clear H;
+    elim r; simplify;
+     [ reflexivity
+     | rewrite > denominator_integral_factor_finv;
+       unfold Zopp;
+       elim (denominator_integral_fraction (finv f));
+       simplify;
+        [ reflexivity
+        | generalize in match (lt_O_defactorize_aux (nat_fact_of_integral_fraction a) O);
+          elim (defactorize_aux (nat_fact_of_integral_fraction a) O);
+          simplify;
+           [ elim (Not_lt_n_n ? H)
+           | reflexivity]]]]
+qed.
+
+theorem is_positive_enumerator_Qinv:
+  ∀q. is_positive q → enumerator (Qinv q) = denominator q.
+ intros;
+ lapply (is_positive_denominator_Qinv (Qinv q));
+  [ rewrite > Qinv_Qinv in Hletin;
+    assumption
+  | generalize in match H; elim q; assumption]
+qed.
+
+theorem is_negative_enumerator_Qinv:
+  ∀q. is_negative q → enumerator (Qinv q) = -(denominator q).
+ intros;
+ lapply (is_negative_denominator_Qinv (Qinv q));
+  [ rewrite > Qinv_Qinv in Hletin;
+    assumption
+  | generalize in match H; elim q; assumption]
+qed.
\ No newline at end of file
diff --git a/helm/software/matita/library/Q/q.ma b/helm/software/matita/library/Q/q.ma
index af70c3b73..bc1fff067 100644
--- a/helm/software/matita/library/Q/q.ma
+++ b/helm/software/matita/library/Q/q.ma
@@ -139,7 +139,7 @@ definition enumerator ≝
  λq.
   match q with
    [ OQ ⇒ OZ
-   | Qpos r ⇒ pos (pred (enumerator_of_fraction r))
+   | Qpos r ⇒ (enumerator_of_fraction r : Z)
    | Qneg r ⇒ neg(pred (enumerator_of_fraction r))
    ].
 
-- 
2.39.2