From e85acd6f01bccc0b4a6750dd6d2710d7b511948a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 6 Jun 2008 18:02:15 +0000 Subject: [PATCH] Even more Q stuff moved around. --- helm/software/matita/library/Q/frac.ma | 108 +------------- .../matita/library/Q/fraction/finv.ma | 67 +-------- .../matita/library/Q/fraction/fraction.ma | 50 ------- .../Q/fraction/numerator_denominator.ma | 132 ++++++++++++++++++ helm/software/matita/library/Q/q/q.ma | 1 + helm/software/matita/library/Q/q/qtimes.ma | 50 +++++++ helm/software/matita/library/depends | 3 +- 7 files changed, 191 insertions(+), 220 deletions(-) create mode 100644 helm/software/matita/library/Q/fraction/numerator_denominator.ma diff --git a/helm/software/matita/library/Q/frac.ma b/helm/software/matita/library/Q/frac.ma index d00cd3158..a1f0cd54a 100644 --- a/helm/software/matita/library/Q/frac.ma +++ b/helm/software/matita/library/Q/frac.ma @@ -52,112 +52,8 @@ reflexivity. qed. *) -(* la prova seguente e' tutta una ripetizione. Sistemare. *) -(*CSC -theorem Qtimes1: \forall f:fraction. -Qtimes (nat_fact_all_to_Q (numerator f)) -(Qinv (nat_fact_all_to_Q (numerator (finv 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 - |simplify. - rewrite > H2.rewrite > H1.simplify. - rewrite > Hcut.reflexivity - |simplify. - rewrite > H2.rewrite > H1.simplify. - rewrite > Hcut.reflexivity - ] - |generalize in match H. - rewrite > H2.rewrite > H1.simplify. - intro.destruct H3.assumption - ] - |elim H1.clear H1. - elim z - [simplify. - rewrite > H2.rewrite > H2.simplify. - elim (or_numerator_nfa_one_nfa_proper (finv f1)) - [elim H1.clear H1. - rewrite > H3.simplify. - cut (nat_fact_to_fraction a = f1) - [rewrite > Hcut.reflexivity - |generalize in match H. - rewrite > H2. - rewrite > H3. - rewrite > Qtimes_q_Qone. - intro. - destruct H1. - assumption - ] - |elim H1.clear H1. - generalize in match H. - rewrite > H2. - rewrite > H3.simplify. - intro. - destruct H1. - rewrite > Hcut. - simplify.reflexivity - ] - |simplify.rewrite > H2.simplify. - elim (or_numerator_nfa_one_nfa_proper (finv f1)) - [elim H1.clear H1. - rewrite > H3.simplify. - cut (nat_fact_to_fraction a = f1) - [rewrite > Hcut.reflexivity - |generalize in match H. - rewrite > H2. - rewrite > H3. - rewrite > Qtimes_q_Qone. - intro. - destruct H1. - assumption - ] - |elim H1.clear H1. - generalize in match H. - rewrite > H2. - rewrite > H3.simplify. - intro. - destruct H1. - rewrite > Hcut. - simplify.reflexivity - ] - |simplify.rewrite > H2.simplify. - elim (or_numerator_nfa_one_nfa_proper (finv f1)) - [elim H1.clear H1. - rewrite > H3.simplify. - cut (nat_fact_to_fraction a = f1) - [rewrite > Hcut.reflexivity - |generalize in match H. - rewrite > H2. - rewrite > H3. - rewrite > Qtimes_q_Qone. - intro. - destruct H1. - assumption - ] - |elim H1.clear H1. - generalize in match H. - rewrite > H2. - rewrite > H3.simplify. - intro. - destruct H1. - rewrite > Hcut. - simplify.reflexivity - ] - ] - ] - ] -qed. -*) +Qtimes1 == Qtimes_numerator_denominator + (* definition numQ:Q \to Z \def \lambda q. diff --git a/helm/software/matita/library/Q/fraction/finv.ma b/helm/software/matita/library/Q/fraction/finv.ma index 2868bece0..ce05b29c7 100644 --- a/helm/software/matita/library/Q/fraction/finv.ma +++ b/helm/software/matita/library/Q/fraction/finv.ma @@ -15,11 +15,11 @@ include "Z/plus.ma". include "Q/fraction/fraction.ma". -let rec finv f \def +let rec finv f ≝ match f with - [ (pp n) \Rightarrow (nn n) - | (nn n) \Rightarrow (pp n) - | (cons x g) \Rightarrow (cons (Zopp x) (finv g))]. + [ pp n ⇒ nn n + | nn n ⇒ pp n + | cons x g ⇒ cons (Zopp x) (finv g)]. theorem finv_finv: ∀f. finv (finv f) = f. intro; @@ -31,62 +31,3 @@ theorem finv_finv: ∀f. finv (finv f) = f. reflexivity ] qed. - -theorem or_numerator_nfa_one_nfa_proper: -∀f. - (numerator f = nfa_one ∧ ∃g.numerator (finv f) = nfa_proper g) ∨ - ∃g.numerator f = nfa_proper g. -intro.elim f - [simplify.right. - apply (ex_intro ? ? (nf_last n)).reflexivity - |simplify.left.split - [reflexivity - |apply (ex_intro ? ? (nf_last n)).reflexivity - ] - |elim H;clear H - [elim H1.clear H1. - elim H2.clear H2. - elim z - [simplify. - rewrite > H.rewrite > H1.simplify. - left.split - [reflexivity - |apply (ex_intro ? ? (nf_cons O a)).reflexivity - ] - |simplify. - rewrite > H.rewrite > H1.simplify. - right.apply (ex_intro ? ? (nf_last n)).reflexivity - |simplify. - rewrite > H.rewrite > H1.simplify. - left.split - [reflexivity - |apply (ex_intro ? ? (nf_cons (S n) a)).reflexivity - ] - ] - |elim H1.clear H1. - elim z - [simplify. - rewrite > H.simplify. - right. - apply (ex_intro ? ? (nf_cons O a)).reflexivity - |simplify. - rewrite > H.simplify. - right.apply (ex_intro ? ? (nf_cons (S n) a)).reflexivity - |simplify. - rewrite > H.simplify. - right. - apply (ex_intro ? ? (nf_cons O a)).reflexivity - ] - ] - ] -qed. - -theorem eq_nfa_one_to_eq_finv_nfa_proper: -∀f.numerator f = nfa_one → ∃h.numerator (finv f) = nfa_proper h. - intros; - elim (or_numerator_nfa_one_nfa_proper f); cases H1; - [ assumption - | rewrite > H in H2; - destruct - ] -qed. diff --git a/helm/software/matita/library/Q/fraction/fraction.ma b/helm/software/matita/library/Q/fraction/fraction.ma index 81b60de91..ba4b417f6 100644 --- a/helm/software/matita/library/Q/fraction/fraction.ma +++ b/helm/software/matita/library/Q/fraction/fraction.ma @@ -29,56 +29,6 @@ let rec nat_fact_to_fraction n ≝ | nf_cons m l ⇒ cons (Z_of_nat m) (nat_fact_to_fraction l) ]. -(* returns the numerator of a fraction in the form of a nat_fact_all *) -let rec numerator f \def - match f with - [pp a \Rightarrow nfa_proper (nf_last a) - |nn a \Rightarrow nfa_one - |cons a l \Rightarrow - let n \def numerator l in - match n with - [nfa_zero \Rightarrow (* this case is vacuous *) nfa_zero - |nfa_one \Rightarrow - match a with - [OZ \Rightarrow nfa_one - |pos x \Rightarrow nfa_proper (nf_last x) - |neg x \Rightarrow nfa_one - ] - |nfa_proper g \Rightarrow - match a with - [OZ \Rightarrow nfa_proper (nf_cons O g) - |pos x \Rightarrow nfa_proper (nf_cons (S x) g) - |neg x \Rightarrow nfa_proper (nf_cons O g) - ] - ] - ]. - -theorem not_eq_numerator_nfa_zero: -\forall f.numerator f \neq nfa_zero. -intro.elim f - [simplify.intro.destruct H - |simplify.intro.destruct H - |simplify.generalize in match H. - cases (numerator f1) - [intro.elim H1.reflexivity - |simplify.intro. - cases z;simplify;intro;destruct H2 - |simplify.intro. - cases z;simplify;intro;destruct H2 - ] - ] -qed. - -theorem numerator_nat_fact_to_fraction: \forall g:nat_fact. -numerator (nat_fact_to_fraction g) = nfa_proper g. -intro. -elim g - [simplify.reflexivity. - |simplify.rewrite > H.simplify. - cases n;reflexivity - ] -qed. - (* double elimination principles *) theorem fraction_elim2: \forall R:fraction \to fraction \to Prop. diff --git a/helm/software/matita/library/Q/fraction/numerator_denominator.ma b/helm/software/matita/library/Q/fraction/numerator_denominator.ma new file mode 100644 index 000000000..0b51d1112 --- /dev/null +++ b/helm/software/matita/library/Q/fraction/numerator_denominator.ma @@ -0,0 +1,132 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "Q/fraction/finv.ma". + +(* returns the numerator of a fraction in the form of a nat_fact_all *) +let rec numerator f \def + match f with + [pp a \Rightarrow nfa_proper (nf_last a) + |nn a \Rightarrow nfa_one + |cons a l \Rightarrow + let n \def numerator l in + match n with + [nfa_zero \Rightarrow (* this case is vacuous *) nfa_zero + |nfa_one \Rightarrow + match a with + [OZ \Rightarrow nfa_one + |pos x \Rightarrow nfa_proper (nf_last x) + |neg x \Rightarrow nfa_one + ] + |nfa_proper g \Rightarrow + match a with + [OZ \Rightarrow nfa_proper (nf_cons O g) + |pos x \Rightarrow nfa_proper (nf_cons (S x) g) + |neg x \Rightarrow nfa_proper (nf_cons O g) + ]]]. + +definition denominator ≝ λf.numerator (finv f). + +theorem not_eq_numerator_nfa_zero: ∀f.numerator f ≠ nfa_zero. +intro.elim f + [simplify.intro.destruct H + |simplify.intro.destruct H + |simplify.generalize in match H. + cases (numerator f1) + [intro.elim H1.reflexivity + |simplify.intro. + cases z;simplify;intro;destruct H2 + |simplify.intro. + cases z;simplify;intro;destruct H2]] +qed. + +theorem not_eq_denominator_nfa_zero: ∀f.denominator f ≠ nfa_zero. + unfold denominator; intro; apply not_eq_numerator_nfa_zero. +qed. + +theorem numerator_nat_fact_to_fraction: ∀g:nat_fact. +numerator (nat_fact_to_fraction g) = nfa_proper g. +intro. +elim g + [simplify.reflexivity. + |simplify.rewrite > H.simplify. + cases n;reflexivity + ] +qed. + +theorem denominator_nat_fact_to_fraction: ∀g:nat_fact. +denominator (finv (nat_fact_to_fraction g)) = nfa_proper g. + unfold denominator; + intro; + rewrite > finv_finv; + apply numerator_nat_fact_to_fraction. +qed. + +theorem or_numerator_nfa_one_nfa_proper: +∀f. + (numerator f = nfa_one ∧ ∃g.denominator f = nfa_proper g) ∨ + ∃g.numerator f = nfa_proper g. +intro.elim f + [simplify.right. + apply (ex_intro ? ? (nf_last n)).reflexivity + |simplify.left.split + [reflexivity + |apply (ex_intro ? ? (nf_last n)).reflexivity + ] + |elim H;clear H + [elim H1.clear H1. + elim H2.clear H2. + elim z + [simplify. + rewrite > H.rewrite > H1.simplify. + left.split + [reflexivity + |apply (ex_intro ? ? (nf_cons O a)).reflexivity + ] + |simplify. + rewrite > H.rewrite > H1.simplify. + right.apply (ex_intro ? ? (nf_last n)).reflexivity + |simplify. + rewrite > H.rewrite > H1.simplify. + left.split + [reflexivity + |apply (ex_intro ? ? (nf_cons (S n) a)).reflexivity + ] + ] + |elim H1.clear H1. + elim z + [simplify. + rewrite > H.simplify. + right. + apply (ex_intro ? ? (nf_cons O a)).reflexivity + |simplify. + rewrite > H.simplify. + right.apply (ex_intro ? ? (nf_cons (S n) a)).reflexivity + |simplify. + rewrite > H.simplify. + right. + apply (ex_intro ? ? (nf_cons O a)).reflexivity + ] + ] + ] +qed. + +theorem eq_nfa_one_to_eq_finv_nfa_proper: +∀f.numerator f = nfa_one → ∃h.denominator f = nfa_proper h. + intros; + elim (or_numerator_nfa_one_nfa_proper f); cases H1; + [ assumption + | rewrite > H in H2; + destruct] +qed. \ No newline at end of file diff --git a/helm/software/matita/library/Q/q/q.ma b/helm/software/matita/library/Q/q/q.ma index 43b090fef..960756abe 100644 --- a/helm/software/matita/library/Q/q/q.ma +++ b/helm/software/matita/library/Q/q/q.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "Q/ratio/ratio.ma". +include "Q/fraction/numerator_denominator.ma". (* a rational number is either O or a ratio with a sign *) inductive Q : Set \def diff --git a/helm/software/matita/library/Q/q/qtimes.ma b/helm/software/matita/library/Q/q/qtimes.ma index 52246e5a5..3b4b24b79 100644 --- a/helm/software/matita/library/Q/q/qtimes.ma +++ b/helm/software/matita/library/Q/q/qtimes.ma @@ -189,3 +189,53 @@ cases p |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. + + diff --git a/helm/software/matita/library/depends b/helm/software/matita/library/depends index b17029e92..2ae7107a4 100644 --- a/helm/software/matita/library/depends +++ b/helm/software/matita/library/depends @@ -32,7 +32,8 @@ Q/ratio/rinv.ma Q/fraction/finv.ma Q/ratio/ratio.ma 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/fraction/ftimes.ma Q/fraction/finv.ma Q/nat_fact/times.ma Q/ratio/ratio.ma Z/times.ma +Q/fraction/numerator_denominator.ma Q/fraction/finv.ma Q/nat_fact/times.ma nat/factorization.ma datatypes/compare.ma datatypes/constructors.ma logic/equality.ma -- 2.39.2