(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/Q/q".
-
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 *)
| 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.
| 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
+ | 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 ⇒ pos (pred (enumerator_of_fraction r))
+ | 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
+ ].
+
(* double elimination principles *)
theorem fraction_elim2:
\forall R:fraction \to fraction \to Prop.
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.
+ 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.
-
-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.
projects / helm.git / blobdiff