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 "Q/fraction/finv.ma".
17 (* returns the numerator of a fraction in the form of a nat_fact_all *)
18 let rec numerator f \def
20 [pp a \Rightarrow nfa_proper (nf_last a)
21 |nn a \Rightarrow nfa_one
23 let n \def numerator l in
25 [nfa_zero \Rightarrow (* this case is vacuous *) nfa_zero
28 [OZ \Rightarrow nfa_one
29 |pos x \Rightarrow nfa_proper (nf_last x)
30 |neg x \Rightarrow nfa_one
32 |nfa_proper g \Rightarrow
34 [OZ \Rightarrow nfa_proper (nf_cons O g)
35 |pos x \Rightarrow nfa_proper (nf_cons (S x) g)
36 |neg x \Rightarrow nfa_proper (nf_cons O g)
39 definition denominator ≝ λf.numerator (finv f).
41 theorem not_eq_numerator_nfa_zero: ∀f.numerator f ≠ nfa_zero.
43 [simplify.intro.destruct H
44 |simplify.intro.destruct H
45 |simplify.generalize in match H.
47 [intro.elim H1.reflexivity
49 cases z;simplify;intro;destruct H2
51 cases z;simplify;intro;destruct H2]]
54 theorem not_eq_denominator_nfa_zero: ∀f.denominator f ≠ nfa_zero.
55 unfold denominator; intro; apply not_eq_numerator_nfa_zero.
58 theorem numerator_nat_fact_to_fraction: ∀g:nat_fact.
59 numerator (nat_fact_to_fraction g) = nfa_proper g.
62 [simplify.reflexivity.
63 |simplify.rewrite > H.simplify.
68 theorem denominator_nat_fact_to_fraction: ∀g:nat_fact.
69 denominator (finv (nat_fact_to_fraction g)) = nfa_proper g.
73 apply numerator_nat_fact_to_fraction.
76 theorem or_numerator_nfa_one_nfa_proper:
78 (numerator f = nfa_one ∧ ∃g.denominator f = nfa_proper g) ∨
79 ∃g.numerator f = nfa_proper g.
82 apply (ex_intro ? ? (nf_last n)).reflexivity
85 |apply (ex_intro ? ? (nf_last n)).reflexivity
92 rewrite > H.rewrite > H1.simplify.
95 |apply (ex_intro ? ? (nf_cons O a)).reflexivity
98 rewrite > H.rewrite > H1.simplify.
99 right.apply (ex_intro ? ? (nf_last n)).reflexivity
101 rewrite > H.rewrite > H1.simplify.
104 |apply (ex_intro ? ? (nf_cons (S n) a)).reflexivity
110 rewrite > H.simplify.
112 apply (ex_intro ? ? (nf_cons O a)).reflexivity
114 rewrite > H.simplify.
115 right.apply (ex_intro ? ? (nf_cons (S n) a)).reflexivity
117 rewrite > H.simplify.
119 apply (ex_intro ? ? (nf_cons O a)).reflexivity
125 theorem eq_nfa_one_to_eq_finv_nfa_proper:
126 ∀f.numerator f = nfa_one → ∃h.denominator f = nfa_proper h.
128 elim (or_numerator_nfa_one_nfa_proper f); cases H1;