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