helm/software/matita/contribs/assembly/compiler/env_to_flatenv1.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
  24 (* ********************** *)
  25 (* GESTIONE AMBIENTE FLAT *)
  26 (* ********************** *)
  27
  28 (* ambiente flat *)
  29 inductive var_flatElem : Type ≝
  30 VAR_FLAT_ELEM: aux_strId_type → desc_elem → var_flatElem.
  31
  32 definition get_name_flatVar ≝ λv:var_flatElem.match v with [ VAR_FLAT_ELEM n _ ⇒ n ].
  33 definition get_desc_flatVar ≝ λv:var_flatElem.match v with [ VAR_FLAT_ELEM _ d ⇒ d ].
  34
  35 definition aux_flatEnv_type ≝ list var_flatElem.
  36
  37 definition empty_flatEnv ≝ nil var_flatElem.
  38
  39 (* mappa: nome + max + cur *)
  40 inductive n_list : nat → Type ≝
  41   n_nil: n_list O
  42 | n_cons: ∀n.option nat → n_list n → n_list (S n).
  43
  44 definition defined_nList ≝
  45 λd.λl:n_list d.match l with [ n_nil ⇒ False | n_cons _ _ _ ⇒ True ].
  46
  47 definition cut_first_nList : Πd.n_list d → ? → n_list (pred d) ≝
  48 λd.λl:n_list d.λp:defined_nList ? l.
  49  let value ≝
  50   match l
  51    return λX.λY:n_list X.defined_nList X Y → n_list (pred X)
  52   with
  53    [ n_nil ⇒ λp:defined_nList O n_nil.False_rect ? p
  54    | n_cons n h t ⇒ λp:defined_nList (S n) (n_cons n h t).t
  55    ] p in value.
  56
  57 definition get_first_nList : Πd.n_list d → ? → option nat ≝
  58 λd.λl:n_list d.λp:defined_nList ? l.
  59  let value ≝
  60   match l
  61    return λX.λY:n_list X.defined_nList X Y → option nat
  62   with
  63    [ n_nil ⇒ λp:defined_nList O n_nil.False_rect ? p
  64    | n_cons n h t ⇒ λp:defined_nList (S n) (n_cons n h t).h
  65    ] p in value.
  66
  67 inductive map_elem (d:nat) : Type ≝
  68 MAP_ELEM: aux_str_type → nat → n_list (S d) → map_elem d.
  69
  70 definition get_name_mapElem ≝ λd.λm:map_elem d.match m with [ MAP_ELEM n _ _ ⇒ n ].
  71 definition get_max_mapElem ≝ λd.λm:map_elem d.match m with [ MAP_ELEM _ m _ ⇒ m ].
  72 definition get_cur_mapElem ≝ λd.λm:map_elem d.match m with [ MAP_ELEM _ _ c ⇒ c ].
  73
  74 definition aux_map_type ≝ λd.list (map_elem d).
  75
  76 definition empty_map ≝ nil (map_elem O).
  77
  78 theorem defined_nList_S_to_true :
  79 ∀d.∀l:n_list (S d).defined_nList (S d) l = True.
  80  intros;
  81  inversion l;
  82   [ intros; destruct H
  83   | intros; simplify; reflexivity
  84   ]
  85 qed.
  86
  87 lemma defined_get_id :
  88  ∀d.∀h:map_elem d.defined_nList (S d) (get_cur_mapElem d h).
  89  intros 2;
  90  rewrite > (defined_nList_S_to_true ? (get_cur_mapElem d h));
  91  apply I.
  92 qed.
  93
  94 (* get_id *)
  95 let rec get_id_map_aux d (map:aux_map_type d) (name:aux_str_type) on map : option nat ≝
  96  match map with
  97   [ nil ⇒ None ?
  98   | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with
  99                 [ true ⇒ get_first_nList (S d) (get_cur_mapElem d h) (defined_get_id ??)
 100                 | false ⇒ get_id_map_aux d t name
 101                 ]
 102   ].
 103
 104 definition get_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
 105  match get_id_map_aux d map name with [ None ⇒ O | Some x ⇒ x ].
 106
 107 (* get_max *)
 108 let rec get_max_map_aux d (map:aux_map_type d) (name:aux_str_type) on map ≝
 109  match map with
 110   [ nil ⇒ None ?
 111   | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with
 112                 [ true ⇒ Some ? (get_max_mapElem d h)
 113                 | false ⇒ get_max_map_aux d t name
 114                 ]
 115   ].
 116
 117 definition get_max_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
 118  match get_max_map_aux d map name with [ None ⇒ O | Some x ⇒ x ].
 119
 120 (* check_id *)
 121 definition check_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
 122  match get_id_map_aux d map name with [ None ⇒ False | Some _ ⇒ True ].
 123
 124 definition checkb_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
 125  match get_id_map_aux d map name with [ None ⇒ false | Some _ ⇒ true ].
 126
 127 lemma checkbidmap_to_checkidmap : ∀d.∀map:aux_map_type d.∀name.checkb_id_map d map name = true → check_id_map d map name.
 128  unfold checkb_id_map;
 129  unfold check_id_map;
 130  intros 3;
 131  elim (get_id_map_aux d map name) 0;
 132  [ simplify; intro; destruct H
 133  | simplify; intros; apply I
 134  ].
 135 qed.
 136
 137 definition checknot_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
 138  match get_id_map_aux d map name with [ None ⇒ True | Some _ ⇒ False ].
 139
 140 definition checknotb_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 lemma checknotbidmap_to_checknotidmap : ∀d.∀map:aux_map_type d.∀name.checknotb_id_map d map name = true → checknot_id_map d map name.
 144  unfold checknotb_id_map;
 145  unfold checknot_id_map;
 146  intros 3;
 147  elim (get_id_map_aux d map name) 0;
 148  [ simplify; intro; apply I
 149  | simplify; intros; destruct H
 150  ].
 151 qed.
 152
 153 (* get_desc *)
 154 let rec get_desc_flatEnv_aux (fe:aux_flatEnv_type) (name:aux_strId_type) on fe ≝
 155  match fe with
 156   [ nil ⇒ None ?
 157   | cons h t ⇒ match eqStrId_str name (get_name_flatVar h) with
 158                [ true ⇒ Some ? (get_desc_flatVar h)
 159                | false ⇒ get_desc_flatEnv_aux t name
 160                ]
 161   ].
 162
 163 definition get_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
 164  match get_desc_flatEnv_aux fe str with
 165   [ None ⇒ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) | Some x ⇒ x ].
 166
 167 definition check_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
 168  match get_desc_flatEnv_aux fe str with [ None ⇒ False | Some _ ⇒ True ].
 169
 170 definition checkb_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
 171  match get_desc_flatEnv_aux fe str with [ None ⇒ false | Some _ ⇒ true ].
 172
 173 lemma checkbdescflatenv_to_checkdescflatenv : ∀fe,str.checkb_desc_flatEnv fe str = true → check_desc_flatEnv fe str.
 174  unfold checkb_desc_flatEnv;
 175  unfold check_desc_flatEnv;
 176  intros 2;
 177  elim (get_desc_flatEnv_aux fe str) 0;
 178  [ simplify; intro; destruct H
 179  | simplify; intros; apply I
 180  ].
 181 qed.
 182
 183 definition checknot_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
 184  match get_desc_flatEnv_aux fe str with [ None ⇒ True | Some _ ⇒ False ].
 185
 186 definition checknotb_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
 187  match get_desc_flatEnv_aux fe str with [ None ⇒ true | Some _ ⇒ false ].
 188
 189 lemma checknotbdescflatenv_to_checknotdescflatenv : ∀fe,str.checknotb_desc_flatEnv fe str = true → checknot_desc_flatEnv fe str.
 190  unfold checknotb_desc_flatEnv;
 191  unfold checknot_desc_flatEnv;
 192  intros 2;
 193  elim (get_desc_flatEnv_aux fe str) 0;
 194  [ simplify; intro; apply I
 195  | simplify; intros; destruct H
 196  ].
 197 qed.
 198
 199 (* fe <= fe' *)
 200 definition eq_flatEnv_elem ≝
 201 λe1,e2.match e1 with
 202  [ VAR_FLAT_ELEM sId1 d1 ⇒ match e2 with
 203   [ VAR_FLAT_ELEM sId2 d2 ⇒ (eqStrId_str sId1 sId2)⊗(eqDesc_elem d1 d2) ]].
 204
 205 lemma eq_to_eqflatenv : ∀e1,e2.e1 = e2 → eq_flatEnv_elem e1 e2 = true.
 206  intros 3;
 207  rewrite < H;
 208  elim e1;
 209  simplify;
 210  rewrite > (eq_to_eqstrid a a (refl_eq ??));
 211  rewrite > (eq_to_eqdescelem d d (refl_eq ??));
 212  reflexivity.
 213 qed.
 214
 215 lemma eqflatenv_to_eq : ∀e1,e2.eq_flatEnv_elem e1 e2 = true → e1 = e2.
 216  intros 2;
 217  elim e1 0;
 218  elim e2 0;
 219  intros 4;
 220  simplify;
 221  intro;
 222  rewrite > (eqstrid_to_eq a1 a (andb_true_true ?? H));
 223  rewrite > (eqdescelem_to_eq d1 d (andb_true_true_r ?? H));
 224  reflexivity.
 225 qed.
 226
 227 let rec le_flatEnv (fe,fe':aux_flatEnv_type) on fe ≝
 228 match fe with
 229   [ nil ⇒ true
 230   | cons h tl ⇒ match fe' with
 231    [ nil ⇒ false | cons h' tl' ⇒ (eq_flatEnv_elem h h')⊗(le_flatEnv tl tl') ]
 232   ].
 233
 234 lemma eq_to_leflatenv : ∀e1,e2.e1 = e2 → le_flatEnv e1 e2 = true.
 235  intros 3;
 236  rewrite < H;
 237  elim e1;
 238  [ reflexivity
 239  | simplify;
 240    rewrite > (eq_to_eqflatenv a a (refl_eq ??));
 241    rewrite > H1;
 242    reflexivity
 243  ].
 244 qed.
 245
 246 lemma leflatEnv_to_le : ∀fe,fe'.le_flatEnv fe fe' = true → ∃x.fe@x=fe'.
 247  intro;
 248  elim fe 0;
 249  [ intros; exists; [ apply fe' | reflexivity ]
 250  | intros 4; elim fe';
 251    [ simplify in H1:(%); destruct H1
 252    | simplify in H2:(%);
 253      rewrite < (eqflatenv_to_eq a a1 (andb_true_true ?? H2));
 254      cases (H l1 (andb_true_true_r ?? H2));
 255      simplify;
 256      rewrite < H3;
 257      exists; [ apply x | reflexivity ]
 258    ]
 259  ].
 260 qed.
 261
 262 lemma le_to_leflatenv : ∀fe,x.le_flatEnv fe (fe@x) = true.
 263  intros;
 264  elim fe;
 265  [ simplify;
 266    reflexivity
 267  | simplify;
 268    rewrite > (eq_to_eqflatenv a a (refl_eq ??));
 269    rewrite > H;
 270    reflexivity
 271  ].
 272 qed.
 273
 274 lemma leflatenv_to_check : ∀fe,fe',str.
 275  (le_flatEnv fe fe' = true) →
 276  (check_desc_flatEnv fe str) →
 277  (check_desc_flatEnv fe' str).
 278  intros 4;
 279  cases (leflatEnv_to_le fe fe' H);
 280  rewrite < H1;
 281  elim fe 0;
 282  [ intro; simplify in H2:(%); elim H2;
 283  | intros 3;
 284    simplify;
 285    cases (eqStrId_str str (get_name_flatVar a));
 286    [ simplify; intro; apply H3
 287    | simplify; apply H2
 288    ]
 289  ].
 290 qed.
 291
 292 lemma leflatenv_to_get : ∀fe,fe',str.
 293  (le_flatEnv fe fe' = true) →
 294  (check_desc_flatEnv fe str) →
 295  (get_desc_flatEnv fe str = get_desc_flatEnv fe' str).
 296  intros 4;
 297  cases (leflatEnv_to_le fe fe' H);
 298  rewrite < H1;
 299  elim fe 0;
 300  [ intro;
 301    simplify in H2:(%);
 302    elim H2
 303  | simplify;
 304    intros 2;
 305    cases (eqStrId_str str (get_name_flatVar a));
 306    [ simplify;
 307      intros;
 308      reflexivity
 309    | simplify;
 310      unfold check_desc_flatEnv;
 311      unfold get_desc_flatEnv;
 312      cases (get_desc_flatEnv_aux l str);
 313      [ simplify; intros; elim H3
 314      | simplify; intros; rewrite < (H2 H3); reflexivity
 315      ]
 316    ]
 317  ].
 318 qed.
 319
 320 (* invariante *)
 321 definition env_to_flatEnv_inv ≝
 322  λd.λe:aux_env_type.λmap:aux_map_type d.λfe:aux_flatEnv_type.
 323   ∀str.
 324    check_desc_env e str →
 325    (check_id_map d map str ∧
 326     check_desc_flatEnv fe (STR_ID str (get_id_map d map str)) ∧
 327     get_desc_env e str = get_desc_flatEnv fe (STR_ID str (get_id_map d map str))).
 328
 329 lemma inv_to_checkdescflatenv :
 330  ∀d.∀e.∀map:aux_map_type d.∀fe.
 331  env_to_flatEnv_inv d e map fe →
 332  (∀str.check_desc_env e str → check_desc_flatEnv fe (STR_ID str (get_id_map d map str))).
 333  intros 7;
 334  unfold env_to_flatEnv_inv in H:(%);
 335  lapply (H str H1);
 336  apply (proj2 ?? (proj1 ?? Hletin));
 337 qed.
 338
 339 lemma env_map_flatEnv_empty_aux : env_to_flatEnv_inv O empty_env empty_map empty_flatEnv.
 340  unfold env_to_flatEnv_inv;
 341  unfold empty_env;
 342  unfold empty_map;
 343  unfold empty_flatEnv;
 344  simplify;
 345  intros;
 346  split;
 347  [ split; apply H | reflexivity ].
 348 qed.
 349
 350 lemma leflatenv_to_inv :
 351  ∀d.∀e.∀map:aux_map_type d.∀fe,fe'.
 352   le_flatEnv fe fe' = true →
 353   env_to_flatEnv_inv d e map fe →
 354   env_to_flatEnv_inv d e map fe'.
 355  intros 6;
 356  unfold env_to_flatEnv_inv;
 357  intros;
 358  split;
 359  [ split;
 360    [ lapply (H1 str H2);
 361      apply (proj1 ?? (proj1 ?? Hletin))
 362    | lapply (H1 str H2);
 363      apply (leflatenv_to_check fe fe' ? H (proj2 ?? (proj1 ?? Hletin)))
 364    ]
 365  | lapply (H1 str H2);
 366    rewrite < (leflatenv_to_get fe fe' ? H (proj2 ?? (proj1 ?? Hletin)));
 367    apply (proj2 ?? Hletin)
 368  ].
 369 qed.
 370
 371 (* enter: propaga in testa la vecchia testa (il "cur" precedente) *)
 372 let rec enter_map d (map:aux_map_type d) on map ≝
 373  match map with
 374   [ nil ⇒ []
 375   | cons h t ⇒
 376    (MAP_ELEM (S d)
 377              (get_name_mapElem d h)
 378              (get_max_mapElem d h)
 379              (n_cons (S d)
 380                      (get_first_nList ? (get_cur_mapElem d h) (defined_get_id ??))
 381                      (get_cur_mapElem d h))
 382    )::(enter_map d t)
 383   ].
 384
 385 lemma getidmap_to_enter :
 386  ∀d.∀m:aux_map_type d.∀str.
 387   get_id_map_aux (S d) (enter_map d m) str = get_id_map_aux d m str.
 388  intros;
 389  elim m;
 390  [ simplify; reflexivity
 391  | simplify; rewrite > H; reflexivity
 392  ]
 393 qed.
 394
 395 lemma env_map_flatEnv_enter_aux :
 396  ∀d.∀e.∀map:aux_map_type d.∀fe.
 397   env_to_flatEnv_inv d e map fe → env_to_flatEnv_inv (S d) (enter_env e) (enter_map d map) fe.
 398  intros 3;
 399  unfold enter_env;
 400  unfold empty_env;
 401  unfold env_to_flatEnv_inv;
 402  simplify;
 403  elim e 0;
 404  [ elim map 0;
 405    [ simplify; intros; split;
 406      [ apply (proj1 ?? (H str H1)) | apply (proj2 ?? (H str H1)); ]
 407    | simplify; intros; split;
 408      [ rewrite > (getidmap_to_enter d l str); apply (proj1 ?? (H1 str H2))
 409      | rewrite > (getidmap_to_enter d l str); apply (proj2 ?? (H1 str H2))
 410      ]
 411    ]
 412  | elim map 0;
 413    [ simplify; intros; split;
 414      [ apply (proj1 ?? (H1 str H2)) | apply (proj2 ?? (H1 str H2)) ]
 415    | simplify; intros; split;
 416      [ rewrite > (getidmap_to_enter d l str); apply (proj1 ?? (H2 str H3))
 417      | rewrite > (getidmap_to_enter d l str); apply (proj2 ?? (H2 str H3))
 418      ]
 419    ]
 420  ].
 421 qed.
 422
 423 (* leave: elimina la testa (il "cur" corrente) *)
 424 let rec leave_map d (map:aux_map_type (S d)) on map ≝
 425  match map with
 426   [ nil ⇒ []
 427   | cons h t ⇒
 428    (MAP_ELEM d
 429              (get_name_mapElem (S d) h)
 430              (get_max_mapElem (S d) h)
 431              (cut_first_nList ? (get_cur_mapElem (S d) h) (defined_get_id ??))
 432    )::(leave_map d t)
 433   ].
 434
 435 (* aggiungi descrittore *)
 436 let rec new_map_elem_from_depth_aux (d:nat) on d ≝
 437  match d
 438   return λd.n_list d
 439  with
 440   [ O ⇒ n_nil
 441   | S n ⇒ n_cons n (None ?) (new_map_elem_from_depth_aux n)
 442   ].
 443
 444 let rec new_max_map_aux d (map:aux_map_type d) (name:aux_str_type) (max:nat) on map ≝
 445  match map with
 446   [ nil ⇒ []
 447   | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with
 448                 [ true ⇒ MAP_ELEM d name max (n_cons d (Some ? max) (cut_first_nList (S d) (get_cur_mapElem d h) (defined_get_id ??)))
 449                 | false ⇒ h
 450                 ]::(new_max_map_aux d t name max)
 451   ].
 452
 453 definition add_desc_env_flatEnv_map ≝
 454 λd.λmap:aux_map_type d.λstr.
 455  match get_max_map_aux d map str with
 456   [ None ⇒ map@[ MAP_ELEM d str O (n_cons d (Some ? O) (new_map_elem_from_depth_aux d)) ]
 457   | Some x ⇒ new_max_map_aux d map str (S x)
 458   ].
 459
 460 definition add_desc_env_flatEnv_fe ≝
 461 λd.λmap:aux_map_type d.λfe.λstr.λc.λdesc.
 462  fe@[ VAR_FLAT_ELEM (STR_ID str match get_max_map_aux d map str with [ None ⇒ O | Some x ⇒ (S x)])
 463                     (DESC_ELEM c desc) ].
 464
 465 let rec build_trasfEnv_env (trsf:list (Prod3T aux_str_type bool ast_type)) e on trsf ≝
 466  match trsf with
 467   [ nil ⇒ e
 468   | cons h t ⇒ build_trasfEnv_env t (add_desc_env e (fst3T ??? h) (snd3T ??? h) (thd3T ??? h))
 469   ].
 470
 471 let rec build_trasfEnv_mapFe (trasf:list ?) d (mfe:Prod (aux_map_type d) aux_flatEnv_type) on trasf ≝
 472  match trasf with
 473   [ nil ⇒ mfe
 474   | cons h t ⇒
 475    build_trasfEnv_mapFe t d (pair ?? (add_desc_env_flatEnv_map d (fst ?? mfe) (fst3T ??? h))
 476                                      (add_desc_env_flatEnv_fe d (fst ?? mfe) (snd ?? mfe) (fst3T ??? h) (snd3T ??? h) (thd3T ??? h)))
 477   ].
 478
 479 (* avanzamento delle dimostrazioni *)
 480 axiom env_map_flatEnv_add_aux :
 481  ∀d.∀e.∀map:aux_map_type d.∀fe.∀trsf.
 482   env_to_flatEnv_inv d e map fe →
 483   env_to_flatEnv_inv d
 484                      (build_trasfEnv_env trsf e)
 485                      (fst ?? (build_trasfEnv_mapFe trsf d (pair ?? map fe)))
 486                      (snd ?? (build_trasfEnv_mapFe trsf d (pair ?? map fe))).
 487
 488 axiom env_map_flatEnv_add_aux_fe :
 489  ∀d.∀map:aux_map_type d.∀fe,trsf.
 490   ∃x.fe@x = (snd ?? (build_trasfEnv_mapFe trsf d (pair ?? map fe))).
 491
 492 lemma buildtrasfenvadd_to_le :
 493  ∀d.∀m:aux_map_type d.∀fe,trsf.
 494   le_flatEnv fe (snd ?? (build_trasfEnv_mapFe trsf d (pair ?? m fe))) = true.
 495  intros 4;
 496   cases (env_map_flatEnv_add_aux_fe d m fe trsf);
 497  rewrite < H;
 498  rewrite > (le_to_leflatenv fe x);
 499  reflexivity.
 500 qed.
 501
 502 axiom env_map_flatEnv_leave_aux :
 503  ∀d.∀e.∀map:aux_map_type (S d).∀fe.
 504   env_to_flatEnv_inv (S d) e map fe →
 505   env_to_flatEnv_inv d
 506                      (leave_env e)
 507                      (leave_map d map)
 508                      fe.
 509
 510 (* avanzamento congiunto oggetti + dimostrazioni *)
 511 inductive env_map_flatEnv :
 512      Πd.Πe.Πm:aux_map_type d.Πfe,fe'.
 513      env_to_flatEnv_inv d e m fe' →
 514      le_flatEnv fe fe' = true → Type ≝
 515   ENV_MAP_FLATENV_EMPTY: env_map_flatEnv O
 516                                          empty_env
 517                                          empty_map
 518                                          empty_flatEnv
 519                                          empty_flatEnv
 520                                          env_map_flatEnv_empty_aux
 521                                          (eq_to_leflatenv ?? (refl_eq ??))
 522 | ENV_MAP_FLATENV_ENTER: ∀d,e.∀m:aux_map_type d.∀fe,fe'.
 523                       ∀dimInv:env_to_flatEnv_inv d e m fe'.
 524                       ∀dimLe:le_flatEnv fe fe' = true.
 525                          env_map_flatEnv d e m fe fe' dimInv dimLe →
 526                          env_map_flatEnv (S d)
 527                                          (enter_env e)
 528                                          (enter_map d m)
 529                                          fe'
 530                                          fe'
 531                                          (env_map_flatEnv_enter_aux d e m fe' dimInv)
 532                                          (eq_to_leflatenv ?? (refl_eq ??))
 533 | ENV_MAP_FLATENV_ADD: ∀d,e.∀m:aux_map_type d.∀fe,fe'.
 534                     ∀dimInv:env_to_flatEnv_inv d e m fe'.
 535                     ∀dimLe:le_flatEnv fe fe' = true.∀trsf.
 536                        env_map_flatEnv d e m fe fe' dimInv dimLe →
 537                        env_map_flatEnv d
 538                                        (build_trasfEnv_env trsf e)
 539                                        (fst ?? (build_trasfEnv_mapFe trsf d (pair ?? m fe')))
 540                                        fe'
 541                                        (snd ?? (build_trasfEnv_mapFe trsf d (pair ?? m fe')))
 542                                        (env_map_flatEnv_add_aux d e m fe' trsf dimInv)
 543                                        (buildtrasfenvadd_to_le d m fe' trsf)
 544 | ENV_MAP_FLATENV_LEAVE: ∀d,e.∀m:aux_map_type (S d).∀fe,fe'.
 545                       ∀dimInv:env_to_flatEnv_inv (S d) e m fe'.
 546                       ∀dimLe:le_flatEnv fe fe' = true.
 547                          env_map_flatEnv (S d) e m fe fe' dimInv dimLe →
 548                          env_map_flatEnv d
 549                                          (leave_env e)
 550                                          (leave_map d m)
 551                                          fe'
 552                                          fe'
 553                                          (env_map_flatEnv_leave_aux d e m fe' dimInv)
 554                                          (eq_to_leflatenv ?? (refl_eq ??)).