X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Flibrary%2FQ%2Fq.ma;fp=matita%2Flibrary%2FQ%2Fq.ma;h=072532d7bc7a4c8732486f5886a9147f082d5523;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1

diff --git a/matita/library/Q/q.ma b/matita/library/Q/q.ma
new file mode 100644
index 000000000..072532d7b
--- /dev/null
+++ b/matita/library/Q/q.ma
@@ -0,0 +1,341 @@
+(**************************************************************************)
+(*       ___	                                                            *)
+(*      ||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".
+
+(* 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.
+   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.
+   (*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 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.
+
+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)
+    ]
+  ]
+.
+    
\ No newline at end of file