matita/matita/contribs/ng_assembly/compiler/ast_type_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 (*   Sviluppo: 2008-2010                                                  *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "compiler/ast_type.ma".
  24 include "common/list_utility_lemmas.ma".
  25
  26 (* ************************* *)
  27 (* dimensioni degli elementi *)
  28 (* ************************* *)
  29
  30 (*
  31 ndefinition astbasetype_destruct_aux ≝
  32 Πb1,b2:ast_base_type.ΠP:Prop.b1 = b2 →
  33  match eq_astbasetype b1 b2 with [ true ⇒ P → P | false ⇒ P ].
  34
  35 ndefinition astbasetype_destruct : astbasetype_destruct_aux.
  36  #b1; #b2; #P; #H;
  37  nrewrite < H;
  38  nelim b1;
  39  nnormalize;
  40  napply (λx.x).
  41 nqed.
  42 *)
  43
  44 nlemma eq_to_eqastbasetype : ∀n1,n2.n1 = n2 → eq_astbasetype n1 n2 = true.
  45  #n1; #n2; #H;
  46  nrewrite > H;
  47  nelim n2;
  48  nnormalize;
  49  napply refl_eq.
  50 nqed.
  51
  52 nlemma neqastbasetype_to_neq : ∀n1,n2.eq_astbasetype n1 n2 = false → n1 ≠ n2.
  53  #n1; #n2; #H;
  54  napply (not_to_not (n1 = n2) (eq_astbasetype n1 n2 = true) …);
  55  ##[ ##1: napply (eq_to_eqastbasetype n1 n2)
  56  ##| ##2: napply (eqfalse_to_neqtrue … H)
  57  ##]
  58 nqed.
  59
  60 nlemma eqastbasetype_to_eq : ∀b1,b2.eq_astbasetype b1 b2 = true → b1 = b2.
  61  #b1; #b2; ncases b1; ncases b2; nnormalize;
  62  ##[ ##1,5,9: #H; napply refl_eq
  63  ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*)
  64  ##]
  65 nqed.
  66
  67 nlemma neq_to_neqastbasetype : ∀n1,n2.n1 ≠ n2 → eq_astbasetype n1 n2 = false.
  68  #n1; #n2; #H;
  69  napply (neqtrue_to_eqfalse (eq_astbasetype n1 n2));
  70  napply (not_to_not (eq_astbasetype n1 n2 = true) (n1 = n2) ? H);
  71  napply (eqastbasetype_to_eq n1 n2).
  72 nqed.
  73
  74 nlemma decidable_astbasetype : ∀x,y:ast_base_type.decidable (x = y).
  75  #x; #y; nnormalize;
  76  napply (or2_elim (eq_astbasetype x y = true) (eq_astbasetype x y = false) ? (decidable_bexpr ?));
  77  ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqastbasetype_to_eq … H))
  78  ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqastbasetype_to_neq … H))
  79  ##]
  80 nqed.
  81
  82 nlemma symmetric_eqastbasetype : symmetricT ast_base_type bool eq_astbasetype.
  83  #n1; #n2;
  84  napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_astbasetype n1 n2));
  85  ##[ ##1: #H; nrewrite > H; napply refl_eq
  86  ##| ##2: #H; nrewrite > (neq_to_neqastbasetype n1 n2 H);
  87           napply (symmetric_eq ? (eq_astbasetype n2 n1) false);
  88           napply (neq_to_neqastbasetype n2 n1 (symmetric_neq ? n1 n2 H))
  89  ##]
  90 nqed.
  91
  92 nlemma asttype_destruct_base_base : ∀b1,b2.AST_TYPE_BASE b1 = AST_TYPE_BASE b2 → b1 = b2.
  93  #b1; #b2; #H;
  94  nchange with (match AST_TYPE_BASE b2 with [ AST_TYPE_BASE a ⇒ b1 = a | _ ⇒ False ]);
  95  nrewrite < H;
  96  nnormalize;
  97  napply refl_eq.
  98 nqed.
  99
 100 nlemma asttype_destruct_array_array_1 : ∀x1,x2,y1,y2.AST_TYPE_ARRAY x1 y1 = AST_TYPE_ARRAY x2 y2 → x1 = x2.
 101  #x1; #x2; #y1; #y2; #H;
 102  nchange with (match AST_TYPE_ARRAY x2 y2 with [ AST_TYPE_ARRAY a _ ⇒ x1 = a | _ ⇒ False ]);
 103  nrewrite < H;
 104  nnormalize;
 105  napply refl_eq.
 106 nqed.
 107
 108 nlemma asttype_destruct_array_array_2 : ∀x1,x2,y1,y2.AST_TYPE_ARRAY x1 y1 = AST_TYPE_ARRAY x2 y2 → y1 = y2.
 109  #x1; #x2; #y1; #y2; #H;
 110  nchange with (match AST_TYPE_ARRAY x2 y2 with [ AST_TYPE_ARRAY _ b ⇒ y1 = b | _ ⇒ False ]);
 111  nrewrite < H;
 112  nnormalize;
 113  napply refl_eq.
 114 nqed.
 115
 116 nlemma asttype_destruct_struct_struct : ∀b1,b2.AST_TYPE_STRUCT b1 = AST_TYPE_STRUCT b2 → b1 = b2.
 117  #b1; #b2; #H;
 118  nchange with (match AST_TYPE_STRUCT b2 with [ AST_TYPE_STRUCT a ⇒ b1 = a | _ ⇒ False ]);
 119  nrewrite < H;
 120  nnormalize;
 121  napply refl_eq.
 122 nqed.
 123
 124 (*
 125 ndefinition asttype_destruct_aux ≝
 126 Πb1,b2:ast_type.ΠP:Prop.b1 = b2 →
 127  match eq_asttype b1 b2 with [ true ⇒ P → P | false ⇒ P ].
 128
 129 ndefinition asttype_destruct : asttype_destruct_aux.
 130  #b1; #b2; #P; #H;
 131  nrewrite > H;
 132  napply (ast_type_index … b2);
 133  ##[ ##1: #e; nchange with (match eq_astbasetype e e with [ true ⇒ P → P | false ⇒ P ]);
 134           nrewrite > (eq_to_eqastbasetype e e (refl_eq …));
 135           nnormalize; napply (λx.x);
 136  ##| ##2: #e; #n; #H; nchange with (match (eq_asttype e e)⊗(eq_nat n n) with [ true ⇒ P → P | false ⇒ P]);
 137           nrewrite > (eq_to_eqnat n n (refl_eq …));
 138           nrewrite > (symmetric_andbool (eq_asttype e e) true);
 139           nchange with (match eq_asttype e e with [ true ⇒ P → P | false ⇒ P]);
 140           napply H;
 141  ##| ##3: #e; #H; nchange with (match eq_asttype e e with [ true ⇒ P → P | false ⇒ P]);
 142           napply H;
 143  ##| ##4: #hh; #tt; #H;
 144           nchange with (match bfold_right_neList2 ?? tt tt with [ true ⇒ P → P | false ⇒ P ] →
 145                         match (eq_asttype hh hh)⊗(bfold_right_neList2 ?? tt tt) with [ true ⇒ P → P | false ⇒ P ]);
 146           #H1;
 147           ncases (eq_asttype hh hh) in H:(%) ⊢ %; #H;
 148           ncases (bfold_right_neList2 ? (λx1,x2.eq_asttype x1 x2) tt tt) in H1:(%) ⊢ %; #H1;
 149           ##[ ##1: nnormalize; napply (λx.x);
 150           ##| ##3: nnormalize in H:(%) ⊢ %; napply H
 151           ##| ##*: nnormalize in H1:(%) ⊢ %; napply H1
 152           ##]
 153  ##]
 154 nqed.
 155 *)
 156
 157 nlemma eq_to_eqasttype_aux1
 158  : ∀nl1,nl2.
 159   ((eq_asttype (AST_TYPE_STRUCT nl1) (AST_TYPE_STRUCT nl2)) = true) →
 160   ((bfold_right_neList2 ? (λx,y.eq_asttype x y) nl1 nl2) = true).
 161  #nl1; #nl2; #H;
 162  napply H.
 163 nqed.
 164
 165 nlemma eq_to_eqasttype : ∀t1,t2.t1 = t2 → eq_asttype t1 t2 = true.
 166  #t1;
 167  napply (ast_type_index … t1);
 168  ##[ ##1: #b1; #t2; ncases t2;
 169           ##[ ##1: #b2; #H; nrewrite > (asttype_destruct_base_base … H);
 170                    nchange with ((eq_astbasetype b2 b2) = true);
 171                    nrewrite > (eq_to_eqastbasetype b2 b2 (refl_eq …));
 172                    napply refl_eq
 173           ##| ##2: #st2; #n2; #H; ndestruct (*napply (asttype_destruct … H)*)
 174           ##| ##3: #nl2; #H; ndestruct (*napply (asttype_destruct … H)*)
 175           ##]
 176  ##| ##2: #st1; #n1; #H; #t2; ncases t2;
 177           ##[ ##2: #st2; #n2; #H1;  nchange with (((eq_asttype st1 st2)⊗(eq_nat n1 n2)) = true);
 178                    nrewrite > (H st2 (asttype_destruct_array_array_1 … H1));
 179                    nrewrite > (eq_to_eqnat n1 n2 (asttype_destruct_array_array_2 … H1));
 180                    nnormalize;
 181                    napply refl_eq
 182           ##| ##1: #b2; #H1; ndestruct (*napply (asttype_destruct … H1)*)
 183           ##| ##3: #nl2; #H1; ndestruct (*napply (asttype_destruct … H1)*)
 184           ##]
 185  ##| ##3: #hh1; #H; #t2; ncases t2;
 186           ##[ ##3: #nl2; ncases nl2;
 187                    ##[ ##1: #hh2; #H1; nchange with ((eq_asttype hh1 hh2) = true);
 188                             nrewrite > (H hh2 (nelist_destruct_nil_nil ? hh1 hh2 (asttype_destruct_struct_struct … H1)));
 189                             napply refl_eq
 190                    ##| ##2: #hh2; #ll2; #H1;
 191                             (* !!! ndestruct non va *)
 192                             nelim (nelist_destruct_nil_cons ? hh1 hh2 ll2 (asttype_destruct_struct_struct … H1))
 193                    ##]
 194           ##| ##1: #b2; #H1; ndestruct (*napply (asttype_destruct … H1)*)
 195           ##| ##2: #st2; #n2; #H1; ndestruct (*napply (asttype_destruct … H1)*)
 196           ##]
 197  ##| ##4: #hh1; #ll1; #H; #H1; #t2; ncases t2;
 198           ##[ ##3: #nl2; ncases nl2;
 199                    ##[ ##1: #hh2; #H2;
 200                             (* !!! ndestruct non va *)
 201                             nelim (nelist_destruct_cons_nil ? hh1 hh2 ll1 (asttype_destruct_struct_struct … H2))
 202                    ##| ##2: #hh2; #ll2; #H2; nchange with (((eq_asttype hh1 hh2)⊗(bfold_right_neList2 ? (λx,y.eq_asttype x y) ll1 ll2)) = true);
 203                             nrewrite > (H hh2 (nelist_destruct_cons_cons_1 … (asttype_destruct_struct_struct … H2)));
 204                             nrewrite > (eq_to_eqasttype_aux1 ll1 ll2 (H1 (AST_TYPE_STRUCT ll2) ?));
 205                             ##[ ##1: nnormalize; napply refl_eq
 206                             ##| ##2: nrewrite > (nelist_destruct_cons_cons_2 … (asttype_destruct_struct_struct … H2));
 207                                      napply refl_eq
 208                             ##]
 209                    ##]
 210           ##| ##1: #b2; #H2; ndestruct (*napply (asttype_destruct … H2)*)
 211           ##| ##2: #st2; #n2; #H2; ndestruct (*napply (asttype_destruct … H2)*)
 212           ##]
 213  ##]
 214 nqed.
 215
 216 nlemma neqasttype_to_neq : ∀n1,n2.eq_asttype n1 n2 = false → n1 ≠ n2.
 217  #n1; #n2; #H;
 218  napply (not_to_not (n1 = n2) (eq_asttype n1 n2 = true) …);
 219  ##[ ##1: napply (eq_to_eqasttype n1 n2)
 220  ##| ##2: napply (eqfalse_to_neqtrue … H)
 221  ##]
 222 nqed.
 223
 224 nlemma eqasttype_to_eq : ∀t1,t2.eq_asttype t1 t2 = true → t1 = t2.
 225  #t1;
 226  napply (ast_type_index … t1);
 227  ##[ ##1: #b1; #t2; ncases t2;
 228           ##[ ##1: #b2; #H; nchange in H:(%) with ((eq_astbasetype b1 b2) = true);
 229                    nrewrite > (eqastbasetype_to_eq b1 b2 H);
 230                    napply refl_eq
 231           ##| ##2: #st2; #n2; nnormalize; #H; ndestruct (*napply (bool_destruct … H)*)
 232           ##| ##3: #nl2; nnormalize; #H; ndestruct (*napply (bool_destruct … H)*)
 233           ##]
 234  ##| ##2: #st1; #n1; #H; #t2; ncases t2;
 235           ##[ ##2: #st2; #n2; #H1; nchange in H1:(%) with (((eq_asttype st1 st2)⊗(eq_nat n1 n2)) = true);
 236                    nrewrite > (H st2 (andb_true_true_l … H1));
 237                    nrewrite > (eqnat_to_eq n1 n2 (andb_true_true_r … H1));
 238                    napply refl_eq
 239           ##| ##1: #b2; nnormalize; #H1; ndestruct (*napply (bool_destruct … H1)*)
 240           ##| ##3: #nl2; nnormalize; #H1; ndestruct (*napply (bool_destruct … H1)*)
 241           ##]
 242  ##| ##3: #hh1; #H; #t2; ncases t2;
 243           ##[ ##3: #nl2; ncases nl2;
 244                    ##[ ##1: #hh2; #H1; nchange in H1:(%) with ((eq_asttype hh1 hh2) = true);
 245                             nrewrite > (H hh2 H1);
 246                             napply refl_eq
 247                    ##| ##2: #hh2; #ll2; nnormalize; #H1; ndestruct (*napply (bool_destruct … H1)*)
 248                    ##]
 249           ##| ##1: #b2; nnormalize; #H1; ndestruct (*napply (bool_destruct … H1)*)
 250           ##| ##2: #st2; #n2; nnormalize; #H1; ndestruct (*napply (bool_destruct … H1)*)
 251           ##]
 252  ##| ##4: #hh1; #ll1; #H; #H1; #t2; ncases t2;
 253           ##[ ##3: #nl2; ncases nl2;
 254                    ##[ ##1: #hh2; nnormalize; #H2; ndestruct (*napply (bool_destruct … H2)*)
 255                    ##| ##2: #hh2; #ll2; #H2; nchange in H2:(%) with (((eq_asttype hh1 hh2)⊗(bfold_right_neList2 ? (λx,y.eq_asttype x y) ll1 ll2)) = true);
 256                             nrewrite > (H hh2 (andb_true_true_l … H2));
 257                             nrewrite > (asttype_destruct_struct_struct ll1 ll2 (H1 (AST_TYPE_STRUCT ll2) (andb_true_true_r … H2)));
 258                             napply refl_eq
 259                    ##]
 260           ##| ##1: #b2; nnormalize; #H2; ndestruct (*napply (bool_destruct … H2)*)
 261           ##| ##2: #st2; #n2; nnormalize; #H2; ndestruct (*napply (bool_destruct … H2)*)
 262           ##]
 263  ##]
 264 nqed.
 265
 266 nlemma neq_to_neqasttype : ∀n1,n2.n1 ≠ n2 → eq_asttype n1 n2 = false.
 267  #n1; #n2; #H;
 268  napply (neqtrue_to_eqfalse (eq_asttype n1 n2));
 269  napply (not_to_not (eq_asttype n1 n2 = true) (n1 = n2) ? H);
 270  napply (eqasttype_to_eq n1 n2).
 271 nqed.
 272
 273 nlemma decidable_asttype : ∀x,y:ast_type.decidable (x = y).
 274  #x; #y; nnormalize;
 275  napply (or2_elim (eq_asttype x y = true) (eq_asttype x y = false) ? (decidable_bexpr ?));
 276  ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqasttype_to_eq … H))
 277  ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqasttype_to_neq … H))
 278  ##]
 279 nqed.
 280
 281 nlemma symmetric_eqasttype : symmetricT ast_type bool eq_asttype.
 282  #n1; #n2;
 283  napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_asttype n1 n2));
 284  ##[ ##1: #H; nrewrite > H; napply refl_eq
 285  ##| ##2: #H; nrewrite > (neq_to_neqasttype n1 n2 H);
 286           napply (symmetric_eq ? (eq_asttype n2 n1) false);
 287           napply (neq_to_neqasttype n2 n1 (symmetric_neq ? n1 n2 H))
 288  ##]
 289 nqed.
 290
 291 nlemma isbastbasetype_to_isastbasetype : ∀ast.isb_ast_base_type ast = true → is_ast_base_type ast.
 292  #ast;
 293  ncases ast;
 294  nnormalize;
 295  ##[ ##1: #t; #H; napply I
 296  ##| ##2: #t; #n; #H; ndestruct (*napply (bool_destruct … H)*)
 297  ##| ##3: #t; #H; ndestruct (*napply (bool_destruct … H)*)
 298  ##]
 299 nqed.
 300
 301 nlemma isntbastbasetype_to_isntastbasetype : ∀ast.isntb_ast_base_type ast = true → isnt_ast_base_type ast.
 302  #ast;
 303  ncases ast;
 304  nnormalize;
 305  ##[ ##1: #t; #H; ndestruct (*napply (bool_destruct … H)*)
 306  ##| ##2: #t; #n; #H; napply I
 307  ##| ##3: #l; #H; napply I
 308  ##]
 309 nqed.