1. data structure for lables is now more strict

[helm.git] / helm / software / matita / contribs / assembly / compiler / env_to_flatenv.ma

diff --git a/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma b/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma
index d8805d26991be6a98a9ba024e471a4e9587e7ccd..1339f4f9d3aeceda13f57533bf6c26fbeea77bdb 100755 (executable)
--- a/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma
+++ b/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma
@@ -125,7 +125,9 @@ definition check_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
 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;
@@ -141,7 +143,9 @@ definition checknot_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
 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;
@@ -171,7 +175,8 @@ definition check_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
 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;
@@ -187,7 +192,8 @@ definition checknot_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
 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;
@@ -469,17 +475,87 @@ lemma getidmap_to_enter :
  ]
 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)
-  ].
+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 checkenvmapalign_to_enter :
+ ∀de.∀e:aux_env_type de.∀dm.∀m:aux_map_type dm.
+  check_env_map_align de e dm m =
+  check_env_map_align (S de) (enter_env de e) (S dm) (enter_map dm m).
+ intros 4;
+ unfold enter_env;
+ simplify;
+ elim e 0;
+ [ simplify;
+   intro;
+   elim l 0;
+   [ simplify;
+     reflexivity
+   | simplify;
+     intros;
+     rewrite > (getidmap_to_enter ???);
+     rewrite < H;
+     cases (get_id_map_aux dm m (get_name_var a));
+     [ simplify;
+       reflexivity
+     | simplify;
+       rewrite > H;
+       reflexivity
+     ]
+   ]
+ | simplify;
+   intros 2;
+   elim l 0;
+   [ simplify;
+     intros;
+     apply H
+   | intros;
+     simplify;
+     rewrite > (getidmap_to_enter ???);
+     cases (get_id_map_aux dm m (get_name_var a));
+     [ simplify;
+       reflexivity
+     | simplify;
+       apply (H e1 H1)
+     ]
+   ]
+ ].
+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.
+ unfold env_to_flatEnv_inv;
+ intros;
+ split;
+ [ split;
+   [ split;
+     [ split;
+       [ rewrite < (checkenvmapalign_to_enter ???); 
+         apply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (H str (checkdescenter_to_checkdesc ??? H1))))))
+       | (* TO DO !!! *) elim daemon
+       ]
+     | unfold check_id_map;
+       rewrite > (getidmap_to_enter ???);
+       apply (proj2 ?? (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)))
+ ].
+qed.
 
 (* aggiungi descrittore *)
 let rec new_map_elem_from_depth_aux (d:nat) on d ≝
@@ -526,29 +602,15 @@ let rec build_trasfEnv_mapFe (d:nat) (trsf:list (Prod3T aux_str_type bool ast_ty
                             (add_desc_env_flatEnv_fe d (fst ?? x) (snd ?? x) (fst3T ??? h) (snd3T ??? h) (thd3T ??? h))))
   ].
 
-(* avanzamento dell'invariante *)
-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.
- unfold env_to_flatEnv_inv;
- intros;
- split; [ split [ split [ split | ] | ] | ]
-  [ elim daemon
-  | elim daemon;
-  | elim daemon;
-  | elim daemon;
-  | elim daemon;
-  ]
-qed.
-
-axiom env_map_flatEnv_add_aux : 
+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))).
+ (* TO DO !!! *) elim daemon.
+qed.
 
 lemma env_map_flatEnv_addNil_aux :
  ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.
@@ -647,10 +709,17 @@ lemma buildtrasfenvadd_to_le :
  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.
+(* 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)
+  ].
 
 lemma leave_add_enter_env_aux :
  ∀d.∀a:aux_env_type d.∀trsf.∀c.
@@ -674,6 +743,13 @@ lemma leave_add_enter_env :
  reflexivity.
 qed.
 
+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.
+ (* TO DO !!! *) elim daemon.
+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.