]> matita.cs.unibo.it Git - helm.git/blob - matita/library/nat/ord.ma
(co)inductive type declarations are now documented
[helm.git] / 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.simplify.
42 apply (nat_case (n \mod m)).
43 simplify.apply plus_n_O.
44 intros.
45 simplify.apply plus_n_O.
46 simplify. 
47 apply (nat_case1 (n1 \mod m)).intro.
48 simplify.
49 generalize in match (H (n1 / m) m).
50 elim (p_ord_aux n (n1 / m) m).
51 simplify.
52 rewrite > assoc_times.
53 rewrite < H3.rewrite > (plus_n_O (m*(n1 / m))).
54 rewrite < H2.
55 rewrite > sym_times.
56 rewrite < div_mod.reflexivity.
57 assumption.assumption.
58 intros.simplify.apply plus_n_O. 
59 qed.
60
61 theorem p_ord_aux_to_exp: \forall p,n,m,q,r. O < m \to
62   (pair nat nat q r) = p_ord_aux p n m \to n = m \sup q * r.
63 intros.
64 change with 
65 match (pair nat nat q r) with
66   [ (pair q r) \Rightarrow n = m \sup q * r ].
67 rewrite > H1.
68 apply p_ord_aux_to_Prop.
69 assumption.
70 qed.
71 (* questo va spostato in primes1.ma *)
72 theorem p_ord_exp: \forall n,m,i. O < m \to n \mod m \neq O \to
73 \forall p. i \le p \to p_ord_aux p (m \sup i * n) m = pair nat nat i n.
74 intros 5.
75 elim i.
76 simplify.
77 rewrite < plus_n_O.
78 apply (nat_case p).
79 simplify.
80 elim (n \mod m).simplify.reflexivity.simplify.reflexivity.
81 intro.
82 simplify.
83 cut (O < n \mod m \lor O = n \mod m).
84 elim Hcut.apply (lt_O_n_elim (n \mod m) H3).
85 intros. simplify.reflexivity.
86 apply False_ind.
87 apply H1.apply sym_eq.assumption.
88 apply le_to_or_lt_eq.apply le_O_n.
89 generalize in match H3.
90 apply (nat_case p).intro.apply False_ind.apply (not_le_Sn_O n1 H4).
91 intros.
92 simplify. fold simplify (m \sup (S n1)).
93 cut (((m \sup (S n1)*n) \mod m) = O).
94 rewrite > Hcut.
95 simplify.fold simplify (m \sup (S n1)).
96 cut ((m \sup (S n1) *n) / m = m \sup n1 *n).
97 rewrite > Hcut1.
98 rewrite > (H2 m1). simplify.reflexivity.
99 apply le_S_S_to_le.assumption.
100 (* div_exp *)
101 simplify.
102 rewrite > assoc_times.
103 apply (lt_O_n_elim m H).
104 intro.apply div_times.
105 (* mod_exp = O *)
106 apply divides_to_mod_O.
107 assumption.
108 simplify.rewrite > assoc_times.
109 apply (witness ? ? (m \sup n1 *n)).reflexivity.
110 qed.
111
112 theorem p_ord_aux_to_Prop1: \forall p,n,m. (S O) < m \to O < n \to n \le p \to
113   match p_ord_aux p n m with
114   [ (pair q r) \Rightarrow r \mod m \neq O].
115 intro.elim p.absurd (O < n).assumption.
116 apply le_to_not_lt.assumption.
117 simplify.
118 apply (nat_case1 (n1 \mod m)).intro.
119 generalize in match (H (n1 / m) m).
120 elim (p_ord_aux n (n1 / m) m).
121 apply H5.assumption.
122 apply eq_mod_O_to_lt_O_div.
123 apply (trans_lt ? (S O)).unfold lt.apply le_n.
124 assumption.assumption.assumption.
125 apply le_S_S_to_le.
126 apply (trans_le ? n1).change with (n1 / m < n1).
127 apply lt_div_n_m_n.assumption.assumption.assumption.
128 intros.simplify.
129 rewrite > H4.
130 unfold Not.intro.
131 apply (not_eq_O_S m1).
132 rewrite > H5.reflexivity.
133 qed.
134
135 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
136  pair nat nat q r = p_ord_aux p n m \to r \mod m \neq O.
137 intros.
138 change with 
139   match (pair nat nat q r) with
140   [ (pair q r) \Rightarrow r \mod m \neq O].
141 rewrite > H3. 
142 apply p_ord_aux_to_Prop1.
143 assumption.assumption.assumption.
144 qed.
145