matita/matita/contribs/assembly/compiler/env_to_flatenv.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 (*                                                                        *)
  17 (* Sviluppato da:                                                         *)
  18 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
  19 (*                                                                        *)
  20 (* ********************************************************************** *)
  21
  22 include "compiler/environment.ma".
  23 include "compiler/ast_tree.ma".
  24
  25 (* ********************** *)
  26 (* GESTIONE AMBIENTE FLAT *)
  27 (* ********************** *)
  28
  29 (* ambiente flat *)
  30 inductive var_flatElem : Type ≝
  31 VAR_FLAT_ELEM: aux_strId_type → desc_elem → var_flatElem.
  32
  33 definition get_name_flatVar ≝ λv:var_flatElem.match v with [ VAR_FLAT_ELEM n _ ⇒ n ].
  34 definition get_desc_flatVar ≝ λv:var_flatElem.match v with [ VAR_FLAT_ELEM _ d ⇒ d ].
  35
  36 definition aux_flatEnv_type ≝ list var_flatElem.
  37
  38 definition empty_flatEnv ≝ nil var_flatElem.
  39
  40 (* mappa: nome + max + cur *)
  41 inductive map_list : nat → Type ≝
  42   map_nil: map_list O
  43 | map_cons: ∀n.option nat → map_list n → map_list (S n).
  44
  45 definition defined_mapList ≝
  46 λd.λl:map_list d.match l with [ map_nil ⇒ False | map_cons _ _ _ ⇒ True ].
  47
  48 definition cut_first_mapList : Πd.map_list d → ? → map_list (pred d) ≝
  49 λd.λl:map_list d.λp:defined_mapList ? l.
  50  let value ≝
  51   match l
  52    return λX.λY:map_list X.defined_mapList X Y → map_list (pred X)
  53   with
  54    [ map_nil ⇒ λp:defined_mapList O map_nil.False_rect ? p
  55    | map_cons n h t ⇒ λp:defined_mapList (S n) (map_cons n h t).t
  56    ] p in value.
  57
  58 definition get_first_mapList : Πd.map_list d → ? → option nat ≝
  59 λd.λl:map_list d.λp:defined_mapList ? l.
  60  let value ≝
  61   match l
  62    return λX.λY:map_list X.defined_mapList X Y → option nat
  63   with
  64    [ map_nil ⇒ λp:defined_mapList O map_nil.False_rect ? p
  65    | map_cons n h t ⇒ λp:defined_mapList (S n) (map_cons n h t).h
  66    ] p in value.
  67
  68 inductive map_elem (d:nat) : Type ≝
  69 MAP_ELEM: aux_str_type → nat → map_list (S d) → map_elem d.
  70
  71 definition get_name_mapElem ≝ λd.λm:map_elem d.match m with [ MAP_ELEM n _ _ ⇒ n ].
  72 definition get_max_mapElem ≝ λd.λm:map_elem d.match m with [ MAP_ELEM _ m _ ⇒ m ].
  73 definition get_cur_mapElem ≝ λd.λm:map_elem d.match m with [ MAP_ELEM _ _ c ⇒ c ].
  74
  75 definition aux_map_type ≝ λd.list (map_elem d).
  76
  77 definition empty_map ≝ nil (map_elem O).
  78
  79 lemma defined_mapList_S_to_true :
  80 ∀d.∀l:map_list (S d).defined_mapList (S d) l = True.
  81  intros;
  82  inversion l;
  83   [ intros; destruct H
  84   | intros; simplify; reflexivity
  85   ]
  86 qed.
  87
  88 lemma defined_mapList_get :
  89  ∀d.∀h:map_elem d.defined_mapList (S d) (get_cur_mapElem d h).
  90  intros 2;
  91  rewrite > (defined_mapList_S_to_true ? (get_cur_mapElem d h));
  92  apply I.
  93 qed.
  94
  95 (* get_id *)
  96 let rec get_id_map_aux d (map:aux_map_type d) (name:aux_str_type) on map : option nat ≝
  97  match map with
  98   [ nil ⇒ None ?
  99   | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with
 100                 [ true ⇒ get_first_mapList (S d) (get_cur_mapElem d h) (defined_mapList_get ??)
 101                 | false ⇒ get_id_map_aux d t name
 102                 ]
 103   ].
 104
 105 definition get_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
 106  match get_id_map_aux d map name with [ None ⇒ O | Some x ⇒ x ].
 107
 108 (* get_max *)
 109 let rec get_max_map_aux d (map:aux_map_type d) (name:aux_str_type) on map ≝
 110  match map with
 111   [ nil ⇒ None ?
 112   | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with
 113                 [ true ⇒ Some ? (get_max_mapElem d h)
 114                 | false ⇒ get_max_map_aux d t name
 115                 ]
 116   ].
 117
 118 definition get_max_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
 119  match get_max_map_aux d map name with [ None ⇒ O | Some x ⇒ x ].
 120
 121 (* check_id *)
 122 definition check_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
 123  match get_id_map_aux d map name with [ None ⇒ False | Some _ ⇒ True ].
 124
 125 definition checkb_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
 126  match get_id_map_aux d map name with [ None ⇒ false | Some _ ⇒ true ].
 127
 128 lemma checkbidmap_to_checkidmap :
 129  ∀d.∀map:aux_map_type d.∀name.
 130   checkb_id_map d map name = true → check_id_map d map name.
 131  unfold checkb_id_map;
 132  unfold check_id_map;
 133  intros 3;
 134  elim (get_id_map_aux d map name) 0;
 135  [ simplify; intro; destruct H
 136  | simplify; intros; apply I
 137  ].
 138 qed.
 139
 140 definition checknot_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
 141  match get_id_map_aux d map name with [ None ⇒ True | Some _ ⇒ False ].
 142
 143 definition checknotb_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
 144  match get_id_map_aux d map name with [ None ⇒ true | Some _ ⇒ false ].
 145
 146 lemma checknotbidmap_to_checknotidmap :
 147  ∀d.∀map:aux_map_type d.∀name.
 148   checknotb_id_map d map name = true → checknot_id_map d map name.
 149  unfold checknotb_id_map;
 150  unfold checknot_id_map;
 151  intros 3;
 152  elim (get_id_map_aux d map name) 0;
 153  [ simplify; intro; apply I
 154  | simplify; intros; destruct H
 155  ].
 156 qed.
 157
 158 (* get_desc *)
 159 let rec get_desc_flatEnv_aux (fe:aux_flatEnv_type) (name:aux_strId_type) on fe ≝
 160  match fe with
 161   [ nil ⇒ None ?
 162   | cons h t ⇒ match eqStrId_str name (get_name_flatVar h) with
 163                [ true ⇒ Some ? (get_desc_flatVar h)
 164                | false ⇒ get_desc_flatEnv_aux t name
 165                ]
 166   ].
 167
 168 definition get_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
 169  match get_desc_flatEnv_aux fe str with
 170   [ None ⇒ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) | Some x ⇒ x ].
 171
 172 definition check_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
 173  match get_desc_flatEnv_aux fe str with [ None ⇒ False | Some _ ⇒ True ].
 174
 175 definition checkb_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
 176  match get_desc_flatEnv_aux fe str with [ None ⇒ false | Some _ ⇒ true ].
 177
 178 lemma checkbdescflatenv_to_checkdescflatenv :
 179  ∀fe,str.checkb_desc_flatEnv fe str = true → check_desc_flatEnv fe str.
 180  unfold checkb_desc_flatEnv;
 181  unfold check_desc_flatEnv;
 182  intros 2;
 183  elim (get_desc_flatEnv_aux fe str) 0;
 184  [ simplify; intro; destruct H
 185  | simplify; intros; apply I
 186  ].
 187 qed.
 188
 189 definition checknot_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
 190  match get_desc_flatEnv_aux fe str with [ None ⇒ True | Some _ ⇒ False ].
 191
 192 definition checknotb_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
 193  match get_desc_flatEnv_aux fe str with [ None ⇒ true | Some _ ⇒ false ].
 194
 195 lemma checknotbdescflatenv_to_checknotdescflatenv :
 196  ∀fe,str.checknotb_desc_flatEnv fe str = true → checknot_desc_flatEnv fe str.
 197  unfold checknotb_desc_flatEnv;
 198  unfold checknot_desc_flatEnv;
 199  intros 2;
 200  elim (get_desc_flatEnv_aux fe str) 0;
 201  [ simplify; intro; apply I
 202  | simplify; intros; destruct H
 203  ].
 204 qed.
 205
 206 (* leave: elimina la testa (il "cur" corrente) *)
 207 let rec leave_map d (map:aux_map_type (S d)) on map ≝
 208  match map with
 209   [ nil ⇒ []
 210   | cons h t ⇒
 211    (MAP_ELEM d
 212              (get_name_mapElem (S d) h)
 213              (get_max_mapElem (S d) h)
 214              (cut_first_mapList ? (get_cur_mapElem (S d) h) (defined_mapList_get ??))
 215    )::(leave_map d t)
 216   ].
 217
 218 (* enter: propaga in testa la vecchia testa (il "cur" precedente) *)
 219 let rec enter_map d (map:aux_map_type d) on map ≝
 220  match map with
 221   [ nil ⇒ []
 222   | cons h t ⇒
 223    (MAP_ELEM (S d)
 224              (get_name_mapElem d h)
 225              (get_max_mapElem d h)
 226              (map_cons (S d)
 227                        (get_first_mapList ? (get_cur_mapElem d h) (defined_mapList_get ??))
 228                        (get_cur_mapElem d h))
 229    )::(enter_map d t)
 230   ].
 231
 232 (* aggiungi descrittore *)
 233 let rec new_map_elem_from_depth_aux (d:nat) on d ≝
 234  match d
 235   return λd.map_list d
 236  with
 237   [ O ⇒ map_nil
 238   | S n ⇒ map_cons n (None ?) (new_map_elem_from_depth_aux n)
 239   ].
 240
 241 let rec new_max_map_aux d (map:aux_map_type d) (name:aux_str_type) (max:nat) on map ≝
 242  match map with
 243   [ nil ⇒ []
 244   | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with
 245                 [ true ⇒ (MAP_ELEM d name max (map_cons d (Some ? max) (cut_first_mapList (S d) (get_cur_mapElem d h) (defined_mapList_get ??))))::t
 246                 | false ⇒ h::(new_max_map_aux d t name max)
 247                 ]
 248   ].
 249
 250 definition add_desc_env_flatEnv_map ≝
 251 λd.λmap:aux_map_type d.λstr.
 252  match get_max_map_aux d map str with
 253   [ None ⇒ map@[ MAP_ELEM d str O (map_cons d (Some ? O) (new_map_elem_from_depth_aux d)) ]
 254   | Some x ⇒ new_max_map_aux d map str (S x)
 255   ].
 256
 257 definition add_desc_env_flatEnv_fe ≝
 258 λd.λmap:aux_map_type d.λfe.λstr.λc.λdesc.
 259  fe@[ VAR_FLAT_ELEM (STR_ID str match get_max_map_aux d map str with [ None ⇒ O | Some x ⇒ (S x)])
 260                     (DESC_ELEM c desc) ].
 261
 262 let rec build_trasfEnv_env (d:nat) (trsf:list (Prod3T aux_str_type bool ast_type)) on trsf : aux_env_type d → aux_env_type d ≝
 263  match trsf with
 264   [ nil ⇒ (λx.x)
 265   | cons h t ⇒ (λx.(build_trasfEnv_env d t) (add_desc_env d x (fst3T ??? h) (snd3T ??? h) (thd3T ??? h)))
 266   ].
 267
 268 let rec build_trasfEnv_mapFe (d:nat) (trsf:list (Prod3T aux_str_type bool ast_type)) on trsf :
 269  Prod (aux_map_type d) aux_flatEnv_type → Prod (aux_map_type d) aux_flatEnv_type ≝
 270  match trsf with
 271   [ nil ⇒ (λx.x)
 272   | cons h t ⇒ (λx.(build_trasfEnv_mapFe d t)
 273                    (pair ?? (add_desc_env_flatEnv_map d (fst ?? x) (fst3T ??? h))
 274                             (add_desc_env_flatEnv_fe d (fst ?? x) (snd ?? x) (fst3T ??? h) (snd3T ??? h) (thd3T ??? h))))
 275   ].
 276
 277 (* ********************************************* *)
 278
 279 (* fe <= fe' *)
 280 definition eq_flatEnv_elem ≝
 281 λe1,e2.match e1 with
 282  [ VAR_FLAT_ELEM sId1 d1 ⇒ match e2 with
 283   [ VAR_FLAT_ELEM sId2 d2 ⇒ (eqStrId_str sId1 sId2)⊗(eqDesc_elem d1 d2) ]].
 284
 285 lemma eq_to_eqflatenv : ∀e1,e2.e1 = e2 → eq_flatEnv_elem e1 e2 = true.
 286  intros 3;
 287  rewrite < H;
 288  elim e1;
 289  simplify;
 290  rewrite > (eq_to_eqstrid a a (refl_eq ??));
 291  rewrite > (eq_to_eqdescelem d d (refl_eq ??));
 292  reflexivity.
 293 qed.
 294
 295 lemma eqflatenv_to_eq : ∀e1,e2.eq_flatEnv_elem e1 e2 = true → e1 = e2.
 296  intros 2;
 297  elim e1 0;
 298  elim e2 0;
 299  intros 4;
 300  simplify;
 301  intro;
 302  rewrite > (eqstrid_to_eq a1 a (andb_true_true ?? H));
 303  rewrite > (eqdescelem_to_eq d1 d (andb_true_true_r ?? H));
 304  reflexivity.
 305 qed.
 306
 307 let rec le_flatEnv (fe,fe':aux_flatEnv_type) on fe ≝
 308 match fe with
 309   [ nil ⇒ true
 310   | cons h tl ⇒ match fe' with
 311    [ nil ⇒ false | cons h' tl' ⇒ (eq_flatEnv_elem h h')⊗(le_flatEnv tl tl') ]
 312   ].
 313
 314 lemma eq_to_leflatenv : ∀e1,e2.e1 = e2 → le_flatEnv e1 e2 = true.
 315  intros 3;
 316  rewrite < H;
 317  elim e1;
 318  [ reflexivity
 319  | simplify;
 320    rewrite > (eq_to_eqflatenv a a (refl_eq ??));
 321    rewrite > H1;
 322    reflexivity
 323  ].
 324 qed.
 325
 326 lemma leflatenv_to_le : ∀fe,fe'.le_flatEnv fe fe' = true → ∃x.fe@x=fe'.
 327  intro;
 328  elim fe 0;
 329  [ intros; exists; [ apply fe' | reflexivity ]
 330  | intros 4; elim fe';
 331    [ simplify in H1:(%); destruct H1
 332    | simplify in H2:(%);
 333      rewrite < (eqflatenv_to_eq a a1 (andb_true_true ?? H2));
 334      cases (H l1 (andb_true_true_r ?? H2));
 335      simplify;
 336      rewrite < H3;
 337      exists; [ apply x | reflexivity ]
 338    ]
 339  ].
 340 qed.
 341
 342 lemma le_to_leflatenv : ∀fe,x.le_flatEnv fe (fe@x) = true.
 343  intros;
 344  elim fe;
 345  [ simplify;
 346    reflexivity
 347  | simplify;
 348    rewrite > (eq_to_eqflatenv a a (refl_eq ??));
 349    rewrite > H;
 350    reflexivity
 351  ].
 352 qed.
 353
 354 lemma leflatenv_to_check :
 355  ∀fe,fe',str.
 356   (le_flatEnv fe fe' = true) →
 357   (check_desc_flatEnv fe str) →
 358   (check_desc_flatEnv fe' str).
 359  intros 4;
 360  cases (leflatenv_to_le fe fe' H);
 361  rewrite < H1;
 362  elim fe 0;
 363  [ intro; simplify in H2:(%); elim H2;
 364  | intros 3;
 365    simplify;
 366    cases (eqStrId_str str (get_name_flatVar a));
 367    [ simplify; intro; apply H3
 368    | simplify; apply H2
 369    ]
 370  ].
 371 qed.
 372
 373 lemma leflatenv_to_get :
 374  ∀fe,fe',str.
 375   (le_flatEnv fe fe' = true) →
 376   (check_desc_flatEnv fe str) →
 377   (get_desc_flatEnv fe str = get_desc_flatEnv fe' str).
 378  intros 4;
 379  cases (leflatenv_to_le fe fe' H);
 380  rewrite < H1;
 381  elim fe 0;
 382  [ intro;
 383    simplify in H2:(%);
 384    elim H2
 385  | simplify;
 386    intros 2;
 387    cases (eqStrId_str str (get_name_flatVar a));
 388    [ simplify;
 389      intros;
 390      reflexivity
 391    | simplify;
 392      unfold check_desc_flatEnv;
 393      unfold get_desc_flatEnv;
 394      cases (get_desc_flatEnv_aux l str);
 395      [ simplify; intros; elim H3
 396      | simplify; intros; rewrite < (H2 H3); reflexivity
 397      ]
 398    ]
 399  ].
 400 qed.
 401
 402 lemma leflatenv_trans :
 403  ∀fe,fe',fe''.
 404   le_flatEnv fe fe' = true →
 405   le_flatEnv fe' fe'' = true →
 406   le_flatEnv fe fe'' = true.
 407  intros 4;
 408  cases (leflatenv_to_le fe ? H);
 409  rewrite < H1;
 410  intro;
 411  cases (leflatenv_to_le (fe@x) fe'' H2);
 412  rewrite < H3;
 413  rewrite > associative_append;
 414  apply (le_to_leflatenv fe ?).
 415 qed.
 416
 417 lemma env_map_flatEnv_add_aux_fe_al :
 418  ∀trsf.∀d.∀m:aux_map_type d.∀a,l.
 419   snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m (a::l))) =
 420   a::(snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m l))).
 421  intro;
 422  elim trsf;
 423  [ simplify; reflexivity
 424  | simplify;
 425    elim a;
 426    simplify;
 427    rewrite > (H ????);
 428    reflexivity
 429  ].
 430 qed.
 431
 432 lemma env_map_flatEnv_add_aux_fe_l :
 433  ∀trsf.∀d.∀m:aux_map_type d.∀l.
 434   snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m l)) =
 435   l@(snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m []))).
 436  intros;
 437  elim l;
 438  [ simplify; reflexivity
 439  | rewrite > (env_map_flatEnv_add_aux_fe_al ????);
 440    rewrite > H;
 441    reflexivity
 442  ].
 443 qed.
 444
 445 lemma env_map_flatEnv_add_aux_fe :
 446  ∀d.∀map:aux_map_type d.∀fe,trsf.
 447   ∃x.fe@x = (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))).
 448  intros 3;
 449  elim fe 0;
 450  [ simplify;
 451    intro;
 452    exists;
 453    [ apply (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map [])))
 454    | reflexivity
 455    ]
 456  | intros 4;
 457    exists;
 458    [ apply (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map [])))
 459    | rewrite > (env_map_flatEnv_add_aux_fe_al trsf d map a l);
 460      rewrite > (env_map_flatEnv_add_aux_fe_l trsf d map l);
 461      rewrite < (cons_append_commute ????);
 462      reflexivity
 463    ]
 464  ].
 465 qed.
 466
 467 lemma buildtrasfenvadd_to_le :
 468  ∀d.∀m:aux_map_type d.∀fe,trsf.
 469   le_flatEnv fe (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m fe))) = true.
 470  intros 4;
 471   cases (env_map_flatEnv_add_aux_fe d m fe trsf);
 472  rewrite < H;
 473  rewrite > (le_to_leflatenv fe x);
 474  reflexivity.
 475 qed.
 476
 477 (* ********************************************* *)
 478
 479 (* miscellanea *)
 480 lemma leave_env_enter_env : ∀d.∀e:aux_env_type d.leave_env d (enter_env d e) = e.
 481  intros;
 482  elim e;
 483  reflexivity.
 484 qed.
 485
 486 lemma leave_map_enter_map : ∀d.∀map. leave_map d (enter_map d map) = map.
 487  intros;
 488  elim map;
 489   [ reflexivity
 490   | simplify;
 491     rewrite > H;
 492     cases a;
 493     simplify;
 494     reflexivity
 495   ]
 496 qed.
 497
 498 lemma leave_add_enter_env_aux :
 499  ∀d.∀a:aux_env_type d.∀trsf.∀c.
 500   ∃b.build_trasfEnv_env (S d) trsf (env_cons d c a) = (env_cons d b a).
 501  intros 3;
 502  elim trsf;
 503  [ simplify; exists; [ apply c | reflexivity ]
 504  | simplify; apply H
 505  ].
 506 qed.
 507
 508 lemma leave_add_enter_env :
 509  ∀d.∀e:aux_env_type d.∀trsf.
 510   leave_env d (build_trasfEnv_env (S d) trsf (enter_env d e)) = e.
 511  intros;
 512  unfold enter_env;
 513  lapply (leave_add_enter_env_aux d e trsf []);
 514  cases Hletin;
 515  rewrite > H;
 516  simplify;
 517  reflexivity.
 518 qed.
 519
 520 (* ********************************************* *)
 521
 522 (* invariante a un livello *)
 523 definition env_to_flatEnv_inv_one_level ≝
 524  λd.λe:aux_env_type d.λmap:aux_map_type d.λfe:aux_flatEnv_type.
 525   ∀str.
 526    check_desc_env d e str →
 527     check_id_map d map str ∧
 528     check_desc_flatEnv fe (STR_ID str (get_id_map d map str)) ∧
 529     get_desc_env d e str = get_desc_flatEnv fe (STR_ID str (get_id_map d map str)).
 530
 531 (* invariante su tutti i livelli *)
 532 let rec env_to_flatEnv_inv (d:nat) : aux_env_type d → aux_map_type d → aux_flatEnv_type → Prop ≝
 533  match d
 534   return λd.aux_env_type d → aux_map_type d → aux_flatEnv_type → Prop
 535  with
 536   [ O ⇒ λe:aux_env_type O.λmap:aux_map_type O.λfe:aux_flatEnv_type.
 537    env_to_flatEnv_inv_one_level O e map fe
 538   | S n ⇒ λe:aux_env_type (S n).λmap:aux_map_type (S n).λfe:aux_flatEnv_type.
 539    env_to_flatEnv_inv_one_level (S n) e map fe ∧
 540    env_to_flatEnv_inv n (leave_env n e) (leave_map n map) fe
 541   ].
 542
 543 (* invariante full -> invariante a un livello *)
 544 lemma env_to_flatEnv_inv_last :
 545  ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.
 546   env_to_flatEnv_inv d e map fe →
 547   env_to_flatEnv_inv_one_level d e map fe.
 548  intro;
 549  cases d;
 550  intros;
 551   [ apply H
 552   | simplify in H;
 553     apply (proj1 ?? H)
 554   ]
 555 qed.
 556
 557 (* invariante caso base *)
 558 lemma env_map_flatEnv_empty_aux : env_to_flatEnv_inv O empty_env empty_map empty_flatEnv.
 559  unfold env_to_flatEnv_inv;
 560  unfold empty_env;
 561  unfold empty_map;
 562  unfold empty_flatEnv;
 563  simplify;
 564  intros;
 565  elim H.
 566 qed.
 567
 568 (* invariante & leflatenv *)
 569 lemma leflatenv_to_inv :
 570  ∀d.∀e.∀map:aux_map_type d.∀fe,fe'.
 571   le_flatEnv fe fe' = true →
 572   env_to_flatEnv_inv d e map fe →
 573   env_to_flatEnv_inv d e map fe'.
 574  intro;
 575  elim d;
 576  [ simplify;
 577    unfold env_to_flatEnv_inv_one_level;
 578    intros;
 579    split;
 580    [ split;
 581      [ lapply (H1 str H2);
 582        apply (proj1 ?? (proj1 ?? Hletin))
 583      | lapply (H1 str H2);
 584        apply (leflatenv_to_check fe fe' ? H (proj2 ?? (proj1 ?? Hletin)))
 585      ]
 586    | lapply (H1 str H2);
 587      rewrite < (leflatenv_to_get fe fe' ? H (proj2 ?? (proj1 ?? Hletin)));
 588      apply (proj2 ?? Hletin)
 589    ]
 590  | simplify in H2 ⊢ %;
 591    cases H2;
 592    split;
 593    [ unfold env_to_flatEnv_inv_one_level;
 594      intros;
 595      split;
 596      [ split;
 597        [ lapply (H3 str H5);
 598          apply (proj1 ?? (proj1 ?? Hletin))
 599        | lapply (H3 str H5);
 600          apply (leflatenv_to_check fe fe' ? H1 (proj2 ?? (proj1 ?? Hletin)))
 601        ]
 602      | lapply (H3 str H5);
 603        rewrite < (leflatenv_to_get fe fe' ? H1 (proj2 ?? (proj1 ?? Hletin)));
 604        apply (proj2 ?? Hletin)
 605      ]
 606    | apply (H ???? H1 H4)
 607    ]
 608  ].
 609 qed.
 610
 611 (* invariante & enter *)
 612 lemma getidmap_to_enter :
 613  ∀d.∀m:aux_map_type d.∀str.
 614   get_id_map_aux (S d) (enter_map d m) str = get_id_map_aux d m str.
 615  intros;
 616  elim m;
 617  [ simplify; reflexivity
 618  | simplify; rewrite > H; reflexivity
 619  ]
 620 qed.
 621
 622 lemma checkdescenter_to_checkdesc :
 623  ∀d.∀e:aux_env_type d.∀str.
 624   check_desc_env (S d) (enter_env d e) str →
 625   check_desc_env d e str.
 626  intros;
 627  unfold enter_env in H:(%);
 628  simplify in H:(%);
 629  apply H.
 630 qed.
 631
 632
 633 lemma env_map_flatEnv_enter_aux :
 634  ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.
 635   env_to_flatEnv_inv d e map fe →
 636   env_to_flatEnv_inv (S d) (enter_env d e) (enter_map d map) fe.
 637  intro;
 638  elim d;
 639  [ simplify in H;
 640    split;
 641    [ unfold env_to_flatEnv_inv_one_level;
 642      intros;
 643      split;
 644      [ split;
 645        [ unfold check_id_map;
 646          rewrite > (getidmap_to_enter ???);
 647          apply (proj1 ?? (proj1 ?? (H str (checkdescenter_to_checkdesc ??? H1))))
 648        | unfold get_id_map;
 649          rewrite > (getidmap_to_enter ???);
 650          apply (proj2 ?? (proj1 ?? (H str (checkdescenter_to_checkdesc ??? H1))))
 651        ]
 652      | unfold get_id_map;
 653        rewrite > (getidmap_to_enter ???);
 654        apply (proj2 ?? (H str (checkdescenter_to_checkdesc ??? H1)))
 655      ]
 656    | rewrite > leave_env_enter_env;
 657      rewrite > leave_map_enter_map;
 658      change with (env_to_flatEnv_inv_one_level O e map fe);
 659      apply H
 660    ]
 661  | split;
 662    [ cases H1;
 663      simplify in H2;
 664      unfold env_to_flatEnv_inv_one_level;
 665      intros;
 666      split;
 667      [ split;
 668        [ unfold check_id_map;
 669          rewrite > (getidmap_to_enter ???);
 670          apply (proj1 ?? (proj1 ?? (H2 str (checkdescenter_to_checkdesc ??? H4))))
 671        | unfold get_id_map;
 672          rewrite > (getidmap_to_enter ???);
 673          apply (proj2 ?? (proj1 ?? (H2 str (checkdescenter_to_checkdesc ??? H4))))
 674        ]
 675      | unfold get_id_map;
 676        rewrite > (getidmap_to_enter ???);
 677        apply (proj2 ?? (H2 str (checkdescenter_to_checkdesc ??? H4)))
 678      ]
 679    | rewrite > leave_env_enter_env;
 680      rewrite > leave_map_enter_map;
 681      change with (env_to_flatEnv_inv (S n) e map fe);
 682      apply H1
 683    ]
 684  ]
 685 qed.
 686
 687 (* invariante & leave *)
 688 lemma env_map_flatEnv_leave_aux :
 689  ∀d.∀e:aux_env_type (S d).∀map:aux_map_type (S d).∀fe.∀trsf.
 690   env_to_flatEnv_inv (S d) (build_trasfEnv_env (S d) trsf e) map fe →
 691   env_to_flatEnv_inv d (leave_env d (build_trasfEnv_env (S d) trsf e)) (leave_map d map) fe.
 692  intros;
 693  simplify in H;
 694  cases H;
 695  apply H2.
 696 qed.
 697
 698 (* invariante & add *)
 699 definition occurs_in_trsf ≝
 700 λtrsf:list (Prod3T aux_str_type bool ast_type).λstr.
 701  fold_right_list ?? (λhe,b.eqStr_str (fst3T ??? he) str ⊕ b) false trsf.
 702
 703 lemma occurs_in_subTrsf_r :
 704  ∀a,l,str.
 705   occurs_in_trsf (a::l) str = false →
 706   occurs_in_trsf l str = false.
 707  intros;
 708  simplify in H:(%);
 709  rewrite > (orb_false_false_r ?? H);
 710  reflexivity.
 711 qed.
 712
 713 lemma occurs_in_subTrsf_l :
 714  ∀a,l,str.
 715   occurs_in_trsf (a::l) str = false →
 716   eqStr_str (fst3T ??? a) str = false.
 717  intros;
 718  simplify in H:(%);
 719  rewrite > (orb_false_false ?? H);
 720  reflexivity.
 721 qed.
 722
 723 axiom get_id_map_aux_add_not_occurs :
 724  ∀d.∀map:aux_map_type d.∀fe,trsf,str.
 725   occurs_in_trsf trsf str = false →
 726   get_id_map_aux d map str =
 727   get_id_map_aux d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str.
 728
 729 lemma get_id_map_add_not_occurs :
 730  ∀d.∀map:aux_map_type d.∀fe,trsf,str.
 731   occurs_in_trsf trsf str = false →
 732   get_id_map d map str =
 733   get_id_map d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str.
 734  intros;
 735  unfold get_id_map;
 736  rewrite < (get_id_map_aux_add_not_occurs ????? H);
 737  reflexivity.
 738 qed.
 739
 740 lemma check_id_map_not_occurs :
 741  ∀d.∀map:aux_map_type d.∀fe.∀trsf.∀str.
 742   occurs_in_trsf trsf str = false →
 743   check_id_map d map str →
 744   check_id_map d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str.
 745  intros;
 746  whd in H1 ⊢ %;
 747  rewrite < (get_id_map_aux_add_not_occurs ????? H);
 748  apply H1.
 749 qed.
 750
 751 lemma check_desc_flatEnv_not_occurs :
 752  ∀d.∀map:aux_map_type d.∀fe.∀trsf.∀str.
 753   occurs_in_trsf trsf str = false →
 754   check_desc_flatEnv fe (STR_ID str (get_id_map d map str)) →
 755   check_desc_flatEnv (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe)))
 756                      (STR_ID str (get_id_map d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str)).
 757  intros;
 758  rewrite < (get_id_map_add_not_occurs ????? H);
 759  apply (leflatenv_to_check ??? (buildtrasfenvadd_to_le ????) H1).
 760 qed.
 761
 762 lemma get_desc_flatEnv_not_occurs :
 763  ∀d.∀map:aux_map_type d.∀fe.∀trsf.∀str.
 764   occurs_in_trsf trsf str = false →
 765   check_desc_flatEnv fe (STR_ID str (get_id_map d map str)) →
 766   get_desc_flatEnv (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe)))
 767                    (STR_ID str (get_id_map d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str)) =
 768   get_desc_flatEnv fe (STR_ID str (get_id_map d map str)).
 769  intros;
 770  rewrite < (get_id_map_add_not_occurs ????? H);
 771  rewrite < (leflatenv_to_get ??? (buildtrasfenvadd_to_le ????) H1);
 772  reflexivity.
 773 qed.
 774
 775 axiom get_desc_env_aux_not_occurs :
 776  ∀d.∀e:aux_env_type d.∀trsf.∀str.
 777   occurs_in_trsf trsf str = false →
 778   get_desc_env_aux d (build_trasfEnv_env d trsf e) str =
 779   get_desc_env_aux d e str.
 780
 781 lemma get_desc_env_not_occurs :
 782  ∀d.∀e:aux_env_type d.∀trsf.∀str.
 783   occurs_in_trsf trsf str = false →
 784   get_desc_env d (build_trasfEnv_env d trsf e) str =
 785   get_desc_env d e str.
 786  intros;
 787  unfold get_desc_env;
 788  rewrite > (get_desc_env_aux_not_occurs ???? H);
 789  reflexivity.
 790 qed.
 791
 792 lemma check_desc_env_not_occurs :
 793  ∀d.∀e:aux_env_type d.∀trsf.∀str.
 794   occurs_in_trsf trsf str = false →
 795   check_desc_env d (build_trasfEnv_env d trsf e) str →
 796   check_desc_env d e str.
 797  intros 5;
 798  unfold check_desc_env;
 799  intro;
 800  rewrite < (get_desc_env_aux_not_occurs ???? H);
 801  apply H1.
 802 qed.
 803
 804 axiom get_id_map_aux_add_occurs :
 805  ∀d.∀map:aux_map_type d.∀fe,trsf,str.
 806   occurs_in_trsf trsf str = true →
 807   ∃x.get_id_map_aux d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str = Some ? x.
 808
 809 lemma check_id_map_occurs :
 810  ∀d.∀map:aux_map_type d.∀fe.∀trsf.∀str.
 811   occurs_in_trsf trsf str = true →
 812   check_id_map d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str.
 813  intros;
 814  cases (get_id_map_aux_add_occurs d map fe trsf str H);
 815  unfold check_id_map;
 816  rewrite > H1;
 817  simplify;
 818  apply I.
 819 qed.
 820
 821 axiom check_desc_flatEnv_occurs :
 822  ∀d.∀map:aux_map_type d.∀fe.∀trsf.∀str.
 823   occurs_in_trsf trsf str = true →
 824   check_desc_flatEnv (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe)))
 825                      (STR_ID str (get_id_map d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str)).
 826
 827 axiom get_desc_env_eq_get_desc_flatEnv_occurs :
 828  ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.∀trsf.∀str.
 829  occurs_in_trsf trsf str = true →
 830  get_desc_env d (build_trasfEnv_env d trsf e) str =
 831  get_desc_flatEnv (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe)))
 832                   (STR_ID str (get_id_map d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str)).
 833
 834 axiom leave_env_build_trasfEnv :
 835  ∀d.∀e:aux_env_type (S d).∀trsf.
 836   leave_env d (build_trasfEnv_env (S d) trsf e) = leave_env d e.
 837
 838 axiom leave_map_build_trasfEnv_mapFe:
 839  ∀d.∀map:aux_map_type (S d).∀fe.∀trsf.
 840   leave_map d (fst ?? (build_trasfEnv_mapFe (S d) trsf (pair ?? map fe))) =
 841   leave_map d map.
 842
 843 lemma env_map_flatEnv_add_aux :
 844  ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.∀trsf.
 845   env_to_flatEnv_inv d e map fe →
 846   env_to_flatEnv_inv d
 847                      (build_trasfEnv_env d trsf e)
 848                      (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe)))
 849                      (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))).
 850  intro;
 851  cases d;
 852  [ intros;
 853    simplify in H;
 854    simplify;
 855    intros 2;
 856    apply (bool_elim ? (occurs_in_trsf trsf str));
 857    [ intro;
 858      split
 859      [ split
 860        [ apply (check_id_map_occurs ????? H2)
 861        | apply (check_desc_flatEnv_occurs ????? H2)
 862        ]
 863      | apply (get_desc_env_eq_get_desc_flatEnv_occurs ?????? H2)
 864      ]
 865    | intro;
 866      cases (H str (check_desc_env_not_occurs ???? H2 H1));
 867      split
 868      [ split
 869        [ apply (check_id_map_not_occurs ????? H2 (proj1 ?? H3))
 870        | apply (check_desc_flatEnv_not_occurs ????? H2 (proj2 ?? H3))
 871        ]
 872      | rewrite > (get_desc_flatEnv_not_occurs ????? H2 (proj2 ?? H3));
 873        rewrite > (get_desc_env_not_occurs ???? H2);
 874        apply H4
 875      ]
 876    ]
 877  | intros;
 878    simplify in H;
 879    cases H;
 880    unfold env_to_flatEnv_inv_one_level in H1;
 881    split;
 882    [ intros 2;
 883      apply (bool_elim ? (occurs_in_trsf trsf str));
 884      [ intro;
 885        split
 886        [ split
 887          [ apply (check_id_map_occurs ????? H4)
 888          | apply (check_desc_flatEnv_occurs ????? H4)
 889          ]
 890        | apply (get_desc_env_eq_get_desc_flatEnv_occurs ?????? H4)
 891        ]
 892      | intro;
 893        split;
 894        [ split
 895          [ apply (check_id_map_not_occurs ????? H4 (proj1 ?? (proj1 ?? (H1 str (check_desc_env_not_occurs ???? H4 H3)))))
 896          | apply (check_desc_flatEnv_not_occurs ????? H4 (proj2 ?? (proj1 ?? (H1 str (check_desc_env_not_occurs ???? H4 H3)))))
 897          ]
 898        | rewrite > (get_desc_flatEnv_not_occurs ????? H4 (proj2 ?? (proj1 ?? (H1 str (check_desc_env_not_occurs ???? H4 H3)))));
 899          rewrite > (get_desc_env_not_occurs ???? H4);
 900          apply (proj2 ?? (H1 str (check_desc_env_not_occurs ???? H4 H3)))
 901        ]
 902      ]
 903    | change with (env_to_flatEnv_inv n (leave_env n (build_trasfEnv_env (S n) trsf e))
 904                  (leave_map n (fst ?? (build_trasfEnv_mapFe (S n) trsf (pair ?? map fe))))
 905                  (snd ?? (build_trasfEnv_mapFe (S n) trsf (pair ?? map fe))));
 906      rewrite > leave_map_build_trasfEnv_mapFe;
 907      rewrite > leave_env_build_trasfEnv;
 908      apply (leflatenv_to_inv ?????? H2);
 909      apply buildtrasfenvadd_to_le
 910    ]
 911  ].
 912 qed.
 913
 914 lemma env_map_flatEnv_addNil_aux :
 915  ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.
 916   env_to_flatEnv_inv d e map fe →
 917   env_to_flatEnv_inv d
 918                      (build_trasfEnv_env d [] e)
 919                      (fst ?? (build_trasfEnv_mapFe d [] (pair ?? map fe)))
 920                      (snd ?? (build_trasfEnv_mapFe d [] (pair ?? map fe))).
 921  intros;
 922  simplify;
 923  apply H.
 924 qed.
 925
 926 lemma env_map_flatEnv_addSingle_aux :
 927  ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.∀name,const,desc.
 928   env_to_flatEnv_inv d e map fe →
 929   env_to_flatEnv_inv d
 930                      (add_desc_env d e name const desc)
 931                      (fst ?? (build_trasfEnv_mapFe d [ tripleT ??? name const desc ] (pair ?? map fe)))
 932                      (snd ?? (build_trasfEnv_mapFe d [ tripleT ??? name const desc ] (pair ?? map fe))).
 933  intros;
 934  apply (env_map_flatEnv_add_aux d e map fe [ tripleT ??? name const desc ]);
 935  apply H.
 936 qed.
 937
 938 lemma env_map_flatEnv_addJoin_aux :
 939  ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe:aux_flatEnv_type.∀name,const,desc,trsf.
 940   env_to_flatEnv_inv d
 941                      (build_trasfEnv_env d trsf (add_desc_env d e name const desc))
 942                      map fe →
 943   env_to_flatEnv_inv d
 944                      (build_trasfEnv_env d ([ tripleT ??? name const desc ]@trsf) e)
 945                      map fe.
 946  intros;
 947  simplify;
 948  apply H.
 949 qed.
 950
 951 (* ********************************************* *)
 952
 953 lemma newid_from_init :
 954  ∀d.∀e:aux_env_type d.∀name,const,desc.
 955   ast_id d (add_desc_env d e name const desc) const desc.
 956  intros;
 957  lapply (AST_ID d (add_desc_env d e name const desc) name ?);
 958  [ elim e;
 959    simplify;
 960    rewrite > (eq_to_eqstr ?? (refl_eq ??));
 961    simplify;
 962    apply I
 963  | cut (const = get_const_desc (get_desc_env d (add_desc_env d e name const desc) name) ∧
 964         desc = get_type_desc (get_desc_env d (add_desc_env d e name const desc) name));
 965    [ rewrite > (proj1 ?? Hcut) in ⊢ (? ? ? % ?);
 966      rewrite > (proj2 ?? Hcut) in ⊢ (? ? ? ? %);
 967      apply Hletin
 968    | split;
 969      [ elim e;
 970        simplify;
 971        rewrite > (eq_to_eqstr ?? (refl_eq ??));
 972        simplify;
 973        reflexivity
 974      | elim e;
 975        simplify;
 976        rewrite > (eq_to_eqstr ?? (refl_eq ??));
 977        simplify;
 978        reflexivity
 979      ]
 980    ]
 981  ].
 982 qed.