X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2FQ%2Fq%2Fqtimes.ma;h=3b4b24b7971179f25ca96747d2bef57cc6a7bfad;hb=bfb1d0076c4adf923f0507e4e2ab26519e689b88;hp=e288ef412c4732badb25cee471c2952d75e96e6d;hpb=9d7d400d540ba79edaab1e0c8345127e1a79bb53;p=helm.git

diff --git a/helm/software/matita/library/Q/q/qtimes.ma b/helm/software/matita/library/Q/q/qtimes.ma
index e288ef412..3b4b24b79 100644
--- a/helm/software/matita/library/Q/q/qtimes.ma
+++ b/helm/software/matita/library/Q/q/qtimes.ma
@@ -75,3 +75,167 @@ theorem Qtimes_Qinv: ∀q. q ≠ OQ → q * (Qinv q) = Qpos one.
      reflexivity
   ]
 qed.
+
+theorem times_fa_Qtimes: \forall f,g. nat_fact_all_to_Q (times_fa f g) =
+Qtimes (nat_fact_all_to_Q f) (nat_fact_all_to_Q g).
+intros.
+cases f;simplify
+  [reflexivity
+  |cases g;reflexivity
+  |cases g;simplify
+    [reflexivity
+    |reflexivity
+    |rewrite > times_f_ftimes.reflexivity]]
+qed.
+
+theorem times_Qtimes: \forall p,q.
+(nat_to_Q (p*q)) = Qtimes (nat_to_Q p) (nat_to_Q q).
+intros.unfold nat_to_Q.
+rewrite < times_fa_Qtimes.
+rewrite < eq_times_times_fa.
+reflexivity.
+qed.
+
+theorem associative_Qtimes:associative ? Qtimes.
+unfold.intros.
+cases x
+  [reflexivity
+   (* non posso scrivere 2,3: ... ?? *)
+  |cases y
+    [reflexivity.
+    |cases z
+      [reflexivity
+      |simplify.rewrite > associative_rtimes.
+       reflexivity.
+      |simplify.rewrite > associative_rtimes.
+       reflexivity
+      ]
+    |cases z
+      [reflexivity
+      |simplify.rewrite > associative_rtimes.
+       reflexivity.
+      |simplify.rewrite > associative_rtimes.
+       reflexivity
+      ]
+    ]
+  |cases y
+    [reflexivity.
+    |cases z
+      [reflexivity
+      |simplify.rewrite > associative_rtimes.
+       reflexivity.
+      |simplify.rewrite > associative_rtimes.
+       reflexivity
+      ]
+    |cases z
+      [reflexivity
+      |simplify.rewrite > associative_rtimes.
+       reflexivity.
+      |simplify.rewrite > associative_rtimes.
+       reflexivity]]]
+qed.
+
+theorem eq_Qtimes_OQ_to_eq_OQ: \forall p,q.
+Qtimes p q = OQ \to p = OQ \lor q = OQ.
+intros 2.
+cases p
+  [intro.left.reflexivity
+  |cases q
+    [intro.right.reflexivity
+    |simplify.intro.destruct H
+    |simplify.intro.destruct H
+    ]
+  |cases q
+    [intro.right.reflexivity
+    |simplify.intro.destruct H
+    |simplify.intro.destruct H]]
+qed.
+
+theorem Qinv_Qtimes: \forall p,q.
+p \neq OQ \to q \neq OQ \to Qinv(Qtimes p q) = Qtimes (Qinv p) (Qinv q).
+intros.
+rewrite < Qtimes_Qone_q in ⊢ (? ? ? %).
+rewrite < (Qtimes_Qinv (Qtimes p q))
+  [lapply (Qtimes_Qinv ? H).
+   lapply (Qtimes_Qinv ? H1).
+   rewrite > symmetric_Qtimes in ⊢ (? ? ? (? % ?)).
+   rewrite > associative_Qtimes.
+   rewrite > associative_Qtimes.
+   rewrite < associative_Qtimes in ⊢ (? ? ? (? ? (? ? %))).
+   rewrite < symmetric_Qtimes in ⊢ (? ? ? (? ? (? ? (? % ?)))).
+   rewrite > associative_Qtimes in ⊢ (? ? ? (? ? (? ? %))).
+   rewrite > Hletin1.
+   rewrite > Qtimes_q_Qone.
+   rewrite > Hletin.
+   rewrite > Qtimes_q_Qone.
+   reflexivity
+  |intro.
+   elim (eq_Qtimes_OQ_to_eq_OQ ? ? H2)
+    [apply (H H3)|apply (H1 H3)]]
+qed.
+
+(* a stronger version, taking advantage of inv(O) = O *)
+theorem Qinv_Qtimes': \forall p,q. Qinv(Qtimes p q) = Qtimes (Qinv p) (Qinv q).
+intros.
+cases p
+  [reflexivity
+  |cases q
+    [reflexivity
+    |apply Qinv_Qtimes;intro;destruct H
+    |apply Qinv_Qtimes;intro;destruct H
+    ]
+  |cases q
+    [reflexivity
+    |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.
+
+