update in groud_2 and models

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

diff --git a/helm/software/matita/library/Q/inv.ma b/helm/software/matita/library/Q/inv.ma
index 6725f5c99e802ce7ca1bbe17afe7a5fba8bf66da..4cc38f191a47a1735045b289bf2f4d10d49d26f1 100644 (file)
--- a/helm/software/matita/library/Q/inv.ma
+++ b/helm/software/matita/library/Q/inv.ma
@@ -12,24 +12,82 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "Q/q/q.ma".
 include "Q/q.ma".
+include "Q/fraction/finv.ma".
 
-let rec finv f \def
-  match f with
-  [ (pp n) \Rightarrow (nn n)
-  | (nn n) \Rightarrow (pp n)
-  | (cons x g) \Rightarrow (cons (Zopp x) (finv g))].
-
-definition rinv : ratio \to ratio \def
-\lambda r:ratio.
-  match r with
-  [one \Rightarrow one
-  | (frac f) \Rightarrow frac (finv f)].
-
-definition Qinv : Q → Q ≝
- λp.
-  match p with
-   [ OQ ⇒ OQ  (* arbitrary value *)
-   | Qpos r ⇒ Qpos (rinv r)
-   | Qneg r ⇒ Qneg (rinv r)
+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
+  | elim q in H ⊢ %; 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
+  | elim q in H ⊢ %; assumption]
+qed.
+*)
\ No newline at end of file