Even more Q stuff classified.

diff --git a/helm/software/matita/library/Q/frac.ma b/helm/software/matita/library/Q/frac.ma
index abc1fb4ceb449ed4c4361514162890ffe7c5b5ea..d00cd3158956c72f9f59e3a479a9b7850eebfa79 100644 (file)
--- a/helm/software/matita/library/Q/frac.ma
+++ b/helm/software/matita/library/Q/frac.ma
@@ -32,305 +32,10 @@ definition nat_fact_all_to_Q_inv \def
 
 definition nat_to_Q_inv \def
 \lambda n. nat_fact_all_to_Q_inv (factorize n).
-*)
 
 definition frac:nat \to nat \to Q \def
 \lambda p,q. Qtimes (nat_to_Q p) (Qinv (nat_to_Q q)).
 
-let rec times_f h g \def
-  match h with
-  [nf_last a \Rightarrow 
-    match g with
-    [nf_last b \Rightarrow nf_last (S (a+b))
-    |nf_cons b g1 \Rightarrow nf_cons (S (a+b)) g1
-    ]
-  |nf_cons a h1 \Rightarrow 
-    match g with
-    [nf_last b \Rightarrow nf_cons (S (a+b)) h1
-    |nf_cons b g1 \Rightarrow nf_cons (a+b) (times_f h1 g1)
-    ]
-  ]
-.
-
-definition times_fa \def 
-\lambda f,g.
-match f with
-[nfa_zero \Rightarrow nfa_zero
-|nfa_one \Rightarrow g
-|nfa_proper f1 \Rightarrow match g with
-  [nfa_zero \Rightarrow nfa_zero
-  |nfa_one \Rightarrow nfa_proper f1
-  |nfa_proper g1 \Rightarrow nfa_proper (times_f f1 g1)
-  ]
-]
-.
-
-theorem eq_times_f_times1:\forall g,h,m. defactorize_aux (times_f g h) m
-=defactorize_aux g m*defactorize_aux h m.
-intro.elim g
-  [elim h;simplify;autobatch
-  |elim h
-    [simplify;autobatch
-    |simplify.rewrite > (H n3 (S m)).autobatch
-    ]
-  ]
-qed.
-    
-theorem eq_times_fa_times: \forall f,g.
-defactorize (times_fa f g) = defactorize f*defactorize g.
-intros.
-elim f
-  [reflexivity
-  |simplify.apply plus_n_O
-  |elim g;simplify
-    [apply times_n_O
-    |apply times_n_SO
-    |apply eq_times_f_times1
-    ]
-  ]
-qed.
-
-theorem eq_times_times_fa: \forall n,m.
-factorize (n*m) = times_fa (factorize n) (factorize m).
-intros.
-rewrite <(factorize_defactorize (times_fa (factorize n) (factorize m))).
-rewrite > eq_times_fa_times.
-rewrite > defactorize_factorize.
-rewrite > defactorize_factorize.
-reflexivity.
-qed.
-
-
-theorem eq_plus_Zplus: \forall n,m:nat. Z_of_nat (n+m) =
-Z_of_nat n + Z_of_nat m.
-intro.cases n;intro
-  [reflexivity
-  |cases m
-    [simplify.rewrite < plus_n_O.reflexivity
-    |simplify.reflexivity.
-    ]
-  ]
-qed.
-
-theorem times_f_ftimes: \forall n,m.
-frac (nat_fact_to_fraction (times_f n m))
-= ftimes (nat_fact_to_fraction n) (nat_fact_to_fraction m).
-intro.
-elim n
-  [elim m
-    [simplify.
-     rewrite < plus_n_Sm.reflexivity
-    |elim n2
-      [simplify.rewrite < plus_n_O.reflexivity
-      |simplify.reflexivity.
-      ]    
-    ]
-  |elim m
-    [elim n1
-      [simplify.reflexivity
-      |simplify.rewrite < plus_n_Sm.reflexivity
-      ]
-    |simplify.
-     cut (\exist h.ftimes (nat_fact_to_fraction n2) (nat_fact_to_fraction n4) = frac h)
-      [elim Hcut.
-       rewrite > H2.
-       simplify.apply eq_f.
-       apply eq_f2
-        [apply eq_plus_Zplus
-        |apply injective_frac.
-         rewrite < H2.
-         apply H
-        ]
-      |generalize in match n4.
-       elim n2
-        [cases n6;simplify;autobatch
-        |cases n7;simplify
-          [autobatch
-          |elim (H2 n9).
-           rewrite > H3.
-           simplify.
-           autobatch
-          ]
-        ]
-      ]
-    ]
-  ]
-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 rtimes_Zplus3: \forall x,y:Z.\forall f,g:fraction. 
-(rtimes (frac f) (frac g) = one \land 
- rtimes (frac (cons x f)) (frac (cons y g)) = nat_frac_item_to_ratio (x + y))
-\lor (\exists h.rtimes (frac f) (frac g) = frac h \land
-rtimes (frac (cons x f)) (frac (cons y g)) =
-frac (cons (x + y) h)).
-intros.
-simplify.
-elim (rtimes (frac f) (frac g));simplify
-  [left.split;reflexivity
-  |right.
-   apply (ex_intro ? ? f1).
-   split;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 Qtimes_OQ: \forall q.Qtimes q OQ = OQ.
-intro.cases q;reflexivity.
-qed.
-
-theorem symmetric_Qtimes: symmetric ? Qtimes.
-unfold.intros.
-cases x
-  [simplify in ⊢ (? ? % ?).rewrite > Qtimes_OQ.reflexivity
-  |elim y
-    [reflexivity
-    |simplify.rewrite > symmetric_rtimes.reflexivity
-    |simplify.rewrite > symmetric_rtimes.reflexivity
-    ]
-  |elim y
-    [reflexivity
-    |simplify.rewrite > symmetric_rtimes.reflexivity
-    |simplify.rewrite > symmetric_rtimes.reflexivity
-    ]
-  ]
-qed.
-
-theorem Qtimes_Qinv: \forall q. q \neq OQ \to Qtimes q (Qinv q) = Qone.
-intro.
-cases q;intro
-  [elim H.reflexivity
-  |simplify.rewrite > rtimes_rinv.reflexivity
-  |simplify.rewrite > rtimes_rinv.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_frac_frac: \forall p,q,r,s.
 Qtimes (frac p q) (frac r s) = (frac (p*r) (q*s)).
 intros.
@@ -345,7 +50,7 @@ rewrite < Qinv_Qtimes'.
 rewrite < times_Qtimes.
 reflexivity.
 qed.
-
+*)
 
 (* la prova seguente e' tutta una ripetizione. Sistemare. *)
 (*CSC
@@ -469,12 +174,6 @@ definition numQ:Q \to nat \def
 definition denomQ:Q \to nat \def
 \lambda q. defactorize (numeratorQ (Qinv q)).
 
-definition Qopp:Q \to Q \def \lambda q.
-match q with
-[OQ \Rightarrow OQ
-|Qpos q \Rightarrow Qneg q
-|Qneg q \Rightarrow Qpos q
-].
 (*CSC
 theorem frac_numQ_denomQ1: \forall r:ratio. 
 frac (numQ (Qpos r)) (denomQ (Qpos r)) = (Qpos r).

diff --git a/helm/software/matita/library/Q/fraction/ftimes.ma b/helm/software/matita/library/Q/fraction/ftimes.ma
index 2e5871d7390a897df7acfbd48f402d2ec433a2de..bcc7358b27a5ed0b3098c5cbb859a7a12d95a1fd 100644 (file)
--- a/helm/software/matita/library/Q/fraction/ftimes.ma
+++ b/helm/software/matita/library/Q/fraction/ftimes.ma
@@ -14,6 +14,8 @@
 
 include "Q/ratio/ratio.ma".
 include "Q/fraction/finv.ma".
+include "Q/nat_fact/times.ma".
+include "Z/times.ma".
 
 definition nat_frac_item_to_ratio: Z \to ratio \def
 \lambda x:Z. match x with
@@ -88,3 +90,44 @@ intro.elim f.
   | (frac h) \Rightarrow frac (cons (z + - z) h)] = one).
   rewrite > H.rewrite > Zplus_Zopp.reflexivity.
 qed.
+
+theorem times_f_ftimes: \forall n,m.
+frac (nat_fact_to_fraction (times_f n m))
+= ftimes (nat_fact_to_fraction n) (nat_fact_to_fraction m).
+intro.
+elim n
+  [elim m
+    [simplify.
+     rewrite < plus_n_Sm.reflexivity
+    |elim n2
+      [simplify.rewrite < plus_n_O.reflexivity
+      |simplify.reflexivity.
+      ]
+    ]
+  |elim m
+    [elim n1
+      [simplify.reflexivity
+      |simplify.rewrite < plus_n_Sm.reflexivity
+      ]
+    |simplify.
+     cut (\exist h.ftimes (nat_fact_to_fraction n2) (nat_fact_to_fraction n4) = frac h)
+      [elim Hcut.
+       rewrite > H2.
+       simplify.apply eq_f.
+       apply eq_f2
+        [apply eq_plus_Zplus
+        |apply injective_frac.
+         rewrite < H2.
+         apply H
+        ]
+      |generalize in match n4.
+       elim n2
+        [cases n6;simplify;autobatch
+        |cases n7;simplify
+          [autobatch
+          |elim (H2 n9).
+           rewrite > H3.
+           simplify.
+           autobatch
+          ]]]]]
+qed.
\ No newline at end of file

diff --git a/helm/software/matita/library/Q/nat_fact/times.ma b/helm/software/matita/library/Q/nat_fact/times.ma
new file mode 100644 (file)
index 0000000..43c213c
--- /dev/null
+++ b/helm/software/matita/library/Q/nat_fact/times.ma
@@ -0,0 +1,75 @@
+(**************************************************************************)
+(*       ___                                                               *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "nat/factorization.ma".
+
+let rec times_f h g \def
+  match h with
+  [nf_last a \Rightarrow 
+    match g with
+    [nf_last b \Rightarrow nf_last (S (a+b))
+    |nf_cons b g1 \Rightarrow nf_cons (S (a+b)) g1
+    ]
+  |nf_cons a h1 \Rightarrow 
+    match g with
+    [nf_last b \Rightarrow nf_cons (S (a+b)) h1
+    |nf_cons b g1 \Rightarrow nf_cons (a+b) (times_f h1 g1)
+    ]].
+
+theorem eq_times_f_times1:\forall g,h,m. defactorize_aux (times_f g h) m
+=defactorize_aux g m*defactorize_aux h m.
+intro.elim g
+  [elim h;simplify;autobatch
+  |elim h
+    [simplify;autobatch
+    |simplify.rewrite > (H n3 (S m)).autobatch
+    ]]
+qed.
+
+
+(******************* times_fa *********************)
+
+definition times_fa \def 
+\lambda f,g.
+match f with
+[nfa_zero \Rightarrow nfa_zero
+|nfa_one \Rightarrow g
+|nfa_proper f1 \Rightarrow match g with
+  [nfa_zero \Rightarrow nfa_zero
+  |nfa_one \Rightarrow nfa_proper f1
+  |nfa_proper g1 \Rightarrow nfa_proper (times_f f1 g1)
+  ]].
+
+theorem eq_times_fa_times: \forall f,g.
+defactorize (times_fa f g) = defactorize f*defactorize g.
+intros.
+elim f
+  [reflexivity
+  |simplify.apply plus_n_O
+  |elim g;simplify
+    [apply times_n_O
+    |apply times_n_SO
+    |apply eq_times_f_times1
+    ]]
+qed.
+
+theorem eq_times_times_fa: \forall n,m.
+factorize (n*m) = times_fa (factorize n) (factorize m).
+intros.
+rewrite <(factorize_defactorize (times_fa (factorize n) (factorize m))).
+rewrite > eq_times_fa_times.
+rewrite > defactorize_factorize.
+rewrite > defactorize_factorize.
+reflexivity.
+qed.
\ No newline at end of file

diff --git a/helm/software/matita/library/Q/q/qtimes.ma b/helm/software/matita/library/Q/q/qtimes.ma
index e288ef412c4732badb25cee471c2952d75e96e6d..52246e5a57794a159c34d7445c3f0cd6c9c114b8 100644 (file)
--- a/helm/software/matita/library/Q/q/qtimes.ma
+++ b/helm/software/matita/library/Q/q/qtimes.ma
@@ -75,3 +75,117 @@ 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.

diff --git a/helm/software/matita/library/Q/ratio/rtimes.ma b/helm/software/matita/library/Q/ratio/rtimes.ma
index 3c7859dbedcdee7c29a615863be077c4190b24ab..a8255afef85d43f274e15979cd1dd8aa2a9ccb43 100644 (file)
--- a/helm/software/matita/library/Q/ratio/rtimes.ma
+++ b/helm/software/matita/library/Q/ratio/rtimes.ma
@@ -443,3 +443,18 @@ intro.elim r.
 reflexivity.
 simplify.apply ftimes_finv.
 qed.
+
+theorem rtimes_Zplus3: \forall x,y:Z.\forall f,g:fraction.
+(rtimes (frac f) (frac g) = one \land
+ rtimes (frac (cons x f)) (frac (cons y g)) = nat_frac_item_to_ratio (x + y))
+\lor (\exists h.rtimes (frac f) (frac g) = frac h \land
+rtimes (frac (cons x f)) (frac (cons y g)) =
+frac (cons (x + y) h)).
+intros.
+simplify.
+elim (rtimes (frac f) (frac g));simplify
+  [left.split;reflexivity
+  |right.
+   apply (ex_intro ? ? f1).
+   split;reflexivity]
+qed.
\ No newline at end of file

diff --git a/helm/software/matita/library/Z/times.ma b/helm/software/matita/library/Z/times.ma
index 90a71b520ff3fde852bb2026812af9beea519cbe..c81c0dfca85537d72f218c8c0eab8a66dfb5368a 100644 (file)
--- a/helm/software/matita/library/Z/times.ma
+++ b/helm/software/matita/library/Z/times.ma
@@ -251,3 +251,13 @@ qed.
 variant distr_Ztimes_Zplus: \forall x,y,z.
 x * (y + z) = x*y + x*z \def
 distributive_Ztimes_Zplus.
+
+theorem eq_plus_Zplus: \forall n,m:nat. Z_of_nat (n+m) =
+Z_of_nat n + Z_of_nat m.
+intro.cases n;intro
+  [reflexivity
+  |cases m
+    [simplify.rewrite < plus_n_O.reflexivity
+    |simplify.reflexivity.
+    ]]
+qed.

diff --git a/helm/software/matita/library/depends b/helm/software/matita/library/depends
index 328e2088fcb6ca2d170f9eb0233d4e82277228be..b17029e9226db6deb50c1fc949d3a11dc55bceb6 100644 (file)
--- a/helm/software/matita/library/depends
+++ b/helm/software/matita/library/depends
@@ -33,6 +33,7 @@ Q/ratio/rtimes.ma Q/fraction/ftimes.ma Q/ratio/rinv.ma
 Q/fraction/fraction.ma Z/compare.ma nat/factorization.ma
 Q/fraction/finv.ma Q/fraction/fraction.ma Z/plus.ma
 Q/fraction/ftimes.ma Q/fraction/finv.ma Q/ratio/ratio.ma
+Q/nat_fact/times.ma nat/factorization.ma
 datatypes/compare.ma 
 datatypes/constructors.ma logic/equality.ma
 datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma