Semantic analysis implemented (sort of).

[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..8ad0220ffa804cc0db0823a12593a35efbd7e39a 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,43 @@ 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).
+ do 2 intro;
+ cases t1; cases t2;
+ [ 2,3,4,6,7,8: normalize; intro; destruct H
+ | 1: change in ⊢ (? ? % ?→?) with (eq_ast_base_type a a1);
+      intro;
+      apply (eq_f ?? (λx.? x) a a1 (eqastbasetype_to_eq a a1 H))
+ | 5: change in ⊢ (? ? % ?→?) with ((eq_ast_type a a1) ⊗ (eqb n n1));
+      intro;
+      cut (a = a1 ∧ n = n1);
+      elim daemon.
+ | 9: elim daemon
+ ].
+qed.
+
+(* PERCHE' ??
+ se in testa includo
+ include "demo/natural_deduction.ma".
+ la dimostrazione va fino in fondo ma poi impazzisce ast_tree.ma
+ dicendo che la dichiarazione ast_id e' scorretta
+ 
+      [ 1: alias id "And_elim_l" = "cic:/matita/demo/natural_deduction/And_elim_l.con".
+           alias id "And_elim_r" = "cic:/matita/demo/natural_deduction/And_elim_r.con".
+           apply (eq_f2 ??? (λx.λy.? x y) a a1 n n1 (And_elim_l ?? Hcut) (And_elim_r ?? Hcut))
+      | 2: split;
+           [ 2: apply (eqb_true_to_eq n n1 (andb_true_true_r ?? H))
+           | 1: cut (eq_ast_Type a a1 = true);
+                [ 2: apply (andb_true_true ?? H)
+                | 1: TODO elim daemon
+                ]
+           ]
+      ]
+ | 9: TODO elim daemon
+ ]
+qed.
+*)
+
 definition is_ast_base_type ≝
 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ True | _ ⇒ False ].