From c7d638f7312eaabd7481d2a7cfb0d8508610f92b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 21 Jul 2008 10:55:23 +0000 Subject: [PATCH] ... --- .../contribs/assembly/compiler/ast_type.ma | 44 +++++-------------- 1 file changed, 12 insertions(+), 32 deletions(-) diff --git a/helm/software/matita/contribs/assembly/compiler/ast_type.ma b/helm/software/matita/contribs/assembly/compiler/ast_type.ma index 8ad0220ff..b1ad547e9 100755 --- a/helm/software/matita/contribs/assembly/compiler/ast_type.ma +++ b/helm/software/matita/contribs/assembly/compiler/ast_type.ma @@ -76,42 +76,22 @@ let rec eq_ast_type (t1,t2:ast_type) on t1 ≝ ]. 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; + 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)) - | 5: change in ⊢ (? ? % ?→?) with ((eq_ast_type a a1) ⊗ (eqb n n1)); - intro; - cut (a = a1 ∧ n = n1); - elim daemon. - | 9: elim daemon + | 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. -(* 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 ]. -- 2.39.2