]> matita.cs.unibo.it Git - helm.git/blob - matita/library/nat/compare.ma
(co)inductive type declarations are now documented
[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_to_Prop: \forall n,m:nat. 
117 match (leb n m) with
118 [ true  \Rightarrow n \leq m 
119 | false \Rightarrow n \nleq m].
120 intros.
121 apply (nat_elim2
122 (\lambda n,m:nat.match (leb n m) with
123 [ true  \Rightarrow n \leq m 
124 | false \Rightarrow n \nleq m])).
125 simplify.exact le_O_n.
126 simplify.exact not_le_Sn_O.
127 intros 2.simplify.elim ((leb n1 m1)).
128 simplify.apply le_S_S.apply H.
129 simplify.unfold Not.intros.apply H.apply le_S_S_to_le.assumption.
130 qed.
131
132 theorem leb_elim: \forall n,m:nat. \forall P:bool \to Prop. 
133 (n \leq m \to (P true)) \to (n \nleq m \to (P false)) \to
134 P (leb n m).
135 intros.
136 cut 
137 (match (leb n m) with
138 [ true  \Rightarrow n \leq m
139 | false \Rightarrow n \nleq m] \to (P (leb n m))).
140 apply Hcut.apply leb_to_Prop.
141 elim (leb n m).
142 apply ((H H2)).
143 apply ((H1 H2)).
144 qed.
145
146 let rec nat_compare n m: compare \def
147 match n with
148 [ O \Rightarrow 
149     match m with 
150       [ O \Rightarrow EQ
151       | (S q) \Rightarrow LT ]
152 | (S p) \Rightarrow 
153     match m with 
154       [ O \Rightarrow GT
155       | (S q) \Rightarrow nat_compare p q]].
156
157 theorem nat_compare_n_n: \forall n:nat. nat_compare n n = EQ.
158 intro.elim n.
159 simplify.reflexivity.
160 simplify.assumption.
161 qed.
162
163 theorem nat_compare_S_S: \forall n,m:nat. 
164 nat_compare n m = nat_compare (S n) (S m).
165 intros.simplify.reflexivity.
166 qed.
167
168 theorem S_pred: \forall n:nat.lt O n \to eq nat n (S (pred n)).
169 intro.elim n.apply False_ind.exact (not_le_Sn_O O H).
170 apply eq_f.apply pred_Sn.
171 qed.
172
173 theorem nat_compare_pred_pred: 
174 \forall n,m:nat.lt O n \to lt O m \to 
175 eq compare (nat_compare n m) (nat_compare (pred n) (pred m)).
176 intros.
177 apply (lt_O_n_elim n H).
178 apply (lt_O_n_elim m H1).
179 intros.
180 simplify.reflexivity.
181 qed.
182
183 theorem nat_compare_to_Prop: \forall n,m:nat. 
184 match (nat_compare n m) with
185   [ LT \Rightarrow n < m
186   | EQ \Rightarrow n=m
187   | GT \Rightarrow m < n ].
188 intros.
189 apply (nat_elim2 (\lambda n,m.match (nat_compare n m) with
190   [ LT \Rightarrow n < m
191   | EQ \Rightarrow n=m
192   | GT \Rightarrow m < n ])).
193 intro.elim n1.simplify.reflexivity.
194 simplify.unfold lt.apply le_S_S.apply le_O_n.
195 intro.simplify.unfold lt.apply le_S_S. apply le_O_n.
196 intros 2.simplify.elim ((nat_compare n1 m1)).
197 simplify. unfold lt. apply le_S_S.apply H.
198 simplify. apply eq_f. apply H.
199 simplify. unfold lt.apply le_S_S.apply H.
200 qed.
201
202 theorem nat_compare_n_m_m_n: \forall n,m:nat. 
203 nat_compare n m = compare_invert (nat_compare m n).
204 intros. 
205 apply (nat_elim2 (\lambda n,m. nat_compare n m = compare_invert (nat_compare m n))).
206 intros.elim n1.simplify.reflexivity.
207 simplify.reflexivity.
208 intro.elim n1.simplify.reflexivity.
209 simplify.reflexivity.
210 intros.simplify.elim H.reflexivity.
211 qed.
212      
213 theorem nat_compare_elim : \forall n,m:nat. \forall P:compare \to Prop.
214 (n < m \to P LT) \to (n=m \to P EQ) \to (m < n \to P GT) \to 
215 (P (nat_compare n m)).
216 intros.
217 cut (match (nat_compare n m) with
218 [ LT \Rightarrow n < m
219 | EQ \Rightarrow n=m
220 | GT \Rightarrow m < n] \to
221 (P (nat_compare n m))).
222 apply Hcut.apply nat_compare_to_Prop.
223 elim ((nat_compare n m)).
224 apply ((H H3)).
225 apply ((H1 H3)).
226 apply ((H2 H3)).
227 qed.