From: Claudio Sacerdoti Coen Date: Fri, 6 Jun 2008 12:53:35 +0000 (+0000) Subject: First snapshot at trying to clean up the Q library. X-Git-Tag: make_still_working~5072 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=13ee180b4b982b7a150e8d727ed4b83813ac3fa2;p=helm.git First snapshot at trying to clean up the Q library. --- diff --git a/helm/software/matita/library/Q/Qplus_andrea.ma b/helm/software/matita/library/Q/Qplus_andrea.ma index 027a3ee6a..64c74dc90 100644 --- a/helm/software/matita/library/Q/Qplus_andrea.ma +++ b/helm/software/matita/library/Q/Qplus_andrea.ma @@ -17,11 +17,6 @@ set "baseuri" "cic:/matita/Q/Qplus". include "nat/factorization.ma". include "Q/frac.ma". -definition Qplus: \lambda p,q. - - - - (* transformation from nat_fact to fracion *) let rec nat_fact_to_fraction l \def match l with diff --git a/helm/software/matita/library/Q/frac.ma b/helm/software/matita/library/Q/frac.ma index b5871dc94..334f1c868 100644 --- a/helm/software/matita/library/Q/frac.ma +++ b/helm/software/matita/library/Q/frac.ma @@ -17,146 +17,16 @@ set "baseuri" "cic:/matita/Q/frac". include "nat/factorization.ma". include "Q/q.ma". -(* transformation from nat_fact to fracion *) -let rec nat_fact_to_fraction l \def - match l with - [nf_last a \Rightarrow pp a - |nf_cons a p \Rightarrow - cons (Z_of_nat a) (nat_fact_to_fraction p) - ] -. - -(* 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 or_numerator_nfa_one_nfa_proper: -\forall f.(numerator f = nfa_one \land \exists g.numerator (finv f) = -nfa_proper g) \lor \exists 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: -\forall f.numerator f = nfa_one \to -\exist h.numerator (finv f) = nfa_proper h. -intro.elim f - [simplify in H.destruct H - |simplify.apply (ex_intro ? ? (nf_last n)).reflexivity - |generalize in match H1.clear H1. - generalize in match H.clear H. - simplify. - cases (numerator f1);simplify - [intros;destruct H1 - |intros;elim (H (refl_eq ? ?)). - rewrite > H2.simplify. - elim z;simplify - [apply (ex_intro ? ? (nf_cons O a)).reflexivity - |apply (ex_intro ? ? (nf_cons O a)).reflexivity - |apply (ex_intro ? ? (nf_cons (S n) a)).reflexivity - ] - |elim z;destruct H1 - ] - ] -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. definition numeratorQ \def \lambda q.match q with [OQ \Rightarrow nfa_zero - |pos r \Rightarrow + |Qpos r \Rightarrow match r with [one \Rightarrow nfa_one |frac x \Rightarrow numerator x ] - |neg r \Rightarrow + |Qneg r \Rightarrow match r with [one \Rightarrow nfa_one |frac x \Rightarrow numerator x @@ -193,6 +63,7 @@ let rec nat_fact_to_fraction_inv l \def ] . + (* definition nat_fact_all_to_Q_inv \def \lambda n. @@ -488,7 +359,7 @@ rtimes (rtimes (Z_to_ratio z) (frac f1)) (frac f2) =rtimes (Z_to_ratio z) (rtimes (frac f1) (frac f2)). intros 2.elim f1 [elim f2 - [change with + [ change with (rtimes (rtimes (Z_to_ratio z) (Z_to_ratio (pos n))) (Z_to_ratio (pos n1)) =rtimes (Z_to_ratio z) (rtimes (Z_to_ratio (pos n)) (Z_to_ratio (pos n1)))). rewrite > rtimes_Zplus.rewrite > rtimes_Zplus. @@ -874,7 +745,8 @@ cases x [simplify in ⊢ (? ? % ?).rewrite > Qtimes_OQ.reflexivity |elim y [reflexivity - |simplify.rewrite > symmetric_rtimes.reflexivity + |simplify.alias id "symmetric_rtimes" = "cic:/matita/Q/times/symmetric_rtimes.con". +rewrite > symmetric_rtimes.reflexivity |simplify.rewrite > symmetric_rtimes.reflexivity ] |elim y @@ -889,7 +761,8 @@ 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.alias id "rtimes_rinv" = "cic:/matita/Q/times/rtimes_rinv.con". +rewrite > rtimes_rinv.reflexivity |simplify.rewrite > rtimes_rinv.reflexivity ] qed. @@ -975,7 +848,7 @@ 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)))) @@ -1079,7 +952,7 @@ intro.elim f ] ] qed. - +*) (* definition numQ:Q \to Z \def \lambda q. @@ -1102,7 +975,7 @@ match q with |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). intro. @@ -1118,8 +991,9 @@ elim r |apply Qtimes1. ] ] -qed. +qed.*) +(*CSC theorem frac_numQ_denomQ2: \forall r:ratio. frac (numQ (Qneg r)) (denomQ (Qneg r)) = (Qpos r). intro. @@ -1135,7 +1009,7 @@ elim r |apply Qtimes1. ] ] -qed. +qed.*) definition Qabs:Q \to Q \def \lambda q. match q with @@ -1143,7 +1017,7 @@ match q with |Qpos q \Rightarrow Qpos q |Qneg q \Rightarrow Qpos q ]. - +(*CSC theorem frac_numQ_denomQ: \forall q. frac (numQ q) (denomQ q) = (Qabs q). intros. @@ -1152,8 +1026,8 @@ cases q |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ1 |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ2 ] -qed. - +qed.*) +(*CSC definition Qfrac: Z \to nat \to Q \def \lambda z,n.match z with [OZ \Rightarrow OQ @@ -1190,4 +1064,4 @@ cases q |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ2 ] qed. - +*) diff --git a/helm/software/matita/library/Q/fraction/finv.ma b/helm/software/matita/library/Q/fraction/finv.ma new file mode 100644 index 000000000..d9bf715b1 --- /dev/null +++ b/helm/software/matita/library/Q/fraction/finv.ma @@ -0,0 +1,93 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "Z/plus.ma". +include "Q/fraction/fraction.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))]. + +theorem finv_finv: ∀f. finv (finv f) = f. + intro; + elim f; + [1,2: reflexivity + | simplify; + rewrite > H; + rewrite > Zopp_Zopp; + 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 new file mode 100644 index 000000000..81b60de91 --- /dev/null +++ b/helm/software/matita/library/Q/fraction/fraction.ma @@ -0,0 +1,253 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "Z/compare.ma". +include "nat/factorization.ma". + +(* a fraction is a list of Z-coefficients for primes, in natural +order. The last coefficient must eventually be different from 0 *) + +inductive fraction : Set \def + pp : nat \to fraction +| nn: nat \to fraction +| cons : Z \to fraction \to fraction. + +let rec nat_fact_to_fraction n ≝ + match n with + [ nf_last m ⇒ pp m + | 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. +(\forall n:nat.\forall g:fraction.R (pp n) g) \to +(\forall n:nat.\forall g:fraction.R (nn n) g) \to +(\forall x:Z.\forall f:fraction.\forall m:nat.R (cons x f) (pp m)) \to +(\forall x:Z.\forall f:fraction.\forall m:nat.R (cons x f) (nn m)) \to +(\forall x,y:Z.\forall f,g:fraction.R f g \to R (cons x f) (cons y g)) \to +\forall f,g:fraction. R f g. +intros 7.elim f. + apply H. + apply H1. + elim g. + apply H2. + apply H3. + apply H4.apply H5. +qed. + +(* boolean equality *) +let rec eqfb f g \def +match f with +[ (pp n) \Rightarrow + match g with + [ (pp m) \Rightarrow eqb n m + | (nn m) \Rightarrow false + | (cons y g1) \Rightarrow false] +| (nn n) \Rightarrow + match g with + [ (pp m) \Rightarrow false + | (nn m) \Rightarrow eqb n m + | (cons y g1) \Rightarrow false] +| (cons x f1) \Rightarrow + match g with + [ (pp m) \Rightarrow false + | (nn m) \Rightarrow false + | (cons y g1) \Rightarrow andb (eqZb x y) (eqfb f1 g1)]]. + +(* discrimination *) +definition aux \def + \lambda f. match f with + [ (pp n) \Rightarrow n + | (nn n) \Rightarrow n + | (cons x f) \Rightarrow O]. + +definition fhd \def +\lambda f. match f with + [ (pp n) \Rightarrow (pos n) + | (nn n) \Rightarrow (neg n) + | (cons x f) \Rightarrow x]. + +definition ftl \def +\lambda f. match f with + [ (pp n) \Rightarrow (pp n) + | (nn n) \Rightarrow (nn n) + | (cons x f) \Rightarrow f]. + +theorem injective_pp : injective nat fraction pp. +unfold injective.intros. +change with ((aux (pp x)) = (aux (pp y))). +apply eq_f.assumption. +qed. + +theorem injective_nn : injective nat fraction nn. +unfold injective.intros. +change with ((aux (nn x)) = (aux (nn y))). +apply eq_f.assumption. +qed. + +theorem eq_cons_to_eq1: \forall f,g:fraction.\forall x,y:Z. +(cons x f) = (cons y g) \to x = y. +intros. +change with ((fhd (cons x f)) = (fhd (cons y g))). +apply eq_f.assumption. +qed. + +theorem eq_cons_to_eq2: \forall x,y:Z.\forall f,g:fraction. +(cons x f) = (cons y g) \to f = g. +intros. +change with ((ftl (cons x f)) = (ftl (cons y g))). +apply eq_f.assumption. +qed. + +theorem not_eq_pp_nn: \forall n,m:nat. pp n \neq nn m. +intros.unfold Not. intro. +change with match (pp n) with +[ (pp n) \Rightarrow False +| (nn n) \Rightarrow True +| (cons x f) \Rightarrow True]. +rewrite > H. +simplify.exact I. +qed. + +theorem not_eq_pp_cons: +\forall n:nat.\forall x:Z. \forall f:fraction. +pp n \neq cons x f. +intros.unfold Not. intro. +change with match (pp n) with +[ (pp n) \Rightarrow False +| (nn n) \Rightarrow True +| (cons x f) \Rightarrow True]. +rewrite > H. +simplify.exact I. +qed. + +theorem not_eq_nn_cons: +\forall n:nat.\forall x:Z. \forall f:fraction. +nn n \neq cons x f. +intros.unfold Not. intro. +change with match (nn n) with +[ (pp n) \Rightarrow True +| (nn n) \Rightarrow False +| (cons x f) \Rightarrow True]. +rewrite > H. +simplify.exact I. +qed. + +theorem decidable_eq_fraction: \forall f,g:fraction. +decidable (f = g). +intros.unfold decidable. +apply (fraction_elim2 (\lambda f,g. f=g \lor (f=g \to False))). + intros.elim g1. + elim ((decidable_eq_nat n n1) : n=n1 \lor (n=n1 \to False)). + left.apply eq_f. assumption. + right.intro.apply H.apply injective_pp.assumption. + right.apply not_eq_pp_nn. + right.apply not_eq_pp_cons. + intros. elim g1. + right.intro.apply (not_eq_pp_nn n1 n).apply sym_eq. assumption. + elim ((decidable_eq_nat n n1) : n=n1 \lor (n=n1 \to False)). + left. apply eq_f. assumption. + right.intro.apply H.apply injective_nn.assumption. + right.apply not_eq_nn_cons. + intros.right.intro.apply (not_eq_pp_cons m x f1).apply sym_eq.assumption. + intros.right.intro.apply (not_eq_nn_cons m x f1).apply sym_eq.assumption. + intros.elim H. + elim ((decidable_eq_Z x y) : x=y \lor (x=y \to False)). + left.apply eq_f2.assumption. + assumption. + right.intro.apply H2.apply (eq_cons_to_eq1 f1 g1).assumption. + right.intro.apply H1.apply (eq_cons_to_eq2 x y f1 g1).assumption. +qed. + +theorem eqfb_to_Prop: \forall f,g:fraction. +match (eqfb f g) with +[true \Rightarrow f=g +|false \Rightarrow f \neq g]. +intros.apply (fraction_elim2 +(\lambda f,g.match (eqfb f g) with +[true \Rightarrow f=g +|false \Rightarrow f \neq g])). + intros.elim g1. + simplify.apply eqb_elim. + intro.simplify.apply eq_f.assumption. + intro.simplify.unfold Not.intro.apply H.apply injective_pp.assumption. + simplify.apply not_eq_pp_nn. + simplify.apply not_eq_pp_cons. + intros.elim g1. + simplify.unfold Not.intro.apply (not_eq_pp_nn n1 n).apply sym_eq. assumption. + simplify.apply eqb_elim.intro.simplify.apply eq_f.assumption. + intro.simplify.unfold Not.intro.apply H.apply injective_nn.assumption. + simplify.apply not_eq_nn_cons. + intros.simplify.unfold Not.intro.apply (not_eq_pp_cons m x f1).apply sym_eq. assumption. + intros.simplify.unfold Not.intro.apply (not_eq_nn_cons m x f1).apply sym_eq. assumption. + intros. + simplify. + apply eqZb_elim. + intro.generalize in match H.elim (eqfb f1 g1). + simplify.apply eq_f2.assumption. + apply H2. + simplify.unfold Not.intro.apply H2.apply (eq_cons_to_eq2 x y).assumption. + intro.simplify.unfold Not.intro.apply H1.apply (eq_cons_to_eq1 f1 g1).assumption. +qed. diff --git a/helm/software/matita/library/Q/fraction/ftimes.ma b/helm/software/matita/library/Q/fraction/ftimes.ma new file mode 100644 index 000000000..2e5871d73 --- /dev/null +++ b/helm/software/matita/library/Q/fraction/ftimes.ma @@ -0,0 +1,90 @@ +(**************************************************************************) +(* ___ *) +(* ||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/ratio/ratio.ma". +include "Q/fraction/finv.ma". + +definition nat_frac_item_to_ratio: Z \to ratio \def +\lambda x:Z. match x with +[ OZ \Rightarrow one +| (pos n) \Rightarrow frac (pp n) +| (neg n) \Rightarrow frac (nn n)]. + +let rec ftimes f g \def + match f with + [ (pp n) \Rightarrow + match g with + [(pp m) \Rightarrow nat_frac_item_to_ratio (pos n + pos m) + | (nn m) \Rightarrow nat_frac_item_to_ratio (pos n + neg m) + | (cons y g1) \Rightarrow frac (cons (pos n + y) g1)] + | (nn n) \Rightarrow + match g with + [(pp m) \Rightarrow nat_frac_item_to_ratio (neg n + pos m) + | (nn m) \Rightarrow nat_frac_item_to_ratio (neg n + neg m) + | (cons y g1) \Rightarrow frac (cons (neg n + y) g1)] + | (cons x f1) \Rightarrow + match g with + [ (pp m) \Rightarrow frac (cons (x + pos m) f1) + | (nn m) \Rightarrow frac (cons (x + neg m) f1) + | (cons y g1) \Rightarrow + match ftimes f1 g1 with + [ one \Rightarrow nat_frac_item_to_ratio (x + y) + | (frac h) \Rightarrow frac (cons (x + y) h)]]]. + +theorem symmetric2_ftimes: symmetric2 fraction ratio ftimes. +unfold symmetric2. intros.apply (fraction_elim2 (\lambda f,g.ftimes f g = ftimes g f)). + intros.elim g. + change with (nat_frac_item_to_ratio (pos n + pos n1) = nat_frac_item_to_ratio (pos n1 + pos n)). + apply eq_f.apply sym_Zplus. + change with (nat_frac_item_to_ratio (pos n + neg n1) = nat_frac_item_to_ratio (neg n1 + pos n)). + apply eq_f.apply sym_Zplus. + change with (frac (cons (pos n + z) f) = frac (cons (z + pos n) f)). + rewrite < sym_Zplus.reflexivity. + intros.elim g. + change with (nat_frac_item_to_ratio (neg n + pos n1) = nat_frac_item_to_ratio (pos n1 + neg n)). + apply eq_f.apply sym_Zplus. + change with (nat_frac_item_to_ratio (neg n + neg n1) = nat_frac_item_to_ratio (neg n1 + neg n)). + apply eq_f.apply sym_Zplus. + change with (frac (cons (neg n + z) f) = frac (cons (z + neg n) f)). + rewrite < sym_Zplus.reflexivity. + intros.change with (frac (cons (x1 + pos m) f) = frac (cons (pos m + x1) f)). + rewrite < sym_Zplus.reflexivity. + intros.change with (frac (cons (x1 + neg m) f) = frac (cons (neg m + x1) f)). + rewrite < sym_Zplus.reflexivity. + intros. + (*CSC: simplify does something nasty here because of a redex in Zplus *) + change with + (match ftimes f g with + [ one \Rightarrow nat_frac_item_to_ratio (x1 + y1) + | (frac h) \Rightarrow frac (cons (x1 + y1) h)] = + match ftimes g f with + [ one \Rightarrow nat_frac_item_to_ratio (y1 + x1) + | (frac h) \Rightarrow frac (cons (y1 + x1) h)]). + rewrite < H.rewrite < sym_Zplus.reflexivity. +qed. + +theorem ftimes_finv : \forall f:fraction. ftimes f (finv f) = one. +intro.elim f. + change with (nat_frac_item_to_ratio (pos n + - (pos n)) = one). + rewrite > Zplus_Zopp.reflexivity. + change with (nat_frac_item_to_ratio (neg n + - (neg n)) = one). + rewrite > Zplus_Zopp.reflexivity. + (*CSC: simplify does something nasty here because of a redex in Zplus *) +(* again: we would need something to help finding the right change *) + change with + (match ftimes f1 (finv f1) with + [ one \Rightarrow nat_frac_item_to_ratio (z + - z) + | (frac h) \Rightarrow frac (cons (z + - z) h)] = one). + rewrite > H.rewrite > Zplus_Zopp.reflexivity. +qed. diff --git a/helm/software/matita/library/Q/inv.ma b/helm/software/matita/library/Q/inv.ma index 39b9c776e..8c6f1db95 100644 --- a/helm/software/matita/library/Q/inv.ma +++ b/helm/software/matita/library/Q/inv.ma @@ -14,55 +14,6 @@ include "Q/q.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))]. - -theorem finv_finv: ∀f. finv (finv f) = f. - intro; - elim f; - [1,2: reflexivity - | simplify; - rewrite > H; - rewrite > Zopp_Zopp; - reflexivity - ] -qed. - -definition rinv : ratio \to ratio \def -\lambda r:ratio. - match r with - [one \Rightarrow one - | (frac f) \Rightarrow frac (finv f)]. - -theorem rinv_rinv: ∀r. rinv (rinv r) = r. - intro; - elim r; - [ reflexivity - | simplify; - rewrite > finv_finv; - reflexivity] -qed. - -definition Qinv : Q → Q ≝ - λp. - match p with - [ OQ ⇒ OQ (* arbitrary value *) - | Qpos r ⇒ Qpos (rinv r) - | Qneg r ⇒ Qneg (rinv r) - ]. - -theorem Qinv_Qinv: ∀q. Qinv (Qinv q) = q. - intro; - elim q; - [ reflexivity - |*:simplify; - rewrite > rinv_rinv; - reflexivity] -qed. - theorem denominator_integral_factor_finv: ∀f. enumerator_integral_fraction f = denominator_integral_fraction (finv f). intro; @@ -135,4 +86,4 @@ theorem is_negative_enumerator_Qinv: [ rewrite > Qinv_Qinv in Hletin; assumption | generalize in match H; elim q; assumption] -qed. \ No newline at end of file +qed. diff --git a/helm/software/matita/library/Q/q.ma b/helm/software/matita/library/Q/q.ma index bc1fff067..683ddeb88 100644 --- a/helm/software/matita/library/Q/q.ma +++ b/helm/software/matita/library/Q/q.ma @@ -16,62 +16,6 @@ include "Z/compare.ma". include "Z/plus.ma". include "nat/factorization.ma". -(* a fraction is a list of Z-coefficients for primes, in natural -order. The last coefficient must eventually be different from 0 *) - -inductive fraction : Set \def - pp : nat \to fraction -| nn: nat \to fraction -| cons : Z \to fraction \to fraction. - -let rec fraction_of_nat_fact n ≝ - match n with - [ nf_last m ⇒ pp m - | nf_cons m l ⇒ cons (Z_of_nat (S m)) (fraction_of_nat_fact l) - ]. - -(* a fraction is integral if every coefficient is not negative *) -let rec nat_fact_of_integral_fraction n ≝ - match n with - [ pp n ⇒ nf_last n - | nn _ ⇒ nf_last O (* dummy value *) - | cons z l ⇒ - match z with - [ OZ ⇒ nf_cons O (nat_fact_of_integral_fraction l) - | pos n ⇒ nf_cons n (nat_fact_of_integral_fraction l) - | neg n ⇒ nf_last O (* dummy value *) - ] - ]. - -theorem nat_fact_of_integral_fraction_fraction_of_nat_fact: - ∀n. nat_fact_of_integral_fraction (fraction_of_nat_fact n) = n. - intro; - elim n; - [ reflexivity; - | simplify; - rewrite > H; - reflexivity - ] -qed. - -inductive ratio : Set \def - one : ratio - | frac : fraction \to ratio. - -(* a rational number is either O or a ratio with a sign *) -inductive Q : Set \def - OQ : Q - | Qpos : ratio \to Q - | Qneg : ratio \to Q. - -definition Q_of_nat ≝ - λn. - match factorize n with - [ nfa_zero ⇒ OQ - | nfa_one ⇒ Qpos one - | nfa_proper l ⇒ Qpos (frac (fraction_of_nat_fact l)) - ]. - let rec enumerator_integral_fraction l ≝ match l with [ pp n ⇒ Some ? l @@ -150,176 +94,3 @@ definition denominator ≝ | Qpos r ⇒ denominator_of_fraction r | Qneg r ⇒ denominator_of_fraction r ]. - -(* double elimination principles *) -theorem fraction_elim2: -\forall R:fraction \to fraction \to Prop. -(\forall n:nat.\forall g:fraction.R (pp n) g) \to -(\forall n:nat.\forall g:fraction.R (nn n) g) \to -(\forall x:Z.\forall f:fraction.\forall m:nat.R (cons x f) (pp m)) \to -(\forall x:Z.\forall f:fraction.\forall m:nat.R (cons x f) (nn m)) \to -(\forall x,y:Z.\forall f,g:fraction.R f g \to R (cons x f) (cons y g)) \to -\forall f,g:fraction. R f g. -intros 7.elim f. - apply H. - apply H1. - elim g. - apply H2. - apply H3. - apply H4.apply H5. -qed. - -(* boolean equality *) -let rec eqfb f g \def -match f with -[ (pp n) \Rightarrow - match g with - [ (pp m) \Rightarrow eqb n m - | (nn m) \Rightarrow false - | (cons y g1) \Rightarrow false] -| (nn n) \Rightarrow - match g with - [ (pp m) \Rightarrow false - | (nn m) \Rightarrow eqb n m - | (cons y g1) \Rightarrow false] -| (cons x f1) \Rightarrow - match g with - [ (pp m) \Rightarrow false - | (nn m) \Rightarrow false - | (cons y g1) \Rightarrow andb (eqZb x y) (eqfb f1 g1)]]. - -(* discrimination *) -definition aux \def - \lambda f. match f with - [ (pp n) \Rightarrow n - | (nn n) \Rightarrow n - | (cons x f) \Rightarrow O]. - -definition fhd \def -\lambda f. match f with - [ (pp n) \Rightarrow (pos n) - | (nn n) \Rightarrow (neg n) - | (cons x f) \Rightarrow x]. - -definition ftl \def -\lambda f. match f with - [ (pp n) \Rightarrow (pp n) - | (nn n) \Rightarrow (nn n) - | (cons x f) \Rightarrow f]. - -theorem injective_pp : injective nat fraction pp. -unfold injective.intros. -change with ((aux (pp x)) = (aux (pp y))). -apply eq_f.assumption. -qed. - -theorem injective_nn : injective nat fraction nn. -unfold injective.intros. -change with ((aux (nn x)) = (aux (nn y))). -apply eq_f.assumption. -qed. - -theorem eq_cons_to_eq1: \forall f,g:fraction.\forall x,y:Z. -(cons x f) = (cons y g) \to x = y. -intros. -change with ((fhd (cons x f)) = (fhd (cons y g))). -apply eq_f.assumption. -qed. - -theorem eq_cons_to_eq2: \forall x,y:Z.\forall f,g:fraction. -(cons x f) = (cons y g) \to f = g. -intros. -change with ((ftl (cons x f)) = (ftl (cons y g))). -apply eq_f.assumption. -qed. - -theorem not_eq_pp_nn: \forall n,m:nat. pp n \neq nn m. -intros.unfold Not. intro. -change with match (pp n) with -[ (pp n) \Rightarrow False -| (nn n) \Rightarrow True -| (cons x f) \Rightarrow True]. -rewrite > H. -simplify.exact I. -qed. - -theorem not_eq_pp_cons: -\forall n:nat.\forall x:Z. \forall f:fraction. -pp n \neq cons x f. -intros.unfold Not. intro. -change with match (pp n) with -[ (pp n) \Rightarrow False -| (nn n) \Rightarrow True -| (cons x f) \Rightarrow True]. -rewrite > H. -simplify.exact I. -qed. - -theorem not_eq_nn_cons: -\forall n:nat.\forall x:Z. \forall f:fraction. -nn n \neq cons x f. -intros.unfold Not. intro. -change with match (nn n) with -[ (pp n) \Rightarrow True -| (nn n) \Rightarrow False -| (cons x f) \Rightarrow True]. -rewrite > H. -simplify.exact I. -qed. - -theorem decidable_eq_fraction: \forall f,g:fraction. -decidable (f = g). -intros.unfold decidable. -apply (fraction_elim2 (\lambda f,g. f=g \lor (f=g \to False))). - intros.elim g1. - elim ((decidable_eq_nat n n1) : n=n1 \lor (n=n1 \to False)). - left.apply eq_f. assumption. - right.intro.apply H.apply injective_pp.assumption. - right.apply not_eq_pp_nn. - right.apply not_eq_pp_cons. - intros. elim g1. - right.intro.apply (not_eq_pp_nn n1 n).apply sym_eq. assumption. - elim ((decidable_eq_nat n n1) : n=n1 \lor (n=n1 \to False)). - left. apply eq_f. assumption. - right.intro.apply H.apply injective_nn.assumption. - right.apply not_eq_nn_cons. - intros.right.intro.apply (not_eq_pp_cons m x f1).apply sym_eq.assumption. - intros.right.intro.apply (not_eq_nn_cons m x f1).apply sym_eq.assumption. - intros.elim H. - elim ((decidable_eq_Z x y) : x=y \lor (x=y \to False)). - left.apply eq_f2.assumption. - assumption. - right.intro.apply H2.apply (eq_cons_to_eq1 f1 g1).assumption. - right.intro.apply H1.apply (eq_cons_to_eq2 x y f1 g1).assumption. -qed. - -theorem eqfb_to_Prop: \forall f,g:fraction. -match (eqfb f g) with -[true \Rightarrow f=g -|false \Rightarrow f \neq g]. -intros.apply (fraction_elim2 -(\lambda f,g.match (eqfb f g) with -[true \Rightarrow f=g -|false \Rightarrow f \neq g])). - intros.elim g1. - simplify.apply eqb_elim. - intro.simplify.apply eq_f.assumption. - intro.simplify.unfold Not.intro.apply H.apply injective_pp.assumption. - simplify.apply not_eq_pp_nn. - simplify.apply not_eq_pp_cons. - intros.elim g1. - simplify.unfold Not.intro.apply (not_eq_pp_nn n1 n).apply sym_eq. assumption. - simplify.apply eqb_elim.intro.simplify.apply eq_f.assumption. - intro.simplify.unfold Not.intro.apply H.apply injective_nn.assumption. - simplify.apply not_eq_nn_cons. - intros.simplify.unfold Not.intro.apply (not_eq_pp_cons m x f1).apply sym_eq. assumption. - intros.simplify.unfold Not.intro.apply (not_eq_nn_cons m x f1).apply sym_eq. assumption. - intros. - simplify. - apply eqZb_elim. - intro.generalize in match H.elim (eqfb f1 g1). - simplify.apply eq_f2.assumption. - apply H2. - simplify.unfold Not.intro.apply H2.apply (eq_cons_to_eq2 x y).assumption. - intro.simplify.unfold Not.intro.apply H1.apply (eq_cons_to_eq1 f1 g1).assumption. -qed. diff --git a/helm/software/matita/library/Q/q/q.ma b/helm/software/matita/library/Q/q/q.ma new file mode 100644 index 000000000..86f6d1dcf --- /dev/null +++ b/helm/software/matita/library/Q/q/q.ma @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||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/ratio/ratio.ma". + +(* a rational number is either O or a ratio with a sign *) +inductive Q : Set \def + OQ : Q + | Qpos : ratio \to Q + | Qneg : ratio \to Q. + +definition Q_of_nat ≝ + λn. + match factorize n with + [ nfa_zero ⇒ OQ + | nfa_one ⇒ Qpos one + | nfa_proper l ⇒ Qpos (frac (nat_fact_to_fraction l)) + ]. diff --git a/helm/software/matita/library/Q/q/qinv.ma b/helm/software/matita/library/Q/q/qinv.ma new file mode 100644 index 000000000..819437633 --- /dev/null +++ b/helm/software/matita/library/Q/q/qinv.ma @@ -0,0 +1,33 @@ +(**************************************************************************) +(* ___ *) +(* ||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/q/q.ma". +include "Q/ratio/rinv.ma". + +definition Qinv : Q → Q ≝ + λp. + match p with + [ OQ ⇒ OQ (* arbitrary value *) + | Qpos r ⇒ Qpos (rinv r) + | Qneg r ⇒ Qneg (rinv r) + ]. + +theorem Qinv_Qinv: ∀q. Qinv (Qinv q) = q. + intro; + elim q; + [ reflexivity + |*:simplify; + rewrite > rinv_rinv; + reflexivity] +qed. diff --git a/helm/software/matita/library/Q/q/qplus.ma b/helm/software/matita/library/Q/q/qplus.ma new file mode 100644 index 000000000..74b40808c --- /dev/null +++ b/helm/software/matita/library/Q/q/qplus.ma @@ -0,0 +1,18 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/Q/Qplus". + +include "nat/factorization.ma". + diff --git a/helm/software/matita/library/Q/q/qtimes.ma b/helm/software/matita/library/Q/q/qtimes.ma new file mode 100644 index 000000000..8a94d2b35 --- /dev/null +++ b/helm/software/matita/library/Q/q/qtimes.ma @@ -0,0 +1,63 @@ +(**************************************************************************) +(* ___ *) +(* ||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/q/qinv.ma". +include "Q/ratio/rtimes.ma". + +definition Qtimes : Q \to Q \to Q \def +\lambda p,q. + match p with + [OQ \Rightarrow OQ + |Qpos p1 \Rightarrow + match q with + [OQ \Rightarrow OQ + |Qpos q1 \Rightarrow Qpos (rtimes p1 q1) + |Qneg q1 \Rightarrow Qneg (rtimes p1 q1) + ] + |Qneg p1 \Rightarrow + match q with + [OQ \Rightarrow OQ + |Qpos q1 \Rightarrow Qneg (rtimes p1 q1) + |Qneg q1 \Rightarrow Qpos (rtimes p1 q1) + ] + ]. + +interpretation "rational times" 'times x y = (cic:/matita/Q/q/qtimes/Qtimes.con x y). + +theorem Qtimes_q_OQ: ∀q. q * OQ = OQ. + intro; + elim q; + reflexivity. +qed. + +theorem symmetric_Qtimes: symmetric ? Qtimes. + intros 2; + elim x; + [ rewrite > Qtimes_q_OQ; reflexivity + |*:elim y; + simplify; + try rewrite > sym_rtimes; + reflexivity + ] +qed. + +theorem Qtimes_Qinv: ∀q. q ≠ OQ → q * (Qinv q) = Qpos one. + intro; + elim q; + [ elim H; reflexivity + |*:simplify; + rewrite > rtimes_rinv; + reflexivity + ] +qed. diff --git a/helm/software/matita/library/Q/ratio/ratio.ma b/helm/software/matita/library/Q/ratio/ratio.ma new file mode 100644 index 000000000..38f2f07b1 --- /dev/null +++ b/helm/software/matita/library/Q/ratio/ratio.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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/fraction.ma". + +inductive ratio : Set \def + one : ratio + | frac : fraction \to ratio. diff --git a/helm/software/matita/library/Q/ratio/rinv.ma b/helm/software/matita/library/Q/ratio/rinv.ma new file mode 100644 index 000000000..72c152c25 --- /dev/null +++ b/helm/software/matita/library/Q/ratio/rinv.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||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/ratio/ratio.ma". +include "Q/fraction/finv.ma". + +definition rinv : ratio \to ratio \def +\lambda r:ratio. + match r with + [one \Rightarrow one + | (frac f) \Rightarrow frac (finv f)]. + +theorem rinv_rinv: ∀r. rinv (rinv r) = r. + intro; + elim r; + [ reflexivity + | simplify; + rewrite > finv_finv; + reflexivity] +qed. diff --git a/helm/software/matita/library/Q/ratio/rtimes.ma b/helm/software/matita/library/Q/ratio/rtimes.ma new file mode 100644 index 000000000..e11dbea9f --- /dev/null +++ b/helm/software/matita/library/Q/ratio/rtimes.ma @@ -0,0 +1,44 @@ +(**************************************************************************) +(* ___ *) +(* ||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/ratio/rinv.ma". +include "Q/fraction/ftimes.ma". + +definition rtimes : ratio \to ratio \to ratio \def +\lambda r,s:ratio. + match r with + [one \Rightarrow s + | (frac f) \Rightarrow + match s with + [one \Rightarrow frac f + | (frac g) \Rightarrow ftimes f g]]. + +theorem symmetric_rtimes : symmetric ratio rtimes. +change with (\forall r,s:ratio. rtimes r s = rtimes s r). +intros. +elim r. elim s. +reflexivity. +reflexivity. +elim s. +reflexivity. +simplify.apply symmetric2_ftimes. +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. +intro.elim r. +reflexivity. +simplify.apply ftimes_finv. +qed. \ No newline at end of file diff --git a/helm/software/matita/library/Q/times.ma b/helm/software/matita/library/Q/times.ma deleted file mode 100644 index 2f625ba9b..000000000 --- a/helm/software/matita/library/Q/times.ma +++ /dev/null @@ -1,164 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/inv.ma". - -definition Z_to_ratio: Z \to ratio \def -\lambda x:Z. match x with -[ OZ \Rightarrow one -| (pos n) \Rightarrow frac (pp n) -| (neg n) \Rightarrow frac (nn n)]. - -let rec ftimes f g \def - match f with - [ (pp n) \Rightarrow - match g with - [(pp m) \Rightarrow Z_to_ratio (pos n + pos m) - | (nn m) \Rightarrow Z_to_ratio (pos n + neg m) - | (cons y g1) \Rightarrow frac (cons (pos n + y) g1)] - | (nn n) \Rightarrow - match g with - [(pp m) \Rightarrow Z_to_ratio (neg n + pos m) - | (nn m) \Rightarrow Z_to_ratio (neg n + neg m) - | (cons y g1) \Rightarrow frac (cons (neg n + y) g1)] - | (cons x f1) \Rightarrow - match g with - [ (pp m) \Rightarrow frac (cons (x + pos m) f1) - | (nn m) \Rightarrow frac (cons (x + neg m) f1) - | (cons y g1) \Rightarrow - match ftimes f1 g1 with - [ one \Rightarrow Z_to_ratio (x + y) - | (frac h) \Rightarrow frac (cons (x + y) h)]]]. - -theorem symmetric2_ftimes: symmetric2 fraction ratio ftimes. -unfold symmetric2. intros.apply (fraction_elim2 (\lambda f,g.ftimes f g = ftimes g f)). - intros.elim g. - change with (Z_to_ratio (pos n + pos n1) = Z_to_ratio (pos n1 + pos n)). - apply eq_f.apply sym_Zplus. - change with (Z_to_ratio (pos n + neg n1) = Z_to_ratio (neg n1 + pos n)). - apply eq_f.apply sym_Zplus. - change with (frac (cons (pos n + z) f) = frac (cons (z + pos n) f)). - rewrite < sym_Zplus.reflexivity. - intros.elim g. - change with (Z_to_ratio (neg n + pos n1) = Z_to_ratio (pos n1 + neg n)). - apply eq_f.apply sym_Zplus. - change with (Z_to_ratio (neg n + neg n1) = Z_to_ratio (neg n1 + neg n)). - apply eq_f.apply sym_Zplus. - change with (frac (cons (neg n + z) f) = frac (cons (z + neg n) f)). - rewrite < sym_Zplus.reflexivity. - intros.change with (frac (cons (x1 + pos m) f) = frac (cons (pos m + x1) f)). - rewrite < sym_Zplus.reflexivity. - intros.change with (frac (cons (x1 + neg m) f) = frac (cons (neg m + x1) f)). - rewrite < sym_Zplus.reflexivity. - intros. - (*CSC: simplify does something nasty here because of a redex in Zplus *) - change with - (match ftimes f g with - [ one \Rightarrow Z_to_ratio (x1 + y1) - | (frac h) \Rightarrow frac (cons (x1 + y1) h)] = - match ftimes g f with - [ one \Rightarrow Z_to_ratio (y1 + x1) - | (frac h) \Rightarrow frac (cons (y1 + x1) h)]). - rewrite < H.rewrite < sym_Zplus.reflexivity. -qed. - -theorem ftimes_finv : \forall f:fraction. ftimes f (finv f) = one. -intro.elim f. - change with (Z_to_ratio (pos n + - (pos n)) = one). - rewrite > Zplus_Zopp.reflexivity. - change with (Z_to_ratio (neg n + - (neg n)) = one). - rewrite > Zplus_Zopp.reflexivity. - (*CSC: simplify does something nasty here because of a redex in Zplus *) -(* again: we would need something to help finding the right change *) - change with - (match ftimes f1 (finv f1) with - [ one \Rightarrow Z_to_ratio (z + - z) - | (frac h) \Rightarrow frac (cons (z + - z) h)] = one). - rewrite > H.rewrite > Zplus_Zopp.reflexivity. -qed. - -definition rtimes : ratio \to ratio \to ratio \def -\lambda r,s:ratio. - match r with - [one \Rightarrow s - | (frac f) \Rightarrow - match s with - [one \Rightarrow frac f - | (frac g) \Rightarrow ftimes f g]]. - -theorem rtimes_rinv: \forall r:ratio. rtimes r (rinv r) = one. -intro.elim r. -reflexivity. -simplify.apply ftimes_finv. -qed. - -theorem symmetric_rtimes : symmetric ratio rtimes. -change with (\forall r,s:ratio. rtimes r s = rtimes s r). -intros. -elim r. elim s. -reflexivity. -reflexivity. -elim s. -reflexivity. -simplify.apply symmetric2_ftimes. -qed. - -variant sym_rtimes : ∀x,y:ratio. rtimes x y = rtimes y x ≝ symmetric_rtimes. - -definition Qtimes : Q \to Q \to Q \def -\lambda p,q. - match p with - [OQ \Rightarrow OQ - |Qpos p1 \Rightarrow - match q with - [OQ \Rightarrow OQ - |Qpos q1 \Rightarrow Qpos (rtimes p1 q1) - |Qneg q1 \Rightarrow Qneg (rtimes p1 q1) - ] - |Qneg p1 \Rightarrow - match q with - [OQ \Rightarrow OQ - |Qpos q1 \Rightarrow Qneg (rtimes p1 q1) - |Qneg q1 \Rightarrow Qpos (rtimes p1 q1) - ] - ]. - -interpretation "rational times" 'times x y = (cic:/matita/Q/times/Qtimes.con x y). - -theorem Qtimes_q_OQ: ∀q. q * OQ = OQ. - intro; - elim q; - reflexivity. -qed. - -theorem symmetric_Qtimes: symmetric ? Qtimes. - intros 2; - elim x; - [ rewrite > Qtimes_q_OQ; reflexivity - |*:elim y; - simplify; - try rewrite > sym_rtimes; - reflexivity - ] -qed. - -theorem Qtimes_Qinv: ∀q. q ≠ OQ → q * (Qinv q) = Qpos one. - intro; - elim q; - [ elim H; reflexivity - |*:simplify; - rewrite > rtimes_rinv; - reflexivity - ] -qed. diff --git a/helm/software/matita/library/depends b/helm/software/matita/library/depends index bfc5a3a72..bbf2c8079 100644 --- a/helm/software/matita/library/depends +++ b/helm/software/matita/library/depends @@ -1,4 +1,3 @@ -formal_topology.ma logic/connectives.ma list/sort.ma datatypes/bool.ma datatypes/constructors.ma list/in.ma list/list.ma datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma nat/nat.ma nat/orders.ma nat/plus.ma list/in.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma @@ -22,10 +21,19 @@ higher_order_defs/ordering.ma logic/equality.ma higher_order_defs/relations.ma logic/connectives.ma Q/q.ma Z/compare.ma Z/plus.ma nat/factorization.ma Q/Qaxioms.ma Z/compare.ma Z/times.ma nat/iteration2.ma -Q/frac.ma Q/times.ma Q/inv.ma Q/q.ma nat/factorization.ma -Q/times.ma Q/inv.ma +Q/frac.ma Q/q.ma nat/factorization.ma Q/inv.ma Q/q.ma Q/Qplus_andrea.ma Q/frac.ma nat/factorization.ma +Q/q/qtimes.ma Q/q/qinv.ma Q/ratio/rtimes.ma +Q/q/q.ma Q/ratio/ratio.ma +Q/q/qinv.ma Q/q/q.ma Q/ratio/rinv.ma +Q/q/qplus.ma nat/factorization.ma +Q/ratio/ratio.ma Q/fraction/fraction.ma +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 datatypes/compare.ma datatypes/constructors.ma logic/equality.ma datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma