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=abaf651b3d3ff230cac0b85bcd2cf70461400d05;hp=5939fe4f4155b8e1f13c94fbc06e462a6778813c;hpb=21f1fb39b5e1187ef87387f20522e60abe4f7c19;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 5939fe4f4..f1d78197c 100755 --- a/helm/software/matita/contribs/assembly/compiler/ast_type.ma +++ b/helm/software/matita/contribs/assembly/compiler/ast_type.ma @@ -47,6 +47,40 @@ 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. + +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 @@ -54,17 +88,192 @@ 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 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. + definition is_ast_base_type ≝ λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ True | _ ⇒ False ].