X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2FQ%2Fq.ma;h=2e34b3c24555d4a2f5282209ac8aa35faf51e7f7;hb=dcef667a444aa0f189225855c1433d26b65fb8b7;hp=340154979777529f94387cd1c630c6234cf21ab5;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git diff --git a/helm/software/matita/library/Q/q.ma b/helm/software/matita/library/Q/q.ma index 340154979..2e34b3c24 100644 --- a/helm/software/matita/library/Q/q.ma +++ b/helm/software/matita/library/Q/q.ma @@ -12,309 +12,88 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/Q/q". - include "Z/compare.ma". include "Z/plus.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. - -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. - -(* 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. - change in match (eqfb (cons x f1) (cons y g1)) - with (andb (eqZb x y) (eqfb f1 g1)). - 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. - -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))]. - -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. - 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. -(* 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 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. - -definition rinv : ratio \to ratio \def -\lambda r:ratio. - match r with - [one \Rightarrow one - | (frac f) \Rightarrow frac (finv f)]. - -theorem rtimes_rinv: \forall r:ratio. rtimes r (rinv r) = one. -intro.elim r. -reflexivity. -simplify.apply ftimes_finv. -qed. +include "nat/factorization.ma". +include "Q/fraction/fraction.ma". + +let rec enumerator_integral_fraction l ≝ + match l with + [ pp n ⇒ Some ? l + | nn _ ⇒ None ? + | cons z r ⇒ + match enumerator_integral_fraction r with + [ None ⇒ + match z with + [ pos n ⇒ Some ? (pp n) + | _ ⇒ None ? + ] + | Some r' ⇒ + Some ? + match z with + [ neg _ ⇒ cons OZ r' + | _ ⇒ cons z r' + ] + ] + ]. + +let rec denominator_integral_fraction l ≝ + match l with + [ pp _ ⇒ None ? + | nn n ⇒ Some ? (pp n) + | cons z r ⇒ + match denominator_integral_fraction r with + [ None ⇒ + match z with + [ neg n ⇒ Some ? (pp n) + | _ ⇒ None ? + ] + | Some r' ⇒ + Some ? + match z with + [ pos _ ⇒ cons OZ r' + | neg m ⇒ cons (pos m) r' + | OZ ⇒ cons OZ r' + ] + ] + ]. + +(* +definition enumerator_of_fraction ≝ + λq. + match q with + [ one ⇒ S O + | frac f ⇒ + match enumerator_integral_fraction f with + [ None ⇒ S O + | Some l ⇒ defactorize_aux (nat_fact_of_integral_fraction l) O + ] + ]. + +definition denominator_of_fraction ≝ + λq. + match q with + [ one ⇒ S O + | frac f ⇒ + match denominator_integral_fraction f with + [ None ⇒ S O + | Some l ⇒ defactorize_aux (nat_fact_of_integral_fraction l) O + ] + ]. + +definition enumerator ≝ + λq. + match q with + [ OQ ⇒ OZ + | Qpos r ⇒ (enumerator_of_fraction r : Z) + | Qneg r ⇒ neg(pred (enumerator_of_fraction r)) + ]. + +definition denominator ≝ + λq. + match q with + [ OQ ⇒ S O + | Qpos r ⇒ denominator_of_fraction r + | Qneg r ⇒ denominator_of_fraction r + ]. +*) \ No newline at end of file