helm/software/matita/contribs/ng_assembly2/num/bitrigesim.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 "common/comp.ma".
  24 include "num/bool_lemmas.ma".
  25
  26 (* ************* *)
  27 (* BITRIGESIMALI *)
  28 (* ************* *)
  29
  30 ninductive bitrigesim : Type ≝
  31   t00: bitrigesim
  32 | t01: bitrigesim
  33 | t02: bitrigesim
  34 | t03: bitrigesim
  35 | t04: bitrigesim
  36 | t05: bitrigesim
  37 | t06: bitrigesim
  38 | t07: bitrigesim
  39 | t08: bitrigesim
  40 | t09: bitrigesim
  41 | t0A: bitrigesim
  42 | t0B: bitrigesim
  43 | t0C: bitrigesim
  44 | t0D: bitrigesim
  45 | t0E: bitrigesim
  46 | t0F: bitrigesim
  47 | t10: bitrigesim
  48 | t11: bitrigesim
  49 | t12: bitrigesim
  50 | t13: bitrigesim
  51 | t14: bitrigesim
  52 | t15: bitrigesim
  53 | t16: bitrigesim
  54 | t17: bitrigesim
  55 | t18: bitrigesim
  56 | t19: bitrigesim
  57 | t1A: bitrigesim
  58 | t1B: bitrigesim
  59 | t1C: bitrigesim
  60 | t1D: bitrigesim
  61 | t1E: bitrigesim
  62 | t1F: bitrigesim.
  63
  64 (* operatore = *)
  65 ndefinition eq_bit ≝
  66 λt1,t2:bitrigesim.
  67  match t1 with
  68   [ t00 ⇒ match t2 with [ t00 ⇒ true | _ ⇒ false ] | t01 ⇒ match t2 with [ t01 ⇒ true | _ ⇒ false ]
  69   | t02 ⇒ match t2 with [ t02 ⇒ true | _ ⇒ false ] | t03 ⇒ match t2 with [ t03 ⇒ true | _ ⇒ false ]
  70   | t04 ⇒ match t2 with [ t04 ⇒ true | _ ⇒ false ] | t05 ⇒ match t2 with [ t05 ⇒ true | _ ⇒ false ]
  71   | t06 ⇒ match t2 with [ t06 ⇒ true | _ ⇒ false ] | t07 ⇒ match t2 with [ t07 ⇒ true | _ ⇒ false ]
  72   | t08 ⇒ match t2 with [ t08 ⇒ true | _ ⇒ false ] | t09 ⇒ match t2 with [ t09 ⇒ true | _ ⇒ false ]
  73   | t0A ⇒ match t2 with [ t0A ⇒ true | _ ⇒ false ] | t0B ⇒ match t2 with [ t0B ⇒ true | _ ⇒ false ]
  74   | t0C ⇒ match t2 with [ t0C ⇒ true | _ ⇒ false ] | t0D ⇒ match t2 with [ t0D ⇒ true | _ ⇒ false ]
  75   | t0E ⇒ match t2 with [ t0E ⇒ true | _ ⇒ false ] | t0F ⇒ match t2 with [ t0F ⇒ true | _ ⇒ false ]
  76   | t10 ⇒ match t2 with [ t10 ⇒ true | _ ⇒ false ] | t11 ⇒ match t2 with [ t11 ⇒ true | _ ⇒ false ]
  77   | t12 ⇒ match t2 with [ t12 ⇒ true | _ ⇒ false ] | t13 ⇒ match t2 with [ t13 ⇒ true | _ ⇒ false ]
  78   | t14 ⇒ match t2 with [ t14 ⇒ true | _ ⇒ false ] | t15 ⇒ match t2 with [ t15 ⇒ true | _ ⇒ false ]
  79   | t16 ⇒ match t2 with [ t16 ⇒ true | _ ⇒ false ] | t17 ⇒ match t2 with [ t17 ⇒ true | _ ⇒ false ]
  80   | t18 ⇒ match t2 with [ t18 ⇒ true | _ ⇒ false ] | t19 ⇒ match t2 with [ t19 ⇒ true | _ ⇒ false ]
  81   | t1A ⇒ match t2 with [ t1A ⇒ true | _ ⇒ false ] | t1B ⇒ match t2 with [ t1B ⇒ true | _ ⇒ false ]
  82   | t1C ⇒ match t2 with [ t1C ⇒ true | _ ⇒ false ] | t1D ⇒ match t2 with [ t1D ⇒ true | _ ⇒ false ]
  83   | t1E ⇒ match t2 with [ t1E ⇒ true | _ ⇒ false ] | t1F ⇒ match t2 with [ t1F ⇒ true | _ ⇒ false ]
  84   ].
  85
  86 (* iteratore sui bitrigesimali *)
  87 ndefinition forall_bit ≝ λP.
  88  P t00 ⊗ P t01 ⊗ P t02 ⊗ P t03 ⊗ P t04 ⊗ P t05 ⊗ P t06 ⊗ P t07 ⊗
  89  P t08 ⊗ P t09 ⊗ P t0A ⊗ P t0B ⊗ P t0C ⊗ P t0D ⊗ P t0E ⊗ P t0F ⊗
  90  P t10 ⊗ P t11 ⊗ P t12 ⊗ P t13 ⊗ P t14 ⊗ P t15 ⊗ P t16 ⊗ P t17 ⊗
  91  P t18 ⊗ P t19 ⊗ P t1A ⊗ P t1B ⊗ P t1C ⊗ P t1D ⊗ P t1E ⊗ P t1F.
  92
  93 (* operatore successore *)
  94 ndefinition succ_bit ≝
  95 λn.match n with
  96  [ t00 ⇒ t01 | t01 ⇒ t02 | t02 ⇒ t03 | t03 ⇒ t04 | t04 ⇒ t05 | t05 ⇒ t06 | t06 ⇒ t07 | t07 ⇒ t08
  97  | t08 ⇒ t09 | t09 ⇒ t0A | t0A ⇒ t0B | t0B ⇒ t0C | t0C ⇒ t0D | t0D ⇒ t0E | t0E ⇒ t0F | t0F ⇒ t10
  98  | t10 ⇒ t11 | t11 ⇒ t12 | t12 ⇒ t13 | t13 ⇒ t14 | t14 ⇒ t15 | t15 ⇒ t16 | t16 ⇒ t17 | t17 ⇒ t18
  99  | t18 ⇒ t19 | t19 ⇒ t1A | t1A ⇒ t1B | t1B ⇒ t1C | t1C ⇒ t1D | t1D ⇒ t1E | t1E ⇒ t1F | t1F ⇒ t00
 100  ].
 101
 102 (* bitrigesimali ricorsivi *)
 103 ninductive rec_bitrigesim : bitrigesim → Type ≝
 104   bi_O : rec_bitrigesim t00
 105 | bi_S : ∀n.rec_bitrigesim n → rec_bitrigesim (succ_bit n).
 106
 107 (* bitrigesimali → bitrigesimali ricorsivi *)
 108 ndefinition bit_to_recbit ≝
 109 λn.match n return λx.rec_bitrigesim x with
 110  [ t00 ⇒ bi_O
 111  | t01 ⇒ bi_S ? bi_O
 112  | t02 ⇒ bi_S ? (bi_S ? bi_O)
 113  | t03 ⇒ bi_S ? (bi_S ? (bi_S ? bi_O))
 114  | t04 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))
 115  | t05 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))
 116  | t06 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))
 117  | t07 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))
 118  | t08 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 119          bi_O)))))))
 120  | t09 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 121         (bi_S ? bi_O))))))))
 122  | t0A ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 123         (bi_S ? (bi_S ? bi_O)))))))))
 124  | t0B ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 125         (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))
 126  | t0C ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 127         (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))))
 128  | t0D ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 129         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))
 130  | t0E ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 131         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))))))
 132  | t0F ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 133         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))
 134  | t10 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 135         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 136          bi_O)))))))))))))))
 137  | t11 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 138         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 139         (bi_S ? bi_O))))))))))))))))
 140  | t12 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 141         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 142         (bi_S ? (bi_S ? bi_O)))))))))))))))))
 143  | t13 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 144         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 145         (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))))))
 146  | t14 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 147         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 148         (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))))))))))))
 149  | t15 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 150         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 151         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))))))))
 152  | t16 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 153         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 154         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))))))))))))))
 155  | t17 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 156         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 157         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))))))))))
 158  | t18 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 159         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 160         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 161          bi_O)))))))))))))))))))))))
 162  | t19 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 163         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 164         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 165         (bi_S ? bi_O))))))))))))))))))))))))
 166  | t1A ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 167         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 168         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 169         (bi_S ? (bi_S ? bi_O)))))))))))))))))))))))))
 170  | t1B ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 171         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 172         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 173         (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))))))))))))))
 174  | t1C ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 175         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 176         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 177         (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))))))))))))))))))))
 178  | t1D ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 179         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 180         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 181         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))))))))))))))))
 182  | t1E ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 183         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 184         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 185         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))))))))))))))))))))))
 186  | t1F ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 187         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 188         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
 189         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))))))))))))))))))
 190  ].
 191
 192 ndefinition bitrigesim_destruct_aux ≝
 193 Πt1,t2:bitrigesim.ΠP:Prop.t1 = t2 →
 194  match eq_bit t1 t2 with [ true ⇒ P → P | false ⇒ P ].
 195
 196 ndefinition bitrigesim_destruct : bitrigesim_destruct_aux.
 197  #t1; #t2; #P; #H;
 198  nrewrite < H;
 199  nelim t1;
 200  nnormalize;
 201  napply (λx.x).
 202 nqed.
 203
 204 nlemma eq_to_eqbit : ∀n1,n2.n1 = n2 → eq_bit n1 n2 = true.
 205  #n1; #n2; #H;
 206  nrewrite > H;
 207  nelim n2;
 208  nnormalize;
 209  napply refl_eq.
 210 nqed.
 211
 212 nlemma neqbit_to_neq : ∀n1,n2.eq_bit n1 n2 = false → n1 ≠ n2.
 213  #n1; #n2; #H;
 214  napply (not_to_not (n1 = n2) (eq_bit n1 n2 = true) …);
 215  ##[ ##1: napply (eq_to_eqbit n1 n2)
 216  ##| ##2: napply (eqfalse_to_neqtrue … H)
 217  ##]
 218 nqed.
 219
 220 (* !!! per brevita... *)
 221 naxiom eqbit_to_eq : ∀t1,t2.eq_bit t1 t2 = true → t1 = t2.
 222
 223 nlemma neq_to_neqbit : ∀n1,n2.n1 ≠ n2 → eq_bit n1 n2 = false.
 224  #n1; #n2; #H;
 225  napply (neqtrue_to_eqfalse (eq_bit n1 n2));
 226  napply (not_to_not (eq_bit n1 n2 = true) (n1 = n2) ? H);
 227  napply (eqbit_to_eq n1 n2).
 228 nqed.
 229
 230 nlemma decidable_bit : ∀x,y:bitrigesim.decidable (x = y).
 231  #x; #y; nnormalize;
 232  napply (or2_elim (eq_bit x y = true) (eq_bit x y = false) ? (decidable_bexpr ?));
 233  ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqbit_to_eq … H))
 234  ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqbit_to_neq … H))
 235  ##]
 236 nqed.
 237
 238 nlemma symmetric_eqbit : symmetricT bitrigesim bool eq_bit.
 239  #n1; #n2;
 240  napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_bit n1 n2));
 241  ##[ ##1: #H; nrewrite > H; napply refl_eq
 242  ##| ##2: #H; nrewrite > (neq_to_neqbit n1 n2 H);
 243           napply (symmetric_eq ? (eq_bit n2 n1) false);
 244           napply (neq_to_neqbit n2 n1 (symmetric_neq ? n1 n2 H))
 245  ##]
 246 nqed.
 247
 248 nlemma bitrigesim_is_comparable : comparable.
 249  @ bitrigesim
 250   ##[ napply t00
 251   ##| napply forall_bit
 252   ##| napply eq_bit
 253   ##| napply eqbit_to_eq
 254   ##| napply eq_to_eqbit
 255   ##| napply neqbit_to_neq
 256   ##| napply neq_to_neqbit
 257   ##| napply decidable_bit
 258   ##| napply symmetric_eqbit
 259   ##]
 260 nqed.
 261
 262 unification hint 0 ≔ ⊢ carr bitrigesim_is_comparable ≡ bitrigesim.