X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2FQ%2Fratio%2Frtimes.ma;h=3c7859dbedcdee7c29a615863be077c4190b24ab;hb=bb6f711dd0c8378d27118b73981515aff05f5750;hp=e11dbea9fcc89bfc94da5a2909fe2149dc95e0de;hpb=9d7d400d540ba79edaab1e0c8345127e1a79bb53;p=helm.git

diff --git a/helm/software/matita/library/Q/ratio/rtimes.ma b/helm/software/matita/library/Q/ratio/rtimes.ma
index e11dbea9f..3c7859dbe 100644
--- a/helm/software/matita/library/Q/ratio/rtimes.ma
+++ b/helm/software/matita/library/Q/ratio/rtimes.ma
@@ -15,17 +15,17 @@
 include "Q/ratio/rinv.ma".
 include "Q/fraction/ftimes.ma".
 
-definition rtimes : ratio \to ratio \to ratio \def
-\lambda r,s:ratio.
+definition rtimes : ratio → ratio → ratio ≝
+λr,s:ratio.
   match r with
-  [one \Rightarrow s
-  | (frac f) \Rightarrow 
+  [one ⇒ s
+  | (frac f) ⇒ 
       match s with 
-      [one \Rightarrow frac f
-      | (frac g) \Rightarrow ftimes f g]].
+      [one ⇒ frac f
+      | (frac g) ⇒ ftimes f g]].
 
 theorem symmetric_rtimes : symmetric ratio rtimes.
-change with (\forall r,s:ratio. rtimes r s = rtimes s r).
+change with (∀r,s:ratio. rtimes r s = rtimes s r).
 intros.
 elim r. elim s.
 reflexivity.
@@ -37,8 +37,409 @@ qed.
 
 variant sym_rtimes : ∀x,y:ratio. rtimes x y = rtimes y x ≝ symmetric_rtimes.
 
-theorem rtimes_rinv: \forall r:ratio. rtimes r (rinv r) = one.
+theorem rtimes_r_one: ∀r.rtimes r one = r.
+ intro; cases r;reflexivity.
+qed.
+
+theorem rtimes_one_r: ∀r.rtimes one r = r.
+intro; cases r;reflexivity.
+qed.
+
+theorem rtimes_Zplus: \forall x,y.
+rtimes (nat_frac_item_to_ratio x) (nat_frac_item_to_ratio y) =
+nat_frac_item_to_ratio (x + y).
+intro.
+elim x
+  [reflexivity
+  |*:elim y;reflexivity
+  ]
+qed.
+
+theorem rtimes_Zplus1: \forall x,y,f.
+rtimes (nat_frac_item_to_ratio x) (frac (cons y f)) =
+frac (cons ((x + y)) f).
+intro.
+elim x
+  [reflexivity
+  |*:elim y;reflexivity
+  ]
+qed.
+
+theorem rtimes_Zplus2: \forall x,y,f.
+rtimes (frac (cons y f)) (nat_frac_item_to_ratio x) =
+frac (cons ((y + x)) f).
+intros.
+elim x
+  [elim y;reflexivity
+  |*:elim y;reflexivity
+  ]
+qed.
+
+theorem or_one_frac: \forall f,g.
+rtimes (frac f) (frac g) = one \lor
+\exists h.rtimes (frac f) (frac g) = frac h.
+intros.
+elim (rtimes (frac f) (frac g))
+  [left.reflexivity
+  |right.apply (ex_intro ? ? f1).reflexivity
+  ]
+qed.
+
+theorem one_to_rtimes_Zplus3: \forall x,y:Z.\forall f,g:fraction.
+rtimes (frac f) (frac g) = one \to
+rtimes (frac (cons x f)) (frac (cons y g)) = nat_frac_item_to_ratio (x + y).
+intros.simplify.simplify in H.rewrite > H.simplify.
+reflexivity.
+qed.
+
+theorem frac_to_rtimes_Zplus3: \forall x,y:Z.\forall f,g:fraction.
+\forall h.rtimes (frac f) (frac g) = frac h \to
+rtimes (frac (cons x f)) (frac (cons y g)) = frac (cons (x + y) h).
+intros.simplify.simplify in H.rewrite > H.simplify.
+reflexivity.
+qed.
+
+
+theorem nat_frac_item_to_ratio_frac_frac: \forall z,f1,f2.
+rtimes (rtimes (nat_frac_item_to_ratio z) (frac f1)) (frac f2)
+=rtimes (nat_frac_item_to_ratio z) (rtimes (frac f1) (frac f2)).
+intros 2.elim f1
+  [elim f2
+    [change with
+     (rtimes (rtimes (nat_frac_item_to_ratio z) (nat_frac_item_to_ratio (pos n))) (nat_frac_item_to_ratio (pos n1))
+      =rtimes (nat_frac_item_to_ratio z) (rtimes (nat_frac_item_to_ratio (pos n)) (nat_frac_item_to_ratio (pos n1)))).
+     rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
+     rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
+     rewrite > assoc_Zplus.reflexivity
+    |change with
+     (rtimes (rtimes (nat_frac_item_to_ratio z) (nat_frac_item_to_ratio (pos n))) (nat_frac_item_to_ratio (neg n1))
+      =rtimes (nat_frac_item_to_ratio z) (rtimes (nat_frac_item_to_ratio (pos n)) (nat_frac_item_to_ratio (neg n1)))).
+     rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
+     rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
+     rewrite > assoc_Zplus.reflexivity
+    |change with
+      (rtimes (rtimes (nat_frac_item_to_ratio z) (nat_frac_item_to_ratio (pos n))) (frac (cons z1 f))
+       = rtimes (nat_frac_item_to_ratio z) (rtimes (nat_frac_item_to_ratio (pos n)) (frac (cons z1 f)))).
+     rewrite > rtimes_Zplus.rewrite > rtimes_Zplus1.
+     rewrite > rtimes_Zplus1.rewrite > rtimes_Zplus1.
+     rewrite > assoc_Zplus.reflexivity
+    ]
+  |elim f2
+    [change with
+     (rtimes (rtimes (nat_frac_item_to_ratio z) (nat_frac_item_to_ratio (neg n))) (nat_frac_item_to_ratio (pos n1))
+      =rtimes (nat_frac_item_to_ratio z) (rtimes (nat_frac_item_to_ratio (neg n)) (nat_frac_item_to_ratio (pos n1)))).
+     rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
+     rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
+     rewrite > assoc_Zplus.reflexivity
+    |change with
+     (rtimes (rtimes (nat_frac_item_to_ratio z) (nat_frac_item_to_ratio (neg n))) (nat_frac_item_to_ratio (neg n1))
+      =rtimes (nat_frac_item_to_ratio z) (rtimes (nat_frac_item_to_ratio (neg n)) (nat_frac_item_to_ratio (neg n1)))).
+     rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
+     rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
+     rewrite > assoc_Zplus.reflexivity
+    |change with
+      (rtimes (rtimes (nat_frac_item_to_ratio z) (nat_frac_item_to_ratio (neg n))) (frac (cons z1 f))
+       = rtimes (nat_frac_item_to_ratio z) (rtimes (nat_frac_item_to_ratio (neg n)) (frac (cons z1 f)))).
+     rewrite > rtimes_Zplus.rewrite > rtimes_Zplus1.
+     rewrite > rtimes_Zplus1.rewrite > rtimes_Zplus1.
+     rewrite > assoc_Zplus.reflexivity
+    ]
+  |elim f2
+    [change with
+     (rtimes (rtimes (nat_frac_item_to_ratio z) (frac (cons z1 f))) (nat_frac_item_to_ratio (pos n))
+      =rtimes (nat_frac_item_to_ratio z) (rtimes (frac (cons z1 f)) (nat_frac_item_to_ratio (pos n)))).
+     rewrite > rtimes_Zplus1.rewrite > rtimes_Zplus2.
+     rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus1.
+     rewrite > assoc_Zplus.reflexivity
+    |change with
+     (rtimes (rtimes (nat_frac_item_to_ratio z) (frac (cons z1 f))) (nat_frac_item_to_ratio (neg n))
+      =rtimes (nat_frac_item_to_ratio z) (rtimes (frac (cons z1 f)) (nat_frac_item_to_ratio (neg n)))).  
+     rewrite > rtimes_Zplus1.rewrite > rtimes_Zplus2.
+     rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus1.
+     rewrite > assoc_Zplus.reflexivity
+    |elim (or_one_frac f f3)
+      [rewrite > rtimes_Zplus1.
+       rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
+       rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
+       rewrite > rtimes_Zplus.
+       rewrite > assoc_Zplus.reflexivity
+      |elim H2.clear H2.
+       rewrite > rtimes_Zplus1.
+       rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H3).
+       rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H3).
+       rewrite > rtimes_Zplus1.
+       rewrite > assoc_Zplus.reflexivity
+      ]
+    ]
+  ]
+qed.
+
+theorem cons_frac_frac: \forall f1,z,f,f2.
+rtimes (rtimes (frac (cons z f)) (frac f1)) (frac f2)
+=rtimes (frac (cons z f)) (rtimes (frac f1) (frac f2)).
+intro.elim f1
+  [elim f2
+    [change with
+     (rtimes (rtimes (frac (cons z f)) (nat_frac_item_to_ratio (pos n))) (nat_frac_item_to_ratio (pos n1))
+      =rtimes (frac (cons z f)) (rtimes (nat_frac_item_to_ratio (pos n)) (nat_frac_item_to_ratio (pos n1)))).
+     rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus2.
+     rewrite > rtimes_Zplus.rewrite > rtimes_Zplus2.
+     rewrite > assoc_Zplus.reflexivity
+    |change with
+     (rtimes (rtimes (frac (cons z f)) (nat_frac_item_to_ratio (pos n))) (nat_frac_item_to_ratio (neg n1))
+      =rtimes (frac (cons z f)) (rtimes (nat_frac_item_to_ratio (pos n)) (nat_frac_item_to_ratio (neg n1)))).
+     rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus2.
+     rewrite > rtimes_Zplus.rewrite > rtimes_Zplus2.
+     rewrite > assoc_Zplus.reflexivity
+    |change with
+      (rtimes (rtimes (frac (cons z f)) (nat_frac_item_to_ratio (pos n))) (frac (cons z1 f3))
+       = rtimes (frac (cons z f)) (rtimes (nat_frac_item_to_ratio (pos n)) (frac (cons z1 f3)))).
+     rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus1.
+     elim (or_one_frac f f3)
+      [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
+       rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
+       rewrite > assoc_Zplus.reflexivity
+      |elim H1.clear H1.
+       rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
+       rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
+       rewrite > assoc_Zplus.reflexivity
+      ]
+    ]
+  |elim f2
+    [change with
+     (rtimes (rtimes (frac (cons z f)) (nat_frac_item_to_ratio (neg n))) (nat_frac_item_to_ratio (pos n1))
+      =rtimes (frac (cons z f)) (rtimes (nat_frac_item_to_ratio (neg n)) (nat_frac_item_to_ratio (pos n1)))).
+     rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus2.
+     rewrite > rtimes_Zplus.rewrite > rtimes_Zplus2.
+     rewrite > assoc_Zplus.reflexivity
+    |change with
+     (rtimes (rtimes (frac (cons z f)) (nat_frac_item_to_ratio (neg n))) (nat_frac_item_to_ratio (neg n1))
+      =rtimes (frac (cons z f)) (rtimes (nat_frac_item_to_ratio (neg n)) (nat_frac_item_to_ratio (neg n1)))).
+     rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus2.
+     rewrite > rtimes_Zplus.rewrite > rtimes_Zplus2.
+     rewrite > assoc_Zplus.reflexivity
+    |change with
+      (rtimes (rtimes (frac (cons z f)) (nat_frac_item_to_ratio (neg n))) (frac (cons z1 f3))
+       = rtimes (frac (cons z f)) (rtimes (nat_frac_item_to_ratio (neg n)) (frac (cons z1 f3)))).
+     rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus1.
+     elim (or_one_frac f f3)
+      [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
+       rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
+       rewrite > assoc_Zplus.reflexivity
+      |elim H1.clear H1.
+       rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
+       rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
+       rewrite > assoc_Zplus.reflexivity
+      ]
+    ]
+  |elim f3
+    [change with
+     (rtimes (rtimes (frac (cons z1 f2)) (frac (cons z f))) (nat_frac_item_to_ratio (pos n))
+      =rtimes (frac (cons z1 f2)) (rtimes (frac (cons z f)) (nat_frac_item_to_ratio (pos n)))).
+     rewrite > rtimes_Zplus2.
+     elim (or_one_frac f2 f)
+      [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
+       rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
+       rewrite > rtimes_Zplus.
+       rewrite > assoc_Zplus.reflexivity
+      |elim H1.clear H1.
+       rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
+       rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
+       rewrite > rtimes_Zplus2.
+       rewrite > assoc_Zplus.reflexivity
+      ]
+    |change with
+     (rtimes (rtimes (frac (cons z1 f2)) (frac (cons z f))) (nat_frac_item_to_ratio (neg n))
+      =rtimes (frac (cons z1 f2)) (rtimes (frac (cons z f)) (nat_frac_item_to_ratio (neg n)))).
+     rewrite > rtimes_Zplus2.
+     elim (or_one_frac f2 f)
+      [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
+       rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
+       rewrite > rtimes_Zplus.
+       rewrite > assoc_Zplus.reflexivity
+      |elim H1.clear H1.
+       rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
+       rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
+       rewrite > rtimes_Zplus2.
+       rewrite > assoc_Zplus.reflexivity
+      ]
+    |elim (or_one_frac f2 f)
+      [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
+       rewrite > rtimes_Zplus1.
+       elim (or_one_frac f f4)
+        [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H3).
+         rewrite > rtimes_Zplus2.
+         cut (f4 = f2)
+          [rewrite > Hcut.
+           rewrite > assoc_Zplus.reflexivity
+          |apply injective_frac.
+           rewrite < rtimes_one_r.
+           rewrite < H2.
+           (* problema inaspettato: mi serve l'unicita' dell'inversa,
+              che richiede (?) l'associativita. Per fortuna basta 
+              l'ipotesi induttiva. *)
+           cases f2
+            [change with 
+             (rtimes (rtimes (nat_frac_item_to_ratio (pos n)) (frac f)) (frac f4)=nat_frac_item_to_ratio (pos n)).
+             rewrite > nat_frac_item_to_ratio_frac_frac.
+             rewrite > H3.
+             rewrite > rtimes_r_one.
+             reflexivity
+            |change with 
+             (rtimes (rtimes (nat_frac_item_to_ratio (neg n)) (frac f)) (frac f4)=nat_frac_item_to_ratio (neg n)).
+             rewrite > nat_frac_item_to_ratio_frac_frac.
+             rewrite > H3.
+             rewrite > rtimes_r_one.
+             reflexivity
+            |rewrite > H.
+             rewrite > H3.
+             rewrite > rtimes_r_one.
+             reflexivity
+            ]
+          ]
+        |elim H3.clear H3.
+         rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H4).
+         cut (rtimes (frac f2) (frac a) = frac f4)
+          [rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? f4 Hcut).
+           rewrite > assoc_Zplus.reflexivity
+          |rewrite < H4.
+           generalize in match H2.
+           cases f2;intro
+            [change with 
+             (rtimes (nat_frac_item_to_ratio (pos n)) (rtimes (frac f)(frac f4)) =frac f4).
+             rewrite < nat_frac_item_to_ratio_frac_frac.
+             rewrite > H3.
+             rewrite > rtimes_one_r.
+             reflexivity
+            |change with 
+             (rtimes (nat_frac_item_to_ratio (neg n)) (rtimes (frac f)(frac f4)) =frac f4).
+             rewrite < nat_frac_item_to_ratio_frac_frac.
+             rewrite > H3.
+             rewrite > rtimes_one_r.
+             reflexivity
+            |rewrite < H.
+             rewrite > H3.
+             rewrite > rtimes_one_r.
+             reflexivity
+            ]
+          ]
+        ]
+      |elim H2.clear H2.
+       rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H3).
+       elim (or_one_frac f f4)
+        [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
+         rewrite > rtimes_Zplus2.
+         cut (rtimes (frac a) (frac f4) = frac f2)
+          [rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? f2 Hcut).
+           rewrite > assoc_Zplus.reflexivity
+          |rewrite < H3.
+           generalize in match H2.
+           cases f2;intro
+            [change with 
+             (rtimes (rtimes (nat_frac_item_to_ratio (pos n)) (frac f)) (frac f4)=nat_frac_item_to_ratio (pos n)).
+             rewrite > nat_frac_item_to_ratio_frac_frac.
+             rewrite > H4.
+             rewrite > rtimes_r_one.
+             reflexivity
+            |change with 
+             (rtimes (rtimes (nat_frac_item_to_ratio (neg n)) (frac f)) (frac f4)=nat_frac_item_to_ratio (neg n)).
+             rewrite > nat_frac_item_to_ratio_frac_frac.
+             rewrite > H4.
+             rewrite > rtimes_r_one.
+             reflexivity
+            |rewrite > H.
+             rewrite > H4.
+             rewrite > rtimes_r_one.
+             reflexivity
+            ]
+          ]
+        |elim H2.clear H2.
+         rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a1 H4).
+         elim (or_one_frac a f4)
+          [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
+           cut (rtimes (frac f2) (frac a1) = one)
+            [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? Hcut).
+             rewrite > assoc_Zplus.reflexivity
+            |rewrite < H4.
+             generalize in match H3.
+             cases f2;intro
+              [change with 
+               (rtimes (nat_frac_item_to_ratio (pos n)) (rtimes (frac f)(frac f4)) = one).
+               rewrite < nat_frac_item_to_ratio_frac_frac.
+               rewrite > H5.
+               assumption
+              |change with 
+               (rtimes (nat_frac_item_to_ratio (neg n)) (rtimes (frac f)(frac f4)) = one).
+               rewrite < nat_frac_item_to_ratio_frac_frac.
+               rewrite > H5.
+               assumption
+              |rewrite < H.
+               rewrite > H5.
+               assumption
+              ]
+            ]
+          |elim H2.clear H2.
+           rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a2 H5).
+           cut (rtimes (frac f2) (frac a1) = frac a2)
+            [rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a2 Hcut).
+             rewrite > assoc_Zplus.reflexivity
+            |rewrite < H4.
+             generalize in match H3.
+             cases f2;intro
+              [change with 
+               (rtimes (nat_frac_item_to_ratio (pos n)) (rtimes (frac f)(frac f4)) = frac a2).
+               rewrite < nat_frac_item_to_ratio_frac_frac.
+               rewrite > H2.
+               assumption
+              |change with 
+               (rtimes (nat_frac_item_to_ratio (neg n)) (rtimes (frac f)(frac f4)) = frac a2).
+               rewrite < nat_frac_item_to_ratio_frac_frac.
+               rewrite > H2.
+               assumption
+              |rewrite < H.
+               rewrite > H2.
+               assumption
+              ]
+            ]
+          ]
+        ]
+      ]
+    ]
+  ]
+qed.
+       
+theorem frac_frac_fracaux: ∀f,f1,f2.
+rtimes (rtimes (frac f) (frac f1)) (frac f2)
+=rtimes (frac f) (rtimes (frac f1) (frac f2)).
+intros.
+cases f
+  [change with
+   (rtimes (rtimes (nat_frac_item_to_ratio (pos n)) (frac f1)) (frac f2)
+    =rtimes (nat_frac_item_to_ratio (pos n)) (rtimes (frac f1) (frac f2))).
+   apply nat_frac_item_to_ratio_frac_frac
+  |change with
+   (rtimes (rtimes (nat_frac_item_to_ratio (neg n)) (frac f1)) (frac f2)
+    =rtimes (nat_frac_item_to_ratio (neg n)) (rtimes (frac f1) (frac f2))).
+   apply nat_frac_item_to_ratio_frac_frac
+  |apply cons_frac_frac]
+qed.
+
+
+theorem associative_rtimes:associative ? rtimes.
+unfold.intros.
+cases x
+  [reflexivity
+  |cases y
+    [reflexivity.
+    |cases z
+      [rewrite > rtimes_r_one.rewrite > rtimes_r_one.reflexivity
+      |apply frac_frac_fracaux
+      ]]]
+qed.
+
+
+theorem rtimes_rinv: ∀r:ratio. rtimes r (rinv r) = one.
 intro.elim r.
 reflexivity.
 simplify.apply ftimes_finv.
-qed.
\ No newline at end of file
+qed.