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=b1ad547e9485e4d189df2e3cc3828d9cc6f9f870;hpb=c7d638f7312eaabd7481d2a7cfb0d8508610f92b;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 b1ad547e9..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,31 +88,189 @@ 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 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. + 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; + 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 + ] + | 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.