]> matita.cs.unibo.it Git - helm.git/blob - helm/matita/library/nat/ord.ma
fix
[helm.git] / helm / matita / library / nat / ord.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 (*       \ /        Matita is distributed under the terms of the          *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 set "baseuri" "cic:/matita/nat/log".
16
17 include "datatypes/constructors.ma".
18 include "nat/exp.ma".
19 include "nat/lt_arith.ma".
20 include "nat/primes.ma".
21
22 (* this definition of log is based on pairs, with a remainder *)
23
24 let rec p_ord_aux p n m \def
25   match n \mod m with
26   [ O \Rightarrow 
27     match p with
28       [ O \Rightarrow pair nat nat O n
29       | (S p) \Rightarrow 
30        match (p_ord_aux p (n / m) m) with
31        [ (pair q r) \Rightarrow pair nat nat (S q) r] ]
32   | (S a) \Rightarrow pair nat nat O n].
33   
34 (* p_ord n m = <q,r> if m divides n q times, with remainder r *)
35 definition p_ord \def \lambda n,m:nat.p_ord_aux n n m.
36
37 theorem p_ord_aux_to_Prop: \forall p,n,m. O < m \to
38   match p_ord_aux p n m with
39   [ (pair q r) \Rightarrow n = m \sup q *r ].
40 intro.
41 elim p.
42 change with 
43 match (
44 match n \mod m with
45   [ O \Rightarrow pair nat nat O n
46   | (S a) \Rightarrow pair nat nat O n] )
47 with
48   [ (pair q r) \Rightarrow n = m \sup q * r ].
49 apply (nat_case (n \mod m)).
50 simplify.apply plus_n_O.
51 intros.
52 simplify.apply plus_n_O. 
53 change with 
54 match (
55 match n1 \mod m with
56   [ O \Rightarrow 
57      match (p_ord_aux n (n1 / m) m) with
58        [ (pair q r) \Rightarrow pair nat nat (S q) r]
59   | (S a) \Rightarrow pair nat nat O n1] )
60 with
61   [ (pair q r) \Rightarrow n1 = m \sup q * r].
62 apply (nat_case1 (n1 \mod m)).intro.
63 change with 
64 match (
65  match (p_ord_aux n (n1 / m) m) with
66    [ (pair q r) \Rightarrow pair nat nat (S q) r])
67 with
68   [ (pair q r) \Rightarrow n1 = m \sup q * r].
69 generalize in match (H (n1 / m) m).
70 elim (p_ord_aux n (n1 / m) m).
71 simplify.
72 rewrite > assoc_times.
73 rewrite < H3.rewrite > (plus_n_O (m*(n1 / m))).
74 rewrite < H2.
75 rewrite > sym_times.
76 rewrite < div_mod.reflexivity.
77 assumption.assumption.
78 intros.simplify.apply plus_n_O. 
79 qed.
80
81 theorem p_ord_aux_to_exp: \forall p,n,m,q,r. O < m \to
82   (pair nat nat q r) = p_ord_aux p n m \to n = m \sup q * r.
83 intros.
84 change with 
85 match (pair nat nat q r) with
86   [ (pair q r) \Rightarrow n = m \sup q * r ].
87 rewrite > H1.
88 apply p_ord_aux_to_Prop.
89 assumption.
90 qed.
91 (* questo va spostato in primes1.ma *)
92 theorem p_ord_exp: \forall n,m,i. O < m \to n \mod m \neq O \to
93 \forall p. i \le p \to p_ord_aux p (m \sup i * n) m = pair nat nat i n.
94 intros 5.
95 elim i.
96 simplify.
97 rewrite < plus_n_O.
98 apply (nat_case p).
99 change with
100  (match n \mod m with
101   [ O \Rightarrow pair nat nat O n
102   | (S a) \Rightarrow pair nat nat O n]
103   = pair nat nat O n).
104 elim (n \mod m).simplify.reflexivity.simplify.reflexivity.
105 intro.
106 change with
107  (match n \mod m with
108   [ O \Rightarrow 
109        match (p_ord_aux m1 (n / m) m) with
110        [ (pair q r) \Rightarrow pair nat nat (S q) r]
111   | (S a) \Rightarrow pair nat nat O n]
112   = pair nat nat O n).
113 cut (O < n \mod m \lor O = n \mod m).
114 elim Hcut.apply (lt_O_n_elim (n \mod m) H3).
115 intros. simplify.reflexivity.
116 apply False_ind.
117 apply H1.apply sym_eq.assumption.
118 apply le_to_or_lt_eq.apply le_O_n.
119 generalize in match H3.
120 apply (nat_case p).intro.apply False_ind.apply (not_le_Sn_O n1 H4).
121 intros.
122 change with
123  (match ((m \sup (S n1) *n) \mod m) with
124   [ O \Rightarrow 
125        match (p_ord_aux m1 ((m \sup (S n1) *n) / m) m) with
126        [ (pair q r) \Rightarrow pair nat nat (S q) r]
127   | (S a) \Rightarrow pair nat nat O (m \sup (S n1) *n)]
128   = pair nat nat (S n1) n).
129 cut (((m \sup (S n1)*n) \mod m) = O).
130 rewrite > Hcut.
131 change with
132 (match (p_ord_aux m1 ((m \sup (S n1)*n) / m) m) with
133        [ (pair q r) \Rightarrow pair nat nat (S q) r] 
134   = pair nat nat (S n1) n). 
135 cut ((m \sup (S n1) *n) / m = m \sup n1 *n).
136 rewrite > Hcut1.
137 rewrite > (H2 m1). simplify.reflexivity.
138 apply le_S_S_to_le.assumption.
139 (* div_exp *)
140 change with ((m* m \sup n1 *n) / m = m \sup n1 * n).
141 rewrite > assoc_times.
142 apply (lt_O_n_elim m H).
143 intro.apply div_times.
144 (* mod_exp = O *)
145 apply divides_to_mod_O.
146 assumption.
147 simplify.rewrite > assoc_times.
148 apply (witness ? ? (m \sup n1 *n)).reflexivity.
149 qed.
150
151 theorem p_ord_aux_to_Prop1: \forall p,n,m. (S O) < m \to O < n \to n \le p \to
152   match p_ord_aux p n m with
153   [ (pair q r) \Rightarrow r \mod m \neq O].
154 intro.elim p.absurd (O < n).assumption.
155 apply le_to_not_lt.assumption.
156 change with
157 match 
158   (match n1 \mod m with
159     [ O \Rightarrow 
160         match (p_ord_aux n(n1 / m) m) with
161         [ (pair q r) \Rightarrow pair nat nat (S q) r]
162     | (S a) \Rightarrow pair nat nat O n1])
163 with
164   [ (pair q r) \Rightarrow r \mod m \neq O].
165 apply (nat_case1 (n1 \mod m)).intro.
166 generalize in match (H (n1 / m) m).
167 elim (p_ord_aux n (n1 / m) m).
168 apply H5.assumption.
169 apply eq_mod_O_to_lt_O_div.
170 apply (trans_lt ? (S O)).unfold lt.apply le_n.
171 assumption.assumption.assumption.
172 apply le_S_S_to_le.
173 apply (trans_le ? n1).change with (n1 / m < n1).
174 apply lt_div_n_m_n.assumption.assumption.assumption.
175 intros.
176 change with (n1 \mod m \neq O).
177 rewrite > H4.
178 unfold Not.intro.
179 apply (not_eq_O_S m1).
180 rewrite > H5.reflexivity.
181 qed.
182
183 theorem p_ord_aux_to_not_mod_O: \forall p,n,m,q,r. (S O) < m \to O < n \to n \le p \to
184  pair nat nat q r = p_ord_aux p n m \to r \mod m \neq O.
185 intros.
186 change with 
187   match (pair nat nat q r) with
188   [ (pair q r) \Rightarrow r \mod m \neq O].
189 rewrite > H3. 
190 apply p_ord_aux_to_Prop1.
191 assumption.assumption.assumption.
192 qed.
193