helm/software/matita/contribs/ng_assembly2/num/comp_num.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/comp_ext.ma".
  24 include "num/bool_lemmas.ma".
  25
  26 (* ******** *)
  27 (* COMPOSTI *)
  28 (* ******** *)
  29
  30 nrecord comp_num (T:Type) : Type ≝
  31  {
  32  cnH: T;
  33  cnL: T
  34  }.
  35
  36 (* operatore = *)
  37 ndefinition eq_cn ≝
  38 λT.λfeq:T → T → bool.
  39 λcn1,cn2:comp_num T.
  40  (feq (cnH ? cn1) (cnH ? cn2)) ⊗ (feq (cnL ? cn1) (cnL ? cn2)).
  41
  42 nlemma cn_destruct_1 :
  43 ∀T.∀x1,x2,y1,y2:T.
  44  mk_comp_num T x1 y1 = mk_comp_num T x2 y2 → x1 = x2.
  45  #T; #x1; #x2; #y1; #y2; #H;
  46  nchange with (match mk_comp_num ? x2 y2 with [ mk_comp_num a _ ⇒ x1 = a ]);
  47  nrewrite < H;
  48  nnormalize;
  49  napply refl_eq.
  50 nqed.
  51
  52 nlemma cn_destruct_2 :
  53 ∀T.∀x1,x2,y1,y2:T.
  54  mk_comp_num T x1 y1 = mk_comp_num T x2 y2 → y1 = y2.
  55  #T; #x1; #x2; #y1; #y2; #H;
  56  nchange with (match mk_comp_num ? x2 y2 with [ mk_comp_num _ b ⇒ y1 = b ]);
  57  nrewrite < H;
  58  nnormalize;
  59  napply refl_eq.
  60 nqed.
  61
  62 nlemma symmetric_eqcn :
  63 ∀T.∀feq:T → T → bool.
  64  (symmetricT T bool feq) →
  65  (symmetricT (comp_num T) bool (eq_cn T feq)).
  66  #T; #feq; #H;
  67  #b1; nelim b1; #e1; #e2;
  68  #b2; nelim b2; #e3; #e4;
  69  nchange with (((feq e1 e3)⊗(feq e2 e4)) = ((feq e3 e1)⊗(feq e4 e2)));
  70  nrewrite > (H e1 e3);
  71  nrewrite > (H e2 e4);
  72  napply refl_eq.
  73 nqed.
  74
  75 nlemma eqcn_to_eq :
  76 ∀T.∀feq:T → T → bool.
  77  (∀x,y:T.(feq x y = true) → (x = y)) →
  78  (∀b1,b2:comp_num T.
  79   ((eq_cn T feq b1 b2 = true) → (b1 = b2))).
  80  #T; #feq; #H; #b1; #b2;
  81  nelim b1; #e1; #e2;
  82  nelim b2; #e3; #e4;
  83  nchange in ⊢ (% → ?) with (((feq e1 e3)⊗(feq e2 e4)) = true);
  84  #H1;
  85  nrewrite < (H … (andb_true_true_l … H1));
  86  nrewrite < (H … (andb_true_true_r … H1));
  87  napply refl_eq.
  88 nqed.
  89
  90 nlemma eq_to_eqcn :
  91 ∀T.∀feq:T → T → bool.
  92  (∀x,y:T.(x = y) → (feq x y = true)) →
  93  (∀b1,b2:comp_num T.
  94   ((b1 = b2) → (eq_cn T feq b1 b2 = true))).
  95  #T; #feq; #H; #b1; #b2;
  96  nelim b1; #e1; #e2;
  97  nelim b2; #e3; #e4;
  98  #H1;
  99  nrewrite < (cn_destruct_1 … H1);
 100  nrewrite < (cn_destruct_2 … H1);
 101  nchange with (((feq e1 e1)⊗(feq e2 e2)) = true);
 102  nrewrite > (H e1 e1 (refl_eq …));
 103  nrewrite > (H e2 e2 (refl_eq …));
 104  nnormalize;
 105  napply refl_eq.
 106 nqed.
 107
 108 nlemma decidable_cn_aux1 :
 109 ∀T.∀e1,e2,e3,e4:T.e1 ≠ e3 → (mk_comp_num T e1 e2) ≠ (mk_comp_num T e3 e4).
 110  #T; #e1; #e2; #e3; #e4;
 111  nnormalize; #H; #H1;
 112  napply (H (cn_destruct_1 … H1)).
 113 nqed.
 114
 115 nlemma decidable_cn_aux2 :
 116 ∀T.∀e1,e2,e3,e4:T.e2 ≠ e4 → (mk_comp_num T e1 e2) ≠ (mk_comp_num T e3 e4).
 117  #T; #e1; #e2; #e3; #e4;
 118  nnormalize; #H; #H1;
 119  napply (H (cn_destruct_2 … H1)).
 120 nqed.
 121
 122 nlemma decidable_cn :
 123 ∀T.(∀x,y:T.decidable (x = y)) →
 124    (∀b1,b2:comp_num T.
 125     (decidable (b1 = b2))).
 126  #T; #H;
 127  #b1; nelim b1; #e1; #e2;
 128  #b2; nelim b2; #e3; #e4;
 129  nnormalize;
 130  napply (or2_elim (e1 = e3) (e1 ≠ e3) ? (H e1 e3) …);
 131  ##[ ##2: #H1; napply (or2_intro2 … (decidable_cn_aux1 T e1 e2 e3 e4 H1))
 132  ##| ##1: #H1; napply (or2_elim (e2 = e4) (e2 ≠ e4) ? (H e2 e4) …);
 133           ##[ ##2: #H2; napply (or2_intro2 … (decidable_cn_aux2 T e1 e2 e3 e4 H2))
 134           ##| ##1: #H2; nrewrite > H1; nrewrite > H2;
 135                         napply (or2_intro1 … (refl_eq ? (mk_comp_num T e3 e4)))
 136           ##]
 137  ##]
 138 nqed.
 139
 140 nlemma neqcn_to_neq :
 141 ∀T.∀feq:T → T → bool.
 142  (∀x,y:T.(feq x y = false) → (x ≠ y)) →
 143  (∀b1,b2:comp_num T.
 144   ((eq_cn T feq b1 b2 = false) → (b1 ≠ b2))).
 145  #T; #feq; #H; #b1; #b2;
 146  nelim b1; #e1; #e2;
 147  nelim b2; #e3; #e4;
 148  nchange with ((((feq e1 e3) ⊗ (feq e2 e4)) = false) → ?);
 149  #H1;
 150  napply (or2_elim ((feq e1 e3) = false) ((feq e2 e4) = false) ? (andb_false2 … H1) …);
 151  ##[ ##1: #H2; napply (decidable_cn_aux1 … (H … H2))
 152  ##| ##2: #H2; napply (decidable_cn_aux2 … (H … H2))
 153  ##]
 154 nqed.
 155
 156 nlemma cn_destruct :
 157 ∀T.(∀x,y:T.decidable (x = y)) →
 158    (∀e1,e2,e3,e4:T.
 159     ((mk_comp_num T e1 e2) ≠ (mk_comp_num T e3 e4)) →
 160     ((e1 ≠ e3) ∨ (e2 ≠ e4))).
 161  #T; #H; #e1; #e2; #e3; #e4;
 162  nnormalize; #H1;
 163  napply (or2_elim (e1 = e3) (e1 ≠ e3) ? (H e1 e3) …);
 164  ##[ ##2: #H2; napply (or2_intro1 … H2)
 165  ##| ##1: #H2; napply (or2_elim (e2 = e4) (e2 ≠ e4) ? (H e2 e4) …);
 166           ##[ ##2: #H3; napply (or2_intro2 … H3)
 167           ##| ##1: #H3; nrewrite > H2 in H1:(%);
 168                    nrewrite > H3;
 169                    #H1; nelim (H1 (refl_eq …))
 170           ##]
 171  ##]
 172 nqed.
 173
 174 nlemma neq_to_neqcn :
 175 ∀T.∀feq:T → T → bool.
 176  (∀x,y:T.(x ≠ y) → (feq x y = false)) →
 177  (∀x,y:T.decidable (x = y)) →
 178  (∀b1,b2:comp_num T.
 179   ((b1 ≠ b2) → (eq_cn T feq b1 b2 = false))).
 180  #T; #feq; #H; #H1; #b1; #b2;
 181  nelim b1; #e1; #e2;
 182  nelim b2; #e3; #e4;
 183  #H2; nchange with (((feq e1 e3) ⊗ (feq e2 e4)) = false);
 184  napply (or2_elim (e1 ≠ e3) (e2 ≠ e4) ? (cn_destruct T H1 e1 e2 e3 e4 … H2) …);
 185  ##[ ##1: #H3; nrewrite > (H … H3); nnormalize; napply refl_eq
 186  ##| ##2: #H3; nrewrite > (H … H3);
 187           nrewrite > (symmetric_andbool (feq e1 e3) false);
 188           nnormalize; napply refl_eq
 189  ##]
 190 nqed.
 191
 192 nlemma cn_is_comparable : comparable → comparable.
 193  #T; @ (comp_num T)
 194   (* zero *)
 195   ##[ napply (mk_comp_num ? (zeroc ?) (zeroc ?))
 196   (* forall *)
 197   ##| napply (λP.forallc T
 198               (λh.forallc T
 199                (λl.P (mk_comp_num ? h l))))
 200   (* eq *)
 201   ##| napply (eq_cn ? (eqc T))
 202   (* eqc_to_eq *)
 203   ##| napply (eqcn_to_eq … (eqc_to_eq T))
 204   (* eq_to_eqc *)
 205   ##| napply (eq_to_eqcn … (eq_to_eqc T))
 206   (* neqc_to_neq *)
 207   ##| napply (neqcn_to_neq … (neqc_to_neq T))
 208   (* neq_to_neqc *)
 209   ##| napply (neq_to_neqcn … (neq_to_neqc T));
 210       napply (decidable_c T)
 211   (* decidable_c *)
 212   ##| napply (decidable_cn … (decidable_c T))
 213   (* symmetric_eqc *)
 214   ##| napply (symmetric_eqcn … (symmetric_eqc T))
 215   ##]
 216 nqed.
 217
 218 nlemma cn_is_comparable_ext : comparable_ext → comparable_ext.
 219  #T; nelim T; #c;
 220  #ltc; #lec; #gtc; #gec; #andc; #orc; #xorc;
 221  #getMSBc; #setMSBc; #clrMSBc; #getLSBc; #setLSBc; #clrLSBc;
 222  #rcrc; #shrc; #rorc; #rclc; #shlc; #rolc; #notc;
 223  #plusc_dc_dc; #plusc_d_dc; #plusc_dc_d; #plusc_d_d; #plusc_dc_c; #plusc_d_c;
 224  #predc; #succc; #complc; #absc; #inrangec;
 225  napply (mk_comparable_ext);
 226   ##[ napply (cn_is_comparable c)
 227   (* lt *)
 228   ##| napply (λx,y.(ltc (cnH ? x) (cnH ? y)) ⊕
 229                    (((eqc c) (cnH ? x) (cnH ? y)) ⊗ (ltc (cnL ? x) (cnL ? y))))
 230   (* le *)
 231   ##| napply (λx,y.(ltc (cnH ? x) (cnH ? y)) ⊕
 232                     (((eqc c) (cnH ? x) (cnH ? y)) ⊗ (lec (cnL ? x) (cnL ? y))))
 233   (* gt *)
 234   ##| napply (λx,y.(gtc (cnH ? x) (cnH ? y)) ⊕
 235                    (((eqc c) (cnH ? x) (cnH ? y)) ⊗ (gtc (cnL ? x) (cnL ? y))))
 236   (* ge *)
 237   ##| napply (λx,y.(gtc (cnH ? x) (cnH ? y)) ⊕
 238                    (((eqc c) (cnH ? x) (cnH ? y)) ⊗ (gec (cnL ? x) (cnL ? y))))
 239   (* and *)
 240   ##| napply (λx,y.mk_comp_num ? (andc (cnH ? x) (cnH ? y))
 241                                  (andc (cnL ? x) (cnL ? y)))
 242   (* or *)
 243   ##| napply (λx,y.mk_comp_num ? (orc (cnH ? x) (cnH ? y))
 244                                  (orc (cnL ? x) (cnL ? y)))
 245   (* xor *)
 246   ##| napply (λx,y.mk_comp_num ? (xorc (cnH ? x) (cnH ? y))
 247                                  (xorc (cnL ? x) (cnL ? y)))
 248   (* getMSB *)
 249   ##| napply (λx.getMSBc (cnH ? x))
 250   (* setMSB *)
 251   ##| napply (λx.mk_comp_num ? (setMSBc (cnH ? x)) (cnL ? x))
 252   (* clrMSB *)
 253   ##| napply (λx.mk_comp_num ? (clrMSBc (cnH ? x)) (cnL ? x))
 254   (* getLSB *)
 255   ##| napply (λx.getLSBc (cnL ? x))
 256   (* setLSB *)
 257   ##| napply (λx.mk_comp_num ? (cnH ? x) (setLSBc (cnL ? x)))
 258   (* clrLSB *)
 259   ##| napply (λx.mk_comp_num ? (cnH ? x) (clrLSBc (cnL ? x)))
 260   (* rcr *)
 261   ##| napply (λcy,x.match rcrc cy (cnH ? x) with
 262               [ pair cy' cnh' ⇒ match rcrc cy' (cnL ? x) with
 263               [ pair cy'' cnl' ⇒ pair … cy'' (mk_comp_num ? cnh' cnl')]])
 264   (* shr *)
 265   ##| napply (λx.match shrc (cnH ? x) with
 266               [ pair cy' cnh' ⇒ match rcrc cy' (cnL ? x) with
 267               [ pair cy'' cnl' ⇒ pair … cy'' (mk_comp_num ? cnh' cnl')]])
 268   (* ror *)
 269   ##| napply (λx.match shrc (cnH ? x) with
 270               [ pair cy' cnh' ⇒ match rcrc cy' (cnL ? x) with
 271               [ pair cy'' cnl' ⇒ mk_comp_num ?
 272                (match cy'' with [ true ⇒ setMSBc
 273                                 | false ⇒ λh.h ] cnh') cnl']])
 274   (* rcl *)
 275   ##| napply (λcy,x.match rclc cy (cnL ? x) with
 276               [ pair cy' cnl' ⇒ match rclc cy' (cnH ? x) with
 277               [ pair cy'' cnh' ⇒ pair … cy'' (mk_comp_num ? cnh' cnl')]])
 278   (* shl *)
 279   ##| napply (λx.match shlc (cnL ? x) with
 280               [ pair cy' cnl' ⇒ match rclc cy' (cnH ? x) with
 281               [ pair cy'' cnh' ⇒ pair … cy'' (mk_comp_num ? cnh' cnl')]])
 282   (* rol *)
 283   ##| napply (λx.match shlc (cnL ? x) with
 284               [ pair cy' cnl' ⇒ match rclc cy' (cnH ? x) with
 285               [ pair cy'' cnh' ⇒ mk_comp_num ?
 286                cnh' (match cy'' with [ true ⇒ setLSBc
 287                                      | false ⇒ λh.h ] cnl')]])
 288   (* not *)
 289   ##| napply (λx.mk_comp_num ? (notc (cnH ? x)) (notc (cnL ? x)))
 290   (* plus_dc_dc *)
 291   ##| napply (λcy,x,y.match plusc_dc_dc cy (cnL ? x) (cnL ? y) with
 292               [ pair cy' cnl' ⇒ match plusc_dc_dc cy' (cnH ? x) (cnH ? y) with
 293               [ pair cy'' cnh' ⇒ pair … cy'' (mk_comp_num ? cnh' cnl')]])
 294   (* plus_d_dc *)
 295   ##| napply (λx,y.match plusc_d_dc (cnL ? x) (cnL ? y) with
 296               [ pair cy' cnl' ⇒ match plusc_dc_dc cy' (cnH ? x) (cnH ? y) with
 297               [ pair cy'' cnh' ⇒ pair … cy'' (mk_comp_num ? cnh' cnl')]])
 298   (* plus_dc_d *)
 299   ##| napply (λcy,x,y.match plusc_dc_dc cy (cnL ? x) (cnL ? y) with
 300               [ pair cy' cnl' ⇒ mk_comp_num ? (plusc_dc_d cy' (cnH ? x) (cnH ? y)) cnl'])
 301   (* plus_d_d *)
 302   ##| napply (λx,y.match plusc_d_dc (cnL ? x) (cnL ? y) with
 303               [ pair cy' cnl' ⇒ mk_comp_num ? (plusc_dc_d cy' (cnH ? x) (cnH ? y)) cnl'])
 304   (* plus_dc_c *)
 305   ##| napply (λcy,x,y.plusc_dc_c (plusc_dc_c cy (cnL ? x) (cnL ? y))
 306                                  (cnH ? x) (cnH ? y))
 307   (* plus_d_c *)
 308   ##| napply (λx,y.plusc_dc_c (plusc_d_c (cnL ? x) (cnL ? y))
 309                               (cnH ? x) (cnH ? y))
 310   (* pred *)
 311   ##| napply (λx.match (eqc c) (zeroc c) (cnL ? x) with
 312               [ true ⇒ mk_comp_num ? (predc (cnH ? x)) (predc (cnL ? x))
 313               | false ⇒ mk_comp_num ? (cnH ? x) (predc (cnL ? x)) ])
 314   (* succ *)
 315   ##| napply (λx.match (eqc c) (predc (zeroc c)) (cnL ? x) with
 316               [ true ⇒ mk_comp_num ? (succc (cnH ? x)) (succc (cnL ? x))
 317               | false ⇒ mk_comp_num ? (cnH ? x) (succc (cnL ? x)) ])
 318   (* compl *)
 319   ##| napply (λx.(match (eqc c) (zeroc c) (cnL ? x) with
 320                [ true ⇒ mk_comp_num ? (complc (cnH ? x)) (complc (cnL ? x))
 321               | false ⇒ mk_comp_num ? (notc (cnH ? x)) (complc (cnL ? x)) ]))
 322   (* abs *)
 323   ##| napply (λx.match getMSBc (cnH ? x) with
 324               [ true ⇒ match (eqc c) (zeroc c) (cnL ? x) with
 325                [ true ⇒ mk_comp_num ? (complc (cnH ? x)) (complc (cnL ? x))
 326                | false ⇒ mk_comp_num ? (notc (cnH ? x)) (complc (cnL ? x)) ]
 327               | false ⇒ x ])
 328   (* inrange *)
 329   ##| napply (λx,inf,sup.
 330               match (ltc (cnH ? inf) (cnH ? sup)) ⊕
 331                     (((eqc c) (cnH ? inf) (cnH ? sup)) ⊗ (lec (cnL ? inf) (cnL ? sup))) with
 332                [ true ⇒ and_bool | false ⇒ or_bool ]
 333               ((ltc (cnH ? inf) (cnH ? x)) ⊕
 334               (((eqc c) (cnH ? inf) (cnH ? x)) ⊗ (lec (cnL ? inf) (cnL ? x))))
 335               ((ltc (cnH ? x) (cnH ? sup)) ⊕
 336               (((eqc c) (cnH ? x) (cnH ? sup)) ⊗ (lec (cnL ? x) (cnL ? sup)))))
 337   ##]
 338 nqed.
 339
 340 ndefinition zeroc ≝ λx:comparable_ext.zeroc (comp_base x).
 341 ndefinition forallc ≝ λx:comparable_ext.forallc (comp_base x).
 342 ndefinition eqc ≝ λx:comparable_ext.eqc (comp_base x).
 343 ndefinition eqc_to_eq ≝ λx:comparable_ext.eqc_to_eq (comp_base x).
 344 ndefinition eq_to_eqc ≝ λx:comparable_ext.eq_to_eqc (comp_base x).
 345 ndefinition neqc_to_neq ≝ λx:comparable_ext.neqc_to_neq (comp_base x).
 346 ndefinition neq_to_neqc ≝ λx:comparable_ext.neq_to_neqc (comp_base x).
 347 ndefinition decidable_c ≝ λx:comparable_ext.decidable_c (comp_base x).
 348 ndefinition symmetric_eqc ≝ λx:comparable_ext.symmetric_eqc (comp_base x).
 349
 350
 351 unification hint 0 ≔ S: comparable;
 352          T ≟ (carr S),
 353          X ≟ (cn_is_comparable S)
 354  (*********************************************) ⊢
 355          carr X ≡ comp_num T.