helm/software/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 (* fe <= fe' *)
 207 definition eq_flatEnv_elem ≝
 208 λe1,e2.match e1 with
 209  [ VAR_FLAT_ELEM sId1 d1 ⇒ match e2 with
 210   [ VAR_FLAT_ELEM sId2 d2 ⇒ (eqStrId_str sId1 sId2)⊗(eqDesc_elem d1 d2) ]].
 211
 212 lemma eq_to_eqflatenv : ∀e1,e2.e1 = e2 → eq_flatEnv_elem e1 e2 = true.
 213  intros 3;
 214  rewrite < H;
 215  elim e1;
 216  simplify;
 217  rewrite > (eq_to_eqstrid a a (refl_eq ??));
 218  rewrite > (eq_to_eqdescelem d d (refl_eq ??));
 219  reflexivity.
 220 qed.
 221
 222 lemma eqflatenv_to_eq : ∀e1,e2.eq_flatEnv_elem e1 e2 = true → e1 = e2.
 223  intros 2;
 224  elim e1 0;
 225  elim e2 0;
 226  intros 4;
 227  simplify;
 228  intro;
 229  rewrite > (eqstrid_to_eq a1 a (andb_true_true ?? H));
 230  rewrite > (eqdescelem_to_eq d1 d (andb_true_true_r ?? H));
 231  reflexivity.
 232 qed.
 233
 234 let rec le_flatEnv (fe,fe':aux_flatEnv_type) on fe ≝
 235 match fe with
 236   [ nil ⇒ true
 237   | cons h tl ⇒ match fe' with
 238    [ nil ⇒ false | cons h' tl' ⇒ (eq_flatEnv_elem h h')⊗(le_flatEnv tl tl') ]
 239   ].
 240
 241 lemma eq_to_leflatenv : ∀e1,e2.e1 = e2 → le_flatEnv e1 e2 = true.
 242  intros 3;
 243  rewrite < H;
 244  elim e1;
 245  [ reflexivity
 246  | simplify;
 247    rewrite > (eq_to_eqflatenv a a (refl_eq ??));
 248    rewrite > H1;
 249    reflexivity
 250  ].
 251 qed.
 252
 253 lemma leflatenv_to_le : ∀fe,fe'.le_flatEnv fe fe' = true → ∃x.fe@x=fe'.
 254  intro;
 255  elim fe 0;
 256  [ intros; exists; [ apply fe' | reflexivity ]
 257  | intros 4; elim fe';
 258    [ simplify in H1:(%); destruct H1
 259    | simplify in H2:(%);
 260      rewrite < (eqflatenv_to_eq a a1 (andb_true_true ?? H2));
 261      cases (H l1 (andb_true_true_r ?? H2));
 262      simplify;
 263      rewrite < H3;
 264      exists; [ apply x | reflexivity ]
 265    ]
 266  ].
 267 qed.
 268
 269 lemma le_to_leflatenv : ∀fe,x.le_flatEnv fe (fe@x) = true.
 270  intros;
 271  elim fe;
 272  [ simplify;
 273    reflexivity
 274  | simplify;
 275    rewrite > (eq_to_eqflatenv a a (refl_eq ??));
 276    rewrite > H;
 277    reflexivity
 278  ].
 279 qed.
 280
 281 lemma leflatenv_to_check : ∀fe,fe',str.
 282  (le_flatEnv fe fe' = true) →
 283  (check_desc_flatEnv fe str) →
 284  (check_desc_flatEnv fe' str).
 285  intros 4;
 286  cases (leflatenv_to_le fe fe' H);
 287  rewrite < H1;
 288  elim fe 0;
 289  [ intro; simplify in H2:(%); elim H2;
 290  | intros 3;
 291    simplify;
 292    cases (eqStrId_str str (get_name_flatVar a));
 293    [ simplify; intro; apply H3
 294    | simplify; apply H2
 295    ]
 296  ].
 297 qed.
 298
 299 lemma leflatenv_to_get : ∀fe,fe',str.
 300  (le_flatEnv fe fe' = true) →
 301  (check_desc_flatEnv fe str) →
 302  (get_desc_flatEnv fe str = get_desc_flatEnv fe' str).
 303  intros 4;
 304  cases (leflatenv_to_le fe fe' H);
 305  rewrite < H1;
 306  elim fe 0;
 307  [ intro;
 308    simplify in H2:(%);
 309    elim H2
 310  | simplify;
 311    intros 2;
 312    cases (eqStrId_str str (get_name_flatVar a));
 313    [ simplify;
 314      intros;
 315      reflexivity
 316    | simplify;
 317      unfold check_desc_flatEnv;
 318      unfold get_desc_flatEnv;
 319      cases (get_desc_flatEnv_aux l str);
 320      [ simplify; intros; elim H3
 321      | simplify; intros; rewrite < (H2 H3); reflexivity
 322      ]
 323    ]
 324  ].
 325 qed.
 326
 327 (* controllo di coerenza env <-> map *)
 328 let rec check_map_env_align_auxEnv (d:nat) (e:aux_env_type d) (str:aux_str_type) (res:nat) on e ≝
 329  match e with
 330   [ env_nil h ⇒ λf.f h
 331   | env_cons d' h t ⇒ λf.check_map_env_align_auxEnv d' t str (f h)
 332   ] (λx.match get_desc_from_lev_env x str with [ None ⇒ S res | Some _ ⇒ O ]).
 333
 334 let rec check_map_env_align_auxMap (d:nat) (map:map_list d) (res:nat) on map ≝
 335  match map with
 336   [ map_nil ⇒ eqb res O
 337   | map_cons d' h t ⇒ match eqb res O with
 338    [ true ⇒ match h with
 339     [ None ⇒ check_map_env_align_auxMap d' t O | Some _ ⇒ false ]
 340    | false ⇒ match h with
 341     [ None ⇒ false | Some _ ⇒ check_map_env_align_auxMap d' t (pred res) ]
 342    ]
 343   ].
 344
 345 (* esprimendolo in lingua umana il vincolo che controlla e':
 346    ∀name ϵ map.
 347     la map_list "cur" deve avere la seguente struttura
 348      - Some _ ; ... ; Some _ ; None ; ... None
 349      - il numero di Some _ deve essere pari a (d + 1 - x) con x
 350        ricavato scandendo in avanti tutti gli ambienti e
 351        numerando quanti ambienti CONSECUTIVI non contengono la definizione di name
 352
 353    ex: scandendo e in avanti si trova la seguente sequenza di check per il nome "pippo"
 354        no si no si NO NO
 355        quindi sapendo che d=5 (6 partendo da 0) e che check_env_align_aux ha restituito 2
 356        sappiamo che la mappa alla voce "pippo" deve avere la seguente struttura scandita in avanti
 357        Some _ ; Some _ ; Some _ ; Some _ ; None ; None
 358        cioe' 5+1-2 Some seguiti da solo None
 359
 360    NB: e' solo meta' perche' cosi' si asserisce map ≤ env
 361
 362 *)
 363 let rec check_map_env_align (d:nat) (e:aux_env_type d) (map:aux_map_type d) on map ≝
 364  match map with
 365   [ nil ⇒ true
 366   | cons h t ⇒ (check_map_env_align_auxMap (S d) (get_cur_mapElem d h) (d + 1 - (check_map_env_align_auxEnv d e (get_name_mapElem d h) O)))⊗
 367                (check_map_env_align d e t)
 368   ].
 369
 370 let rec check_env_map_align_aux (d:nat) (map:aux_map_type d) (le:list var_elem) on le ≝
 371  match le with
 372   [ nil ⇒ true
 373   | cons h t ⇒ match get_id_map_aux d map (get_name_var h) with
 374    [ None ⇒ false | Some _ ⇒ check_env_map_align_aux d map t ]
 375   ].
 376
 377 (* esprimendolo in lingua umana il vincolo che controlla e':
 378    ∀name ϵ e.name ϵ map
 379
 380    NB: e' l'altra meta' perche' cosi' asserisce env ≤ map
 381 *)
 382 let rec check_env_map_align (de:nat) (e:aux_env_type de) (dm:nat) (map:aux_map_type dm) on e ≝
 383  match e with
 384   [ env_nil h ⇒ check_env_map_align_aux dm map h
 385   | env_cons d' h t ⇒ (check_env_map_align_aux dm map h)⊗(check_env_map_align d' t dm map)
 386   ].
 387
 388 (* invariante *)
 389 definition env_to_flatEnv_inv ≝
 390  λd.λe:aux_env_type d.λmap:aux_map_type d.λfe:aux_flatEnv_type.
 391   ∀str.
 392    check_desc_env d e str →
 393     check_env_map_align d e d map = true ∧ check_map_env_align d e map = true ∧
 394     check_id_map d map str ∧
 395     check_desc_flatEnv fe (STR_ID str (get_id_map d map str)) ∧
 396     get_desc_env d e str = get_desc_flatEnv fe (STR_ID str (get_id_map d map str)).
 397
 398 lemma inv_to_checkdescflatenv :
 399  ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.
 400  env_to_flatEnv_inv d e map fe →
 401  (∀str.check_desc_env d e str → check_desc_flatEnv fe (STR_ID str (get_id_map d map str))).
 402  intros 7;
 403  unfold env_to_flatEnv_inv in H:(%);
 404  lapply (H str H1);
 405  apply (proj2 ?? (proj1 ?? Hletin));
 406 qed.
 407
 408 lemma env_map_flatEnv_empty_aux : env_to_flatEnv_inv O empty_env empty_map empty_flatEnv.
 409  unfold env_to_flatEnv_inv;
 410  unfold empty_env;
 411  unfold empty_map;
 412  unfold empty_flatEnv;
 413  simplify;
 414  intros;
 415  elim H.
 416 qed.
 417
 418 lemma leflatenv_to_inv :
 419  ∀d.∀e.∀map:aux_map_type d.∀fe,fe'.
 420   le_flatEnv fe fe' = true →
 421   env_to_flatEnv_inv d e map fe →
 422   env_to_flatEnv_inv d e map fe'.
 423  intros 6;
 424  unfold env_to_flatEnv_inv;
 425  intros;
 426  split;
 427  [ split;
 428    [ lapply (H1 str H2);
 429      apply (proj1 ?? (proj1 ?? Hletin))
 430    | lapply (H1 str H2);
 431      apply (leflatenv_to_check fe fe' ? H (proj2 ?? (proj1 ?? Hletin)))
 432    ]
 433  | lapply (H1 str H2);
 434    rewrite < (leflatenv_to_get fe fe' ? H (proj2 ?? (proj1 ?? Hletin)));
 435    apply (proj2 ?? Hletin)
 436  ].
 437 qed.
 438
 439 lemma leflatenv_trans :
 440  ∀fe,fe',fe''.
 441   le_flatEnv fe fe' = true →
 442   le_flatEnv fe' fe'' = true →
 443   le_flatEnv fe fe'' = true.
 444  intros 4;
 445  cases (leflatenv_to_le fe ? H);
 446  rewrite < H1;
 447  intro;
 448  cases (leflatenv_to_le (fe@x) fe'' H2);
 449  rewrite < H3;
 450  rewrite > associative_append;
 451  apply (le_to_leflatenv fe ?).
 452 qed.
 453
 454 (* enter: propaga in testa la vecchia testa (il "cur" precedente) *)
 455 let rec enter_map d (map:aux_map_type d) on map ≝
 456  match map with
 457   [ nil ⇒ []
 458   | cons h t ⇒
 459    (MAP_ELEM (S d)
 460              (get_name_mapElem d h)
 461              (get_max_mapElem d h)
 462              (map_cons (S d)
 463                        (get_first_mapList ? (get_cur_mapElem d h) (defined_mapList_get ??))
 464                        (get_cur_mapElem d h))
 465    )::(enter_map d t)
 466   ].
 467
 468 lemma getidmap_to_enter :
 469  ∀d.∀m:aux_map_type d.∀str.
 470   get_id_map_aux (S d) (enter_map d m) str = get_id_map_aux d m str.
 471  intros;
 472  elim m;
 473  [ simplify; reflexivity
 474  | simplify; rewrite > H; reflexivity
 475  ]
 476 qed.
 477
 478 lemma checkdescenter_to_checkdesc :
 479  ∀d.∀e:aux_env_type d.∀str.
 480   check_desc_env (S d) (enter_env d e) str →
 481   check_desc_env d e str.
 482  intros;
 483  unfold enter_env in H:(%);
 484  simplify in H:(%);
 485  apply H.
 486 qed.
 487
 488 lemma checkenvmapalign_to_enter :
 489  ∀de.∀e:aux_env_type de.∀dm.∀m:aux_map_type dm.
 490   check_env_map_align de e dm m =
 491   check_env_map_align (S de) (enter_env de e) (S dm) (enter_map dm m).
 492  intros 4;
 493  unfold enter_env;
 494  simplify;
 495  elim e 0;
 496  [ simplify;
 497    intro;
 498    elim l 0;
 499    [ simplify;
 500      reflexivity
 501    | simplify;
 502      intros;
 503      rewrite > (getidmap_to_enter ???);
 504      rewrite < H;
 505      cases (get_id_map_aux dm m (get_name_var a));
 506      [ simplify;
 507        reflexivity
 508      | simplify;
 509        rewrite > H;
 510        reflexivity
 511      ]
 512    ]
 513  | simplify;
 514    intros 2;
 515    elim l 0;
 516    [ simplify;
 517      intros;
 518      apply H
 519    | intros;
 520      simplify;
 521      rewrite > (getidmap_to_enter ???);
 522      cases (get_id_map_aux dm m (get_name_var a));
 523      [ simplify;
 524        reflexivity
 525      | simplify;
 526        apply (H e1 H1)
 527      ]
 528    ]
 529  ].
 530 qed.
 531
 532 lemma env_map_flatEnv_enter_aux :
 533  ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.
 534   env_to_flatEnv_inv d e map fe →
 535   env_to_flatEnv_inv (S d) (enter_env d e) (enter_map d map) fe.
 536  unfold env_to_flatEnv_inv;
 537  intros;
 538  split;
 539  [ split;
 540    [ split;
 541      [ split;
 542        [ rewrite < (checkenvmapalign_to_enter ???);
 543          apply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (H str (checkdescenter_to_checkdesc ??? H1))))))
 544        | (* TO DO !!! *) elim daemon
 545        ]
 546      | unfold check_id_map;
 547        rewrite > (getidmap_to_enter ???);
 548        apply (proj2 ?? (proj1 ?? (proj1 ?? (H str (checkdescenter_to_checkdesc ??? H1)))))
 549      ]
 550    | unfold get_id_map;
 551      rewrite > (getidmap_to_enter ???);
 552      apply (proj2 ?? (proj1 ?? (H str (checkdescenter_to_checkdesc ??? H1))))
 553    ]
 554  | unfold get_id_map;
 555    rewrite > (getidmap_to_enter ???);
 556    apply (proj2 ?? (H str (checkdescenter_to_checkdesc ??? H1)))
 557  ].
 558 qed.
 559
 560 (* aggiungi descrittore *)
 561 let rec new_map_elem_from_depth_aux (d:nat) on d ≝
 562  match d
 563   return λd.map_list d
 564  with
 565   [ O ⇒ map_nil
 566   | S n ⇒ map_cons n (None ?) (new_map_elem_from_depth_aux n)
 567   ].
 568
 569 let rec new_max_map_aux d (map:aux_map_type d) (name:aux_str_type) (max:nat) on map ≝
 570  match map with
 571   [ nil ⇒ []
 572   | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with
 573                 [ true ⇒ MAP_ELEM d name max (map_cons d (Some ? max) (cut_first_mapList (S d) (get_cur_mapElem d h) (defined_mapList_get ??)))
 574                 | false ⇒ h
 575                 ]::(new_max_map_aux d t name max)
 576   ].
 577
 578 definition add_desc_env_flatEnv_map ≝
 579 λd.λmap:aux_map_type d.λstr.
 580  match get_max_map_aux d map str with
 581   [ None ⇒ map@[ MAP_ELEM d str O (map_cons d (Some ? O) (new_map_elem_from_depth_aux d)) ]
 582   | Some x ⇒ new_max_map_aux d map str (S x)
 583   ].
 584
 585 definition add_desc_env_flatEnv_fe ≝
 586 λd.λmap:aux_map_type d.λfe.λstr.λc.λdesc.
 587  fe@[ VAR_FLAT_ELEM (STR_ID str match get_max_map_aux d map str with [ None ⇒ O | Some x ⇒ (S x)])
 588                     (DESC_ELEM c desc) ].
 589
 590 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 ≝
 591  match trsf with
 592   [ nil ⇒ (λx.x)
 593   | cons h t ⇒ (λx.(build_trasfEnv_env d t) (add_desc_env d x (fst3T ??? h) (snd3T ??? h) (thd3T ??? h)))
 594   ].
 595
 596 let rec build_trasfEnv_mapFe (d:nat) (trsf:list (Prod3T aux_str_type bool ast_type)) on trsf :
 597  Prod (aux_map_type d) aux_flatEnv_type → Prod (aux_map_type d) aux_flatEnv_type ≝
 598  match trsf with
 599   [ nil ⇒ (λx.x)
 600   | cons h t ⇒ (λx.(build_trasfEnv_mapFe d t)
 601                    (pair ?? (add_desc_env_flatEnv_map d (fst ?? x) (fst3T ??? h))
 602                             (add_desc_env_flatEnv_fe d (fst ?? x) (snd ?? x) (fst3T ??? h) (snd3T ??? h) (thd3T ??? h))))
 603   ].
 604
 605 lemma env_map_flatEnv_add_aux :
 606  ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.∀trsf.
 607   env_to_flatEnv_inv d e map fe →
 608   env_to_flatEnv_inv d
 609                      (build_trasfEnv_env d trsf e)
 610                      (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe)))
 611                      (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))).
 612  (* TO DO !!! *) elim daemon.
 613 qed.
 614
 615 lemma env_map_flatEnv_addNil_aux :
 616  ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.
 617   env_to_flatEnv_inv d e map fe →
 618   env_to_flatEnv_inv d
 619                      (build_trasfEnv_env d [] e)
 620                      (fst ?? (build_trasfEnv_mapFe d [] (pair ?? map fe)))
 621                      (snd ?? (build_trasfEnv_mapFe d [] (pair ?? map fe))).
 622  intros;
 623  simplify;
 624  apply H.
 625 qed.
 626
 627 lemma env_map_flatEnv_addSingle_aux :
 628  ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.∀name,const,desc.
 629   env_to_flatEnv_inv d e map fe →
 630   env_to_flatEnv_inv d
 631                      (add_desc_env d e name const desc)
 632                      (fst ?? (build_trasfEnv_mapFe d [ tripleT ??? name const desc ] (pair ?? map fe)))
 633                      (snd ?? (build_trasfEnv_mapFe d [ tripleT ??? name const desc ] (pair ?? map fe))).
 634  intros;
 635  apply (env_map_flatEnv_add_aux d e map fe [ tripleT ??? name const desc ]);
 636  apply H.
 637 qed.
 638
 639 lemma env_map_flatEnv_addJoin_aux :
 640  ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe:aux_flatEnv_type.∀name,const,desc,trsf.
 641   env_to_flatEnv_inv d
 642                      (build_trasfEnv_env d trsf (add_desc_env d e name const desc))
 643                      map fe →
 644   env_to_flatEnv_inv d
 645                      (build_trasfEnv_env d ([ tripleT ??? name const desc ]@trsf) e)
 646                      map fe.
 647  intros;
 648  simplify;
 649  apply H.
 650 qed.
 651
 652 lemma env_map_flatEnv_add_aux_fe_al :
 653  ∀trsf.∀d.∀m:aux_map_type d.∀a,l.
 654   snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m (a::l))) =
 655   a::(snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m l))).
 656  intro;
 657  elim trsf;
 658  [ simplify; reflexivity
 659  | simplify;
 660    elim a;
 661    simplify;
 662    rewrite > (H ????);
 663    reflexivity
 664  ].
 665 qed.
 666
 667 lemma env_map_flatEnv_add_aux_fe_l :
 668  ∀trsf.∀d.∀m:aux_map_type d.∀l.
 669   snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m l)) =
 670   l@(snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m []))).
 671  intros;
 672  elim l;
 673  [ simplify; reflexivity
 674  | rewrite > (env_map_flatEnv_add_aux_fe_al ????);
 675    rewrite > H;
 676    reflexivity
 677  ].
 678 qed.
 679
 680 lemma env_map_flatEnv_add_aux_fe :
 681  ∀d.∀map:aux_map_type d.∀fe,trsf.
 682   ∃x.fe@x = (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))).
 683  intros 3;
 684  elim fe 0;
 685  [ simplify;
 686    intro;
 687    exists;
 688    [ apply (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map [])))
 689    | reflexivity
 690    ]
 691  | intros 4;
 692    exists;
 693    [ apply (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map [])))
 694    | rewrite > (env_map_flatEnv_add_aux_fe_al trsf d map a l);
 695      rewrite > (env_map_flatEnv_add_aux_fe_l trsf d map l);
 696      rewrite < (cons_append_commute ????);
 697      reflexivity
 698    ]
 699  ].
 700 qed.
 701
 702 lemma buildtrasfenvadd_to_le :
 703  ∀d.∀m:aux_map_type d.∀fe,trsf.
 704   le_flatEnv fe (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m fe))) = true.
 705  intros 4;
 706   cases (env_map_flatEnv_add_aux_fe d m fe trsf);
 707  rewrite < H;
 708  rewrite > (le_to_leflatenv fe x);
 709  reflexivity.
 710 qed.
 711
 712 (* leave: elimina la testa (il "cur" corrente) *)
 713 let rec leave_map d (map:aux_map_type (S d)) on map ≝
 714  match map with
 715   [ nil ⇒ []
 716   | cons h t ⇒
 717    (MAP_ELEM d
 718              (get_name_mapElem (S d) h)
 719              (get_max_mapElem (S d) h)
 720              (cut_first_mapList ? (get_cur_mapElem (S d) h) (defined_mapList_get ??))
 721    )::(leave_map d t)
 722   ].
 723
 724 lemma leave_add_enter_env_aux :
 725  ∀d.∀a:aux_env_type d.∀trsf.∀c.
 726   ∃b.build_trasfEnv_env (S d) trsf (env_cons d c a) = (env_cons d b a).
 727  intros 3;
 728  elim trsf;
 729  [ simplify; exists; [ apply c | reflexivity ]
 730  | simplify; apply H
 731  ].
 732 qed.
 733
 734 lemma leave_add_enter_env :
 735  ∀d.∀e:aux_env_type d.∀trsf.
 736   leave_env d (build_trasfEnv_env (S d) trsf (enter_env d e)) = e.
 737  intros;
 738  unfold enter_env;
 739  lapply (leave_add_enter_env_aux d e trsf []);
 740  cases Hletin;
 741  rewrite > H;
 742  simplify;
 743  reflexivity.
 744 qed.
 745
 746 lemma env_map_flatEnv_leave_aux :
 747  ∀d.∀e:aux_env_type (S d).∀map:aux_map_type (S d).∀fe.∀trsf.
 748   env_to_flatEnv_inv (S d) (build_trasfEnv_env (S d) trsf e) map fe →
 749   env_to_flatEnv_inv d (leave_env d (build_trasfEnv_env (S d) trsf e)) (leave_map d map) fe.
 750  (* TO DO !!! *) elim daemon.
 751 qed.
 752
 753 lemma newid_from_init :
 754  ∀d.∀e:aux_env_type d.∀name,const,desc.
 755   ast_id d (add_desc_env d e name const desc) const desc.
 756  intros;
 757  lapply (AST_ID d (add_desc_env d e name const desc) name ?);
 758  [ elim e;
 759    simplify;
 760    rewrite > (eq_to_eqstr ?? (refl_eq ??));
 761    simplify;
 762    apply I
 763  | cut (const = get_const_desc (get_desc_env d (add_desc_env d e name const desc) name) ∧
 764         desc = get_type_desc (get_desc_env d (add_desc_env d e name const desc) name));
 765    [ rewrite > (proj1 ?? Hcut) in ⊢ (? ? ? % ?);
 766      rewrite > (proj2 ?? Hcut) in ⊢ (? ? ? ? %);
 767      apply Hletin
 768    | split;
 769      [ elim e;
 770        simplify;
 771        rewrite > (eq_to_eqstr ?? (refl_eq ??));
 772        simplify;
 773        reflexivity
 774      | elim e;
 775        simplify;
 776        rewrite > (eq_to_eqstr ?? (refl_eq ??));
 777        simplify;
 778        reflexivity
 779      ]
 780    ]
 781  ].
 782 qed.