From 3ef4de9e58e795bf60a54f03b89a2d5b9257f473 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 18 Dec 2008 20:35:07 +0000
Subject: [PATCH] Many axioms are now proved... using many more (but simpler)
 axioms.

---
 .../assembly/compiler/ast_to_astfe.ma         |   6 +-
 .../assembly/compiler/env_to_flatenv.ma       | 826 +++++++++++-------
 .../contribs/assembly/compiler/utility.ma     |  15 +
 .../contribs/assembly/freescale/extra.ma      |  21 +
 .../matita/contribs/assembly/string/string.ma |  24 +
 5 files changed, 575 insertions(+), 317 deletions(-)

diff --git a/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma b/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma
index 5d7a6a622..90a59130a 100755
--- a/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma
+++ b/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma
@@ -36,12 +36,11 @@ lemma ast_to_astfe_id :
  ∀dimInv:env_to_flatEnv_inv d e m fe.
  astfe_id fe b t.
  intros 7;
- unfold env_to_flatEnv_inv;
  elim a 0;
  intros 3;
  lapply (ASTFE_ID fe (STR_ID a1 (get_id_map d m a1)) ?);
- [ apply (proj2 ?? (proj1 ?? (H1 a1 H)))
- | rewrite > (proj2 ?? (H1 a1 H));
+ [ apply (proj2 ?? (proj1 ?? ((env_to_flatEnv_inv_last ???? H1) a1 H)))
+ | rewrite > (proj2 ?? ((env_to_flatEnv_inv_last ???? H1) a1 H));
    apply Hletin
  ].
 qed.
@@ -53,7 +52,6 @@ lemma ast_to_astfe_retype_id :
  ∀dimLe:le_flatEnv fe fe' = true.
  astfe_id fe' b t.
  intros 8;
- unfold env_to_flatEnv_inv;
  elim a 0;
  intros 4;
  lapply (ASTFE_ID fe' a1 ?);
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 1339f4f9d..e9298cc90 100755
--- a/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma
+++ b/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma
@@ -203,6 +203,79 @@ lemma checknotbdescflatenv_to_checknotdescflatenv :
  ].
 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
@@ -278,10 +351,11 @@ lemma le_to_leflatenv : ∀fe,x.le_flatEnv fe (fe@x) = true.
  ].
 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;
@@ -296,10 +370,11 @@ lemma leflatenv_to_check : ∀fe,fe',str.
  ].
 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;
@@ -324,87 +399,162 @@ lemma leflatenv_to_get : ∀fe,fe',str.
  ].
 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 ]).
+lemma leflatenv_trans :
+ ∀fe,fe',fe''.
+  le_flatEnv fe fe' = true →
+  le_flatEnv fe' fe'' = true →
+  le_flatEnv fe fe'' = true.
+ intros 4;
+ cases (leflatenv_to_le fe ? H);
+ rewrite < H1;
+ intro;
+ cases (leflatenv_to_le (fe@x) fe'' H2);
+ rewrite < H3;
+ rewrite > associative_append;
+ apply (le_to_leflatenv fe ?).
+qed.
 
-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) ]
+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))) =
+  a::(snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m l))).
+ intro;
+ elim trsf;
+ [ simplify; reflexivity
+ | simplify;
+   elim a;
+   simplify;
+   rewrite > (H ????);
+   reflexivity
+ ].
+qed.
+
+lemma env_map_flatEnv_add_aux_fe_l :
+ ∀trsf.∀d.∀m:aux_map_type d.∀l.
+  snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m l)) =
+  l@(snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m []))).
+ intros;
+ elim l;
+ [ simplify; reflexivity
+ | rewrite > (env_map_flatEnv_add_aux_fe_al ????);
+   rewrite > H;
+   reflexivity
+ ].
+qed.
+
+lemma env_map_flatEnv_add_aux_fe :
+ ∀d.∀map:aux_map_type d.∀fe,trsf.
+  ∃x.fe@x = (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))).
+ intros 3;
+ elim fe 0;
+ [ simplify;
+   intro;
+   exists;
+   [ apply (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map [])))
+   | reflexivity
    ]
-  ].
+ | intros 4;
+   exists;
+   [ apply (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map [])))
+   | rewrite > (env_map_flatEnv_add_aux_fe_al trsf d map a l);
+     rewrite > (env_map_flatEnv_add_aux_fe_l trsf d map l);
+     rewrite < (cons_append_commute ????);
+     reflexivity
+   ]
+ ].
+qed.
 
-(* 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)
-  ].
+lemma buildtrasfenvadd_to_le :
+ ∀d.∀m:aux_map_type d.∀fe,trsf.
+  le_flatEnv fe (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m fe))) = true.
+ intros 4;
+  cases (env_map_flatEnv_add_aux_fe d m fe trsf);
+ rewrite < H;
+ rewrite > (le_to_leflatenv fe x);
+ reflexivity.
+qed.
 
-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)
-  ].
+(* 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.
 
-(* invariante *)
-definition env_to_flatEnv_inv ≝
+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.
+  ∃b.build_trasfEnv_env (S d) trsf (env_cons d c a) = (env_cons d b a).
+ intros 3;
+ elim trsf;
+ [ simplify; exists; [ apply c | reflexivity ]
+ | simplify; apply H
+ ].
+qed.
+
+lemma leave_add_enter_env :
+ ∀d.∀e:aux_env_type d.∀trsf.
+  leave_env d (build_trasfEnv_env (S d) trsf (enter_env d e)) = e.
+ intros;
+ unfold enter_env;
+ lapply (leave_add_enter_env_aux d e trsf []);
+ cases Hletin;
+ rewrite > H;
+ simplify;
+ 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_env_map_align d e d map = true ∧ 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 :
+(* 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 →
- (∀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));
+  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;
@@ -415,56 +565,50 @@ lemma env_map_flatEnv_empty_aux : env_to_flatEnv_inv O empty_env empty_map empty
  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'.
- intros 6;
- unfold env_to_flatEnv_inv;
- intros;
- split;
- [ split;
-   [ lapply (H1 str H2);
-     apply (proj1 ?? (proj1 ?? Hletin))
+ 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);
-     apply (leflatenv_to_check fe fe' ? H (proj2 ?? (proj1 ?? Hletin)))
+     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)
    ]
- | 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 →
-  le_flatEnv fe' fe'' = true →
-  le_flatEnv fe fe'' = true.
- intros 4;
- cases (leflatenv_to_le fe ? H);
- rewrite < H1;
- intro;
- cases (leflatenv_to_le (fe@x) fe'' H2);
- rewrite < H3;
- rewrite > associative_append;
- 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)
-  ].
-
+(* 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.
@@ -485,122 +629,216 @@ lemma checkdescenter_to_checkdesc :
  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;
+ intro;
+ elim d;
+ [ simplify in H;
+   split;
+   [ unfold env_to_flatEnv_inv_one_level;
+     intros;
+     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 (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 check_id_map;
+     | unfold get_id_map;
        rewrite > (getidmap_to_enter ???);
-       apply (proj2 ?? (proj1 ?? (proj1 ?? (H str (checkdescenter_to_checkdesc ??? H1)))))
+       apply (proj2 ?? (H str (checkdescenter_to_checkdesc ??? H1)))
      ]
-   | unfold get_id_map;
-     rewrite > (getidmap_to_enter ???);
-     apply (proj2 ?? (proj1 ?? (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
    ]
- | unfold get_id_map;
-   rewrite > (getidmap_to_enter ???);
-   apply (proj2 ?? (H str (checkdescenter_to_checkdesc ??? H1)))
- ].
+ | 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.
 
-(* 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)
-  ].
+(* 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.
 
-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) 
-  ].
+(* 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.
 
-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)
-  ].
+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.
 
-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) ].
+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.
 
-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)))
-  ].
+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.
 
-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))))
-  ].
+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.
@@ -609,7 +847,68 @@ lemma env_map_flatEnv_add_aux :
                      (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.
+ 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 :
@@ -649,106 +948,7 @@ lemma env_map_flatEnv_addJoin_aux :
  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))) =
-  a::(snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m l))).
- intro;
- elim trsf;
- [ simplify; reflexivity
- | simplify;
-   elim a;
-   simplify;
-   rewrite > (H ????);
-   reflexivity
- ].
-qed.
-
-lemma env_map_flatEnv_add_aux_fe_l :
- ∀trsf.∀d.∀m:aux_map_type d.∀l.
-  snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m l)) =
-  l@(snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m []))).
- intros;
- elim l;
- [ simplify; reflexivity
- | rewrite > (env_map_flatEnv_add_aux_fe_al ????);
-   rewrite > H;
-   reflexivity
- ].
-qed.
-
-lemma env_map_flatEnv_add_aux_fe :
- ∀d.∀map:aux_map_type d.∀fe,trsf.
-  ∃x.fe@x = (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))).
- intros 3;
- elim fe 0;
- [ simplify;
-   intro;
-   exists;
-   [ apply (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map [])))
-   | reflexivity
-   ]
- | intros 4;
-   exists;
-   [ apply (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map [])))
-   | rewrite > (env_map_flatEnv_add_aux_fe_al trsf d map a l);
-     rewrite > (env_map_flatEnv_add_aux_fe_l trsf d map l);
-     rewrite < (cons_append_commute ????);
-     reflexivity
-   ]
- ].
-qed.
-
-lemma buildtrasfenvadd_to_le :
- ∀d.∀m:aux_map_type d.∀fe,trsf.
-  le_flatEnv fe (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m fe))) = true.
- intros 4;
-  cases (env_map_flatEnv_add_aux_fe d m fe trsf);
- rewrite < H;
- rewrite > (le_to_leflatenv fe x);
- 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)
-  ].
-
-lemma leave_add_enter_env_aux :
- ∀d.∀a:aux_env_type d.∀trsf.∀c.
-  ∃b.build_trasfEnv_env (S d) trsf (env_cons d c a) = (env_cons d b a).
- intros 3;
- elim trsf;
- [ simplify; exists; [ apply c | reflexivity ]
- | simplify; apply H
- ].
-qed.
-
-lemma leave_add_enter_env :
- ∀d.∀e:aux_env_type d.∀trsf.
-  leave_env d (build_trasfEnv_env (S d) trsf (enter_env d e)) = e.
- intros;
- unfold enter_env;
- lapply (leave_add_enter_env_aux d e trsf []);
- cases Hletin;
- rewrite > H;
- simplify;
- 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.
diff --git a/helm/software/matita/contribs/assembly/compiler/utility.ma b/helm/software/matita/contribs/assembly/compiler/utility.ma
index c67298d39..014d598df 100755
--- a/helm/software/matita/contribs/assembly/compiler/utility.ma
+++ b/helm/software/matita/contribs/assembly/compiler/utility.ma
@@ -198,6 +198,21 @@ lemma isbemptylist_to_isemptylist : ∀T,l.isb_empty_list T l = true → is_empt
    normalize; autobatch ]
 qed.
 
+definition isnot_empty_list ≝
+λT:Type.λl:list T.match l with [ nil ⇒ False | cons _ _ ⇒ True ].
+
+definition isnotb_empty_list ≝
+λT:Type.λl:list T.match l with [ nil ⇒ false | cons _ _ ⇒ true ].
+
+lemma isnotbemptylist_to_isnotemptylist : ∀T,l.isnotb_empty_list T l = true → isnot_empty_list T l.
+ unfold isnotb_empty_list;
+ unfold isnot_empty_list;
+ intros;
+ elim l;
+ [ normalize; autobatch |
+   normalize; autobatch ]
+qed.
+
 lemma isempty_to_eq : ∀T,l.isb_empty_list T l = true → l = [].
  do 2 intro;
  elim l 0;
diff --git a/helm/software/matita/contribs/assembly/freescale/extra.ma b/helm/software/matita/contribs/assembly/freescale/extra.ma
index f683ecf8f..207a5a267 100644
--- a/helm/software/matita/contribs/assembly/freescale/extra.ma
+++ b/helm/software/matita/contribs/assembly/freescale/extra.ma
@@ -78,6 +78,27 @@ lemma xorbool_switch : ∀b1,b2.xor_bool b1 b2 = xor_bool b2 b1.
  reflexivity.
 qed.
 
+
+lemma orb_false_false :
+ ∀b1,b2:bool.((or_bool b1 b2) = false) → b1 = false.
+ intros 2;
+ elim b1 0;
+ elim b2;
+ simplify in H;
+ try destruct H;
+ reflexivity.
+qed.
+
+lemma orb_false_false_r :
+ ∀b1,b2:bool.((or_bool b1 b2) = false) → b2 = false.
+ intros 2;
+ elim b1 0;
+ elim b2;
+ simplify in H;
+ try destruct H;
+ reflexivity.
+qed.
+
 lemma eqbool_to_eq : ∀b1,b2:bool.(eq_bool b1 b2 = true) → (b1 = b2).
  unfold eq_bool;
  intros;
diff --git a/helm/software/matita/contribs/assembly/string/string.ma b/helm/software/matita/contribs/assembly/string/string.ma
index 7681c112e..3226eac43 100755
--- a/helm/software/matita/contribs/assembly/string/string.ma
+++ b/helm/software/matita/contribs/assembly/string/string.ma
@@ -49,6 +49,30 @@ let rec eqStr_str (str,str':aux_str_type) ≝
    ]
   ].
 
+lemma eqex_switch : ∀e1,e2.eq_ex e1 e2 = eq_ex e2 e1.
+ intros;
+ elim e1;
+ elim e2;
+ reflexivity.
+qed.
+
+lemma eqb8_switch : ∀b1,b2.eq_b8 b1 b2 = eq_b8 b2 b1.
+ intros;
+ elim b1;
+ elim b2;
+ unfold eq_b8;
+ rewrite > eqex_switch in ⊢ (? ? % ?);
+ rewrite > eqex_switch in ⊢ (? ? (? ? %) ?);
+ reflexivity.
+qed.
+
+lemma eqasciimin_switch : ∀a1,a2.eqAsciiMin a1 a2 = eqAsciiMin a2 a1.
+ intros;
+ unfold eqAsciiMin;
+ rewrite > eqb8_switch in ⊢ (? ? % ?);
+ reflexivity.
+qed.
+
 lemma eq_to_eqstr : ∀s,s'.s = s' → eqStr_str s s' = true.
  do 2 intro;
  intro;
-- 
2.39.2