First attempts at the third phase.

[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 156d9a8bd6a63b199782ec25086c37ad561c32f4..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;
@@ -535,7 +541,7 @@ lemma env_map_flatEnv_enter_aux :
      [ split;
        [ rewrite < (checkenvmapalign_to_enter ???); 
          apply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (H str (checkdescenter_to_checkdesc ??? H1))))))
-       | (* TO DO !!! *) elim daemon;
+       | (* TO DO !!! *) elim daemon
        ]
      | unfold check_id_map;
        rewrite > (getidmap_to_enter ???);
@@ -596,14 +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))))
   ].
 
-(* TO DO !!! *)
-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.
@@ -736,11 +743,12 @@ lemma leave_add_enter_env :
  reflexivity.
 qed.
 
-(* TO DO !!! *)
-axiom env_map_flatEnv_leave_aux :
+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.