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 (* double elimination principles *)
  33 theorem fraction_elim2:
  34 \forall R:fraction \to fraction \to Prop.
  35 (\forall n:nat.\forall g:fraction.R (pp n) g) \to
  36 (\forall n:nat.\forall g:fraction.R (nn n) g) \to
  37 (\forall x:Z.\forall f:fraction.\forall m:nat.R (cons x f) (pp m)) \to
  38 (\forall x:Z.\forall f:fraction.\forall m:nat.R (cons x f) (nn m)) \to
  39 (\forall x,y:Z.\forall f,g:fraction.R f g \to R (cons x f) (cons y g)) \to
  40 \forall f,g:fraction. R f g.
  41 intros 7.elim f.
  42   apply H.
  43   apply H1.
  44   elim g.
  45     apply H2.
  46     apply H3.
  47     apply H4.apply H5.
  48 qed.
  49
  50 (* boolean equality *)
  51 let rec eqfb f g \def
  52 match f with
  53 [ (pp n) \Rightarrow
  54   match g with
  55   [ (pp m) \Rightarrow eqb n m
  56   | (nn m) \Rightarrow false
  57   | (cons y g1) \Rightarrow false]
  58 | (nn n) \Rightarrow
  59   match g with
  60   [ (pp m) \Rightarrow false
  61   | (nn m) \Rightarrow eqb n m
  62   | (cons y g1) \Rightarrow false]
  63 | (cons x f1) \Rightarrow
  64   match g with
  65   [ (pp m) \Rightarrow false
  66   | (nn m) \Rightarrow false
  67   | (cons y g1) \Rightarrow andb (eqZb x y) (eqfb f1 g1)]].
  68
  69 (* discrimination *)
  70 definition aux \def
  71   \lambda f. match f with
  72     [ (pp n) \Rightarrow n
  73     | (nn n) \Rightarrow n
  74     | (cons x f) \Rightarrow O].
  75
  76 definition fhd \def
  77 \lambda f. match f with
  78     [ (pp n) \Rightarrow (pos n)
  79     | (nn n) \Rightarrow (neg n)
  80     | (cons x f) \Rightarrow x].
  81
  82 definition ftl \def
  83 \lambda f. match f with
  84     [ (pp n) \Rightarrow (pp n)
  85     | (nn n) \Rightarrow (nn n)
  86     | (cons x f) \Rightarrow f].
  87
  88 theorem injective_pp : injective nat fraction pp.
  89 unfold injective.intros.
  90 change with ((aux (pp x)) = (aux (pp y))).
  91 apply eq_f.assumption.
  92 qed.
  93
  94 theorem injective_nn : injective nat fraction nn.
  95 unfold injective.intros.
  96 change with ((aux (nn x)) = (aux (nn y))).
  97 apply eq_f.assumption.
  98 qed.
  99
 100 theorem eq_cons_to_eq1: \forall f,g:fraction.\forall x,y:Z.
 101 (cons x f) = (cons y g) \to x = y.
 102 intros.
 103 change with ((fhd (cons x f)) = (fhd (cons y g))).
 104 apply eq_f.assumption.
 105 qed.
 106
 107 theorem eq_cons_to_eq2: \forall x,y:Z.\forall f,g:fraction.
 108 (cons x f) = (cons y g) \to f = g.
 109 intros.
 110 change with ((ftl (cons x f)) = (ftl (cons y g))).
 111 apply eq_f.assumption.
 112 qed.
 113
 114 theorem not_eq_pp_nn: \forall n,m:nat. pp n \neq nn m.
 115 intros.unfold Not. intro.
 116 change with match (pp n) with
 117 [ (pp n) \Rightarrow False
 118 | (nn n) \Rightarrow True
 119 | (cons x f) \Rightarrow True].
 120 rewrite > H.
 121 simplify.exact I.
 122 qed.
 123
 124 theorem not_eq_pp_cons:
 125 \forall n:nat.\forall x:Z. \forall f:fraction.
 126 pp n \neq cons x f.
 127 intros.unfold Not. intro.
 128 change with match (pp n) with
 129 [ (pp n) \Rightarrow False
 130 | (nn n) \Rightarrow True
 131 | (cons x f) \Rightarrow True].
 132 rewrite > H.
 133 simplify.exact I.
 134 qed.
 135
 136 theorem not_eq_nn_cons:
 137 \forall n:nat.\forall x:Z. \forall f:fraction.
 138 nn n \neq cons x f.
 139 intros.unfold Not. intro.
 140 change with match (nn n) with
 141 [ (pp n) \Rightarrow True
 142 | (nn n) \Rightarrow False
 143 | (cons x f) \Rightarrow True].
 144 rewrite > H.
 145 simplify.exact I.
 146 qed.
 147
 148 theorem decidable_eq_fraction: \forall f,g:fraction.
 149 decidable (f = g).
 150 intros.unfold decidable.
 151 apply (fraction_elim2 (\lambda f,g. f=g \lor (f=g \to False))).
 152   intros.elim g1.
 153     elim ((decidable_eq_nat n n1) : n=n1 \lor (n=n1 \to False)).
 154       left.apply eq_f. assumption.
 155       right.intro.apply H.apply injective_pp.assumption.
 156     right.apply not_eq_pp_nn.
 157     right.apply not_eq_pp_cons.
 158   intros. elim g1.
 159       right.intro.apply (not_eq_pp_nn n1 n).apply sym_eq. assumption.
 160       elim ((decidable_eq_nat n n1) : n=n1 \lor (n=n1 \to False)).
 161         left. apply eq_f. assumption.
 162         right.intro.apply H.apply injective_nn.assumption.
 163       right.apply not_eq_nn_cons.
 164   intros.right.intro.apply (not_eq_pp_cons m x f1).apply sym_eq.assumption.
 165   intros.right.intro.apply (not_eq_nn_cons m x f1).apply sym_eq.assumption.
 166   intros.elim H.
 167     elim ((decidable_eq_Z x y) : x=y \lor (x=y \to False)).
 168       left.apply eq_f2.assumption.
 169       assumption.
 170     right.intro.apply H2.apply (eq_cons_to_eq1 f1 g1).assumption.
 171     right.intro.apply H1.apply (eq_cons_to_eq2 x y f1 g1).assumption.
 172 qed.
 173
 174 theorem eqfb_to_Prop: \forall f,g:fraction.
 175 match (eqfb f g) with
 176 [true \Rightarrow f=g
 177 |false \Rightarrow f \neq g].
 178 intros.apply (fraction_elim2
 179 (\lambda f,g.match (eqfb f g) with
 180 [true \Rightarrow f=g
 181 |false \Rightarrow f \neq g])).
 182   intros.elim g1.
 183     simplify.apply eqb_elim.
 184       intro.simplify.apply eq_f.assumption.
 185       intro.simplify.unfold Not.intro.apply H.apply injective_pp.assumption.
 186     simplify.apply not_eq_pp_nn.
 187     simplify.apply not_eq_pp_cons.
 188   intros.elim g1.
 189     simplify.unfold Not.intro.apply (not_eq_pp_nn n1 n).apply sym_eq. assumption.
 190     simplify.apply eqb_elim.intro.simplify.apply eq_f.assumption.
 191     intro.simplify.unfold Not.intro.apply H.apply injective_nn.assumption.
 192   simplify.apply not_eq_nn_cons.
 193   intros.simplify.unfold Not.intro.apply (not_eq_pp_cons m x f1).apply sym_eq. assumption.
 194   intros.simplify.unfold Not.intro.apply (not_eq_nn_cons m x f1).apply sym_eq. assumption.
 195   intros.
 196    simplify.
 197    apply eqZb_elim.
 198       intro.generalize in match H.elim (eqfb f1 g1).
 199         simplify.apply eq_f2.assumption.
 200         apply H2.
 201       simplify.unfold Not.intro.apply H2.apply (eq_cons_to_eq2 x y).assumption.
 202       intro.simplify.unfold Not.intro.apply H1.apply (eq_cons_to_eq1 f1 g1).assumption.
 203 qed.