]> matita.cs.unibo.it Git - helm.git/blob - matitaB/matita/contribs/ng_assembly2/num/bool_lemmas.ma
65afc35277e7310fbb993b774a9315a965b6eafa
[helm.git] / matitaB / matita / contribs / ng_assembly2 / num / bool_lemmas.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* ********************************************************************** *)
16 (*                          Progetto FreeScale                            *)
17 (*                                                                        *)
18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
19 (*   Sviluppo: 2008-2010                                                  *)
20 (*                                                                        *)
21 (* ********************************************************************** *)
22
23 include "num/bool.ma".
24 include "common/comp.ma".
25
26 (* ******** *)
27 (* BOOLEANI *)
28 (* ******** *)
29
30 ndefinition bool_destruct_aux ≝
31 Πb1,b2:bool.ΠP:Prop.b1 = b2 →
32  match eq_bool b1 b2 with [ true ⇒ P → P | false ⇒ P ].
33
34 ndefinition bool_destruct : bool_destruct_aux.
35  #b1; #b2; #P; #H;
36  nrewrite < H;
37  nelim b1;
38  nnormalize;
39  napply (λx.x).
40 nqed.
41
42 nlemma symmetric_eqbool : symmetricT bool bool eq_bool.
43  #b1; #b2;
44  nelim b1;
45  nelim b2;
46  nnormalize;
47  napply refl_eq.
48 nqed.
49
50 nlemma symmetric_andbool : symmetricT bool bool and_bool.
51  #b1; #b2;
52  nelim b1;
53  nelim b2;
54  nnormalize;
55  napply refl_eq.
56 nqed.
57
58 nlemma associative_andbool : ∀b1,b2,b3.((b1 ⊗ b2) ⊗ b3) = (b1 ⊗ (b2 ⊗ b3)).
59  #b1; #b2; #b3;
60  nelim b1;
61  nelim b2;
62  nelim b3;
63  nnormalize;
64  napply refl_eq.
65 nqed.
66
67 nlemma symmetric_orbool : symmetricT bool bool or_bool.
68  #b1; #b2;
69  nelim b1;
70  nelim b2;
71  nnormalize;
72  napply refl_eq.
73 nqed.
74
75 nlemma associative_orbool : ∀b1,b2,b3.((b1 ⊕ b2) ⊕ b3) = (b1 ⊕ (b2 ⊕ b3)).
76  #b1; #b2; #b3;
77  nelim b1;
78  nelim b2;
79  nelim b3;
80  nnormalize;
81  napply refl_eq.
82 nqed.
83
84 nlemma symmetric_xorbool : symmetricT bool bool xor_bool.
85  #b1; #b2;
86  nelim b1;
87  nelim b2;
88  nnormalize;
89  napply refl_eq.
90 nqed.
91
92 nlemma associative_xorbool : ∀b1,b2,b3.((b1 ⊙ b2) ⊙ b3) = (b1 ⊙ (b2 ⊙ b3)).
93  #b1; #b2; #b3;
94  nelim b1;
95  nelim b2;
96  nelim b3;
97  nnormalize;
98  napply refl_eq.
99 nqed.
100
101 nlemma eqbool_to_eq : ∀b1,b2:bool.(eq_bool b1 b2 = true) → (b1 = b2).
102  #b1; #b2;
103  ncases b1;
104  ncases b2;
105  nnormalize;
106  ##[ ##1,4: #H; napply refl_eq
107  ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*)
108  ##]
109 nqed.
110
111 nlemma eq_to_eqbool : ∀b1,b2.b1 = b2 → eq_bool b1 b2 = true.
112  #b1; #b2;
113  ncases b1;
114  ncases b2;
115  nnormalize;
116  ##[ ##1,4: #H; napply refl_eq
117  ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*)
118  ##]
119 nqed.
120
121 nlemma decidable_bool : ∀x,y:bool.decidable (x = y).
122  #x; #y;
123  nnormalize;
124  nelim x;
125  nelim y;
126  ##[ ##1,4: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
127  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …);
128           nnormalize; #H;
129           napply False_ind;
130           ndestruct (*napply (bool_destruct … H)*)
131  ##]
132 nqed.
133
134 nlemma decidable_bexpr : ∀x.(x = true) ∨ (x = false).
135  #x; ncases x;
136  ##[ ##1: napply (or2_intro1 (true = true) (true = false) (refl_eq …))
137  ##| ##2: napply (or2_intro2 (false = true) (false = false) (refl_eq …))
138  ##]
139 nqed.
140
141 nlemma neqbool_to_neq : ∀b1,b2:bool.(eq_bool b1 b2 = false) → (b1 ≠ b2).
142  #b1; #b2;
143  ncases b1;
144  ncases b2;
145  nnormalize;
146  ##[ ##1,4: #H; ndestruct (*napply (bool_destruct … H)*)
147  ##| ##*: #H; #H1; ndestruct (*napply (bool_destruct … H1)*)
148  ##]
149 nqed.
150
151 nlemma neq_to_neqbool : ∀b1,b2.b1 ≠ b2 → eq_bool b1 b2 = false.
152  #b1; #b2;
153  ncases b1;
154  ncases b2;
155  nnormalize;
156  ##[ ##1,4: #H; nelim (H (refl_eq …))
157  ##| ##*: #H; napply refl_eq
158  ##]
159 nqed.
160
161 nlemma eqfalse_to_neqtrue : ∀x.x = false → x ≠ true.
162  #x; nelim x;
163  ##[ ##1: #H; ndestruct (*napply (bool_destruct … H)*)
164  ##| ##2: #H; nnormalize; #H1; ndestruct (*napply (bool_destruct … H1)*)
165  ##]
166 nqed.
167
168 nlemma eqtrue_to_neqfalse : ∀x.x = true → x ≠ false.
169  #x; nelim x;
170  ##[ ##1: #H; nnormalize; #H1; ndestruct (*napply (bool_destruct … H1)*)
171  ##| ##2: #H; ndestruct (*napply (bool_destruct … H)*)
172  ##]
173 nqed.
174
175 nlemma neqfalse_to_eqtrue : ∀x.x ≠ false → x = true.
176  #x; nelim x;
177  ##[ ##1: #H; napply refl_eq
178  ##| ##2: nnormalize; #H; nelim (H (refl_eq …))
179  ##]
180 nqed.
181
182 nlemma neqtrue_to_eqfalse : ∀x.x ≠ true → x = false.
183  #x; nelim x;
184  ##[ ##1: nnormalize; #H; nelim (H (refl_eq …))
185  ##| ##2: #H; napply refl_eq
186  ##]
187 nqed.
188
189 nlemma andb_true_true_l: ∀b1,b2.(b1 ⊗ b2) = true → b1 = true.
190  #b1; #b2;
191  ncases b1;
192  ncases b2;
193  nnormalize;
194  ##[ ##1,2: #H; napply refl_eq
195  ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*)
196  ##]
197 nqed.
198
199 nlemma andb_true_true_r: ∀b1,b2.(b1 ⊗ b2) = true → b2 = true.
200  #b1; #b2;
201  ncases b1;
202  ncases b2;
203  nnormalize;
204  ##[ ##1,3: #H; napply refl_eq
205  ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*)
206  ##]
207 nqed.
208
209 nlemma andb_false2
210  : ∀b1,b2.(b1 ⊗ b2) = false →
211    (b1 = false) ∨ (b2 = false).
212  #b1; #b2;
213  ncases b1;
214  ncases b2;
215  nnormalize;
216  ##[ ##1: #H; ndestruct (*napply (bool_destruct … H)*)
217  ##| ##2,4: #H; napply (or2_intro2 … H)
218  ##| ##3: #H; napply (or2_intro1 … H)
219  ##]
220 nqed.
221
222 nlemma andb_false3
223  : ∀b1,b2,b3.(b1 ⊗ b2 ⊗ b3) = false →
224    Or3 (b1 = false) (b2 = false) (b3 = false).
225  #b1; #b2; #b3;
226  ncases b1;
227  ncases b2;
228  ncases b3;
229  nnormalize;
230  ##[ ##1: #H; ndestruct (*napply (bool_destruct … H)*)
231  ##| ##5,6,7,8: #H; napply (or3_intro1 … H)
232  ##| ##2,4: #H; napply (or3_intro3 … H)
233  ##| ##3: #H; napply (or3_intro2 … H)
234  ##]
235 nqed.
236
237 nlemma andb_false4
238  : ∀b1,b2,b3,b4.(b1 ⊗ b2 ⊗ b3 ⊗ b4) = false →
239    Or4 (b1 = false) (b2 = false) (b3 = false) (b4 = false).
240  #b1; #b2; #b3; #b4;
241  ncases b1;
242  ncases b2;
243  ncases b3;
244  ncases b4;
245  nnormalize;
246  ##[ ##1: #H; ndestruct (*napply (bool_destruct … H)*)
247  ##| ##9,10,11,12,13,14,15,16: #H; napply (or4_intro1 … H)
248  ##| ##5,6,7,8: #H; napply (or4_intro2 … H)
249  ##| ##3,4: #H; napply (or4_intro3 … H)
250  ##| ##2: #H; napply (or4_intro4 … H)
251  ##]
252 nqed.
253
254 nlemma andb_false5
255  : ∀b1,b2,b3,b4,b5.(b1 ⊗ b2 ⊗ b3 ⊗ b4 ⊗ b5) = false →
256    Or5 (b1 = false) (b2 = false) (b3 = false) (b4 = false) (b5 = false).
257  #b1; #b2; #b3; #b4; #b5;
258  ncases b1;
259  ncases b2;
260  ncases b3;
261  ncases b4;
262  ncases b5;
263  nnormalize;
264  ##[ ##1: #H; ndestruct (*napply (bool_destruct … H)*)
265  ##| ##17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #H; napply (or5_intro1 … H)
266  ##| ##9,10,11,12,13,14,15,16: #H; napply (or5_intro2 … H)
267  ##| ##5,6,7,8: #H; napply (or5_intro3 … H)
268  ##| ##3,4: #H; napply (or5_intro4 … H)
269  ##| ##2: #H; napply (or5_intro5 … H)
270  ##]
271 nqed.
272
273 nlemma andb_false2_1 : ∀b.(false ⊗ b) = false.
274  #b; nnormalize; napply refl_eq. nqed.
275 nlemma andb_false2_2 : ∀b.(b ⊗ false) = false.
276  #b; nelim b; nnormalize; napply refl_eq. nqed.
277
278 nlemma andb_false3_1 : ∀b1,b2.(false ⊗ b1 ⊗ b2) = false.
279  #b1; #b2; nnormalize; napply refl_eq. nqed.
280 nlemma andb_false3_2 : ∀b1,b2.(b1 ⊗ false ⊗ b2) = false.
281  #b1; #b2; nelim b1; nnormalize; napply refl_eq. nqed.
282 nlemma andb_false3_3 : ∀b1,b2.(b1 ⊗ b2 ⊗ false) = false.
283  #b1; #b2; nelim b1; nelim b2; nnormalize; napply refl_eq. nqed.
284
285 nlemma andb_false4_1 : ∀b1,b2,b3.(false ⊗ b1 ⊗ b2 ⊗ b3) = false.
286  #b1; #b2; #b3; nnormalize; napply refl_eq. nqed.
287 nlemma andb_false4_2 : ∀b1,b2,b3.(b1 ⊗ false ⊗ b2 ⊗ b3) = false.
288  #b1; #b2; #b3; nelim b1; nnormalize; napply refl_eq. nqed.
289 nlemma andb_false4_3 : ∀b1,b2,b3.(b1 ⊗ b2 ⊗ false ⊗ b3) = false.
290  #b1; #b2; #b3; nelim b1; nelim b2; nnormalize; napply refl_eq. nqed.
291 nlemma andb_false4_4 : ∀b1,b2,b3.(b1 ⊗ b2 ⊗ b3 ⊗ false) = false.
292  #b1; #b2; #b3; nelim b1; nelim b2; nelim b3; nnormalize; napply refl_eq. nqed.
293
294 nlemma andb_false5_1 : ∀b1,b2,b3,b4.(false ⊗ b1 ⊗ b2 ⊗ b3 ⊗ b4) = false.
295  #b1; #b2; #b3; #b4; nnormalize; napply refl_eq. nqed.
296 nlemma andb_false5_2 : ∀b1,b2,b3,b4.(b1 ⊗ false ⊗ b2 ⊗ b3 ⊗ b4) = false.
297  #b1; #b2; #b3; #b4; nelim b1; nnormalize; napply refl_eq. nqed.
298 nlemma andb_false5_3 : ∀b1,b2,b3,b4.(b1 ⊗ b2 ⊗ false ⊗ b3 ⊗ b4) = false.
299  #b1; #b2; #b3; #b4; nelim b1; nelim b2; nnormalize; napply refl_eq. nqed.
300 nlemma andb_false5_4 : ∀b1,b2,b3,b4.(b1 ⊗ b2 ⊗ b3 ⊗ false ⊗ b4) = false.
301  #b1; #b2; #b3; #b4; nelim b1; nelim b2; nelim b3; nnormalize; napply refl_eq. nqed.
302 nlemma andb_false5_5 : ∀b1,b2,b3,b4.(b1 ⊗ b2 ⊗ b3 ⊗ b4 ⊗ false) = false.
303  #b1; #b2; #b3; #b4; nelim b1; nelim b2; nelim b3; nelim b4; nnormalize; napply refl_eq. nqed.
304
305 nlemma orb_false_false_l : ∀b1,b2:bool.(b1 ⊕ b2) = false → b1 = false.
306  #b1; #b2;
307  ncases b1;
308  ncases b2;
309  nnormalize;
310  ##[ ##4: #H; napply refl_eq
311  ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*)
312  ##]
313 nqed.
314
315 nlemma orb_false_false_r : ∀b1,b2:bool.(b1 ⊕ b2) = false → b2 = false.
316  #b1; #b2;
317  ncases b1;
318  ncases b2;
319  nnormalize;
320  ##[ ##4: #H; napply refl_eq
321  ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*)
322  ##]
323 nqed.
324
325 nlemma bool_is_comparable : comparable.
326  @ bool
327   ##[ napply false
328   ##| napply forall_bool
329   ##| napply eq_bool
330   ##| napply eqbool_to_eq
331   ##| napply eq_to_eqbool
332   ##| napply neqbool_to_neq
333   ##| napply neq_to_neqbool
334   ##| napply decidable_bool
335   ##| napply symmetric_eqbool
336   ##]
337 nqed.
338
339 unification hint 0 ≔ ⊢ carr bool_is_comparable ≡ bool.