1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
18 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
20 (* ********************************************************************** *)
22 include "compiler/environment.ma".
23 include "compiler/ast_tree.ma".
25 (* ********************** *)
26 (* GESTIONE AMBIENTE FLAT *)
27 (* ********************** *)
30 inductive var_flatElem : Type ≝
31 VAR_FLAT_ELEM: aux_strId_type → desc_elem → var_flatElem.
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 ].
36 definition aux_flatEnv_type ≝ list var_flatElem.
38 definition empty_flatEnv ≝ nil var_flatElem.
40 (* mappa: nome + max + cur *)
41 inductive map_list : nat → Type ≝
43 | map_cons: ∀n.option nat → map_list n → map_list (S n).
45 definition defined_mapList ≝
46 λd.λl:map_list d.match l with [ map_nil ⇒ False | map_cons _ _ _ ⇒ True ].
48 definition cut_first_mapList : Πd.map_list d → ? → map_list (pred d) ≝
49 λd.λl:map_list d.λp:defined_mapList ? l.
52 return λX.λY:map_list X.defined_mapList X Y → map_list (pred X)
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
58 definition get_first_mapList : Πd.map_list d → ? → option nat ≝
59 λd.λl:map_list d.λp:defined_mapList ? l.
62 return λX.λY:map_list X.defined_mapList X Y → option nat
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
68 inductive map_elem (d:nat) : Type ≝
69 MAP_ELEM: aux_str_type → nat → map_list (S d) → map_elem d.
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 ].
75 definition aux_map_type ≝ λd.list (map_elem d).
77 definition empty_map ≝ nil (map_elem O).
79 lemma defined_mapList_S_to_true :
80 ∀d.∀l:map_list (S d).defined_mapList (S d) l = True.
84 | intros; simplify; reflexivity
88 lemma defined_mapList_get :
89 ∀d.∀h:map_elem d.defined_mapList (S d) (get_cur_mapElem d h).
91 rewrite > (defined_mapList_S_to_true ? (get_cur_mapElem d h));
96 let rec get_id_map_aux d (map:aux_map_type d) (name:aux_str_type) on map : option nat ≝
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
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 ].
109 let rec get_max_map_aux d (map:aux_map_type d) (name:aux_str_type) on map ≝
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
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 ].
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 ].
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 ].
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;
134 elim (get_id_map_aux d map name) 0;
135 [ simplify; intro; destruct H
136 | simplify; intros; apply I
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 ].
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 ].
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;
152 elim (get_id_map_aux d map name) 0;
153 [ simplify; intro; apply I
154 | simplify; intros; destruct H
159 let rec get_desc_flatEnv_aux (fe:aux_flatEnv_type) (name:aux_strId_type) on fe ≝
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
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 ].
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 ].
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 ].
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;
183 elim (get_desc_flatEnv_aux fe str) 0;
184 [ simplify; intro; destruct H
185 | simplify; intros; apply I
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 ].
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 ].
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;
200 elim (get_desc_flatEnv_aux fe str) 0;
201 [ simplify; intro; apply I
202 | simplify; intros; destruct H
207 definition eq_flatEnv_elem ≝
209 [ VAR_FLAT_ELEM sId1 d1 ⇒ match e2 with
210 [ VAR_FLAT_ELEM sId2 d2 ⇒ (eqStrId_str sId1 sId2)⊗(eqDesc_elem d1 d2) ]].
212 lemma eq_to_eqflatenv : ∀e1,e2.e1 = e2 → eq_flatEnv_elem e1 e2 = true.
217 rewrite > (eq_to_eqstrid a a (refl_eq ??));
218 rewrite > (eq_to_eqdescelem d d (refl_eq ??));
222 lemma eqflatenv_to_eq : ∀e1,e2.eq_flatEnv_elem e1 e2 = true → e1 = e2.
229 rewrite > (eqstrid_to_eq a1 a (andb_true_true ?? H));
230 rewrite > (eqdescelem_to_eq d1 d (andb_true_true_r ?? H));
234 let rec le_flatEnv (fe,fe':aux_flatEnv_type) on fe ≝
237 | cons h tl ⇒ match fe' with
238 [ nil ⇒ false | cons h' tl' ⇒ (eq_flatEnv_elem h h')⊗(le_flatEnv tl tl') ]
241 lemma eq_to_leflatenv : ∀e1,e2.e1 = e2 → le_flatEnv e1 e2 = true.
247 rewrite > (eq_to_eqflatenv a a (refl_eq ??));
253 lemma leflatenv_to_le : ∀fe,fe'.le_flatEnv fe fe' = true → ∃x.fe@x=fe'.
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));
264 exists; [ apply x | reflexivity ]
269 lemma le_to_leflatenv : ∀fe,x.le_flatEnv fe (fe@x) = true.
275 rewrite > (eq_to_eqflatenv a a (refl_eq ??));
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).
286 cases (leflatenv_to_le fe fe' H);
289 [ intro; simplify in H2:(%); elim H2;
292 cases (eqStrId_str str (get_name_flatVar a));
293 [ simplify; intro; apply H3
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).
304 cases (leflatenv_to_le fe fe' H);
312 cases (eqStrId_str str (get_name_flatVar a));
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
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 ≝
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 ]).
334 let rec check_map_env_align_auxMap (d:nat) (map:map_list d) (res:nat) on map ≝
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) ]
345 (* esprimendolo in lingua umana il vincolo che controlla e':
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
353 ex: scandendo e in avanti si trova la seguente sequenza di check per il nome "pippo"
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
360 NB: e' solo meta' perche' cosi' si asserisce map ≤ env
363 let rec check_map_env_align (d:nat) (e:aux_env_type d) (map:aux_map_type d) on map ≝
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)
370 let rec check_env_map_align_aux (d:nat) (map:aux_map_type d) (le:list var_elem) on le ≝
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 ]
377 (* esprimendolo in lingua umana il vincolo che controlla e':
380 NB: e' l'altra meta' perche' cosi' asserisce env ≤ map
382 let rec check_env_map_align (de:nat) (e:aux_env_type de) (dm:nat) (map:aux_map_type dm) on e ≝
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)
389 definition env_to_flatEnv_inv ≝
390 λd.λe:aux_env_type d.λmap:aux_map_type d.λfe:aux_flatEnv_type.
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)).
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))).
403 unfold env_to_flatEnv_inv in H:(%);
405 apply (proj2 ?? (proj1 ?? Hletin));
408 lemma env_map_flatEnv_empty_aux : env_to_flatEnv_inv O empty_env empty_map empty_flatEnv.
409 unfold env_to_flatEnv_inv;
412 unfold empty_flatEnv;
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'.
424 unfold env_to_flatEnv_inv;
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)))
433 | lapply (H1 str H2);
434 rewrite < (leflatenv_to_get fe fe' ? H (proj2 ?? (proj1 ?? Hletin)));
435 apply (proj2 ?? Hletin)
439 lemma leflatenv_trans :
441 le_flatEnv fe fe' = true →
442 le_flatEnv fe' fe'' = true →
443 le_flatEnv fe fe'' = true.
445 cases (leflatenv_to_le fe ? H);
448 cases (leflatenv_to_le (fe@x) fe'' H2);
450 rewrite > associative_append;
451 apply (le_to_leflatenv fe ?).
454 (* enter: propaga in testa la vecchia testa (il "cur" precedente) *)
455 let rec enter_map d (map:aux_map_type d) on map ≝
460 (get_name_mapElem d h)
461 (get_max_mapElem d h)
463 (get_first_mapList ? (get_cur_mapElem d h) (defined_mapList_get ??))
464 (get_cur_mapElem d h))
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.
473 [ simplify; reflexivity
474 | simplify; rewrite > H; reflexivity
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.
483 unfold enter_env in H:(%);
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).
503 rewrite > (getidmap_to_enter ???);
505 cases (get_id_map_aux dm m (get_name_var a));
521 rewrite > (getidmap_to_enter ???);
522 cases (get_id_map_aux dm m (get_name_var a));
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;
542 [ rewrite < (checkenvmapalign_to_enter ???);
543 apply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (H str (checkdescenter_to_checkdesc ??? H1))))))
544 | (* TO DO !!! *) elim daemon
546 | unfold check_id_map;
547 rewrite > (getidmap_to_enter ???);
548 apply (proj2 ?? (proj1 ?? (proj1 ?? (H str (checkdescenter_to_checkdesc ??? H1)))))
551 rewrite > (getidmap_to_enter ???);
552 apply (proj2 ?? (proj1 ?? (H str (checkdescenter_to_checkdesc ??? H1))))
555 rewrite > (getidmap_to_enter ???);
556 apply (proj2 ?? (H str (checkdescenter_to_checkdesc ??? H1)))
560 (* aggiungi descrittore *)
561 let rec new_map_elem_from_depth_aux (d:nat) on d ≝
566 | S n ⇒ map_cons n (None ?) (new_map_elem_from_depth_aux n)
569 let rec new_max_map_aux d (map:aux_map_type d) (name:aux_str_type) (max:nat) on map ≝
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 ??)))
575 ]::(new_max_map_aux d t name max)
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)
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) ].
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 ≝
593 | cons h t ⇒ (λx.(build_trasfEnv_env d t) (add_desc_env d x (fst3T ??? h) (snd3T ??? h) (thd3T ??? h)))
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 ≝
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))))
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 →
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.
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 →
619 (build_trasfEnv_env d [] e)
620 (fst ?? (build_trasfEnv_mapFe d [] (pair ?? map fe)))
621 (snd ?? (build_trasfEnv_mapFe d [] (pair ?? map fe))).
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 →
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))).
635 apply (env_map_flatEnv_add_aux d e map fe [ tripleT ??? name const desc ]);
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.
642 (build_trasfEnv_env d trsf (add_desc_env d e name const desc))
645 (build_trasfEnv_env d ([ tripleT ??? name const desc ]@trsf) e)
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))).
658 [ simplify; reflexivity
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 []))).
673 [ simplify; reflexivity
674 | rewrite > (env_map_flatEnv_add_aux_fe_al ????);
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))).
688 [ apply (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map [])))
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 ????);
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.
706 cases (env_map_flatEnv_add_aux_fe d m fe trsf);
708 rewrite > (le_to_leflatenv fe x);
712 (* leave: elimina la testa (il "cur" corrente) *)
713 let rec leave_map d (map:aux_map_type (S d)) on map ≝
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 ??))
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).
729 [ simplify; exists; [ apply c | reflexivity ]
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.
739 lapply (leave_add_enter_env_aux d e trsf []);
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.
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.
757 lapply (AST_ID d (add_desc_env d e name const desc) name ?);
760 rewrite > (eq_to_eqstr ?? (refl_eq ??));
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 ⊢ (? ? ? ? %);
771 rewrite > (eq_to_eqstr ?? (refl_eq ??));
776 rewrite > (eq_to_eqstr ?? (refl_eq ??));