eliminazione di un passaggio di transitività in ast2astfe

[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..156d9a8bd6a63b199782ec25086c37ad561c32f4 100755 (executable)
--- a/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma
+++ b/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma
@@ -469,17 +469,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,22 +596,7 @@ 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.
-
+(* TO DO !!! *)
 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 →
@@ -647,10 +702,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 +736,12 @@ lemma leave_add_enter_env :
  reflexivity.
 qed.
 
+(* TO DO !!! *)
+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.
+
 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.