]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma
freescale porting, work in progress
[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / 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: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
19 (*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
20 (*                                                                        *)
21 (* ********************************************************************** *)
22
23 include "freescale/theory.ma".
24 include "freescale/bool.ma".
25
26 (* ******** *)
27 (* BOOLEANI *)
28 (* ******** *)
29
30 ndefinition bool_destruct_aux ≝
31 Πb1,b2:bool.ΠP:Prop.b1 = b2 →
32  match b1 with
33   [ true ⇒ match b2 with [ true ⇒ P → P | false ⇒ P ]
34   | false ⇒ match b2 with [ true ⇒ P | false ⇒ P → P ]
35   ].
36
37 ndefinition bool_destruct : bool_destruct_aux.
38  #b1; #b2; #P;
39  nelim b1;
40  nelim b2;
41  nnormalize;
42  #H;
43  ##[ ##2: napply False_ind;
44           nchange with (match true with [ true ⇒ False | false ⇒ True]);
45           nrewrite > H;
46           nnormalize;
47           napply I
48  ##| ##3: napply False_ind;
49           nchange with (match true with [ true ⇒ False | false ⇒ True]);
50           nrewrite < H;
51           nnormalize;
52           napply I
53  ##| ##1,4: napply (λx:P.x)
54  ##]
55 nqed.
56
57 nlemma symmetric_eqbool : symmetricT bool bool eq_bool.
58  #b1; #b2;
59  nelim b1;
60  nelim b2;
61  nnormalize;
62  napply refl_eq.
63 nqed.
64
65 nlemma symmetric_andbool : symmetricT bool bool and_bool.
66  #b1; #b2;
67  nelim b1;
68  nelim b2;
69  nnormalize;
70  napply refl_eq.
71 nqed.
72
73 nlemma associative_andbool : ∀b1,b2,b3.((b1 ⊗ b2) ⊗ b3) = (b1 ⊗ (b2 ⊗ b3)).
74  #b1; #b2; #b3;
75  nelim b1;
76  nelim b2;
77  nelim b3;
78  nnormalize;
79  napply refl_eq.
80 nqed.
81
82 nlemma symmetric_orbool : symmetricT bool bool or_bool.
83  #b1; #b2;
84  nelim b1;
85  nelim b2;
86  nnormalize;
87  napply refl_eq.
88 nqed.
89
90 nlemma associative_orbool : ∀b1,b2,b3.((b1 ⊕ b2) ⊕ b3) = (b1 ⊕ (b2 ⊕ b3)).
91  #b1; #b2; #b3;
92  nelim b1;
93  nelim b2;
94  nelim b3;
95  nnormalize;
96  napply refl_eq.
97 nqed.
98
99 nlemma symmetric_xorbool : symmetricT bool bool xor_bool.
100  #b1; #b2;
101  nelim b1;
102  nelim b2;
103  nnormalize;
104  napply refl_eq.
105 nqed.
106
107 nlemma associative_xorbool : ∀b1,b2,b3.((b1 ⊙ b2) ⊙ b3) = (b1 ⊙ (b2 ⊙ b3)).
108  #b1; #b2; #b3;
109  nelim b1;
110  nelim b2;
111  nelim b3;
112  nnormalize;
113  napply refl_eq.
114 nqed.
115
116 nlemma eqbool_to_eq : ∀b1,b2:bool.(eq_bool b1 b2 = true) → (b1 = b2).
117  #b1; #b2;
118  ncases b1;
119  ncases b2;
120  nnormalize;
121  ##[ ##1,4: #H; napply refl_eq
122  ##| ##*: #H; napply (bool_destruct … H)
123  ##]
124 nqed.
125
126 nlemma eq_to_eqbool : ∀b1,b2.b1 = b2 → eq_bool b1 b2 = true.
127  #b1; #b2;
128  ncases b1;
129  ncases b2;
130  nnormalize;
131  ##[ ##1,4: #H; napply refl_eq
132  ##| ##*: #H; napply (bool_destruct … H)
133  ##]
134 nqed.
135
136 nlemma andb_true_true_l: ∀b1,b2.(b1 ⊗ b2) = true → b1 = true.
137  #b1; #b2;
138  ncases b1;
139  ncases b2;
140  nnormalize;
141  ##[ ##1,2: #H; napply refl_eq
142  ##| ##*: #H; napply (bool_destruct … H)
143  ##]
144 nqed.
145
146 nlemma andb_true_true_r: ∀b1,b2.(b1 ⊗ b2) = true → b2 = true.
147  #b1; #b2;
148  ncases b1;
149  ncases b2;
150  nnormalize;
151  ##[ ##1,3: #H; napply refl_eq
152  ##| ##*: #H; napply (bool_destruct … H)
153  ##]
154 nqed.
155
156 nlemma orb_false_false_l : ∀b1,b2:bool.(b1 ⊕ b2) = false → b1 = false.
157  #b1; #b2;
158  ncases b1;
159  ncases b2;
160  nnormalize;
161  ##[ ##4: #H; napply refl_eq
162  ##| ##*: #H; napply (bool_destruct … H)
163  ##]
164 nqed.
165
166 nlemma orb_false_false_r : ∀b1,b2:bool.(b1 ⊕ b2) = false → b2 = false.
167  #b1; #b2;
168  ncases b1;
169  ncases b2;
170  nnormalize;
171  ##[ ##4: #H; napply refl_eq
172  ##| ##*: #H; napply (bool_destruct … H)
173  ##]
174 nqed.