definition checkb_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
match get_id_map_aux d map name with [ None ⇒ false | Some _ ⇒ true ].
-lemma checkbidmap_to_checkidmap : ∀d.∀map:aux_map_type d.∀name.checkb_id_map d map name = true → check_id_map d map name.
+lemma checkbidmap_to_checkidmap :
+ ∀d.∀map:aux_map_type d.∀name.
+ checkb_id_map d map name = true → check_id_map d map name.
unfold checkb_id_map;
unfold check_id_map;
intros 3;
definition checknotb_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
match get_id_map_aux d map name with [ None ⇒ true | Some _ ⇒ false ].
-lemma checknotbidmap_to_checknotidmap : ∀d.∀map:aux_map_type d.∀name.checknotb_id_map d map name = true → checknot_id_map d map name.
+lemma checknotbidmap_to_checknotidmap :
+ ∀d.∀map:aux_map_type d.∀name.
+ checknotb_id_map d map name = true → checknot_id_map d map name.
unfold checknotb_id_map;
unfold checknot_id_map;
intros 3;
definition checkb_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
match get_desc_flatEnv_aux fe str with [ None ⇒ false | Some _ ⇒ true ].
-lemma checkbdescflatenv_to_checkdescflatenv : ∀fe,str.checkb_desc_flatEnv fe str = true → check_desc_flatEnv fe str.
+lemma checkbdescflatenv_to_checkdescflatenv :
+ ∀fe,str.checkb_desc_flatEnv fe str = true → check_desc_flatEnv fe str.
unfold checkb_desc_flatEnv;
unfold check_desc_flatEnv;
intros 2;
definition checknotb_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
match get_desc_flatEnv_aux fe str with [ None ⇒ true | Some _ ⇒ false ].
-lemma checknotbdescflatenv_to_checknotdescflatenv : ∀fe,str.checknotb_desc_flatEnv fe str = true → checknot_desc_flatEnv fe str.
+lemma checknotbdescflatenv_to_checknotdescflatenv :
+ ∀fe,str.checknotb_desc_flatEnv fe str = true → checknot_desc_flatEnv fe str.
unfold checknotb_desc_flatEnv;
unfold checknot_desc_flatEnv;
intros 2;
].
qed.
+(* leave: elimina la testa (il "cur" corrente) *)
+let rec leave_map d (map:aux_map_type (S d)) on map ≝
+ match map with
+ [ nil ⇒ []
+ | cons h t ⇒
+ (MAP_ELEM d
+ (get_name_mapElem (S d) h)
+ (get_max_mapElem (S d) h)
+ (cut_first_mapList ? (get_cur_mapElem (S d) h) (defined_mapList_get ??))
+ )::(leave_map d t)
+ ].
+
+(* enter: propaga in testa la vecchia testa (il "cur" precedente) *)
+let rec enter_map d (map:aux_map_type d) on map ≝
+ match map with
+ [ nil ⇒ []
+ | cons h t ⇒
+ (MAP_ELEM (S d)
+ (get_name_mapElem d h)
+ (get_max_mapElem d h)
+ (map_cons (S d)
+ (get_first_mapList ? (get_cur_mapElem d h) (defined_mapList_get ??))
+ (get_cur_mapElem d h))
+ )::(enter_map d t)
+ ].
+
+(* aggiungi descrittore *)
+let rec new_map_elem_from_depth_aux (d:nat) on d ≝
+ match d
+ return λd.map_list d
+ with
+ [ O ⇒ map_nil
+ | S n ⇒ map_cons n (None ?) (new_map_elem_from_depth_aux n)
+ ].
+
+let rec new_max_map_aux d (map:aux_map_type d) (name:aux_str_type) (max:nat) on map ≝
+ match map with
+ [ nil ⇒ []
+ | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with
+ [ 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
+ | false ⇒ h::(new_max_map_aux d t name max)
+ ]
+ ].
+
+definition add_desc_env_flatEnv_map ≝
+λd.λmap:aux_map_type d.λstr.
+ match get_max_map_aux d map str with
+ [ None ⇒ map@[ MAP_ELEM d str O (map_cons d (Some ? O) (new_map_elem_from_depth_aux d)) ]
+ | Some x ⇒ new_max_map_aux d map str (S x)
+ ].
+
+definition add_desc_env_flatEnv_fe ≝
+λd.λmap:aux_map_type d.λfe.λstr.λc.λdesc.
+ fe@[ VAR_FLAT_ELEM (STR_ID str match get_max_map_aux d map str with [ None ⇒ O | Some x ⇒ (S x)])
+ (DESC_ELEM c desc) ].
+
+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 ≝
+ match trsf with
+ [ nil ⇒ (λx.x)
+ | cons h t ⇒ (λx.(build_trasfEnv_env d t) (add_desc_env d x (fst3T ??? h) (snd3T ??? h) (thd3T ??? h)))
+ ].
+
+let rec build_trasfEnv_mapFe (d:nat) (trsf:list (Prod3T aux_str_type bool ast_type)) on trsf :
+ Prod (aux_map_type d) aux_flatEnv_type → Prod (aux_map_type d) aux_flatEnv_type ≝
+ match trsf with
+ [ nil ⇒ (λx.x)
+ | cons h t ⇒ (λx.(build_trasfEnv_mapFe d t)
+ (pair ?? (add_desc_env_flatEnv_map d (fst ?? x) (fst3T ??? h))
+ (add_desc_env_flatEnv_fe d (fst ?? x) (snd ?? x) (fst3T ??? h) (snd3T ??? h) (thd3T ??? h))))
+ ].
+
+(* ********************************************* *)
+
(* fe <= fe' *)
definition eq_flatEnv_elem ≝
λe1,e2.match e1 with
].
qed.
-lemma leflatenv_to_check : ∀fe,fe',str.
- (le_flatEnv fe fe' = true) →
- (check_desc_flatEnv fe str) →
- (check_desc_flatEnv fe' str).
+lemma leflatenv_to_check :
+ ∀fe,fe',str.
+ (le_flatEnv fe fe' = true) →
+ (check_desc_flatEnv fe str) →
+ (check_desc_flatEnv fe' str).
intros 4;
cases (leflatenv_to_le fe fe' H);
rewrite < H1;
].
qed.
-lemma leflatenv_to_get : ∀fe,fe',str.
- (le_flatEnv fe fe' = true) →
- (check_desc_flatEnv fe str) →
- (get_desc_flatEnv fe str = get_desc_flatEnv fe' str).
+lemma leflatenv_to_get :
+ ∀fe,fe',str.
+ (le_flatEnv fe fe' = true) →
+ (check_desc_flatEnv fe str) →
+ (get_desc_flatEnv fe str = get_desc_flatEnv fe' str).
intros 4;
cases (leflatenv_to_le fe fe' H);
rewrite < H1;
].
qed.
-(* controllo di coerenza env <-> map *)
-let rec check_map_env_align_auxEnv (d:nat) (e:aux_env_type d) (str:aux_str_type) (res:nat) on e ≝
- match e with
- [ env_nil h ⇒ λf.f h
- | env_cons d' h t ⇒ λf.check_map_env_align_auxEnv d' t str (f h)
- ] (λx.match get_desc_from_lev_env x str with [ None ⇒ S res | Some _ ⇒ O ]).
-
-let rec check_map_env_align_auxMap (d:nat) (map:map_list d) (res:nat) on map ≝
- match map with
- [ map_nil ⇒ eqb res O
- | map_cons d' h t ⇒ match eqb res O with
- [ true ⇒ match h with
- [ None ⇒ check_map_env_align_auxMap d' t O | Some _ ⇒ false ]
- | false ⇒ match h with
- [ None ⇒ false | Some _ ⇒ check_map_env_align_auxMap d' t (pred res) ]
- ]
- ].
-
-(* esprimendolo in lingua umana il vincolo che controlla e':
- ∀name ϵ map.
- la map_list "cur" deve avere la seguente struttura
- - Some _ ; ... ; Some _ ; None ; ... None
- - il numero di Some _ deve essere pari a (d + 1 - x) con x
- ricavato scandendo in avanti tutti gli ambienti e
- numerando quanti ambienti CONSECUTIVI non contengono la definizione di name
-
- ex: scandendo e in avanti si trova la seguente sequenza di check per il nome "pippo"
- no si no si NO NO
- quindi sapendo che d=5 (6 partendo da 0) e che check_env_align_aux ha restituito 2
- sappiamo che la mappa alla voce "pippo" deve avere la seguente struttura scandita in avanti
- Some _ ; Some _ ; Some _ ; Some _ ; None ; None
- cioe' 5+1-2 Some seguiti da solo None
-
- NB: e' solo meta' perche' cosi' si asserisce map ≤ env
-
-*)
-let rec check_map_env_align (d:nat) (e:aux_env_type d) (map:aux_map_type d) on map ≝
- match map with
- [ nil ⇒ true
- | 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)))⊗
- (check_map_env_align d e t)
- ].
-
-let rec check_env_map_align_aux (d:nat) (map:aux_map_type d) (le:list var_elem) on le ≝
- match le with
- [ nil ⇒ true
- | cons h t ⇒ match get_id_map_aux d map (get_name_var h) with
- [ None ⇒ false | Some _ ⇒ check_env_map_align_aux d map t ]
- ].
-
-(* esprimendolo in lingua umana il vincolo che controlla e':
- ∀name ϵ e.name ϵ map
-
- NB: e' l'altra meta' perche' cosi' asserisce env ≤ map
-*)
-let rec check_env_map_align (de:nat) (e:aux_env_type de) (dm:nat) (map:aux_map_type dm) on e ≝
- match e with
- [ env_nil h ⇒ check_env_map_align_aux dm map h
- | env_cons d' h t ⇒ (check_env_map_align_aux dm map h)⊗(check_env_map_align d' t dm map)
- ].
-
-(* invariante *)
-definition env_to_flatEnv_inv ≝
- λd.λe:aux_env_type d.λmap:aux_map_type d.λfe:aux_flatEnv_type.
- ∀str.
- check_desc_env d e str →
- (((check_env_map_align d e d map)⊗(check_map_env_align d e map)) = true ∧
- check_id_map d map str ∧
- check_desc_flatEnv fe (STR_ID str (get_id_map d map str)) ∧
- get_desc_env d e str = get_desc_flatEnv fe (STR_ID str (get_id_map d map str))).
-
-lemma inv_to_checkdescflatenv :
- ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.
- env_to_flatEnv_inv d e map fe →
- (∀str.check_desc_env d e str → check_desc_flatEnv fe (STR_ID str (get_id_map d map str))).
- intros 7;
- unfold env_to_flatEnv_inv in H:(%);
- lapply (H str H1);
- apply (proj2 ?? (proj1 ?? Hletin));
-qed.
-
-lemma env_map_flatEnv_empty_aux : env_to_flatEnv_inv O empty_env empty_map empty_flatEnv.
- unfold env_to_flatEnv_inv;
- unfold empty_env;
- unfold empty_map;
- unfold empty_flatEnv;
- simplify;
- intros;
- elim H.
-qed.
-
-lemma leflatenv_to_inv :
- ∀d.∀e.∀map:aux_map_type d.∀fe,fe'.
- le_flatEnv fe fe' = true →
- env_to_flatEnv_inv d e map fe →
- env_to_flatEnv_inv d e map fe'.
- intros 6;
- unfold env_to_flatEnv_inv;
- intros;
- split;
- [ split;
- [ lapply (H1 str H2);
- apply (proj1 ?? (proj1 ?? Hletin))
- | lapply (H1 str H2);
- apply (leflatenv_to_check fe fe' ? H (proj2 ?? (proj1 ?? Hletin)))
- ]
- | lapply (H1 str H2);
- rewrite < (leflatenv_to_get fe fe' ? H (proj2 ?? (proj1 ?? Hletin)));
- apply (proj2 ?? Hletin)
- ].
-qed.
-
lemma leflatenv_trans :
∀fe,fe',fe''.
le_flatEnv fe fe' = true →
apply (le_to_leflatenv fe ?).
qed.
-(* enter: propaga in testa la vecchia testa (il "cur" precedente) *)
-let rec enter_map d (map:aux_map_type d) on map ≝
- match map with
- [ nil ⇒ []
- | cons h t ⇒
- (MAP_ELEM (S d)
- (get_name_mapElem d h)
- (get_max_mapElem d h)
- (map_cons (S d)
- (get_first_mapList ? (get_cur_mapElem d h) (defined_mapList_get ??))
- (get_cur_mapElem d h))
- )::(enter_map d t)
- ].
-
-lemma getidmap_to_enter :
- ∀d.∀m:aux_map_type d.∀str.
- get_id_map_aux (S d) (enter_map d m) str = get_id_map_aux d m str.
- intros;
- elim m;
- [ simplify; reflexivity
- | simplify; rewrite > H; reflexivity
- ]
-qed.
-
-(* leave: elimina la testa (il "cur" corrente) *)
-let rec leave_map d (map:aux_map_type (S d)) on map ≝
- match map with
- [ nil ⇒ []
- | cons h t ⇒
- (MAP_ELEM d
- (get_name_mapElem (S d) h)
- (get_max_mapElem (S d) h)
- (cut_first_mapList ? (get_cur_mapElem (S d) h) (defined_mapList_get ??))
- )::(leave_map d t)
- ].
-
-(* aggiungi descrittore *)
-let rec new_map_elem_from_depth_aux (d:nat) on d ≝
- match d
- return λd.map_list d
- with
- [ O ⇒ map_nil
- | S n ⇒ map_cons n (None ?) (new_map_elem_from_depth_aux n)
- ].
-
-let rec new_max_map_aux d (map:aux_map_type d) (name:aux_str_type) (max:nat) on map ≝
- match map with
- [ nil ⇒ []
- | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with
- [ true ⇒ MAP_ELEM d name max (map_cons d (Some ? max) (cut_first_mapList (S d) (get_cur_mapElem d h) (defined_mapList_get ??)))
- | false ⇒ h
- ]::(new_max_map_aux d t name max)
- ].
-
-definition add_desc_env_flatEnv_map ≝
-λd.λmap:aux_map_type d.λstr.
- match get_max_map_aux d map str with
- [ None ⇒ map@[ MAP_ELEM d str O (map_cons d (Some ? O) (new_map_elem_from_depth_aux d)) ]
- | Some x ⇒ new_max_map_aux d map str (S x)
- ].
-
-definition add_desc_env_flatEnv_fe ≝
-λd.λmap:aux_map_type d.λfe.λstr.λc.λdesc.
- fe@[ VAR_FLAT_ELEM (STR_ID str match get_max_map_aux d map str with [ None ⇒ O | Some x ⇒ (S x)])
- (DESC_ELEM c desc) ].
-
-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 ≝
- match trsf with
- [ nil ⇒ (λx.x)
- | cons h t ⇒ (λx.(build_trasfEnv_env d t) (add_desc_env d x (fst3T ??? h) (snd3T ??? h) (thd3T ??? h)))
- ].
-
-let rec build_trasfEnv_mapFe (d:nat) (trsf:list (Prod3T aux_str_type bool ast_type)) on trsf :
- Prod (aux_map_type d) aux_flatEnv_type → Prod (aux_map_type d) aux_flatEnv_type ≝
- match trsf with
- [ nil ⇒ (λx.x)
- | cons h t ⇒ (λx.(build_trasfEnv_mapFe d t)
- (pair ?? (add_desc_env_flatEnv_map d (fst ?? x) (fst3T ??? h))
- (add_desc_env_flatEnv_fe d (fst ?? x) (snd ?? x) (fst3T ??? h) (snd3T ??? h) (thd3T ??? h))))
- ].
-
-(* avanzamento dell'invariante *)
-axiom env_map_flatEnv_enter_aux :
- ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.
- env_to_flatEnv_inv d e map fe →
- env_to_flatEnv_inv (S d) (enter_env d e) (enter_map d map) fe.
-
-axiom env_map_flatEnv_add_aux :
- ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.∀trsf.
- env_to_flatEnv_inv d e map fe →
- env_to_flatEnv_inv d
- (build_trasfEnv_env d trsf e)
- (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe)))
- (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))).
-
-lemma env_map_flatEnv_addNil_aux :
- ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.
- env_to_flatEnv_inv d e map fe →
- env_to_flatEnv_inv d
- (build_trasfEnv_env d [] e)
- (fst ?? (build_trasfEnv_mapFe d [] (pair ?? map fe)))
- (snd ?? (build_trasfEnv_mapFe d [] (pair ?? map fe))).
- intros;
- simplify;
- apply H.
-qed.
-
-lemma env_map_flatEnv_addSingle_aux :
- ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.∀name,const,desc.
- env_to_flatEnv_inv d e map fe →
- env_to_flatEnv_inv d
- (add_desc_env d e name const desc)
- (fst ?? (build_trasfEnv_mapFe d [ tripleT ??? name const desc ] (pair ?? map fe)))
- (snd ?? (build_trasfEnv_mapFe d [ tripleT ??? name const desc ] (pair ?? map fe))).
- intros;
- apply (env_map_flatEnv_add_aux d e map fe [ tripleT ??? name const desc ]);
- apply H.
-qed.
-
-lemma env_map_flatEnv_addJoin_aux :
- ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe:aux_flatEnv_type.∀name,const,desc,trsf.
- env_to_flatEnv_inv d
- (build_trasfEnv_env d trsf (add_desc_env d e name const desc))
- map fe →
- env_to_flatEnv_inv d
- (build_trasfEnv_env d ([ tripleT ??? name const desc ]@trsf) e)
- map fe.
- intros;
- simplify;
- apply H.
-qed.
-
lemma env_map_flatEnv_add_aux_fe_al :
∀trsf.∀d.∀m:aux_map_type d.∀a,l.
snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m (a::l))) =
reflexivity.
qed.
-axiom env_map_flatEnv_leave_aux :
- ∀d.∀e:aux_env_type (S d).∀map:aux_map_type (S d).∀fe.∀trsf.
- env_to_flatEnv_inv (S d) (build_trasfEnv_env (S d) trsf e) map fe →
- env_to_flatEnv_inv d (leave_env d (build_trasfEnv_env (S d) trsf e)) (leave_map d map) fe.
+(* ********************************************* *)
+
+(* miscellanea *)
+lemma leave_env_enter_env : ∀d.∀e:aux_env_type d.leave_env d (enter_env d e) = e.
+ intros;
+ elim e;
+ reflexivity.
+qed.
+
+lemma leave_map_enter_map : ∀d.∀map. leave_map d (enter_map d map) = map.
+ intros;
+ elim map;
+ [ reflexivity
+ | simplify;
+ rewrite > H;
+ cases a;
+ simplify;
+ reflexivity
+ ]
+qed.
lemma leave_add_enter_env_aux :
∀d.∀a:aux_env_type d.∀trsf.∀c.
reflexivity.
qed.
+(* ********************************************* *)
+
+(* invariante a un livello *)
+definition env_to_flatEnv_inv_one_level ≝
+ λd.λe:aux_env_type d.λmap:aux_map_type d.λfe:aux_flatEnv_type.
+ ∀str.
+ check_desc_env d e str →
+ check_id_map d map str ∧
+ check_desc_flatEnv fe (STR_ID str (get_id_map d map str)) ∧
+ get_desc_env d e str = get_desc_flatEnv fe (STR_ID str (get_id_map d map str)).
+
+(* invariante su tutti i livelli *)
+let rec env_to_flatEnv_inv (d:nat) : aux_env_type d → aux_map_type d → aux_flatEnv_type → Prop ≝
+ match d
+ return λd.aux_env_type d → aux_map_type d → aux_flatEnv_type → Prop
+ with
+ [ O ⇒ λe:aux_env_type O.λmap:aux_map_type O.λfe:aux_flatEnv_type.
+ env_to_flatEnv_inv_one_level O e map fe
+ | S n ⇒ λe:aux_env_type (S n).λmap:aux_map_type (S n).λfe:aux_flatEnv_type.
+ env_to_flatEnv_inv_one_level (S n) e map fe ∧
+ env_to_flatEnv_inv n (leave_env n e) (leave_map n map) fe
+ ].
+
+(* invariante full -> invariante a un livello *)
+lemma env_to_flatEnv_inv_last :
+ ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.
+ env_to_flatEnv_inv d e map fe →
+ env_to_flatEnv_inv_one_level d e map fe.
+ intro;
+ cases d;
+ intros;
+ [ apply H
+ | simplify in H;
+ apply (proj1 ?? H)
+ ]
+qed.
+
+(* invariante caso base *)
+lemma env_map_flatEnv_empty_aux : env_to_flatEnv_inv O empty_env empty_map empty_flatEnv.
+ unfold env_to_flatEnv_inv;
+ unfold empty_env;
+ unfold empty_map;
+ unfold empty_flatEnv;
+ simplify;
+ intros;
+ elim H.
+qed.
+
+(* invariante & leflatenv *)
+lemma leflatenv_to_inv :
+ ∀d.∀e.∀map:aux_map_type d.∀fe,fe'.
+ le_flatEnv fe fe' = true →
+ env_to_flatEnv_inv d e map fe →
+ env_to_flatEnv_inv d e map fe'.
+ intro;
+ elim d;
+ [ simplify;
+ unfold env_to_flatEnv_inv_one_level;
+ intros;
+ split;
+ [ split;
+ [ lapply (H1 str H2);
+ apply (proj1 ?? (proj1 ?? Hletin))
+ | lapply (H1 str H2);
+ apply (leflatenv_to_check fe fe' ? H (proj2 ?? (proj1 ?? Hletin)))
+ ]
+ | lapply (H1 str H2);
+ rewrite < (leflatenv_to_get fe fe' ? H (proj2 ?? (proj1 ?? Hletin)));
+ apply (proj2 ?? Hletin)
+ ]
+ | simplify in H2 ⊢ %;
+ cases H2;
+ split;
+ [ unfold env_to_flatEnv_inv_one_level;
+ intros;
+ split;
+ [ split;
+ [ lapply (H3 str H5);
+ apply (proj1 ?? (proj1 ?? Hletin))
+ | lapply (H3 str H5);
+ apply (leflatenv_to_check fe fe' ? H1 (proj2 ?? (proj1 ?? Hletin)))
+ ]
+ | lapply (H3 str H5);
+ rewrite < (leflatenv_to_get fe fe' ? H1 (proj2 ?? (proj1 ?? Hletin)));
+ apply (proj2 ?? Hletin)
+ ]
+ | apply (H ???? H1 H4)
+ ]
+ ].
+qed.
+
+(* invariante & enter *)
+lemma getidmap_to_enter :
+ ∀d.∀m:aux_map_type d.∀str.
+ get_id_map_aux (S d) (enter_map d m) str = get_id_map_aux d m str.
+ intros;
+ elim m;
+ [ simplify; reflexivity
+ | simplify; rewrite > H; reflexivity
+ ]
+qed.
+
+lemma checkdescenter_to_checkdesc :
+ ∀d.∀e:aux_env_type d.∀str.
+ check_desc_env (S d) (enter_env d e) str →
+ check_desc_env d e str.
+ intros;
+ unfold enter_env in H:(%);
+ simplify in H:(%);
+ apply H.
+qed.
+
+
+lemma env_map_flatEnv_enter_aux :
+ ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.
+ env_to_flatEnv_inv d e map fe →
+ env_to_flatEnv_inv (S d) (enter_env d e) (enter_map d map) fe.
+ intro;
+ elim d;
+ [ simplify in H;
+ split;
+ [ unfold env_to_flatEnv_inv_one_level;
+ intros;
+ split;
+ [ split;
+ [ unfold check_id_map;
+ rewrite > (getidmap_to_enter ???);
+ apply (proj1 ?? (proj1 ?? (H str (checkdescenter_to_checkdesc ??? H1))))
+ | unfold get_id_map;
+ rewrite > (getidmap_to_enter ???);
+ apply (proj2 ?? (proj1 ?? (H str (checkdescenter_to_checkdesc ??? H1))))
+ ]
+ | unfold get_id_map;
+ rewrite > (getidmap_to_enter ???);
+ apply (proj2 ?? (H str (checkdescenter_to_checkdesc ??? H1)))
+ ]
+ | rewrite > leave_env_enter_env;
+ rewrite > leave_map_enter_map;
+ change with (env_to_flatEnv_inv_one_level O e map fe);
+ apply H
+ ]
+ | split;
+ [ cases H1;
+ simplify in H2;
+ unfold env_to_flatEnv_inv_one_level;
+ intros;
+ split;
+ [ split;
+ [ unfold check_id_map;
+ rewrite > (getidmap_to_enter ???);
+ apply (proj1 ?? (proj1 ?? (H2 str (checkdescenter_to_checkdesc ??? H4))))
+ | unfold get_id_map;
+ rewrite > (getidmap_to_enter ???);
+ apply (proj2 ?? (proj1 ?? (H2 str (checkdescenter_to_checkdesc ??? H4))))
+ ]
+ | unfold get_id_map;
+ rewrite > (getidmap_to_enter ???);
+ apply (proj2 ?? (H2 str (checkdescenter_to_checkdesc ??? H4)))
+ ]
+ | rewrite > leave_env_enter_env;
+ rewrite > leave_map_enter_map;
+ change with (env_to_flatEnv_inv (S n) e map fe);
+ apply H1
+ ]
+ ]
+qed.
+
+(* invariante & leave *)
+lemma env_map_flatEnv_leave_aux :
+ ∀d.∀e:aux_env_type (S d).∀map:aux_map_type (S d).∀fe.∀trsf.
+ env_to_flatEnv_inv (S d) (build_trasfEnv_env (S d) trsf e) map fe →
+ env_to_flatEnv_inv d (leave_env d (build_trasfEnv_env (S d) trsf e)) (leave_map d map) fe.
+ intros;
+ simplify in H;
+ cases H;
+ apply H2.
+qed.
+
+(* invariante & add *)
+definition occurs_in_trsf ≝
+λtrsf:list (Prod3T aux_str_type bool ast_type).λstr.
+ fold_right_list ?? (λhe,b.eqStr_str (fst3T ??? he) str ⊕ b) false trsf.
+
+lemma occurs_in_subTrsf_r :
+ ∀a,l,str.
+ occurs_in_trsf (a::l) str = false →
+ occurs_in_trsf l str = false.
+ intros;
+ simplify in H:(%);
+ rewrite > (orb_false_false_r ?? H);
+ reflexivity.
+qed.
+
+lemma occurs_in_subTrsf_l :
+ ∀a,l,str.
+ occurs_in_trsf (a::l) str = false →
+ eqStr_str (fst3T ??? a) str = false.
+ intros;
+ simplify in H:(%);
+ rewrite > (orb_false_false ?? H);
+ reflexivity.
+qed.
+
+axiom get_id_map_aux_add_not_occurs :
+ ∀d.∀map:aux_map_type d.∀fe,trsf,str.
+ occurs_in_trsf trsf str = false →
+ get_id_map_aux d map str =
+ get_id_map_aux d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str.
+
+lemma get_id_map_add_not_occurs :
+ ∀d.∀map:aux_map_type d.∀fe,trsf,str.
+ occurs_in_trsf trsf str = false →
+ get_id_map d map str =
+ get_id_map d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str.
+ intros;
+ unfold get_id_map;
+ rewrite < (get_id_map_aux_add_not_occurs ????? H);
+ reflexivity.
+qed.
+
+lemma check_id_map_not_occurs :
+ ∀d.∀map:aux_map_type d.∀fe.∀trsf.∀str.
+ occurs_in_trsf trsf str = false →
+ check_id_map d map str →
+ check_id_map d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str.
+ intros;
+ whd in H1 ⊢ %;
+ rewrite < (get_id_map_aux_add_not_occurs ????? H);
+ apply H1.
+qed.
+
+lemma check_desc_flatEnv_not_occurs :
+ ∀d.∀map:aux_map_type d.∀fe.∀trsf.∀str.
+ occurs_in_trsf trsf str = false →
+ check_desc_flatEnv fe (STR_ID str (get_id_map d map str)) →
+ check_desc_flatEnv (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe)))
+ (STR_ID str (get_id_map d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str)).
+ intros;
+ rewrite < (get_id_map_add_not_occurs ????? H);
+ apply (leflatenv_to_check ??? (buildtrasfenvadd_to_le ????) H1).
+qed.
+
+lemma get_desc_flatEnv_not_occurs :
+ ∀d.∀map:aux_map_type d.∀fe.∀trsf.∀str.
+ occurs_in_trsf trsf str = false →
+ check_desc_flatEnv fe (STR_ID str (get_id_map d map str)) →
+ get_desc_flatEnv (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe)))
+ (STR_ID str (get_id_map d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str)) =
+ get_desc_flatEnv fe (STR_ID str (get_id_map d map str)).
+ intros;
+ rewrite < (get_id_map_add_not_occurs ????? H);
+ rewrite < (leflatenv_to_get ??? (buildtrasfenvadd_to_le ????) H1);
+ reflexivity.
+qed.
+
+axiom get_desc_env_aux_not_occurs :
+ ∀d.∀e:aux_env_type d.∀trsf.∀str.
+ occurs_in_trsf trsf str = false →
+ get_desc_env_aux d (build_trasfEnv_env d trsf e) str =
+ get_desc_env_aux d e str.
+
+lemma get_desc_env_not_occurs :
+ ∀d.∀e:aux_env_type d.∀trsf.∀str.
+ occurs_in_trsf trsf str = false →
+ get_desc_env d (build_trasfEnv_env d trsf e) str =
+ get_desc_env d e str.
+ intros;
+ unfold get_desc_env;
+ rewrite > (get_desc_env_aux_not_occurs ???? H);
+ reflexivity.
+qed.
+
+lemma check_desc_env_not_occurs :
+ ∀d.∀e:aux_env_type d.∀trsf.∀str.
+ occurs_in_trsf trsf str = false →
+ check_desc_env d (build_trasfEnv_env d trsf e) str →
+ check_desc_env d e str.
+ intros 5;
+ unfold check_desc_env;
+ intro;
+ rewrite < (get_desc_env_aux_not_occurs ???? H);
+ apply H1.
+qed.
+
+axiom get_id_map_aux_add_occurs :
+ ∀d.∀map:aux_map_type d.∀fe,trsf,str.
+ occurs_in_trsf trsf str = true →
+ ∃x.get_id_map_aux d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str = Some ? x.
+
+lemma check_id_map_occurs :
+ ∀d.∀map:aux_map_type d.∀fe.∀trsf.∀str.
+ occurs_in_trsf trsf str = true →
+ check_id_map d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str.
+ intros;
+ cases (get_id_map_aux_add_occurs d map fe trsf str H);
+ unfold check_id_map;
+ rewrite > H1;
+ simplify;
+ apply I.
+qed.
+
+axiom check_desc_flatEnv_occurs :
+ ∀d.∀map:aux_map_type d.∀fe.∀trsf.∀str.
+ occurs_in_trsf trsf str = true →
+ check_desc_flatEnv (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe)))
+ (STR_ID str (get_id_map d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str)).
+
+axiom get_desc_env_eq_get_desc_flatEnv_occurs :
+ ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.∀trsf.∀str.
+ occurs_in_trsf trsf str = true →
+ get_desc_env d (build_trasfEnv_env d trsf e) str =
+ get_desc_flatEnv (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe)))
+ (STR_ID str (get_id_map d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str)).
+
+axiom leave_env_build_trasfEnv :
+ ∀d.∀e:aux_env_type (S d).∀trsf.
+ leave_env d (build_trasfEnv_env (S d) trsf e) = leave_env d e.
+
+axiom leave_map_build_trasfEnv_mapFe:
+ ∀d.∀map:aux_map_type (S d).∀fe.∀trsf.
+ leave_map d (fst ?? (build_trasfEnv_mapFe (S d) trsf (pair ?? map fe))) =
+ leave_map d map.
+
+lemma env_map_flatEnv_add_aux :
+ ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.∀trsf.
+ env_to_flatEnv_inv d e map fe →
+ env_to_flatEnv_inv d
+ (build_trasfEnv_env d trsf e)
+ (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe)))
+ (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))).
+ intro;
+ cases d;
+ [ intros;
+ simplify in H;
+ simplify;
+ intros 2;
+ apply (bool_elim ? (occurs_in_trsf trsf str));
+ [ intro;
+ split
+ [ split
+ [ apply (check_id_map_occurs ????? H2)
+ | apply (check_desc_flatEnv_occurs ????? H2)
+ ]
+ | apply (get_desc_env_eq_get_desc_flatEnv_occurs ?????? H2)
+ ]
+ | intro;
+ cases (H str (check_desc_env_not_occurs ???? H2 H1));
+ split
+ [ split
+ [ apply (check_id_map_not_occurs ????? H2 (proj1 ?? H3))
+ | apply (check_desc_flatEnv_not_occurs ????? H2 (proj2 ?? H3))
+ ]
+ | rewrite > (get_desc_flatEnv_not_occurs ????? H2 (proj2 ?? H3));
+ rewrite > (get_desc_env_not_occurs ???? H2);
+ apply H4
+ ]
+ ]
+ | intros;
+ simplify in H;
+ cases H;
+ unfold env_to_flatEnv_inv_one_level in H1;
+ split;
+ [ intros 2;
+ apply (bool_elim ? (occurs_in_trsf trsf str));
+ [ intro;
+ split
+ [ split
+ [ apply (check_id_map_occurs ????? H4)
+ | apply (check_desc_flatEnv_occurs ????? H4)
+ ]
+ | apply (get_desc_env_eq_get_desc_flatEnv_occurs ?????? H4)
+ ]
+ | intro;
+ split;
+ [ split
+ [ apply (check_id_map_not_occurs ????? H4 (proj1 ?? (proj1 ?? (H1 str (check_desc_env_not_occurs ???? H4 H3)))))
+ | apply (check_desc_flatEnv_not_occurs ????? H4 (proj2 ?? (proj1 ?? (H1 str (check_desc_env_not_occurs ???? H4 H3)))))
+ ]
+ | rewrite > (get_desc_flatEnv_not_occurs ????? H4 (proj2 ?? (proj1 ?? (H1 str (check_desc_env_not_occurs ???? H4 H3)))));
+ rewrite > (get_desc_env_not_occurs ???? H4);
+ apply (proj2 ?? (H1 str (check_desc_env_not_occurs ???? H4 H3)))
+ ]
+ ]
+ | change with (env_to_flatEnv_inv n (leave_env n (build_trasfEnv_env (S n) trsf e))
+ (leave_map n (fst ?? (build_trasfEnv_mapFe (S n) trsf (pair ?? map fe))))
+ (snd ?? (build_trasfEnv_mapFe (S n) trsf (pair ?? map fe))));
+ rewrite > leave_map_build_trasfEnv_mapFe;
+ rewrite > leave_env_build_trasfEnv;
+ apply (leflatenv_to_inv ?????? H2);
+ apply buildtrasfenvadd_to_le
+ ]
+ ].
+qed.
+
+lemma env_map_flatEnv_addNil_aux :
+ ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.
+ env_to_flatEnv_inv d e map fe →
+ env_to_flatEnv_inv d
+ (build_trasfEnv_env d [] e)
+ (fst ?? (build_trasfEnv_mapFe d [] (pair ?? map fe)))
+ (snd ?? (build_trasfEnv_mapFe d [] (pair ?? map fe))).
+ intros;
+ simplify;
+ apply H.
+qed.
+
+lemma env_map_flatEnv_addSingle_aux :
+ ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.∀name,const,desc.
+ env_to_flatEnv_inv d e map fe →
+ env_to_flatEnv_inv d
+ (add_desc_env d e name const desc)
+ (fst ?? (build_trasfEnv_mapFe d [ tripleT ??? name const desc ] (pair ?? map fe)))
+ (snd ?? (build_trasfEnv_mapFe d [ tripleT ??? name const desc ] (pair ?? map fe))).
+ intros;
+ apply (env_map_flatEnv_add_aux d e map fe [ tripleT ??? name const desc ]);
+ apply H.
+qed.
+
+lemma env_map_flatEnv_addJoin_aux :
+ ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe:aux_flatEnv_type.∀name,const,desc,trsf.
+ env_to_flatEnv_inv d
+ (build_trasfEnv_env d trsf (add_desc_env d e name const desc))
+ map fe →
+ env_to_flatEnv_inv d
+ (build_trasfEnv_env d ([ tripleT ??? name const desc ]@trsf) e)
+ map fe.
+ intros;
+ simplify;
+ apply H.
+qed.
+
+(* ********************************************* *)
+
lemma newid_from_init :
∀d.∀e:aux_env_type d.∀name,const,desc.
ast_id d (add_desc_env d e name const desc) const desc.
projects / helm.git / blobdiff