1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 include "Z/compare.ma".
16 include "nat/factorization.ma".
18 (* a fraction is a list of Z-coefficients for primes, in natural
19 order. The last coefficient must eventually be different from 0 *)
21 inductive fraction : Set \def
23 | nn: nat \to fraction
24 | cons : Z \to fraction \to fraction.
26 let rec nat_fact_to_fraction n ≝
29 | nf_cons m l ⇒ cons (Z_of_nat m) (nat_fact_to_fraction l)
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.
50 (* boolean equality *)
55 [ (pp m) \Rightarrow eqb n m
56 | (nn m) \Rightarrow false
57 | (cons y g1) \Rightarrow false]
60 [ (pp m) \Rightarrow false
61 | (nn m) \Rightarrow eqb n m
62 | (cons y g1) \Rightarrow false]
63 | (cons x f1) \Rightarrow
65 [ (pp m) \Rightarrow false
66 | (nn m) \Rightarrow false
67 | (cons y g1) \Rightarrow andb (eqZb x y) (eqfb f1 g1)]].
71 \lambda f. match f with
72 [ (pp n) \Rightarrow n
73 | (nn n) \Rightarrow n
74 | (cons x f) \Rightarrow O].
77 \lambda f. match f with
78 [ (pp n) \Rightarrow (pos n)
79 | (nn n) \Rightarrow (neg n)
80 | (cons x f) \Rightarrow x].
83 \lambda f. match f with
84 [ (pp n) \Rightarrow (pp n)
85 | (nn n) \Rightarrow (nn n)
86 | (cons x f) \Rightarrow f].
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.
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.
100 theorem eq_cons_to_eq1: \forall f,g:fraction.\forall x,y:Z.
101 (cons x f) = (cons y g) \to x = y.
103 change with ((fhd (cons x f)) = (fhd (cons y g))).
104 apply eq_f.assumption.
107 theorem eq_cons_to_eq2: \forall x,y:Z.\forall f,g:fraction.
108 (cons x f) = (cons y g) \to f = g.
110 change with ((ftl (cons x f)) = (ftl (cons y g))).
111 apply eq_f.assumption.
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].
124 theorem not_eq_pp_cons:
125 \forall n:nat.\forall x:Z. \forall f:fraction.
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].
136 theorem not_eq_nn_cons:
137 \forall n:nat.\forall x:Z. \forall f:fraction.
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].
148 theorem decidable_eq_fraction: \forall f,g:fraction.
150 intros.unfold decidable.
151 apply (fraction_elim2 (\lambda f,g. f=g \lor (f=g \to False))).
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.
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.
167 elim ((decidable_eq_Z x y) : x=y \lor (x=y \to False)).
168 left.apply eq_f2.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.
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])).
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.
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.
198 intro.generalize in match H.elim (eqfb f1 g1).
199 simplify.apply eq_f2.assumption.
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.