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/ratio/ratio.ma".
16 include "Q/fraction/finv.ma".
17 include "Q/nat_fact/times.ma".
20 definition nat_frac_item_to_ratio: Z \to ratio \def
21 \lambda x:Z. match x with
23 | (pos n) \Rightarrow frac (pp n)
24 | (neg n) \Rightarrow frac (nn n)].
26 let rec ftimes f g \def
30 [(pp m) \Rightarrow nat_frac_item_to_ratio (pos n + pos m)
31 | (nn m) \Rightarrow nat_frac_item_to_ratio (pos n + neg m)
32 | (cons y g1) \Rightarrow frac (cons (pos n + y) g1)]
35 [(pp m) \Rightarrow nat_frac_item_to_ratio (neg n + pos m)
36 | (nn m) \Rightarrow nat_frac_item_to_ratio (neg n + neg m)
37 | (cons y g1) \Rightarrow frac (cons (neg n + y) g1)]
38 | (cons x f1) \Rightarrow
40 [ (pp m) \Rightarrow frac (cons (x + pos m) f1)
41 | (nn m) \Rightarrow frac (cons (x + neg m) f1)
42 | (cons y g1) \Rightarrow
43 match ftimes f1 g1 with
44 [ one \Rightarrow nat_frac_item_to_ratio (x + y)
45 | (frac h) \Rightarrow frac (cons (x + y) h)]]].
47 theorem symmetric2_ftimes: symmetric2 fraction ratio ftimes.
48 unfold symmetric2. intros.apply (fraction_elim2 (\lambda f,g.ftimes f g = ftimes g f)).
50 change with (nat_frac_item_to_ratio (pos n + pos n1) = nat_frac_item_to_ratio (pos n1 + pos n)).
51 apply eq_f.apply sym_Zplus.
52 change with (nat_frac_item_to_ratio (pos n + neg n1) = nat_frac_item_to_ratio (neg n1 + pos n)).
53 apply eq_f.apply sym_Zplus.
54 change with (frac (cons (pos n + z) f) = frac (cons (z + pos n) f)).
55 rewrite < sym_Zplus.reflexivity.
57 change with (nat_frac_item_to_ratio (neg n + pos n1) = nat_frac_item_to_ratio (pos n1 + neg n)).
58 apply eq_f.apply sym_Zplus.
59 change with (nat_frac_item_to_ratio (neg n + neg n1) = nat_frac_item_to_ratio (neg n1 + neg n)).
60 apply eq_f.apply sym_Zplus.
61 change with (frac (cons (neg n + z) f) = frac (cons (z + neg n) f)).
62 rewrite < sym_Zplus.reflexivity.
63 intros.change with (frac (cons (x1 + pos m) f) = frac (cons (pos m + x1) f)).
64 rewrite < sym_Zplus.reflexivity.
65 intros.change with (frac (cons (x1 + neg m) f) = frac (cons (neg m + x1) f)).
66 rewrite < sym_Zplus.reflexivity.
68 (*CSC: simplify does something nasty here because of a redex in Zplus *)
70 (match ftimes f g with
71 [ one \Rightarrow nat_frac_item_to_ratio (x1 + y1)
72 | (frac h) \Rightarrow frac (cons (x1 + y1) h)] =
74 [ one \Rightarrow nat_frac_item_to_ratio (y1 + x1)
75 | (frac h) \Rightarrow frac (cons (y1 + x1) h)]).
76 rewrite < H.rewrite < sym_Zplus.reflexivity.
79 theorem ftimes_finv : \forall f:fraction. ftimes f (finv f) = one.
81 change with (nat_frac_item_to_ratio (pos n + - (pos n)) = one).
82 rewrite > Zplus_Zopp.reflexivity.
83 change with (nat_frac_item_to_ratio (neg n + - (neg n)) = one).
84 rewrite > Zplus_Zopp.reflexivity.
85 (*CSC: simplify does something nasty here because of a redex in Zplus *)
86 (* again: we would need something to help finding the right change *)
88 (match ftimes f1 (finv f1) with
89 [ one \Rightarrow nat_frac_item_to_ratio (z + - z)
90 | (frac h) \Rightarrow frac (cons (z + - z) h)] = one).
91 rewrite > H.rewrite > Zplus_Zopp.reflexivity.
94 theorem times_f_ftimes: \forall n,m.
95 frac (nat_fact_to_fraction (times_f n m))
96 = ftimes (nat_fact_to_fraction n) (nat_fact_to_fraction m).
101 rewrite < plus_n_Sm.reflexivity
103 [simplify.rewrite < plus_n_O.reflexivity
104 |simplify.reflexivity.
109 [simplify.reflexivity
110 |simplify.rewrite < plus_n_Sm.reflexivity
113 cut (\exist h.ftimes (nat_fact_to_fraction n2) (nat_fact_to_fraction n4) = frac h)
119 |apply injective_frac.
123 |generalize in match n4.
126 [ exists; [2: autobatch;]
127 | exists; [2:autobatch;]
130 [exists;[2:autobatch]