matita/matita/contribs/ng_assembly2/num/oct.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 (* OTTALI *)
  28 (* ****** *)
  29
  30 ninductive oct : Type ≝
  31   o0: oct
  32 | o1: oct
  33 | o2: oct
  34 | o3: oct
  35 | o4: oct
  36 | o5: oct
  37 | o6: oct
  38 | o7: oct.
  39
  40 (* iteratore sugli ottali *)
  41 ndefinition forall_oct ≝ λP.
  42  P o0 ⊗ P o1 ⊗ P o2 ⊗ P o3 ⊗ P o4 ⊗ P o5 ⊗ P o6 ⊗ P o7.
  43
  44 (* operatore = *)
  45 ndefinition eq_oct ≝
  46 λn1,n2:oct.
  47  match n1 with
  48   [ o0 ⇒ match n2 with [ o0 ⇒ true  | _ ⇒ false ]
  49   | o1 ⇒ match n2 with [ o1 ⇒ true  | _ ⇒ false ]
  50   | o2 ⇒ match n2 with [ o2 ⇒ true  | _ ⇒ false ]
  51   | o3 ⇒ match n2 with [ o3 ⇒ true  | _ ⇒ false ]
  52   | o4 ⇒ match n2 with [ o4 ⇒ true  | _ ⇒ false ]
  53   | o5 ⇒ match n2 with [ o5 ⇒ true  | _ ⇒ false ]
  54   | o6 ⇒ match n2 with [ o6 ⇒ true  | _ ⇒ false ]
  55   | o7 ⇒ match n2 with [ o7 ⇒ true  | _ ⇒ false ]
  56   ].
  57
  58 (* operatore and *)
  59 ndefinition and_oct ≝
  60 λe1,e2:oct.match e1 with
  61  [ o0 ⇒ match e2 with
  62   [ o0 ⇒ o0 | o1 ⇒ o0 | o2 ⇒ o0 | o3 ⇒ o0
  63   | o4 ⇒ o0 | o5 ⇒ o0 | o6 ⇒ o0 | o7 ⇒ o0 ]
  64  | o1 ⇒ match e2 with
  65   [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o0 | o3 ⇒ o1
  66   | o4 ⇒ o0 | o5 ⇒ o1 | o6 ⇒ o0 | o7 ⇒ o1 ]
  67  | o2 ⇒ match e2 with
  68   [ o0 ⇒ o0 | o1 ⇒ o0 | o2 ⇒ o2 | o3 ⇒ o2
  69   | o4 ⇒ o0 | o5 ⇒ o0 | o6 ⇒ o2 | o7 ⇒ o2 ]
  70  | o3 ⇒ match e2 with
  71   [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o2 | o3 ⇒ o3
  72   | o4 ⇒ o0 | o5 ⇒ o1 | o6 ⇒ o2 | o7 ⇒ o3 ]
  73  | o4 ⇒ match e2 with
  74   [ o0 ⇒ o0 | o1 ⇒ o0 | o2 ⇒ o0 | o3 ⇒ o0
  75   | o4 ⇒ o4 | o5 ⇒ o4 | o6 ⇒ o4 | o7 ⇒ o4 ]
  76  | o5 ⇒ match e2 with
  77   [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o0 | o3 ⇒ o1
  78   | o4 ⇒ o4 | o5 ⇒ o5 | o6 ⇒ o4 | o7 ⇒ o5 ]
  79  | o6 ⇒ match e2 with
  80   [ o0 ⇒ o0 | o1 ⇒ o0 | o2 ⇒ o2 | o3 ⇒ o2
  81   | o4 ⇒ o4 | o5 ⇒ o4 | o6 ⇒ o6 | o7 ⇒ o6 ]
  82  | o7 ⇒ match e2 with
  83   [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o2 | o3 ⇒ o3
  84   | o4 ⇒ o4 | o5 ⇒ o5 | o6 ⇒ o6 | o7 ⇒ o7 ]
  85  ].
  86
  87 (* operatore or *)
  88 ndefinition or_oct ≝
  89 λe1,e2:oct.match e1 with
  90  [ o0 ⇒ match e2 with
  91   [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o2 | o3 ⇒ o3
  92   | o4 ⇒ o4 | o5 ⇒ o5 | o6 ⇒ o6 | o7 ⇒ o7 ]
  93  | o1 ⇒ match e2 with
  94   [ o0 ⇒ o1 | o1 ⇒ o1 | o2 ⇒ o3 | o3 ⇒ o3
  95   | o4 ⇒ o5 | o5 ⇒ o5 | o6 ⇒ o7 | o7 ⇒ o7 ]
  96  | o2 ⇒ match e2 with
  97   [ o0 ⇒ o2 | o1 ⇒ o3 | o2 ⇒ o2 | o3 ⇒ o3
  98   | o4 ⇒ o6 | o5 ⇒ o7 | o6 ⇒ o6 | o7 ⇒ o7 ]
  99  | o3 ⇒ match e2 with
 100   [ o0 ⇒ o3 | o1 ⇒ o3 | o2 ⇒ o3 | o3 ⇒ o3
 101   | o4 ⇒ o7 | o5 ⇒ o7 | o6 ⇒ o7 | o7 ⇒ o7 ]
 102  | o4 ⇒ match e2 with
 103   [ o0 ⇒ o4 | o1 ⇒ o5 | o2 ⇒ o6 | o3 ⇒ o7
 104   | o4 ⇒ o4 | o5 ⇒ o5 | o6 ⇒ o6 | o7 ⇒ o7 ]
 105  | o5 ⇒ match e2 with
 106   [ o0 ⇒ o5 | o1 ⇒ o5 | o2 ⇒ o7 | o3 ⇒ o7
 107   | o4 ⇒ o5 | o5 ⇒ o5 | o6 ⇒ o7 | o7 ⇒ o7 ]
 108  | o6 ⇒ match e2 with
 109   [ o0 ⇒ o6 | o1 ⇒ o7 | o2 ⇒ o6 | o3 ⇒ o7
 110   | o4 ⇒ o6 | o5 ⇒ o7 | o6 ⇒ o6 | o7 ⇒ o7 ]
 111  | o7 ⇒ match e2 with
 112   [ o0 ⇒ o7 | o1 ⇒ o7 | o2 ⇒ o7 | o3 ⇒ o7
 113   | o4 ⇒ o7 | o5 ⇒ o7 | o6 ⇒ o7 | o7 ⇒ o7 ]
 114  ].
 115
 116 (* operatore xor *)
 117 ndefinition xor_oct ≝
 118 λe1,e2:oct.match e1 with
 119  [ o0 ⇒ match e2 with
 120   [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o2 | o3 ⇒ o3
 121   | o4 ⇒ o4 | o5 ⇒ o5 | o6 ⇒ o6 | o7 ⇒ o7 ]
 122  | o1 ⇒ match e2 with
 123   [ o0 ⇒ o1 | o1 ⇒ o0 | o2 ⇒ o3 | o3 ⇒ o2
 124   | o4 ⇒ o5 | o5 ⇒ o4 | o6 ⇒ o7 | o7 ⇒ o6 ]
 125  | o2 ⇒ match e2 with
 126   [ o0 ⇒ o2 | o1 ⇒ o3 | o2 ⇒ o0 | o3 ⇒ o1
 127   | o4 ⇒ o6 | o5 ⇒ o7 | o6 ⇒ o4 | o7 ⇒ o5 ]
 128  | o3 ⇒ match e2 with
 129   [ o0 ⇒ o3 | o1 ⇒ o2 | o2 ⇒ o1 | o3 ⇒ o0
 130   | o4 ⇒ o7 | o5 ⇒ o6 | o6 ⇒ o5 | o7 ⇒ o4 ]
 131  | o4 ⇒ match e2 with
 132   [ o0 ⇒ o4 | o1 ⇒ o5 | o2 ⇒ o6 | o3 ⇒ o7
 133   | o4 ⇒ o0 | o5 ⇒ o1 | o6 ⇒ o2 | o7 ⇒ o3 ]
 134  | o5 ⇒ match e2 with
 135   [ o0 ⇒ o5 | o1 ⇒ o4 | o2 ⇒ o7 | o3 ⇒ o6
 136   | o4 ⇒ o1 | o5 ⇒ o0 | o6 ⇒ o3 | o7 ⇒ o2 ]
 137  | o6 ⇒ match e2 with
 138   [ o0 ⇒ o6 | o1 ⇒ o7 | o2 ⇒ o4 | o3 ⇒ o5
 139   | o4 ⇒ o2 | o5 ⇒ o3 | o6 ⇒ o0 | o7 ⇒ o1 ]
 140  | o7 ⇒ match e2 with
 141   [ o0 ⇒ o7 | o1 ⇒ o6 | o2 ⇒ o5 | o3 ⇒ o4
 142   | o4 ⇒ o3 | o5 ⇒ o2 | o6 ⇒ o1 | o7 ⇒ o0 ]
 143  ].
 144
 145 (* operatore predecessore *)
 146 ndefinition pred_oct ≝
 147 λn.match n with
 148  [ o0 ⇒ o7 | o1 ⇒ o0 | o2 ⇒ o1 | o3 ⇒ o2 | o4 ⇒ o3 | o5 ⇒ o4 | o6 ⇒ o5 | o7 ⇒ o6 ].
 149
 150 (* operatore successore *)
 151 ndefinition succ_oct ≝
 152 λn.match n with
 153  [ o0 ⇒ o1 | o1 ⇒ o2 | o2 ⇒ o3 | o3 ⇒ o4 | o4 ⇒ o5 | o5 ⇒ o6 | o6 ⇒ o7 | o7 ⇒ o0 ].
 154
 155 (* ottali ricorsivi *)
 156 ninductive rec_oct : oct → Type ≝
 157   oc_O : rec_oct o0
 158 | oc_S : ∀n.rec_oct n → rec_oct (succ_oct n).
 159
 160 (* ottali → ottali ricorsivi *)
 161 ndefinition oct_to_recoct ≝
 162 λn.match n return λx.rec_oct x with
 163  [ o0 ⇒ oc_O
 164  | o1 ⇒ oc_S ? oc_O
 165  | o2 ⇒ oc_S ? (oc_S ? oc_O)
 166  | o3 ⇒ oc_S ? (oc_S ? (oc_S ? oc_O))
 167  | o4 ⇒ oc_S ? (oc_S ? (oc_S ? (oc_S ? oc_O)))
 168  | o5 ⇒ oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? oc_O))))
 169  | o6 ⇒ oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? oc_O)))))
 170  | o7 ⇒ oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? oc_O))))))
 171  ].
 172
 173 ndefinition oct_destruct_aux ≝
 174 Πn1,n2:oct.ΠP:Prop.n1 = n2 →
 175  match eq_oct n1 n2 with [ true ⇒ P → P | false ⇒ P ].
 176
 177 ndefinition oct_destruct : oct_destruct_aux.
 178  #n1; #n2; #P; #H;
 179  nrewrite < H;
 180  nelim n1;
 181  nnormalize;
 182  napply (λx.x).
 183 nqed.
 184
 185 nlemma eq_to_eqoct : ∀n1,n2.n1 = n2 → eq_oct n1 n2 = true.
 186  #n1; #n2; #H;
 187  nrewrite > H;
 188  nelim n2;
 189  nnormalize;
 190  napply refl_eq.
 191 nqed.
 192
 193 nlemma neqoct_to_neq : ∀n1,n2.eq_oct n1 n2 = false → n1 ≠ n2.
 194  #n1; #n2; #H;
 195  napply (not_to_not (n1 = n2) (eq_oct n1 n2 = true) …);
 196  ##[ ##1: napply (eq_to_eqoct n1 n2)
 197  ##| ##2: napply (eqfalse_to_neqtrue … H)
 198  ##]
 199 nqed.
 200
 201 nlemma eqoct_to_eq : ∀n1,n2.eq_oct n1 n2 = true → n1 = n2.
 202  #n1; #n2;
 203  ncases n1;
 204  ncases n2;
 205  nnormalize;
 206  ##[ ##1,10,19,28,37,46,55,64: #H; napply refl_eq
 207  ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*)
 208  ##]
 209 nqed.
 210
 211 nlemma neq_to_neqoct : ∀n1,n2.n1 ≠ n2 → eq_oct n1 n2 = false.
 212  #n1; #n2; #H;
 213  napply (neqtrue_to_eqfalse (eq_oct n1 n2));
 214  napply (not_to_not (eq_oct n1 n2 = true) (n1 = n2) ? H);
 215  napply (eqoct_to_eq n1 n2).
 216 nqed.
 217
 218 nlemma decidable_oct : ∀x,y:oct.decidable (x = y).
 219  #x; #y; nnormalize;
 220  napply (or2_elim (eq_oct x y = true) (eq_oct x y = false) ? (decidable_bexpr ?));
 221  ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqoct_to_eq … H))
 222  ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqoct_to_neq … H))
 223  ##]
 224 nqed.
 225
 226 nlemma symmetric_eqoct : symmetricT oct bool eq_oct.
 227  #n1; #n2;
 228  napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_oct n1 n2));
 229  ##[ ##1: #H; nrewrite > H; napply refl_eq
 230  ##| ##2: #H; nrewrite > (neq_to_neqoct n1 n2 H);
 231           napply (symmetric_eq ? (eq_oct n2 n1) false);
 232           napply (neq_to_neqoct n2 n1 (symmetric_neq ? n1 n2 H))
 233  ##]
 234 nqed.
 235
 236 nlemma oct_is_comparable : comparable.
 237  @ oct
 238   ##[ napply o0
 239   ##| napply forall_oct
 240   ##| napply eq_oct
 241   ##| napply eqoct_to_eq
 242   ##| napply eq_to_eqoct
 243   ##| napply neqoct_to_neq
 244   ##| napply neq_to_neqoct
 245   ##| napply decidable_oct
 246   ##| napply symmetric_eqoct
 247   ##]
 248 nqed.
 249
 250 unification hint 0 ≔ ⊢ carr oct_is_comparable ≡ oct.