From: Andrea Asperti Date: Mon, 22 Aug 2005 08:03:58 +0000 (+0000) Subject: Added q.ma. X-Git-Tag: working_equations_only~27 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4d6bf14d95252ecfd1aaca4568184b4d6dee9b24;p=helm.git Added q.ma. --- diff --git a/helm/matita/library/Q/q.ma b/helm/matita/library/Q/q.ma new file mode 100644 index 000000000..0e6678dc9 --- /dev/null +++ b/helm/matita/library/Q/q.ma @@ -0,0 +1,331 @@ +(**************************************************************************) +(* ___ *) +(* ||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/q". + +include "Z/compare.ma". +include "Z/plus.ma". +include "higher_order_defs/functions.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. +elim g.apply H2. +apply H4.apply H5. +apply H3. +apply H1. +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. +simplify.intros. +change with (aux (pp x)) = (aux (pp y)). +apply eq_f.assumption. +qed. + +theorem injective_nn : injective nat fraction nn. +simplify.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. \lnot (pp n) = (nn m). +intros.simplify. 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. +\lnot (pp n) = (cons x f). +intros.simplify. 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. +\lnot (nn n) = (cons x f). +intros.simplify. 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.simplify. +apply fraction_elim2 (\lambda f,g. Or (f=g) (f=g \to False)). +intros.elim g1. +elim ((decidable_eq_nat n n1) : Or (n=n1) (n=n1 \to False)). +left.apply eq_f. assumption. +right.intro.apply H.apply injective_pp.assumption. +right.apply not_eq_pp_cons. +right.apply not_eq_pp_nn. +intros. elim g1. +right.intro.apply not_eq_pp_nn n1 n ?.apply sym_eq. assumption. +right.apply not_eq_nn_cons. +elim ((decidable_eq_nat n n1) : Or (n=n1) (n=n1 \to False)). +left. apply eq_f. assumption. +right.intro.apply H.apply injective_nn.assumption. +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) : Or (x=y) (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 \lnot f=g]. +intros.apply fraction_elim2 +(\lambda f,g.match (eqfb f g) with +[true \Rightarrow f=g +|false \Rightarrow \lnot f=g]). +intros.elim g1. +simplify. +apply eqb_elim. +intro.simplify.apply eq_f.assumption. +intro.simplify.intro.apply H.apply injective_pp.assumption. +simplify.apply not_eq_pp_cons. +simplify.apply not_eq_pp_nn. +intros. +elim g1.simplify. +intro.apply not_eq_pp_nn n1 n ?.apply sym_eq. assumption. +simplify.apply not_eq_nn_cons. +simplify.apply eqb_elim. +intro.simplify.apply eq_f.assumption. +intro.simplify.intro.apply H.apply injective_nn.assumption. +intros. +simplify.intro.apply not_eq_pp_cons m x f1 ?.apply sym_eq. assumption. +intros.simplify.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.intro.apply H2.apply eq_cons_to_eq2 x y.assumption. +intro.simplify. +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 (Zplus (pos n) (pos m)) + | (nn m) \Rightarrow Z_to_ratio (Zplus (pos n) (neg m)) + | (cons y g1) \Rightarrow frac (cons (Zplus (pos n) y) g1)] + | (nn n) \Rightarrow + match g with + [(pp m) \Rightarrow Z_to_ratio (Zplus (neg n) (pos m)) + | (nn m) \Rightarrow Z_to_ratio (Zplus (neg n) (neg m)) + | (cons y g1) \Rightarrow frac (cons (Zplus (neg n) y) g1)] + | (cons x f1) \Rightarrow + match g with + [ (pp m) \Rightarrow frac (cons (Zplus x (pos m)) f1) + | (nn m) \Rightarrow frac (cons (Zplus x (neg m)) f1) + | (cons y g1) \Rightarrow + match ftimes f1 g1 with + [ one \Rightarrow Z_to_ratio (Zplus x y) + | (frac h) \Rightarrow frac (cons (Zplus x y) h)]]]. + +theorem symmetric2_ftimes: symmetric2 fraction ratio ftimes. +simplify. intros. +apply fraction_elim2 (\lambda f,g.ftimes f g = ftimes g f). +intros.elim g. +change with Z_to_ratio (Zplus (pos n) (pos n1)) = Z_to_ratio (Zplus (pos n1) (pos n)). +apply eq_f.apply sym_Zplus. +change with frac (cons (Zplus (pos n) z) f) = frac (cons (Zplus z (pos n)) f). +rewrite < sym_Zplus.reflexivity. +change with Z_to_ratio (Zplus (pos n) (neg n1)) = Z_to_ratio (Zplus (neg n1) (pos n)). +apply eq_f.apply sym_Zplus. +intros.elim g. +change with Z_to_ratio (Zplus (neg n) (pos n1)) = Z_to_ratio (Zplus (pos n1) (neg n)). +apply eq_f.apply sym_Zplus. +change with frac (cons (Zplus (neg n) z) f) = frac (cons (Zplus z (neg n)) f). +rewrite < sym_Zplus.reflexivity. +change with Z_to_ratio (Zplus (neg n) (neg n1)) = Z_to_ratio (Zplus (neg n1) (neg n)). +apply eq_f.apply sym_Zplus. +intros. +change with frac (cons (Zplus x1 (pos m)) f) = frac (cons (Zplus (pos m) x1) f). +rewrite < sym_Zplus.reflexivity. +intros. +change with frac (cons (Zplus x1 (neg m)) f) = frac (cons (Zplus (neg m) x1) f). +rewrite < sym_Zplus.reflexivity. +intros. +change with + match ftimes f g with + [ one \Rightarrow Z_to_ratio (Zplus x1 y1) + | (frac h) \Rightarrow frac (cons (Zplus x1 y1) h)] = + match ftimes g f with + [ one \Rightarrow Z_to_ratio (Zplus y1 x1) + | (frac h) \Rightarrow frac (cons (Zplus 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 (Zplus (pos n) (Zopp (pos 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 (Zplus z (Zopp z)) + | (frac h) \Rightarrow frac (cons (Zplus z (Zopp z)) h)] = one. +rewrite > H. +rewrite > Zplus_Zopp.reflexivity. +change with Z_to_ratio (Zplus (neg n) (Zopp (neg n))) = one. +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. \ No newline at end of file