X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Fcompiler%2Fast_type.ma;h=f1d78197c839c3d63608cd39d8603e7cb5eef416;hb=7ec26dcce747c05e2f0d12940d7d92237dbe9146;hp=8ad0220ffa804cc0db0823a12593a35efbd7e39a;hpb=f2d9db85559c7a8db11aae1153495fae4a258d54;p=helm.git

diff --git a/helm/software/matita/contribs/assembly/compiler/ast_type.ma b/helm/software/matita/contribs/assembly/compiler/ast_type.ma
index 8ad0220ff..f1d78197c 100755
--- a/helm/software/matita/contribs/assembly/compiler/ast_type.ma
+++ b/helm/software/matita/contribs/assembly/compiler/ast_type.ma
@@ -57,6 +57,30 @@ lemma eqastbasetype_to_eq : ∀t1,t2:ast_base_type.(eq_ast_base_type t1 t2 = tru
  destruct H.
 qed.
 
+lemma eq_to_eqastbasetype : ∀t1,t2.t1 = t2 → eq_ast_base_type t1 t2 = true.
+ do 2 intro;
+ elim t1 0;
+ elim t2 0;
+ normalize;
+ intro;
+ try destruct H;
+ reflexivity.
+qed.
+
+definition eq_ast_type_aux ≝
+λT:Type.λf:T → T → bool.
+ let rec aux (nl1,nl2:ne_list T) on nl1 ≝
+  match nl1 with
+   [ ne_nil h ⇒ match nl2 with
+    [ ne_nil h' ⇒ f h h'
+    | ne_cons h' _ ⇒ false
+    ]
+   | ne_cons h t ⇒ match nl2 with
+    [ ne_nil h' ⇒ false
+    | ne_cons h' t' ⇒ (f h h') ⊗ (aux t t')
+    ]
+   ] in aux.
+
 let rec eq_ast_type (t1,t2:ast_type) on t1 ≝
  match t1 with
   [ AST_TYPE_BASE bType1 ⇒ match t2 with
@@ -64,53 +88,191 @@ let rec eq_ast_type (t1,t2:ast_type) on t1 ≝
   | AST_TYPE_ARRAY subType1 dim1 ⇒ match t2 with
    [ AST_TYPE_ARRAY subType2 dim2 ⇒ (eq_ast_type subType1 subType2) ⊗ (eqb dim1 dim2) | _ ⇒ false ]
   | AST_TYPE_STRUCT nelSubType1 ⇒ match t2 with
-   [ AST_TYPE_STRUCT nelSubType2 ⇒ 
-    fst ?? (fold_right_neList ?? (λh,t.match fst ?? t with
-                                       [ true ⇒ match nth_neList ? nelSubType2 ((len_neList ? nelSubType2)-(snd ?? t)-1) with
-                                        [ None ⇒ pair ?? false (S (snd ?? t))
-                                        | Some cfr ⇒ match eq_ast_type h cfr with
-                                         [ true ⇒ pair ?? true (S (snd ?? t))
-                                         | false ⇒ pair ?? false (S (snd ?? t)) ]]
-                                       | false ⇒ t]) (pair ?? true O) nelSubType1)
+   [ AST_TYPE_STRUCT nelSubType2 ⇒ eq_ast_type_aux ? eq_ast_type nelSubType1 nelSubType2
    | _ ⇒ 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
- ].
+lemma eq_ast_type_elim : 
+ ∀P:ast_type → Prop.
+  (∀x.P (AST_TYPE_BASE x)) → 
+  (∀t:ast_type.∀n.(P t) → (P (AST_TYPE_ARRAY t n))) →
+  (∀x.(P x) → (P (AST_TYPE_STRUCT (ne_nil ? x)))) →
+  (∀x,l.(P x) → (P (AST_TYPE_STRUCT l)) → (P (AST_TYPE_STRUCT (ne_cons ? x l)))) →
+  (∀t.(P t)).
+ intros; 
+ apply
+  (let rec aux t ≝ 
+    match t
+     return λt.P t
+    with
+     [ AST_TYPE_BASE b ⇒ H b
+     | AST_TYPE_ARRAY t n ⇒ H1 t n (aux t)
+     | AST_TYPE_STRUCT l ⇒
+      let rec aux_l (l:ne_list ast_type ) ≝
+       match l
+        return λl.P (AST_TYPE_STRUCT l)
+       with
+        [ ne_nil t => H2 t (aux t)
+        | ne_cons hd tl => H3 hd tl (aux hd) (aux_l tl)
+        ] in aux_l l
+     ] in aux t);
 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
-                ]
+lemma eqasttype_to_eq : ∀t1,t2:ast_type.(eq_ast_type t1 t2 = true) → (t1 = t2).
+ intro;
+ elim t1 using eq_ast_type_elim 0;
+ [ 1: intros 2;
+      elim t2 using eq_ast_type_elim 0;
+      [ 1: intros;
+           simplify in H;
+           rewrite > (eqastbasetype_to_eq ?? H); 
+           reflexivity
+      | 2: simplify;
+           intros;
+           destruct H1
+      | 3: simplify;
+           intros;
+           destruct H1
+      | 4: simplify;
+           intros;
+           destruct H2
+      ]
+ | 2: intros 4;
+      elim t2 using eq_ast_type_elim 0;
+      [ 1: simplify;
+           intros;
+           destruct H1
+      | 2: simplify;
+           intros;
+           lapply (andb_true_true ?? H2) as H3;
+           lapply (andb_true_true_r ?? H2) as H4;
+           rewrite > (H ? H3);
+           rewrite > (eqb_true_to_eq ?? H4);
+           reflexivity
+      | 3: simplify;
+           intros;
+           destruct H2
+      | 4: simplify;
+           intros;
+           destruct H3
+      ]
+ | 3: intros 3;
+      elim t2 using eq_ast_type_elim 0;
+      [ 1: simplify;
+           intros;
+           destruct H1
+      | 2: simplify;
+           intros;
+           destruct H2
+      | 3: intros;
+           simplify in H2;
+           rewrite > (H x1);
+           [ reflexivity
+           | apply H2
            ]
+      | 4: intros;
+           simplify in H3;
+           destruct H3
       ]
- | 9: TODO elim daemon
- ]
+ | 4: intros 5;
+      elim t2 using eq_ast_type_elim 0;
+      [ 1: simplify;
+           intros;
+           destruct H2
+      | 2: simplify;
+           intros;
+           destruct H3
+      | 3: simplify;
+           intros;
+           destruct H3
+      | 4: intros;
+           simplify in H4;
+           lapply (andb_true_true ?? H4) as H5;
+           lapply (andb_true_true_r ?? H4) as H6;
+           rewrite > (H ? H5);
+           lapply depth=0 (H1 (AST_TYPE_STRUCT l1)) as K;
+           destruct (K ?);
+           [ apply H6
+           | reflexivity
+           ]
+      ]
+ ]. 
+qed.
+
+lemma eq_to_eqasttype : ∀t1,t2.t1 = t2 → eq_ast_type t1 t2 = true.
+ intro;
+ elim t1 using eq_ast_type_elim 0;
+ [ 1: intros 2;
+      elim t2 using eq_ast_type_elim 0;
+      [ 1: simplify;
+           intros;
+           destruct H;
+           apply (eq_to_eqastbasetype x x (refl_eq ??))
+      | 2: simplify;
+           intros;
+           destruct H1
+      | 3: simplify;
+           intros;
+           destruct H1
+      | 4: simplify;
+           intros;
+           destruct H2
+      ]
+ | 2: intros 4;
+      elim t2 using eq_ast_type_elim 0;
+      [ 1: simplify;
+           intros;
+           destruct H1
+      | 2: intros;
+           simplify;
+           destruct H2;
+           rewrite > (H t (refl_eq ??));
+           rewrite > (eq_to_eqb_true n n (refl_eq ??));
+           reflexivity
+      | 3: simplify;
+           intros;
+           destruct H2
+      | 4: simplify;
+           intros;
+           destruct H3
+      ]
+ | 3: intros 3;
+      elim t2 using eq_ast_type_elim 0;
+      [ 1: simplify;
+           intros;
+           destruct H1
+      | 2: simplify;
+           intros;
+           destruct H2
+      | 3: intros;
+           simplify;
+           destruct H2;
+           rewrite > (H x (refl_eq ??));
+           reflexivity
+      | 4: simplify;
+           intros;
+           destruct H3
+      ]
+ | 4: intros 5;
+      elim t2 using eq_ast_type_elim 0;
+      [ 1: simplify;
+           intros;
+           destruct H2
+      | 2: simplify;
+           intros;
+           destruct H3
+      | 3: simplify;
+           intros;
+           destruct H3
+      | 4: intros;
+           simplify;
+           destruct H4;
+           rewrite > (H x (refl_eq ??));
+           rewrite > (H1 (AST_TYPE_STRUCT l) (refl_eq ??));
+           reflexivity
+      ]
+ ].
 qed.
-*)
 
 definition is_ast_base_type ≝
 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ True | _ ⇒ False ].