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