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.