new small devel

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

diff --git a/helm/software/matita/contribs/assembly/compiler/ast_type.ma b/helm/software/matita/contribs/assembly/compiler/ast_type.ma
index 5939fe4f4155b8e1f13c94fbc06e462a6778813c..b1ad547e9485e4d189df2e3cc3828d9cc6f9f870 100755 (executable)
--- a/helm/software/matita/contribs/assembly/compiler/ast_type.ma
+++ b/helm/software/matita/contribs/assembly/compiler/ast_type.ma
@@ -47,6 +47,16 @@ definition eq_ast_base_type ≝
   [ AST_BASE_TYPE_WORD32 ⇒ true | _ ⇒ false ]
  ].
 
+lemma eqastbasetype_to_eq : ∀t1,t2:ast_base_type.(eq_ast_base_type t1 t2 = true) → (t1 = t2).
+ unfold eq_ast_base_type;
+ intros;
+ elim t1 in H:(%);
+ elim t2 in H:(%);
+ normalize in H:(%);
+ try reflexivity;
+ destruct H.
+qed.
+
 let rec eq_ast_type (t1,t2:ast_type) on t1 ≝
  match t1 with
   [ AST_TYPE_BASE bType1 ⇒ match t2 with
@@ -65,6 +75,23 @@ let rec eq_ast_type (t1,t2:ast_type) on t1 ≝
    | _ ⇒ false ]
   ].
 
+lemma eqasttype_to_eq : ∀t1,t2:ast_type.(eq_ast_type t1 t2 = true) → (t1 = t2).
+ intro;
+ elim t1 0; [1,3:intros 2 | intros 4] elim t2;
+ [ 2,5,7,9: normalize in H1; destruct H1;
+ | 3,4: normalize in H; destruct H;
+ | 1: simplify in H;
+      apply (eq_f ?? (λx.? x) a a1 (eqastbasetype_to_eq a a1 H))
+ | 8: simplify in H2;
+      lapply (andb_true_true ? ? H2);
+      lapply (andb_true_true_r ? ? H2); clear H2;
+      rewrite > (H ? Hletin);
+      rewrite > (eqb_true_to_eq ?? Hletin1);
+      reflexivity
+ | 6: elim daemon; 
+ ].
+qed.
+
 definition is_ast_base_type ≝
 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ True | _ ⇒ False ].