- setters for data structures now support "commuting conversion"-like

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

diff --git a/helm/software/matita/contribs/assembly/compiler/environment.ma b/helm/software/matita/contribs/assembly/compiler/environment.ma
index 326ed1d2031cf7b0e0581cbe0861e5fd2d9a586f..8131570820a1538c390d4f192a7cfd7e5525737d 100755 (executable)
--- a/helm/software/matita/contribs/assembly/compiler/environment.ma
+++ b/helm/software/matita/contribs/assembly/compiler/environment.ma
@@ -42,36 +42,36 @@ definition aux_env_type ≝ ne_list (list var_elem).
 definition get_const_desc ≝ λd:desc_elem.match d with [ DESC_ELEM c _ ⇒ c ].
 definition get_type_desc ≝ λd:desc_elem.match d with [ DESC_ELEM _ t ⇒ t ].
 
+definition eqDesc_elem ≝ λd,d'.(eq_bool (get_const_desc d) (get_const_desc d'))⊗(eq_ast_type (get_type_desc d) (get_type_desc d')).
+
+lemma eq_to_eqdescelem : ∀d,d'.d = d' → eqDesc_elem d d' = true.
+ intros 3;
+ rewrite < H;
+ elim d;
+ simplify;
+ rewrite > (eq_to_eqbool b b (refl_eq ??));
+ rewrite > (eq_to_eqasttype a a (refl_eq ??));
+ reflexivity.
+qed.
+
+lemma eqdescelem_to_eq : ∀d,d'.eqDesc_elem d d' = true → d = d'.
+ intros 2;
+ elim d 0;
+ elim d' 0;
+ intros 4;
+ simplify;
+ intro;
+ rewrite > (eqbool_to_eq b1 b (andb_true_true ?? H));
+ rewrite > (eqasttype_to_eq a1 a (andb_true_true_r ?? H));
+ reflexivity.
+qed.
+
 definition get_name_var ≝ λv:var_elem.match v with [ VAR_ELEM n _ ⇒ n ].
 definition get_desc_var ≝ λv:var_elem.match v with [ VAR_ELEM _ d ⇒ d ].
 
 (* ambiente vuoto *)
 definition empty_env ≝ ne_nil ? (nil var_elem ).
 
-(* confronto *)
-let rec eq_aux_env_type_aux (subE,subE':list var_elem) on subE ≝
- match subE with
-  [ nil ⇒ match subE' with
-   [ nil ⇒ true | cons _ _ ⇒ false ]
-  | cons h tl ⇒ match subE' with
-   [ nil ⇒ false | cons h' tl' ⇒ (strCmp_str (get_name_var h) (get_name_var h'))⊗
-                                 (eq_bool (get_const_desc (get_desc_var h)) (get_const_desc (get_desc_var h')))⊗
-                                 (eq_ast_type (get_type_desc (get_desc_var h)) (get_type_desc (get_desc_var h')))⊗   
-                                 (eq_aux_env_type_aux tl tl') ]
-  ].
-
-axiom eqbauxenvtypeaux_to_eq : ∀e,e'.eq_aux_env_type_aux e e' = true → e = e'.
-
-let rec eq_aux_env_type (e,e':aux_env_type) on e ≝
- match e with
-  [ ne_nil h ⇒ match e' with
-   [ ne_nil h' ⇒ eq_aux_env_type_aux h h' | ne_cons _ _ ⇒ false ]
-  | ne_cons h tl ⇒ match e' with
-   [ ne_nil h' ⇒ false | ne_cons h' tl' ⇒ (eq_aux_env_type_aux h h')⊗(eq_aux_env_type tl tl') ]
-  ].
-
-axiom eqbauxenvtype_to_eq : ∀e,e':aux_env_type.eq_aux_env_type e e' = true → e = e'.
-
 (* setter *)
 definition enter_env ≝ λe:aux_env_type.empty_env&e.
 definition leave_env ≝ λe:aux_env_type.cut_first_neList ? e.
@@ -80,7 +80,7 @@ definition leave_env ≝ λe:aux_env_type.cut_first_neList ? e.
 let rec get_desc_from_lev_env (env:list var_elem ) (str:aux_str_type) on env ≝
 match env with
  [ nil ⇒ None ?
- | cons h t ⇒ match strCmp_str str (get_name_var h) with
+ | cons h t ⇒ match eqStr_str str (get_name_var h) with
   [ true ⇒ Some ? (get_desc_var h)
   | false ⇒ get_desc_from_lev_env t str ]].
 
@@ -134,5 +134,33 @@ definition add_desc_env ≝
 (*let var ≝ VAR_ELEM str (DESC_ELEM c desc) in*)
  match e with
   [ ne_nil h ⇒ ne_nil ? ((VAR_ELEM str (DESC_ELEM c desc))::h)
-  | ne_cons h tl ⇒ «((VAR_ELEM str (DESC_ELEM c desc))::h) £ »&tl
+  | ne_cons h tl ⇒ «£((VAR_ELEM str (DESC_ELEM c desc))::h)»&tl
   ].
+
+(* controllo e <= e' *)
+definition eq_env_elem ≝
+λe1,e2.match e1 with
+ [ VAR_ELEM s1 d1 ⇒ match e2 with
+  [ VAR_ELEM s2 d2 ⇒ (eqStr_str s1 s2)⊗(eqDesc_elem d1 d2) ]].
+
+lemma eq_to_eqenv : ∀e1,e2.e1 = e2 → eq_env_elem e1 e2 = true.
+ intros 3;
+ rewrite < H;
+ elim e1;
+ simplify;
+ rewrite > (eq_to_eqstr a a (refl_eq ??));
+ rewrite > (eq_to_eqdescelem d d (refl_eq ??));
+ reflexivity.
+qed.
+
+lemma eqenv_to_eq : ∀e1,e2.eq_env_elem e1 e2 = true → e1 = e2.
+ intros 2;
+ elim e1 0;
+ elim e2 0;
+ intros 4;
+ simplify;
+ intro;
+ rewrite > (eqstr_to_eq a1 a (andb_true_true ?? H));
+ rewrite > (eqdescelem_to_eq d1 d (andb_true_true_r ?? H));
+ reflexivity.
+qed.