helm/software/matita/contribs/ng_assembly/num/bitrigesim_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 (*   Ultima modifica: 05/08/2009                                          *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "num/bitrigesim.ma".
  24 include "num/bool_lemmas.ma".
  25
  26 (* ************* *)
  27 (* BITRIGESIMALI *)
  28 (* ************* *)
  29
  30 ndefinition bitrigesim_destruct_aux ≝
  31 Πt1,t2:bitrigesim.ΠP:Prop.t1 = t2 →
  32  match eq_bit t1 t2 with [ true ⇒ P → P | false ⇒ P ].
  33
  34 ndefinition bitrigesim_destruct : bitrigesim_destruct_aux.
  35  #t1; #t2; #P; #H;
  36  nrewrite < H;
  37  nelim t1;
  38  nnormalize;
  39  napply (λx.x).
  40 nqed.
  41
  42 nlemma eq_to_eqbit : ∀n1,n2.n1 = n2 → eq_bit n1 n2 = true.
  43  #n1; #n2; #H;
  44  nrewrite > H;
  45  nelim n2;
  46  nnormalize;
  47  napply refl_eq.
  48 nqed.
  49
  50 nlemma neqbit_to_neq : ∀n1,n2.eq_bit n1 n2 = false → n1 ≠ n2.
  51  #n1; #n2; #H;
  52  napply (not_to_not (n1 = n2) (eq_bit n1 n2 = true) …);
  53  ##[ ##1: napply (eq_to_eqbit n1 n2)
  54  ##| ##2: napply (eqfalse_to_neqtrue … H)
  55  ##]
  56 nqed.
  57
  58 nlemma eqbit_to_eq1 : ∀t2.eq_bit t00 t2 = true → t00 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##1: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
  59 nlemma eqbit_to_eq2 : ∀t2.eq_bit t01 t2 = true → t01 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##2: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
  60 nlemma eqbit_to_eq3 : ∀t2.eq_bit t02 t2 = true → t02 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##3: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
  61 nlemma eqbit_to_eq4 : ∀t2.eq_bit t03 t2 = true → t03 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##4: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
  62 nlemma eqbit_to_eq5 : ∀t2.eq_bit t04 t2 = true → t04 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##5: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
  63 nlemma eqbit_to_eq6 : ∀t2.eq_bit t05 t2 = true → t05 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##6: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
  64 nlemma eqbit_to_eq7 : ∀t2.eq_bit t06 t2 = true → t06 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##7: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
  65 nlemma eqbit_to_eq8 : ∀t2.eq_bit t07 t2 = true → t07 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##8: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
  66 nlemma eqbit_to_eq9 : ∀t2.eq_bit t08 t2 = true → t08 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##9: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
  67 nlemma eqbit_to_eq10 : ∀t2.eq_bit t09 t2 = true → t09 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##10: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
  68 nlemma eqbit_to_eq11 : ∀t2.eq_bit t0A t2 = true → t0A = t2. #t2; ncases t2; nnormalize; #H; ##[ ##11: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
  69 nlemma eqbit_to_eq12 : ∀t2.eq_bit t0B t2 = true → t0B = t2. #t2; ncases t2; nnormalize; #H; ##[ ##12: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
  70 nlemma eqbit_to_eq13 : ∀t2.eq_bit t0C t2 = true → t0C = t2. #t2; ncases t2; nnormalize; #H; ##[ ##13: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
  71 nlemma eqbit_to_eq14 : ∀t2.eq_bit t0D t2 = true → t0D = t2. #t2; ncases t2; nnormalize; #H; ##[ ##14: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
  72 nlemma eqbit_to_eq15 : ∀t2.eq_bit t0E t2 = true → t0E = t2. #t2; ncases t2; nnormalize; #H; ##[ ##15: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
  73 nlemma eqbit_to_eq16 : ∀t2.eq_bit t0F t2 = true → t0F = t2. #t2; ncases t2; nnormalize; #H; ##[ ##16: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
  74 nlemma eqbit_to_eq17 : ∀t2.eq_bit t10 t2 = true → t10 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##17: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
  75 nlemma eqbit_to_eq18 : ∀t2.eq_bit t11 t2 = true → t11 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##18: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
  76 nlemma eqbit_to_eq19 : ∀t2.eq_bit t12 t2 = true → t12 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##19: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
  77 nlemma eqbit_to_eq20 : ∀t2.eq_bit t13 t2 = true → t13 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##20: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
  78 nlemma eqbit_to_eq21 : ∀t2.eq_bit t14 t2 = true → t14 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##21: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
  79 nlemma eqbit_to_eq22 : ∀t2.eq_bit t15 t2 = true → t15 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##22: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
  80 nlemma eqbit_to_eq23 : ∀t2.eq_bit t16 t2 = true → t16 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##23: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
  81 nlemma eqbit_to_eq24 : ∀t2.eq_bit t17 t2 = true → t17 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##24: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
  82 nlemma eqbit_to_eq25 : ∀t2.eq_bit t18 t2 = true → t18 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##25: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
  83 nlemma eqbit_to_eq26 : ∀t2.eq_bit t19 t2 = true → t19 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##26: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
  84 nlemma eqbit_to_eq27 : ∀t2.eq_bit t1A t2 = true → t1A = t2. #t2; ncases t2; nnormalize; #H; ##[ ##27: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
  85 nlemma eqbit_to_eq28 : ∀t2.eq_bit t1B t2 = true → t1B = t2. #t2; ncases t2; nnormalize; #H; ##[ ##28: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
  86 nlemma eqbit_to_eq29 : ∀t2.eq_bit t1C t2 = true → t1C = t2. #t2; ncases t2; nnormalize; #H; ##[ ##29: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
  87 nlemma eqbit_to_eq30 : ∀t2.eq_bit t1D t2 = true → t1D = t2. #t2; ncases t2; nnormalize; #H; ##[ ##30: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
  88 nlemma eqbit_to_eq31 : ∀t2.eq_bit t1E t2 = true → t1E = t2. #t2; ncases t2; nnormalize; #H; ##[ ##31: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
  89 nlemma eqbit_to_eq32 : ∀t2.eq_bit t1F t2 = true → t1F = t2. #t2; ncases t2; nnormalize; #H; ##[ ##32: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
  90
  91 nlemma eqbit_to_eq : ∀t1,t2.eq_bit t1 t2 = true → t1 = t2.
  92  #t1; ncases t1;
  93  ##[ ##1: napply eqbit_to_eq1 ##| ##2: napply eqbit_to_eq2
  94  ##| ##3: napply eqbit_to_eq3 ##| ##4: napply eqbit_to_eq4
  95  ##| ##5: napply eqbit_to_eq5 ##| ##6: napply eqbit_to_eq6
  96  ##| ##7: napply eqbit_to_eq7 ##| ##8: napply eqbit_to_eq8
  97  ##| ##9: napply eqbit_to_eq9 ##| ##10: napply eqbit_to_eq10
  98  ##| ##11: napply eqbit_to_eq11 ##| ##12: napply eqbit_to_eq12
  99  ##| ##13: napply eqbit_to_eq13 ##| ##14: napply eqbit_to_eq14
 100  ##| ##15: napply eqbit_to_eq15 ##| ##16: napply eqbit_to_eq16
 101  ##| ##17: napply eqbit_to_eq17 ##| ##18: napply eqbit_to_eq18
 102  ##| ##19: napply eqbit_to_eq19 ##| ##20: napply eqbit_to_eq20
 103  ##| ##21: napply eqbit_to_eq21 ##| ##22: napply eqbit_to_eq22
 104  ##| ##23: napply eqbit_to_eq23 ##| ##24: napply eqbit_to_eq24
 105  ##| ##25: napply eqbit_to_eq25 ##| ##26: napply eqbit_to_eq26
 106  ##| ##27: napply eqbit_to_eq27 ##| ##28: napply eqbit_to_eq28
 107  ##| ##29: napply eqbit_to_eq29 ##| ##30: napply eqbit_to_eq30
 108  ##| ##31: napply eqbit_to_eq31 ##| ##32: napply eqbit_to_eq32
 109  ##]
 110 nqed.
 111
 112 nlemma neq_to_neqbit : ∀n1,n2.n1 ≠ n2 → eq_bit n1 n2 = false.
 113  #n1; #n2; #H;
 114  napply (neqtrue_to_eqfalse (eq_bit n1 n2));
 115  napply (not_to_not (eq_bit n1 n2 = true) (n1 = n2) ? H);
 116  napply (eqbit_to_eq n1 n2).
 117 nqed.
 118
 119 nlemma decidable_bit : ∀x,y:bitrigesim.decidable (x = y).
 120  #x; #y; nnormalize;
 121  napply (or2_elim (eq_bit x y = true) (eq_bit x y = false) ? (decidable_bexpr ?));
 122  ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqbit_to_eq … H))
 123  ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqbit_to_neq … H))
 124  ##]
 125 nqed.
 126
 127 nlemma symmetric_eqbit : symmetricT bitrigesim bool eq_bit.
 128  #n1; #n2;
 129  napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_bit n1 n2));
 130  ##[ ##1: #H; nrewrite > H; napply refl_eq
 131  ##| ##2: #H; nrewrite > (neq_to_neqbit n1 n2 H);
 132           napply (symmetric_eq ? (eq_bit n2 n1) false);
 133           napply (neq_to_neqbit n2 n1 (symmetric_neq ? n1 n2 H))
 134  ##]
 135 nqed.