helm/software/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.