]> matita.cs.unibo.it Git - helm.git/blob - matita/library/nat/compare.ma
c701cd2e7175c635e1ec67d93b9f0afed1ed8526
[helm.git] / matita / library / nat / compare.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 (*       \ /        This file 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/compare".
16
17 include "datatypes/bool.ma".
18 include "datatypes/compare.ma".
19 include "nat/orders.ma".
20
21 let rec eqb n m \def 
22 match n with 
23   [ O \Rightarrow 
24      match m with 
25      [ O \Rightarrow true
26            | (S q) \Rightarrow false] 
27   | (S p) \Rightarrow
28            match m with 
29      [ O \Rightarrow false
30            | (S q) \Rightarrow eqb p q]].
31            
32 theorem eqb_to_Prop: \forall n,m:nat. 
33 match (eqb n m) with
34 [ true  \Rightarrow n = m 
35 | false \Rightarrow n \neq m].
36 intros.
37 apply (nat_elim2
38 (\lambda n,m:nat.match (eqb n m) with
39 [ true  \Rightarrow n = m 
40 | false \Rightarrow n \neq m])).
41 intro.elim n1.
42 simplify.reflexivity.
43 simplify.apply not_eq_O_S.
44 intro.
45 simplify.unfold Not.
46 intro. apply (not_eq_O_S n1).apply sym_eq.assumption.
47 intros.simplify.
48 generalize in match H.
49 elim ((eqb n1 m1)).
50 simplify.apply eq_f.apply H1.
51 simplify.unfold Not.intro.apply H1.apply inj_S.assumption.
52 qed.
53
54 theorem eqb_elim : \forall n,m:nat.\forall P:bool \to Prop.
55 (n=m \to (P true)) \to (n \neq m \to (P false)) \to (P (eqb n m)). 
56 intros.
57 cut 
58 (match (eqb n m) with
59 [ true  \Rightarrow n = m
60 | false \Rightarrow n \neq m] \to (P (eqb n m))).
61 apply Hcut.apply eqb_to_Prop.
62 elim (eqb n m).
63 apply ((H H2)).
64 apply ((H1 H2)).
65 qed.
66
67 theorem eqb_n_n: \forall n. eqb n n = true.
68 intro.elim n.simplify.reflexivity.
69 simplify.assumption.
70 qed.
71
72 theorem eqb_true_to_eq: \forall n,m:nat.
73 eqb n m = true \to n = m.
74 intros.
75 change with 
76 match true with
77 [ true  \Rightarrow n = m 
78 | false \Rightarrow n \neq m].
79 rewrite < H.
80 apply eqb_to_Prop. 
81 qed.
82
83 theorem eqb_false_to_not_eq: \forall n,m:nat.
84 eqb n m = false \to n \neq m.
85 intros.
86 change with 
87 match false with
88 [ true  \Rightarrow n = m 
89 | false \Rightarrow n \neq m].
90 rewrite < H.
91 apply eqb_to_Prop. 
92 qed.
93
94 theorem eq_to_eqb_true: \forall n,m:nat.
95 n = m \to eqb n m = true.
96 intros.apply (eqb_elim n m).
97 intros. reflexivity.
98 intros.apply False_ind.apply (H1 H).
99 qed.
100
101 theorem not_eq_to_eqb_false: \forall n,m:nat.
102 \lnot (n = m) \to eqb n m = false.
103 intros.apply (eqb_elim n m).
104 intros. apply False_ind.apply (H H1).
105 intros.reflexivity.
106 qed.
107
108 let rec leb n m \def 
109 match n with 
110     [ O \Rightarrow true
111     | (S p) \Rightarrow
112         match m with 
113         [ O \Rightarrow false
114         | (S q) \Rightarrow leb p q]].
115
116 theorem leb_elim: \forall n,m:nat. \forall P:bool \to Prop. 
117 (n \leq m \to (P true)) \to (n \nleq m \to (P false)) \to
118 P (leb n m).
119 apply nat_elim2; intros; simplify
120   [apply H.apply le_O_n
121   |apply H1.apply not_le_Sn_O.
122   |apply H;intros
123     [apply H1.apply le_S_S.assumption.
124     |apply H2.unfold Not.intros.apply H3.apply le_S_S_to_le.assumption
125     ]
126   ]
127 qed.
128
129 (*
130 theorem decidable_le: \forall n,m. n \leq m \lor n \nleq m. 
131 intros.
132 apply (leb_elim n m)
133   [intro.left.assumption
134   |intro.right.assumption
135   ]
136 qed.
137 *)
138
139 theorem le_to_leb_true: \forall n,m. n \leq m \to leb n m = true.
140 intros.apply leb_elim;intros
141   [reflexivity
142   |apply False_ind.apply H1.apply H.
143   ]
144 qed.
145
146 theorem lt_to_leb_false: \forall n,m. m < n \to leb n m = false.
147 intros.apply leb_elim;intros
148   [apply False_ind.apply (le_to_not_lt ? ? H1). assumption
149   |reflexivity
150   ]
151 qed.
152
153 theorem leb_to_Prop: \forall n,m:nat. 
154 match (leb n m) with
155 [ true  \Rightarrow n \leq m 
156 | false \Rightarrow n \nleq m].
157 apply nat_elim2;simplify
158   [exact le_O_n
159   |exact not_le_Sn_O
160   |intros 2.simplify.
161    elim ((leb n m));simplify
162     [apply le_S_S.apply H
163     |unfold Not.intros.apply H.apply le_S_S_to_le.assumption
164     ]
165   ]
166 qed.
167
168 (*
169 theorem leb_elim: \forall n,m:nat. \forall P:bool \to Prop. 
170 (n \leq m \to (P true)) \to (n \nleq m \to (P false)) \to
171 P (leb n m).
172 intros.
173 cut 
174 (match (leb n m) with
175 [ true  \Rightarrow n \leq m
176 | false \Rightarrow n \nleq m] \to (P (leb n m))).
177 apply Hcut.apply leb_to_Prop.
178 elim (leb n m).
179 apply ((H H2)).
180 apply ((H1 H2)).
181 qed.
182 *)
183
184 let rec nat_compare n m: compare \def
185 match n with
186 [ O \Rightarrow 
187     match m with 
188       [ O \Rightarrow EQ
189       | (S q) \Rightarrow LT ]
190 | (S p) \Rightarrow 
191     match m with 
192       [ O \Rightarrow GT
193       | (S q) \Rightarrow nat_compare p q]].
194
195 theorem nat_compare_n_n: \forall n:nat. nat_compare n n = EQ.
196 intro.elim n.
197 simplify.reflexivity.
198 simplify.assumption.
199 qed.
200
201 theorem nat_compare_S_S: \forall n,m:nat. 
202 nat_compare n m = nat_compare (S n) (S m).
203 intros.simplify.reflexivity.
204 qed.
205
206 theorem S_pred: \forall n:nat.lt O n \to eq nat n (S (pred n)).
207 intro.elim n.apply False_ind.exact (not_le_Sn_O O H).
208 apply eq_f.apply pred_Sn.
209 qed.
210
211 theorem nat_compare_pred_pred: 
212 \forall n,m:nat.lt O n \to lt O m \to 
213 eq compare (nat_compare n m) (nat_compare (pred n) (pred m)).
214 intros.
215 apply (lt_O_n_elim n H).
216 apply (lt_O_n_elim m H1).
217 intros.
218 simplify.reflexivity.
219 qed.
220
221 theorem nat_compare_to_Prop: \forall n,m:nat. 
222 match (nat_compare n m) with
223   [ LT \Rightarrow n < m
224   | EQ \Rightarrow n=m
225   | GT \Rightarrow m < n ].
226 intros.
227 apply (nat_elim2 (\lambda n,m.match (nat_compare n m) with
228   [ LT \Rightarrow n < m
229   | EQ \Rightarrow n=m
230   | GT \Rightarrow m < n ])).
231 intro.elim n1.simplify.reflexivity.
232 simplify.unfold lt.apply le_S_S.apply le_O_n.
233 intro.simplify.unfold lt.apply le_S_S. apply le_O_n.
234 intros 2.simplify.elim ((nat_compare n1 m1)).
235 simplify. unfold lt. apply le_S_S.apply H.
236 simplify. apply eq_f. apply H.
237 simplify. unfold lt.apply le_S_S.apply H.
238 qed.
239
240 theorem nat_compare_n_m_m_n: \forall n,m:nat. 
241 nat_compare n m = compare_invert (nat_compare m n).
242 intros. 
243 apply (nat_elim2 (\lambda n,m. nat_compare n m = compare_invert (nat_compare m n))).
244 intros.elim n1.simplify.reflexivity.
245 simplify.reflexivity.
246 intro.elim n1.simplify.reflexivity.
247 simplify.reflexivity.
248 intros.simplify.elim H.reflexivity.
249 qed.
250      
251 theorem nat_compare_elim : \forall n,m:nat. \forall P:compare \to Prop.
252 (n < m \to P LT) \to (n=m \to P EQ) \to (m < n \to P GT) \to 
253 (P (nat_compare n m)).
254 intros.
255 cut (match (nat_compare n m) with
256 [ LT \Rightarrow n < m
257 | EQ \Rightarrow n=m
258 | GT \Rightarrow m < n] \to
259 (P (nat_compare n m))).
260 apply Hcut.apply nat_compare_to_Prop.
261 elim ((nat_compare n m)).
262 apply ((H H3)).
263 apply ((H1 H3)).
264 apply ((H2 H3)).
265 qed.