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
206 (* leave: elimina la testa (il "cur" corrente) *)
207 let rec leave_map d (map:aux_map_type (S d)) on map ≝
212 (get_name_mapElem (S d) h)
213 (get_max_mapElem (S d) h)
214 (cut_first_mapList ? (get_cur_mapElem (S d) h) (defined_mapList_get ??))
218 (* enter: propaga in testa la vecchia testa (il "cur" precedente) *)
219 let rec enter_map d (map:aux_map_type d) on map ≝
224 (get_name_mapElem d h)
225 (get_max_mapElem d h)
227 (get_first_mapList ? (get_cur_mapElem d h) (defined_mapList_get ??))
228 (get_cur_mapElem d h))
232 (* aggiungi descrittore *)
233 let rec new_map_elem_from_depth_aux (d:nat) on d ≝
238 | S n ⇒ map_cons n (None ?) (new_map_elem_from_depth_aux n)
241 let rec new_max_map_aux d (map:aux_map_type d) (name:aux_str_type) (max:nat) on map ≝
244 | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with
245 [ true ⇒ (MAP_ELEM d name max (map_cons d (Some ? max) (cut_first_mapList (S d) (get_cur_mapElem d h) (defined_mapList_get ??))))::t
246 | false ⇒ h::(new_max_map_aux d t name max)
250 definition add_desc_env_flatEnv_map ≝
251 λd.λmap:aux_map_type d.λstr.
252 match get_max_map_aux d map str with
253 [ None ⇒ map@[ MAP_ELEM d str O (map_cons d (Some ? O) (new_map_elem_from_depth_aux d)) ]
254 | Some x ⇒ new_max_map_aux d map str (S x)
257 definition add_desc_env_flatEnv_fe ≝
258 λd.λmap:aux_map_type d.λfe.λstr.λc.λdesc.
259 fe@[ VAR_FLAT_ELEM (STR_ID str match get_max_map_aux d map str with [ None ⇒ O | Some x ⇒ (S x)])
260 (DESC_ELEM c desc) ].
262 let rec build_trasfEnv_env (d:nat) (trsf:list (Prod3T aux_str_type bool ast_type)) on trsf : aux_env_type d → aux_env_type d ≝
265 | cons h t ⇒ (λx.(build_trasfEnv_env d t) (add_desc_env d x (fst3T ??? h) (snd3T ??? h) (thd3T ??? h)))
268 let rec build_trasfEnv_mapFe (d:nat) (trsf:list (Prod3T aux_str_type bool ast_type)) on trsf :
269 Prod (aux_map_type d) aux_flatEnv_type → Prod (aux_map_type d) aux_flatEnv_type ≝
272 | cons h t ⇒ (λx.(build_trasfEnv_mapFe d t)
273 (pair ?? (add_desc_env_flatEnv_map d (fst ?? x) (fst3T ??? h))
274 (add_desc_env_flatEnv_fe d (fst ?? x) (snd ?? x) (fst3T ??? h) (snd3T ??? h) (thd3T ??? h))))
277 (* ********************************************* *)
280 definition eq_flatEnv_elem ≝
282 [ VAR_FLAT_ELEM sId1 d1 ⇒ match e2 with
283 [ VAR_FLAT_ELEM sId2 d2 ⇒ (eqStrId_str sId1 sId2)⊗(eqDesc_elem d1 d2) ]].
285 lemma eq_to_eqflatenv : ∀e1,e2.e1 = e2 → eq_flatEnv_elem e1 e2 = true.
290 rewrite > (eq_to_eqstrid a a (refl_eq ??));
291 rewrite > (eq_to_eqdescelem d d (refl_eq ??));
295 lemma eqflatenv_to_eq : ∀e1,e2.eq_flatEnv_elem e1 e2 = true → e1 = e2.
302 rewrite > (eqstrid_to_eq a1 a (andb_true_true ?? H));
303 rewrite > (eqdescelem_to_eq d1 d (andb_true_true_r ?? H));
307 let rec le_flatEnv (fe,fe':aux_flatEnv_type) on fe ≝
310 | cons h tl ⇒ match fe' with
311 [ nil ⇒ false | cons h' tl' ⇒ (eq_flatEnv_elem h h')⊗(le_flatEnv tl tl') ]
314 lemma eq_to_leflatenv : ∀e1,e2.e1 = e2 → le_flatEnv e1 e2 = true.
320 rewrite > (eq_to_eqflatenv a a (refl_eq ??));
326 lemma leflatenv_to_le : ∀fe,fe'.le_flatEnv fe fe' = true → ∃x.fe@x=fe'.
329 [ intros; exists; [ apply fe' | reflexivity ]
330 | intros 4; elim fe';
331 [ simplify in H1:(%); destruct H1
332 | simplify in H2:(%);
333 rewrite < (eqflatenv_to_eq a a1 (andb_true_true ?? H2));
334 cases (H l1 (andb_true_true_r ?? H2));
337 exists; [ apply x | reflexivity ]
342 lemma le_to_leflatenv : ∀fe,x.le_flatEnv fe (fe@x) = true.
348 rewrite > (eq_to_eqflatenv a a (refl_eq ??));
354 lemma leflatenv_to_check :
356 (le_flatEnv fe fe' = true) →
357 (check_desc_flatEnv fe str) →
358 (check_desc_flatEnv fe' str).
360 cases (leflatenv_to_le fe fe' H);
363 [ intro; simplify in H2:(%); elim H2;
366 cases (eqStrId_str str (get_name_flatVar a));
367 [ simplify; intro; apply H3
373 lemma leflatenv_to_get :
375 (le_flatEnv fe fe' = true) →
376 (check_desc_flatEnv fe str) →
377 (get_desc_flatEnv fe str = get_desc_flatEnv fe' str).
379 cases (leflatenv_to_le fe fe' H);
387 cases (eqStrId_str str (get_name_flatVar a));
392 unfold check_desc_flatEnv;
393 unfold get_desc_flatEnv;
394 cases (get_desc_flatEnv_aux l str);
395 [ simplify; intros; elim H3
396 | simplify; intros; rewrite < (H2 H3); reflexivity
402 lemma leflatenv_trans :
404 le_flatEnv fe fe' = true →
405 le_flatEnv fe' fe'' = true →
406 le_flatEnv fe fe'' = true.
408 cases (leflatenv_to_le fe ? H);
411 cases (leflatenv_to_le (fe@x) fe'' H2);
413 rewrite > associative_append;
414 apply (le_to_leflatenv fe ?).
417 lemma env_map_flatEnv_add_aux_fe_al :
418 ∀trsf.∀d.∀m:aux_map_type d.∀a,l.
419 snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m (a::l))) =
420 a::(snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m l))).
423 [ simplify; reflexivity
432 lemma env_map_flatEnv_add_aux_fe_l :
433 ∀trsf.∀d.∀m:aux_map_type d.∀l.
434 snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m l)) =
435 l@(snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m []))).
438 [ simplify; reflexivity
439 | rewrite > (env_map_flatEnv_add_aux_fe_al ????);
445 lemma env_map_flatEnv_add_aux_fe :
446 ∀d.∀map:aux_map_type d.∀fe,trsf.
447 ∃x.fe@x = (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))).
453 [ apply (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map [])))
458 [ apply (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map [])))
459 | rewrite > (env_map_flatEnv_add_aux_fe_al trsf d map a l);
460 rewrite > (env_map_flatEnv_add_aux_fe_l trsf d map l);
461 rewrite < (cons_append_commute ????);
467 lemma buildtrasfenvadd_to_le :
468 ∀d.∀m:aux_map_type d.∀fe,trsf.
469 le_flatEnv fe (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m fe))) = true.
471 cases (env_map_flatEnv_add_aux_fe d m fe trsf);
473 rewrite > (le_to_leflatenv fe x);
477 (* ********************************************* *)
480 lemma leave_env_enter_env : ∀d.∀e:aux_env_type d.leave_env d (enter_env d e) = e.
486 lemma leave_map_enter_map : ∀d.∀map. leave_map d (enter_map d map) = map.
498 lemma leave_add_enter_env_aux :
499 ∀d.∀a:aux_env_type d.∀trsf.∀c.
500 ∃b.build_trasfEnv_env (S d) trsf (env_cons d c a) = (env_cons d b a).
503 [ simplify; exists; [ apply c | reflexivity ]
508 lemma leave_add_enter_env :
509 ∀d.∀e:aux_env_type d.∀trsf.
510 leave_env d (build_trasfEnv_env (S d) trsf (enter_env d e)) = e.
513 lapply (leave_add_enter_env_aux d e trsf []);
520 (* ********************************************* *)
522 (* invariante a un livello *)
523 definition env_to_flatEnv_inv_one_level ≝
524 λd.λe:aux_env_type d.λmap:aux_map_type d.λfe:aux_flatEnv_type.
526 check_desc_env d e str →
527 check_id_map d map str ∧
528 check_desc_flatEnv fe (STR_ID str (get_id_map d map str)) ∧
529 get_desc_env d e str = get_desc_flatEnv fe (STR_ID str (get_id_map d map str)).
531 (* invariante su tutti i livelli *)
532 let rec env_to_flatEnv_inv (d:nat) : aux_env_type d → aux_map_type d → aux_flatEnv_type → Prop ≝
534 return λd.aux_env_type d → aux_map_type d → aux_flatEnv_type → Prop
536 [ O ⇒ λe:aux_env_type O.λmap:aux_map_type O.λfe:aux_flatEnv_type.
537 env_to_flatEnv_inv_one_level O e map fe
538 | S n ⇒ λe:aux_env_type (S n).λmap:aux_map_type (S n).λfe:aux_flatEnv_type.
539 env_to_flatEnv_inv_one_level (S n) e map fe ∧
540 env_to_flatEnv_inv n (leave_env n e) (leave_map n map) fe
543 (* invariante full -> invariante a un livello *)
544 lemma env_to_flatEnv_inv_last :
545 ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.
546 env_to_flatEnv_inv d e map fe →
547 env_to_flatEnv_inv_one_level d e map fe.
557 (* invariante caso base *)
558 lemma env_map_flatEnv_empty_aux : env_to_flatEnv_inv O empty_env empty_map empty_flatEnv.
559 unfold env_to_flatEnv_inv;
562 unfold empty_flatEnv;
568 (* invariante & leflatenv *)
569 lemma leflatenv_to_inv :
570 ∀d.∀e.∀map:aux_map_type d.∀fe,fe'.
571 le_flatEnv fe fe' = true →
572 env_to_flatEnv_inv d e map fe →
573 env_to_flatEnv_inv d e map fe'.
577 unfold env_to_flatEnv_inv_one_level;
581 [ lapply (H1 str H2);
582 apply (proj1 ?? (proj1 ?? Hletin))
583 | lapply (H1 str H2);
584 apply (leflatenv_to_check fe fe' ? H (proj2 ?? (proj1 ?? Hletin)))
586 | lapply (H1 str H2);
587 rewrite < (leflatenv_to_get fe fe' ? H (proj2 ?? (proj1 ?? Hletin)));
588 apply (proj2 ?? Hletin)
590 | simplify in H2 ⊢ %;
593 [ unfold env_to_flatEnv_inv_one_level;
597 [ lapply (H3 str H5);
598 apply (proj1 ?? (proj1 ?? Hletin))
599 | lapply (H3 str H5);
600 apply (leflatenv_to_check fe fe' ? H1 (proj2 ?? (proj1 ?? Hletin)))
602 | lapply (H3 str H5);
603 rewrite < (leflatenv_to_get fe fe' ? H1 (proj2 ?? (proj1 ?? Hletin)));
604 apply (proj2 ?? Hletin)
606 | apply (H ???? H1 H4)
611 (* invariante & enter *)
612 lemma getidmap_to_enter :
613 ∀d.∀m:aux_map_type d.∀str.
614 get_id_map_aux (S d) (enter_map d m) str = get_id_map_aux d m str.
617 [ simplify; reflexivity
618 | simplify; rewrite > H; reflexivity
622 lemma checkdescenter_to_checkdesc :
623 ∀d.∀e:aux_env_type d.∀str.
624 check_desc_env (S d) (enter_env d e) str →
625 check_desc_env d e str.
627 unfold enter_env in H:(%);
633 lemma env_map_flatEnv_enter_aux :
634 ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.
635 env_to_flatEnv_inv d e map fe →
636 env_to_flatEnv_inv (S d) (enter_env d e) (enter_map d map) fe.
641 [ unfold env_to_flatEnv_inv_one_level;
645 [ unfold check_id_map;
646 rewrite > (getidmap_to_enter ???);
647 apply (proj1 ?? (proj1 ?? (H str (checkdescenter_to_checkdesc ??? H1))))
649 rewrite > (getidmap_to_enter ???);
650 apply (proj2 ?? (proj1 ?? (H str (checkdescenter_to_checkdesc ??? H1))))
653 rewrite > (getidmap_to_enter ???);
654 apply (proj2 ?? (H str (checkdescenter_to_checkdesc ??? H1)))
656 | rewrite > leave_env_enter_env;
657 rewrite > leave_map_enter_map;
658 change with (env_to_flatEnv_inv_one_level O e map fe);
664 unfold env_to_flatEnv_inv_one_level;
668 [ unfold check_id_map;
669 rewrite > (getidmap_to_enter ???);
670 apply (proj1 ?? (proj1 ?? (H2 str (checkdescenter_to_checkdesc ??? H4))))
672 rewrite > (getidmap_to_enter ???);
673 apply (proj2 ?? (proj1 ?? (H2 str (checkdescenter_to_checkdesc ??? H4))))
676 rewrite > (getidmap_to_enter ???);
677 apply (proj2 ?? (H2 str (checkdescenter_to_checkdesc ??? H4)))
679 | rewrite > leave_env_enter_env;
680 rewrite > leave_map_enter_map;
681 change with (env_to_flatEnv_inv (S n) e map fe);
687 (* invariante & leave *)
688 lemma env_map_flatEnv_leave_aux :
689 ∀d.∀e:aux_env_type (S d).∀map:aux_map_type (S d).∀fe.∀trsf.
690 env_to_flatEnv_inv (S d) (build_trasfEnv_env (S d) trsf e) map fe →
691 env_to_flatEnv_inv d (leave_env d (build_trasfEnv_env (S d) trsf e)) (leave_map d map) fe.
698 (* invariante & add *)
699 definition occurs_in_trsf ≝
700 λtrsf:list (Prod3T aux_str_type bool ast_type).λstr.
701 fold_right_list ?? (λhe,b.eqStr_str (fst3T ??? he) str ⊕ b) false trsf.
703 lemma occurs_in_subTrsf_r :
705 occurs_in_trsf (a::l) str = false →
706 occurs_in_trsf l str = false.
709 rewrite > (orb_false_false_r ?? H);
713 lemma occurs_in_subTrsf_l :
715 occurs_in_trsf (a::l) str = false →
716 eqStr_str (fst3T ??? a) str = false.
719 rewrite > (orb_false_false ?? H);
723 axiom get_id_map_aux_add_not_occurs :
724 ∀d.∀map:aux_map_type d.∀fe,trsf,str.
725 occurs_in_trsf trsf str = false →
726 get_id_map_aux d map str =
727 get_id_map_aux d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str.
729 lemma get_id_map_add_not_occurs :
730 ∀d.∀map:aux_map_type d.∀fe,trsf,str.
731 occurs_in_trsf trsf str = false →
732 get_id_map d map str =
733 get_id_map d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str.
736 rewrite < (get_id_map_aux_add_not_occurs ????? H);
740 lemma check_id_map_not_occurs :
741 ∀d.∀map:aux_map_type d.∀fe.∀trsf.∀str.
742 occurs_in_trsf trsf str = false →
743 check_id_map d map str →
744 check_id_map d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str.
747 rewrite < (get_id_map_aux_add_not_occurs ????? H);
751 lemma check_desc_flatEnv_not_occurs :
752 ∀d.∀map:aux_map_type d.∀fe.∀trsf.∀str.
753 occurs_in_trsf trsf str = false →
754 check_desc_flatEnv fe (STR_ID str (get_id_map d map str)) →
755 check_desc_flatEnv (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe)))
756 (STR_ID str (get_id_map d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str)).
758 rewrite < (get_id_map_add_not_occurs ????? H);
759 apply (leflatenv_to_check ??? (buildtrasfenvadd_to_le ????) H1).
762 lemma get_desc_flatEnv_not_occurs :
763 ∀d.∀map:aux_map_type d.∀fe.∀trsf.∀str.
764 occurs_in_trsf trsf str = false →
765 check_desc_flatEnv fe (STR_ID str (get_id_map d map str)) →
766 get_desc_flatEnv (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe)))
767 (STR_ID str (get_id_map d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str)) =
768 get_desc_flatEnv fe (STR_ID str (get_id_map d map str)).
770 rewrite < (get_id_map_add_not_occurs ????? H);
771 rewrite < (leflatenv_to_get ??? (buildtrasfenvadd_to_le ????) H1);
775 axiom get_desc_env_aux_not_occurs :
776 ∀d.∀e:aux_env_type d.∀trsf.∀str.
777 occurs_in_trsf trsf str = false →
778 get_desc_env_aux d (build_trasfEnv_env d trsf e) str =
779 get_desc_env_aux d e str.
781 lemma get_desc_env_not_occurs :
782 ∀d.∀e:aux_env_type d.∀trsf.∀str.
783 occurs_in_trsf trsf str = false →
784 get_desc_env d (build_trasfEnv_env d trsf e) str =
785 get_desc_env d e str.
788 rewrite > (get_desc_env_aux_not_occurs ???? H);
792 lemma check_desc_env_not_occurs :
793 ∀d.∀e:aux_env_type d.∀trsf.∀str.
794 occurs_in_trsf trsf str = false →
795 check_desc_env d (build_trasfEnv_env d trsf e) str →
796 check_desc_env d e str.
798 unfold check_desc_env;
800 rewrite < (get_desc_env_aux_not_occurs ???? H);
804 axiom get_id_map_aux_add_occurs :
805 ∀d.∀map:aux_map_type d.∀fe,trsf,str.
806 occurs_in_trsf trsf str = true →
807 ∃x.get_id_map_aux d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str = Some ? x.
809 lemma check_id_map_occurs :
810 ∀d.∀map:aux_map_type d.∀fe.∀trsf.∀str.
811 occurs_in_trsf trsf str = true →
812 check_id_map d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str.
814 cases (get_id_map_aux_add_occurs d map fe trsf str H);
821 axiom check_desc_flatEnv_occurs :
822 ∀d.∀map:aux_map_type d.∀fe.∀trsf.∀str.
823 occurs_in_trsf trsf str = true →
824 check_desc_flatEnv (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe)))
825 (STR_ID str (get_id_map d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str)).
827 axiom get_desc_env_eq_get_desc_flatEnv_occurs :
828 ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.∀trsf.∀str.
829 occurs_in_trsf trsf str = true →
830 get_desc_env d (build_trasfEnv_env d trsf e) str =
831 get_desc_flatEnv (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe)))
832 (STR_ID str (get_id_map d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str)).
834 axiom leave_env_build_trasfEnv :
835 ∀d.∀e:aux_env_type (S d).∀trsf.
836 leave_env d (build_trasfEnv_env (S d) trsf e) = leave_env d e.
838 axiom leave_map_build_trasfEnv_mapFe:
839 ∀d.∀map:aux_map_type (S d).∀fe.∀trsf.
840 leave_map d (fst ?? (build_trasfEnv_mapFe (S d) trsf (pair ?? map fe))) =
843 lemma env_map_flatEnv_add_aux :
844 ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.∀trsf.
845 env_to_flatEnv_inv d e map fe →
847 (build_trasfEnv_env d trsf e)
848 (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe)))
849 (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))).
856 apply (bool_elim ? (occurs_in_trsf trsf str));
860 [ apply (check_id_map_occurs ????? H2)
861 | apply (check_desc_flatEnv_occurs ????? H2)
863 | apply (get_desc_env_eq_get_desc_flatEnv_occurs ?????? H2)
866 cases (H str (check_desc_env_not_occurs ???? H2 H1));
869 [ apply (check_id_map_not_occurs ????? H2 (proj1 ?? H3))
870 | apply (check_desc_flatEnv_not_occurs ????? H2 (proj2 ?? H3))
872 | rewrite > (get_desc_flatEnv_not_occurs ????? H2 (proj2 ?? H3));
873 rewrite > (get_desc_env_not_occurs ???? H2);
880 unfold env_to_flatEnv_inv_one_level in H1;
883 apply (bool_elim ? (occurs_in_trsf trsf str));
887 [ apply (check_id_map_occurs ????? H4)
888 | apply (check_desc_flatEnv_occurs ????? H4)
890 | apply (get_desc_env_eq_get_desc_flatEnv_occurs ?????? H4)
895 [ apply (check_id_map_not_occurs ????? H4 (proj1 ?? (proj1 ?? (H1 str (check_desc_env_not_occurs ???? H4 H3)))))
896 | apply (check_desc_flatEnv_not_occurs ????? H4 (proj2 ?? (proj1 ?? (H1 str (check_desc_env_not_occurs ???? H4 H3)))))
898 | rewrite > (get_desc_flatEnv_not_occurs ????? H4 (proj2 ?? (proj1 ?? (H1 str (check_desc_env_not_occurs ???? H4 H3)))));
899 rewrite > (get_desc_env_not_occurs ???? H4);
900 apply (proj2 ?? (H1 str (check_desc_env_not_occurs ???? H4 H3)))
903 | change with (env_to_flatEnv_inv n (leave_env n (build_trasfEnv_env (S n) trsf e))
904 (leave_map n (fst ?? (build_trasfEnv_mapFe (S n) trsf (pair ?? map fe))))
905 (snd ?? (build_trasfEnv_mapFe (S n) trsf (pair ?? map fe))));
906 rewrite > leave_map_build_trasfEnv_mapFe;
907 rewrite > leave_env_build_trasfEnv;
908 apply (leflatenv_to_inv ?????? H2);
909 apply buildtrasfenvadd_to_le
914 lemma env_map_flatEnv_addNil_aux :
915 ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.
916 env_to_flatEnv_inv d e map fe →
918 (build_trasfEnv_env d [] e)
919 (fst ?? (build_trasfEnv_mapFe d [] (pair ?? map fe)))
920 (snd ?? (build_trasfEnv_mapFe d [] (pair ?? map fe))).
926 lemma env_map_flatEnv_addSingle_aux :
927 ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.∀name,const,desc.
928 env_to_flatEnv_inv d e map fe →
930 (add_desc_env d e name const desc)
931 (fst ?? (build_trasfEnv_mapFe d [ tripleT ??? name const desc ] (pair ?? map fe)))
932 (snd ?? (build_trasfEnv_mapFe d [ tripleT ??? name const desc ] (pair ?? map fe))).
934 apply (env_map_flatEnv_add_aux d e map fe [ tripleT ??? name const desc ]);
938 lemma env_map_flatEnv_addJoin_aux :
939 ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe:aux_flatEnv_type.∀name,const,desc,trsf.
941 (build_trasfEnv_env d trsf (add_desc_env d e name const desc))
944 (build_trasfEnv_env d ([ tripleT ??? name const desc ]@trsf) e)
951 (* ********************************************* *)
953 lemma newid_from_init :
954 ∀d.∀e:aux_env_type d.∀name,const,desc.
955 ast_id d (add_desc_env d e name const desc) const desc.
957 lapply (AST_ID d (add_desc_env d e name const desc) name ?);
960 rewrite > (eq_to_eqstr ?? (refl_eq ??));
963 | cut (const = get_const_desc (get_desc_env d (add_desc_env d e name const desc) name) ∧
964 desc = get_type_desc (get_desc_env d (add_desc_env d e name const desc) name));
965 [ rewrite > (proj1 ?? Hcut) in ⊢ (? ? ? % ?);
966 rewrite > (proj2 ?? Hcut) in ⊢ (? ? ? ? %);
971 rewrite > (eq_to_eqstr ?? (refl_eq ??));
976 rewrite > (eq_to_eqstr ?? (refl_eq ??));