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
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
]
.
+
(*
definition nat_fact_all_to_Q_inv \def
\lambda n.
=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.
[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
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.
(* 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))))
]
]
qed.
-
+*)
(*
definition numQ:Q \to Z \def
\lambda q.
|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.
|apply Qtimes1.
]
]
-qed.
+qed.*)
+(*CSC
theorem frac_numQ_denomQ2: \forall r:ratio.
frac (numQ (Qneg r)) (denomQ (Qneg r)) = (Qpos r).
intro.
|apply Qtimes1.
]
]
-qed.
+qed.*)
definition Qabs:Q \to Q \def \lambda q.
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.
|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
|simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ2
]
qed.
-
+*)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
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;
[ rewrite > Qinv_Qinv in Hletin;
assumption
| generalize in match H; elim q; assumption]
-qed.
\ No newline at end of file
+qed.
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
| 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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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))
+ ].
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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".
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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.
-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
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
projects / helm.git / commitdiff