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: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Ultima modifica: 05/08/2009                                          *)
  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 ndefinition astbasetype_destruct_aux ≝
  31 Πb1,b2:ast_base_type.ΠP:Prop.b1 = b2 →
  32  match eq_astbasetype b1 b2 with [ true ⇒ P → P | false ⇒ P ].
  33
  34 ndefinition astbasetype_destruct : astbasetype_destruct_aux.
  35  #b1; #b2; #P; #H;
  36  nrewrite < H;
  37  nelim b1;
  38  nnormalize;
  39  napply (λx.x).
  40 nqed.
  41
  42 nlemma symmetric_eqastbasetype : symmetricT ast_base_type bool eq_astbasetype.
  43  #b1; #b2; ncases b1; ncases b2; nnormalize; napply refl_eq. nqed.
  44
  45 nlemma eqastbasetype_to_eq : ∀b1,b2.eq_astbasetype b1 b2 = true → b1 = b2.
  46  #b1; #b2; ncases b1; ncases b2; nnormalize;
  47  ##[ ##1,5,9: #H; napply refl_eq
  48  ##| ##*: #H; napply (bool_destruct … H)
  49  ##]
  50 nqed.
  51
  52 nlemma eq_to_eqastbasetype : ∀b1,b2.b1 = b2 → eq_astbasetype b1 b2 = true.
  53  #b1; #b2; ncases b1; ncases b2; nnormalize;
  54  ##[ ##1,5,9: #H; napply refl_eq
  55  ##| ##*: #H; napply (astbasetype_destruct … H)
  56  ##]
  57 nqed.
  58
  59 nlemma decidable_astbasetype : ∀x,y:ast_base_type.decidable (x = y).
  60  #x; #y;
  61  nnormalize;
  62  nelim x;
  63  nelim y;
  64  ##[ ##1,5,9: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
  65  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …);
  66           nnormalize; #H;
  67           napply False_ind;
  68           napply (astbasetype_destruct … H)
  69  ##]
  70 nqed.
  71
  72 nlemma neqastbasetype_to_neq : ∀b1,b2.(eq_astbasetype b1 b2 = false) → (b1 ≠ b2).
  73  #b1; #b2;
  74  ncases b1;
  75  ncases b2;
  76  nnormalize;
  77  ##[ ##1,5,9: #H; napply (bool_destruct … H)
  78  ##| ##*: #H; #H1; napply (astbasetype_destruct … H1)
  79  ##]
  80 nqed.
  81
  82 nlemma neq_to_neqastbasetype : ∀b1,b2.b1 ≠ b2 → eq_astbasetype b1 b2 = false.
  83  #b1; #b2;
  84  ncases b1;
  85  ncases b2;
  86  nnormalize;
  87  ##[ ##1,5,9: #H; nelim (H (refl_eq …))
  88  ##| ##*: #H; napply refl_eq
  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 ndefinition asttype_destruct_aux ≝
 125 Πb1,b2:ast_type.ΠP:Prop.b1 = b2 →
 126  match eq_asttype b1 b2 with [ true ⇒ P → P | false ⇒ P ].
 127
 128 ndefinition asttype_destruct : asttype_destruct_aux.
 129  #b1; #b2; #P; #H;
 130  nrewrite > H;
 131  napply (ast_type_index … b2);
 132  ##[ ##1: #e; nchange with (match eq_astbasetype e e with [ true ⇒ P → P | false ⇒ P ]);
 133           nrewrite > (eq_to_eqastbasetype e e (refl_eq …));
 134           nnormalize; napply (λx.x);
 135  ##| ##2: #e; #n; #H; nchange with (match (eq_asttype e e)⊗(eq_nat n n) with [ true ⇒ P → P | false ⇒ P]);
 136           nrewrite > (eq_to_eqnat n n (refl_eq …));
 137           nrewrite > (symmetric_andbool (eq_asttype e e) true);
 138           nchange with (match eq_asttype e e with [ true ⇒ P → P | false ⇒ P]);
 139           napply H;
 140  ##| ##3: #e; #H; nchange with (match eq_asttype e e with [ true ⇒ P → P | false ⇒ P]);
 141           napply H;
 142  ##| ##4: #hh; #tt; #H;
 143           nchange with (match bfold_right_neList2 ?? tt tt with [ true ⇒ P → P | false ⇒ P ] →
 144                         match (eq_asttype hh hh)⊗(bfold_right_neList2 ?? tt tt) with [ true ⇒ P → P | false ⇒ P ]);
 145           #H1;
 146           ncases (eq_asttype hh hh) in H:(%) ⊢ %; #H;
 147           ncases (bfold_right_neList2 ? (λx1,x2.eq_asttype x1 x2) tt tt) in H1:(%) ⊢ %; #H1;
 148           ##[ ##1: nnormalize; napply (λx.x);
 149           ##| ##3: nnormalize in H:(%) ⊢ %; napply H
 150           ##| ##*: nnormalize in H1:(%) ⊢ %; napply H1
 151           ##]
 152  ##]
 153 nqed.
 154
 155 nlemma symmetric_eqasttype_aux1
 156  : ∀nl1,nl2.
 157   (eq_asttype (AST_TYPE_STRUCT nl1) (AST_TYPE_STRUCT nl2)) = (eq_asttype (AST_TYPE_STRUCT nl2) (AST_TYPE_STRUCT nl1)) →
 158   (bfold_right_neList2 ? (λx,y.eq_asttype x y) nl1 nl2) = (bfold_right_neList2 ? (λx,y.eq_asttype x y) nl2 nl1).
 159  #nl1; #nl2; #H;
 160  napply H.
 161 nqed.
 162
 163 nlemma symmetric_eqasttype : symmetricT ast_type bool eq_asttype.
 164  #t1; napply (ast_type_index … t1);
 165  ##[ ##1: #b1; #t2; ncases t2;
 166           ##[ ##1: #b2; nchange with ((eq_astbasetype b1 b2) = (eq_astbasetype b2 b1));
 167                    nrewrite > (symmetric_eqastbasetype b1 b2);
 168                    napply refl_eq
 169           ##| ##2: #st2; #n2; nnormalize; napply refl_eq
 170           ##| ##3: #nl2; nnormalize; napply refl_eq
 171           ##]
 172  ##| ##2: #st1; #n1; #H; #t2; ncases t2;
 173           ##[ ##2: #st2; #n2; nchange with (((eq_asttype st1 st2)⊗(eq_nat n1 n2)) = ((eq_asttype st2 st1)⊗(eq_nat n2 n1)));
 174                    nrewrite > (symmetric_eqnat n1 n2);
 175                    nrewrite > (H st2);
 176                    napply refl_eq
 177           ##| ##1: #b2; nnormalize; napply refl_eq
 178           ##| ##3: #nl2; nnormalize; napply refl_eq
 179           ##]
 180  ##| ##3: #hh1; #H; #t2; ncases t2;
 181           ##[ ##3: #nl2; ncases nl2;
 182                    ##[ ##1: #hh2; nchange with ((eq_asttype hh1 hh2) = (eq_asttype hh2 hh1));
 183                             nrewrite > (H hh2);
 184                             napply refl_eq
 185                    ##| ##2: #hh2; #ll2; nnormalize; napply refl_eq
 186                    ##]
 187           ##| ##1: #b2; nnormalize; napply refl_eq
 188           ##| ##2: #st2; #n2; nnormalize; napply refl_eq
 189           ##]
 190  ##| ##4: #hh1; #ll1; #H; #H1; #t2; ncases t2;
 191           ##[ ##3: #nl2; ncases nl2;
 192                    ##[ ##1: #hh2; nnormalize; napply refl_eq
 193                    ##| ##2: #hh2; #ll2; nnormalize;
 194                             nrewrite > (H hh2);
 195                             nrewrite > (symmetric_eqasttype_aux1 ll1 ll2 (H1 (AST_TYPE_STRUCT ll2)));
 196                             napply refl_eq
 197                    ##]
 198           ##| ##1: #b2; nnormalize; napply refl_eq
 199           ##| ##2: #st2; #n2; nnormalize; napply refl_eq
 200           ##]
 201  ##]
 202 nqed.
 203
 204 nlemma eqasttype_to_eq : ∀t1,t2.eq_asttype t1 t2 = true → t1 = t2.
 205  #t1;
 206  napply (ast_type_index … t1);
 207  ##[ ##1: #b1; #t2; ncases t2;
 208           ##[ ##1: #b2; #H; nchange in H:(%) with ((eq_astbasetype b1 b2) = true);
 209                    nrewrite > (eqastbasetype_to_eq b1 b2 H);
 210                    napply refl_eq
 211           ##| ##2: #st2; #n2; nnormalize; #H; napply (bool_destruct … H)
 212           ##| ##3: #nl2; nnormalize; #H; napply (bool_destruct … H)
 213           ##]
 214  ##| ##2: #st1; #n1; #H; #t2; ncases t2;
 215           ##[ ##2: #st2; #n2; #H1; nchange in H1:(%) with (((eq_asttype st1 st2)⊗(eq_nat n1 n2)) = true);
 216                    nrewrite > (H st2 (andb_true_true_l … H1));
 217                    nrewrite > (eqnat_to_eq n1 n2 (andb_true_true_r … H1));
 218                    napply refl_eq
 219           ##| ##1: #b2; nnormalize; #H1; napply (bool_destruct … H1)
 220           ##| ##3: #nl2; nnormalize; #H1; napply (bool_destruct … H1)
 221           ##]
 222  ##| ##3: #hh1; #H; #t2; ncases t2;
 223           ##[ ##3: #nl2; ncases nl2;
 224                    ##[ ##1: #hh2; #H1; nchange in H1:(%) with ((eq_asttype hh1 hh2) = true);
 225                             nrewrite > (H hh2 H1);
 226                             napply refl_eq
 227                    ##| ##2: #hh2; #ll2; nnormalize; #H1; napply (bool_destruct … H1)
 228                    ##]
 229           ##| ##1: #b2; nnormalize; #H1; napply (bool_destruct … H1)
 230           ##| ##2: #st2; #n2; nnormalize; #H1; napply (bool_destruct … H1)
 231           ##]
 232  ##| ##4: #hh1; #ll1; #H; #H1; #t2; ncases t2;
 233           ##[ ##3: #nl2; ncases nl2;
 234                    ##[ ##1: #hh2; nnormalize; #H2; napply (bool_destruct … H2)
 235                    ##| ##2: #hh2; #ll2; #H2; nchange in H2:(%) with (((eq_asttype hh1 hh2)⊗(bfold_right_neList2 ? (λx,y.eq_asttype x y) ll1 ll2)) = true);
 236                             nrewrite > (H hh2 (andb_true_true_l … H2));
 237                             nrewrite > (asttype_destruct_struct_struct ll1 ll2 (H1 (AST_TYPE_STRUCT ll2) (andb_true_true_r … H2)));
 238                             napply refl_eq
 239                    ##]
 240           ##| ##1: #b2; nnormalize; #H2; napply (bool_destruct … H2)
 241           ##| ##2: #st2; #n2; nnormalize; #H2; napply (bool_destruct … H2)
 242           ##]
 243  ##]
 244 nqed.
 245
 246 nlemma eq_to_eqasttype_aux1
 247  : ∀nl1,nl2.
 248   ((eq_asttype (AST_TYPE_STRUCT nl1) (AST_TYPE_STRUCT nl2)) = true) →
 249   ((bfold_right_neList2 ? (λx,y.eq_asttype x y) nl1 nl2) = true).
 250  #nl1; #nl2; #H;
 251  napply H.
 252 nqed.
 253
 254 nlemma eq_to_eqasttype : ∀t1,t2.t1 = t2 → eq_asttype t1 t2 = true.
 255  #t1;
 256  napply (ast_type_index … t1);
 257  ##[ ##1: #b1; #t2; ncases t2;
 258           ##[ ##1: #b2; #H; nrewrite > (asttype_destruct_base_base … H);
 259                    nchange with ((eq_astbasetype b2 b2) = true);
 260                    nrewrite > (eq_to_eqastbasetype b2 b2 (refl_eq …));
 261                    napply refl_eq
 262           ##| ##2: #st2; #n2; #H; napply (asttype_destruct … H)
 263           ##| ##3: #nl2; #H; napply (asttype_destruct … H)
 264           ##]
 265  ##| ##2: #st1; #n1; #H; #t2; ncases t2;
 266           ##[ ##2: #st2; #n2; #H1;  nchange with (((eq_asttype st1 st2)⊗(eq_nat n1 n2)) = true);
 267                    nrewrite > (H st2 (asttype_destruct_array_array_1 … H1));
 268                    nrewrite > (eq_to_eqnat n1 n2 (asttype_destruct_array_array_2 … H1));
 269                    nnormalize;
 270                    napply refl_eq
 271           ##| ##1: #b2; #H1; napply (asttype_destruct … H1)
 272           ##| ##3: #nl2; #H1; napply (asttype_destruct … H1)
 273           ##]
 274  ##| ##3: #hh1; #H; #t2; ncases t2;
 275           ##[ ##3: #nl2; ncases nl2;
 276                    ##[ ##1: #hh2; #H1; nchange with ((eq_asttype hh1 hh2) = true);
 277                             nrewrite > (H hh2 (nelist_destruct_nil_nil ? hh1 hh2 (asttype_destruct_struct_struct … H1)));
 278                             napply refl_eq
 279                    ##| ##2: #hh2; #ll2; #H1; nelim (nelist_destruct_nil_cons ? hh1 hh2 ll2 (asttype_destruct_struct_struct … H1))
 280                    ##]
 281           ##| ##1: #b2; #H1; napply (asttype_destruct … H1)
 282           ##| ##2: #st2; #n2; #H1; napply (asttype_destruct … H1)
 283           ##]
 284  ##| ##4: #hh1; #ll1; #H; #H1; #t2; ncases t2;
 285           ##[ ##3: #nl2; ncases nl2;
 286                    ##[ ##1: #hh2; #H2; nelim (nelist_destruct_cons_nil ? hh1 hh2 ll1 (asttype_destruct_struct_struct … H2))
 287                    ##| ##2: #hh2; #ll2; #H2; nchange with (((eq_asttype hh1 hh2)⊗(bfold_right_neList2 ? (λx,y.eq_asttype x y) ll1 ll2)) = true);
 288                             nrewrite > (H hh2 (nelist_destruct_cons_cons_1 … (asttype_destruct_struct_struct … H2)));
 289                             nrewrite > (eq_to_eqasttype_aux1 ll1 ll2 (H1 (AST_TYPE_STRUCT ll2) ?));
 290                             ##[ ##1: nnormalize; napply refl_eq
 291                             ##| ##2: nrewrite > (nelist_destruct_cons_cons_2 … (asttype_destruct_struct_struct … H2));
 292                                      napply refl_eq
 293                             ##]
 294                    ##]
 295           ##| ##1: #b2; #H2; napply (asttype_destruct … H2)
 296           ##| ##2: #st2; #n2; #H2; napply (asttype_destruct … H2)
 297           ##]
 298  ##]
 299 nqed.
 300
 301 nlemma decidable_asttype : ∀x,y:ast_type.decidable (x = y).
 302  #x;
 303  napply (ast_type_index … x);
 304  ##[ ##1: #b1; #y; ncases y;
 305           ##[ ##1: #b2; nnormalize; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_astbasetype b1 b2));
 306                    ##[ ##1: #H; nrewrite > H; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
 307                    ##| ##2: #H; napply (or2_intro2 (? = ?) (? ≠ ?) …);
 308                             nnormalize;  #H1; napply (H (asttype_destruct_base_base … H1))
 309                    ##]
 310           ##| ##2: #b2; #n2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) …);
 311                    nnormalize; #H; napply (asttype_destruct … H)
 312           ##| ##3: #n2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) …);
 313                    nnormalize; #H; napply (asttype_destruct … H)
 314           ##]
 315  ##| ##2: #b1; #n1; #H; #y; ncases y;
 316           ##[ ##2: #b2; #n2; nnormalize; napply (or2_elim (? = ?) (? ≠ ?) ? (H b2));
 317                    ##[ ##2: #H1; napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize;
 318                             #H2; napply (H1 (asttype_destruct_array_array_1 … H2))
 319                    ##| ##1: #H1; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_nat n1 n2));
 320                             ##[ ##2: #H2; napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize;
 321                                      #H3; napply (H2 (asttype_destruct_array_array_2 … H3))
 322                             ##| ##1: #H2; nrewrite > H1; nrewrite > H2;
 323                                           napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
 324                             ##]
 325                    ##]
 326           ##| ##1: #b2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) …);
 327                    nnormalize; #H1; napply (asttype_destruct … H1)
 328           ##| ##3: #n2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) …);
 329                    nnormalize; #H1; napply (asttype_destruct … H1)
 330           ##]
 331  ##| ##3: #hh1; #H; #y; ncases y;
 332           ##[ ##3: #n2; ncases n2;
 333                    ##[ ##1: #hh2; nnormalize; napply (or2_elim (? = ?) (? ≠ ?) ? (H hh2));
 334                             ##[ ##2: #H1; napply (or2_intro2 (? = ?) (? ≠ ?) …);
 335                                      nnormalize; #H2;
 336                                      napply (H1 (nelist_destruct_nil_nil … (asttype_destruct_struct_struct … H2)))
 337                             ##| ##1: #H1; nrewrite > H1; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
 338                             ##]
 339                    ##| ##2: #hh2; #tt2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) …);
 340                             nnormalize; #H1; napply (nelist_destruct_nil_cons ast_type … (asttype_destruct_struct_struct … H1))
 341                    ##]
 342           ##| ##1: #b2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) …);
 343                    nnormalize; #H1; napply (asttype_destruct … H1)
 344           ##| ##2: #b2; #n2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) …);
 345                    nnormalize; #H1; napply (asttype_destruct … H1)
 346           ##]
 347  ##| ##4: #hh1; #tt1; #H; #H1; #y; ncases y;
 348           ##[ ##3: #n2; ncases n2;
 349                    ##[ ##2: #hh2; #tt2; nnormalize; napply (or2_elim (? = ?) (? ≠ ?) ? (H hh2));
 350                             ##[ ##2: #H2; napply (or2_intro2 (? = ?) (? ≠ ?) …);
 351                                      nnormalize; #H3; napply (H2 (nelist_destruct_cons_cons_1 ast_type … (asttype_destruct_struct_struct … H3)))
 352                             ##| ##1: #H2; napply (or2_elim (? = ?) (? ≠ ?) ? (H1 (AST_TYPE_STRUCT tt2)));
 353                                      ##[ ##2: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) …);
 354                                               nnormalize; #H4; napply H3;
 355                                               nrewrite > (nelist_destruct_cons_cons_2 ast_type … (asttype_destruct_struct_struct … H4));
 356                                               napply refl_eq
 357                                      ##| ##1: #H3; nrewrite > H2; nrewrite > (asttype_destruct_struct_struct … H3);
 358                                                    napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
 359                                      ##]
 360                             ##]
 361                    ##| ##1: #hh2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) …);
 362                             nnormalize; #H2; napply (nelist_destruct_cons_nil ast_type … (asttype_destruct_struct_struct … H2))
 363                    ##]
 364           ##| ##1: #b2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) …);
 365                    nnormalize; #H2; napply (asttype_destruct … H2)
 366           ##| ##2: #b2; #n2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) …);
 367                    nnormalize; #H2; napply (asttype_destruct … H2)
 368           ##]
 369  ##]
 370 nqed.
 371
 372 nlemma neqasttype_to_neq : ∀t1,t2.eq_asttype t1 t2 = false → t1 ≠ t2.
 373  #t1;
 374  napply (ast_type_index … t1);
 375  ##[ ##1: #b1; #t2; ncases t2;
 376           ##[ ##1: #b2; nchange with ((eq_astbasetype b1 b2 = false) → ?); #H;
 377                    nnormalize; #H1; napply (neqastbasetype_to_neq b1 b2 H);
 378                    napply (asttype_destruct_base_base … H1)
 379           ##| ##2: #b2; #n2; nnormalize; #H; #H1; napply (asttype_destruct … H1)
 380           ##| ##3: #n2; nnormalize; #H; #H1; napply (asttype_destruct … H1)
 381           ##]
 382  ##| ##2: #b1; #n1; #H; #t2; ncases t2;
 383           ##[ ##2: #b2; #n2; nchange with ((((eq_asttype b1 b2)⊗(eq_nat n1 n2)) = false) → ?); #H1;
 384                    napply (or2_elim ??? (andb_false2 … H1));
 385                    ##[ ##1: #H2; nnormalize; #H3; napply (H b2 H2); napply (asttype_destruct_array_array_1 … H3)
 386                    ##| ##2: #H2; nnormalize; #H3; napply (neqnat_to_neq n1 n2 H2); napply (asttype_destruct_array_array_2 … H3)
 387                    ##]
 388           ##| ##1: #b2; nnormalize; #H1; #H2; napply (asttype_destruct … H2)
 389           ##| ##3: #n2; nnormalize; #H1; #H2; napply (asttype_destruct … H2)
 390           ##]
 391  ##| ##3: #hh1; #H; #t2; ncases t2;
 392           ##[ ##3: #n2; ncases n2;
 393                    ##[ ##1: #hh2; nchange with ((eq_asttype hh1 hh2 = false) → ?); #H1;
 394                             nnormalize; #H2; napply (H hh2 H1);
 395                             napply (nelist_destruct_nil_nil ast_type … (asttype_destruct_struct_struct … H2))
 396                    ##| ##2: #hh2; #tt2; nnormalize; #H1; #H2;
 397                             napply (nelist_destruct_nil_cons ast_type … (asttype_destruct_struct_struct … H2))
 398                    ##]
 399           ##| ##1: #b2; nnormalize; #H1; #H2; napply (asttype_destruct … H2)
 400           ##| ##2: #b2; #n2; nnormalize; #H1; #H2; napply (asttype_destruct … H2)
 401           ##]
 402  ##| ##4: #hh1; #tt1; #H; #H1; #t2; ncases t2;
 403           ##[ ##3: #n2; ncases n2;
 404                    ##[ ##2: #hh2; #tt2; nchange with ((((eq_asttype hh1 hh2)⊗(bfold_right_neList2 ?? tt1 tt2)) = false) → ?);
 405                             #H2; napply (or2_elim ??? (andb_false2 … H2));
 406                             ##[ ##1: #H3; nnormalize; #H4; napply (H hh2 H3);
 407                                      napply (nelist_destruct_cons_cons_1 ast_type … (asttype_destruct_struct_struct … H4))
 408                             ##| ##2: #H3; nnormalize; #H4; napply (H1 (AST_TYPE_STRUCT tt2) H3);
 409                                      nrewrite > (nelist_destruct_cons_cons_2 ast_type … (asttype_destruct_struct_struct … H4));
 410                                      napply refl_eq
 411                             ##]
 412                    ##| ##1: #hh2; nnormalize; #H2; #H3;
 413                             napply (nelist_destruct_cons_nil ast_type … (asttype_destruct_struct_struct … H3))
 414                    ##]
 415           ##| ##1: #b2; nnormalize; #H2; #H3; napply (asttype_destruct … H3)
 416           ##| ##2: #b2; #n2; nnormalize; #H2; #H3; napply (asttype_destruct … H3)
 417           ##]
 418  ##]
 419 nqed.
 420
 421 nlemma neq_to_neqasttype : ∀t1,t2.t1 ≠ t2 → eq_asttype t1 t2 = false.
 422  #t1;
 423  napply (ast_type_index … t1);
 424  ##[ ##1: #b1; #t2; ncases t2;
 425           ##[ ##1: #b2; nchange with (? → (eq_astbasetype b1 b2 = false)); #H;
 426                    napply (neq_to_neqastbasetype b1 b2 ?); nnormalize; #H1;
 427                    napply H; nrewrite > H1; napply refl_eq
 428           ##| ##2: #b2; #n2; nnormalize; #H; napply refl_eq
 429           ##| ##3: #n2; nnormalize; #H; napply refl_eq
 430           ##]
 431  ##| ##2: #b1; #n1; #H; #t2; ncases t2;
 432           ##[ ##2: #b2; #n2; nchange with (? → ((eq_asttype b1 b2)⊗(eq_nat n1 n2)) = false); #H1;
 433                    napply (or2_elim ??? (decidable_asttype b1 b2));
 434                    ##[ ##2: #H2; nrewrite > (H b2 H2); nnormalize; napply refl_eq
 435                    ##| ##1: #H2; napply (or2_elim ??? (decidable_nat n1 n2))
 436                             ##[ ##2: #H3; nrewrite > (neq_to_neqnat n1 n2 H3);
 437                                      nrewrite > (andb_false2_2 (eq_asttype b1 b2));
 438                                      napply refl_eq
 439                             ##| ##1: #H3; nrewrite > H2 in H1:(%); nrewrite > H3; #H1;
 440                                      nelim (H1 (refl_eq …))
 441                             ##]
 442                    ##]
 443           ##| ##1: #b2; nnormalize; #H1; napply refl_eq
 444           ##| ##3: #n2; nnormalize; #H1; napply refl_eq
 445           ##]
 446  ##| ##3: #hh1; #H; #t2; ncases t2;
 447           ##[ ##3: #n2; ncases n2;
 448                    ##[ ##1: #hh2; nchange with (? → (eq_asttype hh1 hh2 = false)); #H1;
 449                             napply (H hh2); nnormalize; #H2; nrewrite > H2 in H1:(%);
 450                             nnormalize; #H1; napply (H1 (refl_eq …))
 451                    ##| ##2: #hh2; #tt2; nnormalize; #H1; napply refl_eq
 452                    ##]
 453           ##| ##1: #b2; nnormalize; #H1; napply refl_eq
 454           ##| ##2: #b2; #n2; nnormalize; #H1; napply refl_eq
 455           ##]
 456  ##| ##4: #hh1; #tt1; #H; #H1; #t2; ncases t2;
 457           ##[ ##3: #n2; ncases n2;
 458                    ##[ ##2: #hh2; #tt2; nchange with (? → ((eq_asttype hh1 hh2)⊗(bfold_right_neList2 ?? tt1 tt2)) = false);
 459                             #H2; napply (or2_elim (hh1 ≠ hh2) (tt1 ≠ tt2) …);
 460                             ##[ ##2: #H3; nrewrite > (H hh2 H3); nnormalize; napply refl_eq
 461                             ##| ##3: #H3; nchange with (((eq_asttype hh1 hh2)⊗(eq_asttype (AST_TYPE_STRUCT tt1) (AST_TYPE_STRUCT tt2))) = false);
 462                                      nrewrite > (H1 (AST_TYPE_STRUCT tt2) ?);
 463                                      ##[ ##1: nrewrite > (andb_false2_2 (eq_asttype hh1 hh2)); napply refl_eq
 464                                      ##| ##2: nnormalize; #H4; napply (H3 (asttype_destruct_struct_struct … H4))
 465                                      ##]
 466                             ##| ##1: napply (or2_elim ??? (decidable_asttype hh1 hh2));
 467                                      ##[ ##2: #H3; napply (or2_intro1 … H3)
 468                                      ##| ##1: #H3; napply (or2_elim ??? (decidable_nelist ast_type decidable_asttype tt1 tt2));
 469                                               ##[ ##2: #H4; napply (or2_intro2 … H4)
 470                                               ##| ##1: #H4; nrewrite > H3  in H2:(%); nrewrite > H4; #H2;
 471                                                        nelim (H2 (refl_eq …))
 472                                               ##]
 473                                      ##]
 474                             ##]
 475                    ##| ##1: #hh2; nnormalize; #H2; napply refl_eq
 476                    ##]
 477           ##| ##1: #b2; nnormalize; #H2; napply refl_eq
 478           ##| ##2: #b2; #n2; nnormalize; #H2; napply refl_eq
 479           ##]
 480  ##]
 481 nqed.
 482
 483 nlemma isbastbasetype_to_isastbasetype : ∀ast.isb_ast_base_type ast = true → is_ast_base_type ast.
 484  #ast;
 485  ncases ast;
 486  nnormalize;
 487  ##[ ##1: #t; #H; napply I
 488  ##| ##2: #t; #n; #H; napply (bool_destruct … H)
 489  ##| ##3: #t; #H; napply (bool_destruct … H)
 490  ##]
 491 nqed.
 492
 493 nlemma isntbastbasetype_to_isntastbasetype : ∀ast.isntb_ast_base_type ast = true → isnt_ast_base_type ast.
 494  #ast;
 495  ncases ast;
 496  nnormalize;
 497  ##[ ##1: #t; #H; napply (bool_destruct … H)
 498  ##| ##2: #t; #n; #H; napply I
 499  ##| ##3: #l; #H; napply I
 500  ##]
 501 nqed.