helm/software/matita/library/Q/fraction/fraction.ma

   1 (**************************************************************************)
   2 (*       ___                                                                *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "Z/compare.ma".
  16 include "nat/factorization.ma".
  17
  18 (* a fraction is a list of Z-coefficients for primes, in natural
  19 order. The last coefficient must eventually be different from 0 *)
  20
  21 inductive fraction : Set \def
  22   pp : nat \to fraction
  23 | nn: nat \to fraction
  24 | cons : Z \to fraction \to fraction.
  25
  26 let rec nat_fact_to_fraction n ≝
  27  match n with
  28   [ nf_last m ⇒ pp m
  29   | nf_cons m l ⇒ cons (Z_of_nat m) (nat_fact_to_fraction l)
  30   ].
  31
  32 (* returns the numerator of a fraction in the form of a nat_fact_all *)
  33 let rec numerator f \def
  34   match f with
  35   [pp a \Rightarrow nfa_proper (nf_last a)
  36   |nn a \Rightarrow nfa_one
  37   |cons a l \Rightarrow
  38     let n \def numerator l in
  39     match n with
  40     [nfa_zero \Rightarrow (* this case is vacuous *) nfa_zero
  41     |nfa_one  \Rightarrow
  42       match a with
  43       [OZ \Rightarrow nfa_one
  44       |pos x \Rightarrow nfa_proper (nf_last x)
  45       |neg x \Rightarrow nfa_one
  46       ]
  47     |nfa_proper g \Rightarrow
  48       match a with
  49       [OZ \Rightarrow nfa_proper (nf_cons O g)
  50       |pos x \Rightarrow nfa_proper (nf_cons (S x) g)
  51       |neg x \Rightarrow nfa_proper (nf_cons O g)
  52       ]
  53     ]
  54   ].
  55
  56 theorem not_eq_numerator_nfa_zero:
  57 \forall f.numerator f \neq nfa_zero.
  58 intro.elim f
  59   [simplify.intro.destruct H
  60   |simplify.intro.destruct H
  61   |simplify.generalize in match H.
  62    cases (numerator f1)
  63     [intro.elim H1.reflexivity
  64     |simplify.intro.
  65      cases z;simplify;intro;destruct H2
  66     |simplify.intro.
  67      cases z;simplify;intro;destruct H2
  68     ]
  69   ]
  70 qed.
  71
  72 theorem numerator_nat_fact_to_fraction: \forall g:nat_fact.
  73 numerator (nat_fact_to_fraction g) = nfa_proper g.
  74 intro.
  75 elim g
  76   [simplify.reflexivity.
  77   |simplify.rewrite > H.simplify.
  78    cases n;reflexivity
  79   ]
  80 qed.
  81
  82 (* double elimination principles *)
  83 theorem fraction_elim2:
  84 \forall R:fraction \to fraction \to Prop.
  85 (\forall n:nat.\forall g:fraction.R (pp n) g) \to
  86 (\forall n:nat.\forall g:fraction.R (nn n) g) \to
  87 (\forall x:Z.\forall f:fraction.\forall m:nat.R (cons x f) (pp m)) \to
  88 (\forall x:Z.\forall f:fraction.\forall m:nat.R (cons x f) (nn m)) \to
  89 (\forall x,y:Z.\forall f,g:fraction.R f g \to R (cons x f) (cons y g)) \to
  90 \forall f,g:fraction. R f g.
  91 intros 7.elim f.
  92   apply H.
  93   apply H1.
  94   elim g.
  95     apply H2.
  96     apply H3.
  97     apply H4.apply H5.
  98 qed.
  99
 100 (* boolean equality *)
 101 let rec eqfb f g \def
 102 match f with
 103 [ (pp n) \Rightarrow
 104   match g with
 105   [ (pp m) \Rightarrow eqb n m
 106   | (nn m) \Rightarrow false
 107   | (cons y g1) \Rightarrow false]
 108 | (nn n) \Rightarrow
 109   match g with
 110   [ (pp m) \Rightarrow false
 111   | (nn m) \Rightarrow eqb n m
 112   | (cons y g1) \Rightarrow false]
 113 | (cons x f1) \Rightarrow
 114   match g with
 115   [ (pp m) \Rightarrow false
 116   | (nn m) \Rightarrow false
 117   | (cons y g1) \Rightarrow andb (eqZb x y) (eqfb f1 g1)]].
 118
 119 (* discrimination *)
 120 definition aux \def
 121   \lambda f. match f with
 122     [ (pp n) \Rightarrow n
 123     | (nn n) \Rightarrow n
 124     | (cons x f) \Rightarrow O].
 125
 126 definition fhd \def
 127 \lambda f. match f with
 128     [ (pp n) \Rightarrow (pos n)
 129     | (nn n) \Rightarrow (neg n)
 130     | (cons x f) \Rightarrow x].
 131
 132 definition ftl \def
 133 \lambda f. match f with
 134     [ (pp n) \Rightarrow (pp n)
 135     | (nn n) \Rightarrow (nn n)
 136     | (cons x f) \Rightarrow f].
 137
 138 theorem injective_pp : injective nat fraction pp.
 139 unfold injective.intros.
 140 change with ((aux (pp x)) = (aux (pp y))).
 141 apply eq_f.assumption.
 142 qed.
 143
 144 theorem injective_nn : injective nat fraction nn.
 145 unfold injective.intros.
 146 change with ((aux (nn x)) = (aux (nn y))).
 147 apply eq_f.assumption.
 148 qed.
 149
 150 theorem eq_cons_to_eq1: \forall f,g:fraction.\forall x,y:Z.
 151 (cons x f) = (cons y g) \to x = y.
 152 intros.
 153 change with ((fhd (cons x f)) = (fhd (cons y g))).
 154 apply eq_f.assumption.
 155 qed.
 156
 157 theorem eq_cons_to_eq2: \forall x,y:Z.\forall f,g:fraction.
 158 (cons x f) = (cons y g) \to f = g.
 159 intros.
 160 change with ((ftl (cons x f)) = (ftl (cons y g))).
 161 apply eq_f.assumption.
 162 qed.
 163
 164 theorem not_eq_pp_nn: \forall n,m:nat. pp n \neq nn m.
 165 intros.unfold Not. intro.
 166 change with match (pp n) with
 167 [ (pp n) \Rightarrow False
 168 | (nn n) \Rightarrow True
 169 | (cons x f) \Rightarrow True].
 170 rewrite > H.
 171 simplify.exact I.
 172 qed.
 173
 174 theorem not_eq_pp_cons:
 175 \forall n:nat.\forall x:Z. \forall f:fraction.
 176 pp n \neq cons x f.
 177 intros.unfold Not. intro.
 178 change with match (pp n) with
 179 [ (pp n) \Rightarrow False
 180 | (nn n) \Rightarrow True
 181 | (cons x f) \Rightarrow True].
 182 rewrite > H.
 183 simplify.exact I.
 184 qed.
 185
 186 theorem not_eq_nn_cons:
 187 \forall n:nat.\forall x:Z. \forall f:fraction.
 188 nn n \neq cons x f.
 189 intros.unfold Not. intro.
 190 change with match (nn n) with
 191 [ (pp n) \Rightarrow True
 192 | (nn n) \Rightarrow False
 193 | (cons x f) \Rightarrow True].
 194 rewrite > H.
 195 simplify.exact I.
 196 qed.
 197
 198 theorem decidable_eq_fraction: \forall f,g:fraction.
 199 decidable (f = g).
 200 intros.unfold decidable.
 201 apply (fraction_elim2 (\lambda f,g. f=g \lor (f=g \to False))).
 202   intros.elim g1.
 203     elim ((decidable_eq_nat n n1) : n=n1 \lor (n=n1 \to False)).
 204       left.apply eq_f. assumption.
 205       right.intro.apply H.apply injective_pp.assumption.
 206     right.apply not_eq_pp_nn.
 207     right.apply not_eq_pp_cons.
 208   intros. elim g1.
 209       right.intro.apply (not_eq_pp_nn n1 n).apply sym_eq. assumption.
 210       elim ((decidable_eq_nat n n1) : n=n1 \lor (n=n1 \to False)).
 211         left. apply eq_f. assumption.
 212         right.intro.apply H.apply injective_nn.assumption.
 213       right.apply not_eq_nn_cons.
 214   intros.right.intro.apply (not_eq_pp_cons m x f1).apply sym_eq.assumption.
 215   intros.right.intro.apply (not_eq_nn_cons m x f1).apply sym_eq.assumption.
 216   intros.elim H.
 217     elim ((decidable_eq_Z x y) : x=y \lor (x=y \to False)).
 218       left.apply eq_f2.assumption.
 219       assumption.
 220     right.intro.apply H2.apply (eq_cons_to_eq1 f1 g1).assumption.
 221     right.intro.apply H1.apply (eq_cons_to_eq2 x y f1 g1).assumption.
 222 qed.
 223
 224 theorem eqfb_to_Prop: \forall f,g:fraction.
 225 match (eqfb f g) with
 226 [true \Rightarrow f=g
 227 |false \Rightarrow f \neq g].
 228 intros.apply (fraction_elim2
 229 (\lambda f,g.match (eqfb f g) with
 230 [true \Rightarrow f=g
 231 |false \Rightarrow f \neq g])).
 232   intros.elim g1.
 233     simplify.apply eqb_elim.
 234       intro.simplify.apply eq_f.assumption.
 235       intro.simplify.unfold Not.intro.apply H.apply injective_pp.assumption.
 236     simplify.apply not_eq_pp_nn.
 237     simplify.apply not_eq_pp_cons.
 238   intros.elim g1.
 239     simplify.unfold Not.intro.apply (not_eq_pp_nn n1 n).apply sym_eq. assumption.
 240     simplify.apply eqb_elim.intro.simplify.apply eq_f.assumption.
 241     intro.simplify.unfold Not.intro.apply H.apply injective_nn.assumption.
 242   simplify.apply not_eq_nn_cons.
 243   intros.simplify.unfold Not.intro.apply (not_eq_pp_cons m x f1).apply sym_eq. assumption.
 244   intros.simplify.unfold Not.intro.apply (not_eq_nn_cons m x f1).apply sym_eq. assumption.
 245   intros.
 246    simplify.
 247    apply eqZb_elim.
 248       intro.generalize in match H.elim (eqfb f1 g1).
 249         simplify.apply eq_f2.assumption.
 250         apply H2.
 251       simplify.unfold Not.intro.apply H2.apply (eq_cons_to_eq2 x y).assumption.
 252       intro.simplify.unfold Not.intro.apply H1.apply (eq_cons_to_eq1 f1 g1).assumption.
 253 qed.