X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fcompiler%2Fast_type_lemmas.ma;h=4bc55e2d7434bdc45bd0892419bdec665d09b2c9;hb=34cdd4af2d7bdac3bab74a54123fbfcb02fa0403;hp=2753d6118cf510c563dbe01ee9d5b079205d48d1;hpb=fc1e871dde0f9f4cfde6f4a4fda8d18022584e65;p=helm.git diff --git a/helm/software/matita/contribs/ng_assembly/compiler/ast_type_lemmas.ma b/helm/software/matita/contribs/ng_assembly/compiler/ast_type_lemmas.ma index 2753d6118..4bc55e2d7 100755 --- a/helm/software/matita/contribs/ng_assembly/compiler/ast_type_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/compiler/ast_type_lemmas.ma @@ -16,7 +16,7 @@ (* Progetto FreeScale *) (* *) (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Ultima modifica: 05/08/2009 *) +(* Sviluppo: 2008-2010 *) (* *) (* ********************************************************************** *) @@ -27,6 +27,7 @@ include "common/list_utility_lemmas.ma". (* dimensioni degli elementi *) (* ************************* *) +(* ndefinition astbasetype_destruct_aux ≝ Πb1,b2:ast_base_type.ΠP:Prop.b1 = b2 → match eq_astbasetype b1 b2 with [ true ⇒ P → P | false ⇒ P ]. @@ -38,54 +39,53 @@ ndefinition astbasetype_destruct : astbasetype_destruct_aux. nnormalize; napply (λx.x). nqed. +*) -nlemma symmetric_eqastbasetype : symmetricT ast_base_type bool eq_astbasetype. - #b1; #b2; ncases b1; ncases b2; nnormalize; napply refl_eq. nqed. +nlemma eq_to_eqastbasetype : ∀n1,n2.n1 = n2 → eq_astbasetype n1 n2 = true. + #n1; #n2; #H; + nrewrite > H; + nelim n2; + nnormalize; + napply refl_eq. +nqed. -nlemma eqastbasetype_to_eq : ∀b1,b2.eq_astbasetype b1 b2 = true → b1 = b2. - #b1; #b2; ncases b1; ncases b2; nnormalize; - ##[ ##1,5,9: #H; napply refl_eq - ##| ##*: #H; napply (bool_destruct … H) +nlemma neqastbasetype_to_neq : ∀n1,n2.eq_astbasetype n1 n2 = false → n1 ≠ n2. + #n1; #n2; #H; + napply (not_to_not (n1 = n2) (eq_astbasetype n1 n2 = true) …); + ##[ ##1: napply (eq_to_eqastbasetype n1 n2) + ##| ##2: napply (eqfalse_to_neqtrue … H) ##] nqed. -nlemma eq_to_eqastbasetype : ∀b1,b2.b1 = b2 → eq_astbasetype b1 b2 = true. +nlemma eqastbasetype_to_eq : ∀b1,b2.eq_astbasetype b1 b2 = true → b1 = b2. #b1; #b2; ncases b1; ncases b2; nnormalize; ##[ ##1,5,9: #H; napply refl_eq - ##| ##*: #H; napply (astbasetype_destruct … H) + ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*) ##] nqed. -nlemma decidable_astbasetype : ∀x,y:ast_base_type.decidable (x = y). - #x; #y; - nnormalize; - nelim x; - nelim y; - ##[ ##1,5,9: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); - nnormalize; #H; - napply False_ind; - napply (astbasetype_destruct … H) - ##] +nlemma neq_to_neqastbasetype : ∀n1,n2.n1 ≠ n2 → eq_astbasetype n1 n2 = false. + #n1; #n2; #H; + napply (neqtrue_to_eqfalse (eq_astbasetype n1 n2)); + napply (not_to_not (eq_astbasetype n1 n2 = true) (n1 = n2) ? H); + napply (eqastbasetype_to_eq n1 n2). nqed. -nlemma neqastbasetype_to_neq : ∀b1,b2.(eq_astbasetype b1 b2 = false) → (b1 ≠ b2). - #b1; #b2; - ncases b1; - ncases b2; - nnormalize; - ##[ ##1,5,9: #H; napply (bool_destruct … H) - ##| ##*: #H; #H1; napply (astbasetype_destruct … H1) +nlemma decidable_astbasetype : ∀x,y:ast_base_type.decidable (x = y). + #x; #y; nnormalize; + napply (or2_elim (eq_astbasetype x y = true) (eq_astbasetype x y = false) ? (decidable_bexpr ?)); + ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqastbasetype_to_eq … H)) + ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqastbasetype_to_neq … H)) ##] nqed. -nlemma neq_to_neqastbasetype : ∀b1,b2.b1 ≠ b2 → eq_astbasetype b1 b2 = false. - #b1; #b2; - ncases b1; - ncases b2; - nnormalize; - ##[ ##1,5,9: #H; nelim (H (refl_eq …)) - ##| ##*: #H; napply refl_eq +nlemma symmetric_eqastbasetype : symmetricT ast_base_type bool eq_astbasetype. + #n1; #n2; + napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_astbasetype n1 n2)); + ##[ ##1: #H; nrewrite > H; napply refl_eq + ##| ##2: #H; nrewrite > (neq_to_neqastbasetype n1 n2 H); + napply (symmetric_eq ? (eq_astbasetype n2 n1) false); + napply (neq_to_neqastbasetype n2 n1 (symmetric_neq ? n1 n2 H)) ##] nqed. @@ -121,6 +121,7 @@ nlemma asttype_destruct_struct_struct : ∀b1,b2.AST_TYPE_STRUCT b1 = AST_TYPE_S napply refl_eq. nqed. +(* ndefinition asttype_destruct_aux ≝ Πb1,b2:ast_type.ΠP:Prop.b1 = b2 → match eq_asttype b1 b2 with [ true ⇒ P → P | false ⇒ P ]. @@ -151,97 +152,7 @@ ndefinition asttype_destruct : asttype_destruct_aux. ##] ##] nqed. - -nlemma symmetric_eqasttype_aux1 - : ∀nl1,nl2. - (eq_asttype (AST_TYPE_STRUCT nl1) (AST_TYPE_STRUCT nl2)) = (eq_asttype (AST_TYPE_STRUCT nl2) (AST_TYPE_STRUCT nl1)) → - (bfold_right_neList2 ? (λx,y.eq_asttype x y) nl1 nl2) = (bfold_right_neList2 ? (λx,y.eq_asttype x y) nl2 nl1). - #nl1; #nl2; #H; - napply H. -nqed. - -nlemma symmetric_eqasttype : symmetricT ast_type bool eq_asttype. - #t1; napply (ast_type_index … t1); - ##[ ##1: #b1; #t2; ncases t2; - ##[ ##1: #b2; nchange with ((eq_astbasetype b1 b2) = (eq_astbasetype b2 b1)); - nrewrite > (symmetric_eqastbasetype b1 b2); - napply refl_eq - ##| ##2: #st2; #n2; nnormalize; napply refl_eq - ##| ##3: #nl2; nnormalize; napply refl_eq - ##] - ##| ##2: #st1; #n1; #H; #t2; ncases t2; - ##[ ##2: #st2; #n2; nchange with (((eq_asttype st1 st2)⊗(eq_nat n1 n2)) = ((eq_asttype st2 st1)⊗(eq_nat n2 n1))); - nrewrite > (symmetric_eqnat n1 n2); - nrewrite > (H st2); - napply refl_eq - ##| ##1: #b2; nnormalize; napply refl_eq - ##| ##3: #nl2; nnormalize; napply refl_eq - ##] - ##| ##3: #hh1; #H; #t2; ncases t2; - ##[ ##3: #nl2; ncases nl2; - ##[ ##1: #hh2; nchange with ((eq_asttype hh1 hh2) = (eq_asttype hh2 hh1)); - nrewrite > (H hh2); - napply refl_eq - ##| ##2: #hh2; #ll2; nnormalize; napply refl_eq - ##] - ##| ##1: #b2; nnormalize; napply refl_eq - ##| ##2: #st2; #n2; nnormalize; napply refl_eq - ##] - ##| ##4: #hh1; #ll1; #H; #H1; #t2; ncases t2; - ##[ ##3: #nl2; ncases nl2; - ##[ ##1: #hh2; nnormalize; napply refl_eq - ##| ##2: #hh2; #ll2; nnormalize; - nrewrite > (H hh2); - nrewrite > (symmetric_eqasttype_aux1 ll1 ll2 (H1 (AST_TYPE_STRUCT ll2))); - napply refl_eq - ##] - ##| ##1: #b2; nnormalize; napply refl_eq - ##| ##2: #st2; #n2; nnormalize; napply refl_eq - ##] - ##] -nqed. - -nlemma eqasttype_to_eq : ∀t1,t2.eq_asttype t1 t2 = true → t1 = t2. - #t1; - napply (ast_type_index … t1); - ##[ ##1: #b1; #t2; ncases t2; - ##[ ##1: #b2; #H; nchange in H:(%) with ((eq_astbasetype b1 b2) = true); - nrewrite > (eqastbasetype_to_eq b1 b2 H); - napply refl_eq - ##| ##2: #st2; #n2; nnormalize; #H; napply (bool_destruct … H) - ##| ##3: #nl2; nnormalize; #H; napply (bool_destruct … H) - ##] - ##| ##2: #st1; #n1; #H; #t2; ncases t2; - ##[ ##2: #st2; #n2; #H1; nchange in H1:(%) with (((eq_asttype st1 st2)⊗(eq_nat n1 n2)) = true); - nrewrite > (H st2 (andb_true_true_l … H1)); - nrewrite > (eqnat_to_eq n1 n2 (andb_true_true_r … H1)); - napply refl_eq - ##| ##1: #b2; nnormalize; #H1; napply (bool_destruct … H1) - ##| ##3: #nl2; nnormalize; #H1; napply (bool_destruct … H1) - ##] - ##| ##3: #hh1; #H; #t2; ncases t2; - ##[ ##3: #nl2; ncases nl2; - ##[ ##1: #hh2; #H1; nchange in H1:(%) with ((eq_asttype hh1 hh2) = true); - nrewrite > (H hh2 H1); - napply refl_eq - ##| ##2: #hh2; #ll2; nnormalize; #H1; napply (bool_destruct … H1) - ##] - ##| ##1: #b2; nnormalize; #H1; napply (bool_destruct … H1) - ##| ##2: #st2; #n2; nnormalize; #H1; napply (bool_destruct … H1) - ##] - ##| ##4: #hh1; #ll1; #H; #H1; #t2; ncases t2; - ##[ ##3: #nl2; ncases nl2; - ##[ ##1: #hh2; nnormalize; #H2; napply (bool_destruct … H2) - ##| ##2: #hh2; #ll2; #H2; nchange in H2:(%) with (((eq_asttype hh1 hh2)⊗(bfold_right_neList2 ? (λx,y.eq_asttype x y) ll1 ll2)) = true); - nrewrite > (H hh2 (andb_true_true_l … H2)); - nrewrite > (asttype_destruct_struct_struct ll1 ll2 (H1 (AST_TYPE_STRUCT ll2) (andb_true_true_r … H2))); - napply refl_eq - ##] - ##| ##1: #b2; nnormalize; #H2; napply (bool_destruct … H2) - ##| ##2: #st2; #n2; nnormalize; #H2; napply (bool_destruct … H2) - ##] - ##] -nqed. +*) nlemma eq_to_eqasttype_aux1 : ∀nl1,nl2. @@ -259,8 +170,8 @@ nlemma eq_to_eqasttype : ∀t1,t2.t1 = t2 → eq_asttype t1 t2 = true. nchange with ((eq_astbasetype b2 b2) = true); nrewrite > (eq_to_eqastbasetype b2 b2 (refl_eq …)); napply refl_eq - ##| ##2: #st2; #n2; #H; napply (asttype_destruct … H) - ##| ##3: #nl2; #H; napply (asttype_destruct … H) + ##| ##2: #st2; #n2; #H; ndestruct (*napply (asttype_destruct … H)*) + ##| ##3: #nl2; #H; ndestruct (*napply (asttype_destruct … H)*) ##] ##| ##2: #st1; #n1; #H; #t2; ncases t2; ##[ ##2: #st2; #n2; #H1; nchange with (((eq_asttype st1 st2)⊗(eq_nat n1 n2)) = true); @@ -268,22 +179,26 @@ nlemma eq_to_eqasttype : ∀t1,t2.t1 = t2 → eq_asttype t1 t2 = true. nrewrite > (eq_to_eqnat n1 n2 (asttype_destruct_array_array_2 … H1)); nnormalize; napply refl_eq - ##| ##1: #b2; #H1; napply (asttype_destruct … H1) - ##| ##3: #nl2; #H1; napply (asttype_destruct … H1) + ##| ##1: #b2; #H1; ndestruct (*napply (asttype_destruct … H1)*) + ##| ##3: #nl2; #H1; ndestruct (*napply (asttype_destruct … H1)*) ##] ##| ##3: #hh1; #H; #t2; ncases t2; ##[ ##3: #nl2; ncases nl2; ##[ ##1: #hh2; #H1; nchange with ((eq_asttype hh1 hh2) = true); nrewrite > (H hh2 (nelist_destruct_nil_nil ? hh1 hh2 (asttype_destruct_struct_struct … H1))); napply refl_eq - ##| ##2: #hh2; #ll2; #H1; nelim (nelist_destruct_nil_cons ? hh1 hh2 ll2 (asttype_destruct_struct_struct … H1)) + ##| ##2: #hh2; #ll2; #H1; + (* !!! ndestruct non va *) + nelim (nelist_destruct_nil_cons ? hh1 hh2 ll2 (asttype_destruct_struct_struct … H1)) ##] - ##| ##1: #b2; #H1; napply (asttype_destruct … H1) - ##| ##2: #st2; #n2; #H1; napply (asttype_destruct … H1) + ##| ##1: #b2; #H1; ndestruct (*napply (asttype_destruct … H1)*) + ##| ##2: #st2; #n2; #H1; ndestruct (*napply (asttype_destruct … H1)*) ##] ##| ##4: #hh1; #ll1; #H; #H1; #t2; ncases t2; ##[ ##3: #nl2; ncases nl2; - ##[ ##1: #hh2; #H2; nelim (nelist_destruct_cons_nil ? hh1 hh2 ll1 (asttype_destruct_struct_struct … H2)) + ##[ ##1: #hh2; #H2; + (* !!! ndestruct non va *) + nelim (nelist_destruct_cons_nil ? hh1 hh2 ll1 (asttype_destruct_struct_struct … H2)) ##| ##2: #hh2; #ll2; #H2; nchange with (((eq_asttype hh1 hh2)⊗(bfold_right_neList2 ? (λx,y.eq_asttype x y) ll1 ll2)) = true); nrewrite > (H hh2 (nelist_destruct_cons_cons_1 … (asttype_destruct_struct_struct … H2))); nrewrite > (eq_to_eqasttype_aux1 ll1 ll2 (H1 (AST_TYPE_STRUCT ll2) ?)); @@ -292,191 +207,84 @@ nlemma eq_to_eqasttype : ∀t1,t2.t1 = t2 → eq_asttype t1 t2 = true. napply refl_eq ##] ##] - ##| ##1: #b2; #H2; napply (asttype_destruct … H2) - ##| ##2: #st2; #n2; #H2; napply (asttype_destruct … H2) + ##| ##1: #b2; #H2; ndestruct (*napply (asttype_destruct … H2)*) + ##| ##2: #st2; #n2; #H2; ndestruct (*napply (asttype_destruct … H2)*) ##] ##] nqed. -nlemma decidable_asttype : ∀x,y:ast_type.decidable (x = y). - #x; - napply (ast_type_index … x); - ##[ ##1: #b1; #y; ncases y; - ##[ ##1: #b2; nnormalize; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_astbasetype b1 b2)); - ##[ ##1: #H; nrewrite > H; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …)) - ##| ##2: #H; napply (or2_intro2 (? = ?) (? ≠ ?) …); - nnormalize; #H1; napply (H (asttype_destruct_base_base … H1)) - ##] - ##| ##2: #b2; #n2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) …); - nnormalize; #H; napply (asttype_destruct … H) - ##| ##3: #n2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) …); - nnormalize; #H; napply (asttype_destruct … H) - ##] - ##| ##2: #b1; #n1; #H; #y; ncases y; - ##[ ##2: #b2; #n2; nnormalize; napply (or2_elim (? = ?) (? ≠ ?) ? (H b2)); - ##[ ##2: #H1; napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; - #H2; napply (H1 (asttype_destruct_array_array_1 … H2)) - ##| ##1: #H1; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_nat n1 n2)); - ##[ ##2: #H2; napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; - #H3; napply (H2 (asttype_destruct_array_array_2 … H3)) - ##| ##1: #H2; nrewrite > H1; nrewrite > H2; - napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …)) - ##] - ##] - ##| ##1: #b2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) …); - nnormalize; #H1; napply (asttype_destruct … H1) - ##| ##3: #n2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) …); - nnormalize; #H1; napply (asttype_destruct … H1) - ##] - ##| ##3: #hh1; #H; #y; ncases y; - ##[ ##3: #n2; ncases n2; - ##[ ##1: #hh2; nnormalize; napply (or2_elim (? = ?) (? ≠ ?) ? (H hh2)); - ##[ ##2: #H1; napply (or2_intro2 (? = ?) (? ≠ ?) …); - nnormalize; #H2; - napply (H1 (nelist_destruct_nil_nil … (asttype_destruct_struct_struct … H2))) - ##| ##1: #H1; nrewrite > H1; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …)) - ##] - ##| ##2: #hh2; #tt2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) …); - nnormalize; #H1; napply (nelist_destruct_nil_cons ast_type … (asttype_destruct_struct_struct … H1)) - ##] - ##| ##1: #b2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) …); - nnormalize; #H1; napply (asttype_destruct … H1) - ##| ##2: #b2; #n2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) …); - nnormalize; #H1; napply (asttype_destruct … H1) - ##] - ##| ##4: #hh1; #tt1; #H; #H1; #y; ncases y; - ##[ ##3: #n2; ncases n2; - ##[ ##2: #hh2; #tt2; nnormalize; napply (or2_elim (? = ?) (? ≠ ?) ? (H hh2)); - ##[ ##2: #H2; napply (or2_intro2 (? = ?) (? ≠ ?) …); - nnormalize; #H3; napply (H2 (nelist_destruct_cons_cons_1 ast_type … (asttype_destruct_struct_struct … H3))) - ##| ##1: #H2; napply (or2_elim (? = ?) (? ≠ ?) ? (H1 (AST_TYPE_STRUCT tt2))); - ##[ ##2: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) …); - nnormalize; #H4; napply H3; - nrewrite > (nelist_destruct_cons_cons_2 ast_type … (asttype_destruct_struct_struct … H4)); - napply refl_eq - ##| ##1: #H3; nrewrite > H2; nrewrite > (asttype_destruct_struct_struct … H3); - napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …)) - ##] - ##] - ##| ##1: #hh2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) …); - nnormalize; #H2; napply (nelist_destruct_cons_nil ast_type … (asttype_destruct_struct_struct … H2)) - ##] - ##| ##1: #b2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) …); - nnormalize; #H2; napply (asttype_destruct … H2) - ##| ##2: #b2; #n2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) …); - nnormalize; #H2; napply (asttype_destruct … H2) - ##] +nlemma neqasttype_to_neq : ∀n1,n2.eq_asttype n1 n2 = false → n1 ≠ n2. + #n1; #n2; #H; + napply (not_to_not (n1 = n2) (eq_asttype n1 n2 = true) …); + ##[ ##1: napply (eq_to_eqasttype n1 n2) + ##| ##2: napply (eqfalse_to_neqtrue … H) ##] nqed. -nlemma neqasttype_to_neq : ∀t1,t2.eq_asttype t1 t2 = false → t1 ≠ t2. +nlemma eqasttype_to_eq : ∀t1,t2.eq_asttype t1 t2 = true → t1 = t2. #t1; napply (ast_type_index … t1); ##[ ##1: #b1; #t2; ncases t2; - ##[ ##1: #b2; nchange with ((eq_astbasetype b1 b2 = false) → ?); #H; - nnormalize; #H1; napply (neqastbasetype_to_neq b1 b2 H); - napply (asttype_destruct_base_base … H1) - ##| ##2: #b2; #n2; nnormalize; #H; #H1; napply (asttype_destruct … H1) - ##| ##3: #n2; nnormalize; #H; #H1; napply (asttype_destruct … H1) + ##[ ##1: #b2; #H; nchange in H:(%) with ((eq_astbasetype b1 b2) = true); + nrewrite > (eqastbasetype_to_eq b1 b2 H); + napply refl_eq + ##| ##2: #st2; #n2; nnormalize; #H; ndestruct (*napply (bool_destruct … H)*) + ##| ##3: #nl2; nnormalize; #H; ndestruct (*napply (bool_destruct … H)*) ##] - ##| ##2: #b1; #n1; #H; #t2; ncases t2; - ##[ ##2: #b2; #n2; nchange with ((((eq_asttype b1 b2)⊗(eq_nat n1 n2)) = false) → ?); #H1; - napply (or2_elim ??? (andb_false2 … H1)); - ##[ ##1: #H2; nnormalize; #H3; napply (H b2 H2); napply (asttype_destruct_array_array_1 … H3) - ##| ##2: #H2; nnormalize; #H3; napply (neqnat_to_neq n1 n2 H2); napply (asttype_destruct_array_array_2 … H3) - ##] - ##| ##1: #b2; nnormalize; #H1; #H2; napply (asttype_destruct … H2) - ##| ##3: #n2; nnormalize; #H1; #H2; napply (asttype_destruct … H2) + ##| ##2: #st1; #n1; #H; #t2; ncases t2; + ##[ ##2: #st2; #n2; #H1; nchange in H1:(%) with (((eq_asttype st1 st2)⊗(eq_nat n1 n2)) = true); + nrewrite > (H st2 (andb_true_true_l … H1)); + nrewrite > (eqnat_to_eq n1 n2 (andb_true_true_r … H1)); + napply refl_eq + ##| ##1: #b2; nnormalize; #H1; ndestruct (*napply (bool_destruct … H1)*) + ##| ##3: #nl2; nnormalize; #H1; ndestruct (*napply (bool_destruct … H1)*) ##] ##| ##3: #hh1; #H; #t2; ncases t2; - ##[ ##3: #n2; ncases n2; - ##[ ##1: #hh2; nchange with ((eq_asttype hh1 hh2 = false) → ?); #H1; - nnormalize; #H2; napply (H hh2 H1); - napply (nelist_destruct_nil_nil ast_type … (asttype_destruct_struct_struct … H2)) - ##| ##2: #hh2; #tt2; nnormalize; #H1; #H2; - napply (nelist_destruct_nil_cons ast_type … (asttype_destruct_struct_struct … H2)) + ##[ ##3: #nl2; ncases nl2; + ##[ ##1: #hh2; #H1; nchange in H1:(%) with ((eq_asttype hh1 hh2) = true); + nrewrite > (H hh2 H1); + napply refl_eq + ##| ##2: #hh2; #ll2; nnormalize; #H1; ndestruct (*napply (bool_destruct … H1)*) ##] - ##| ##1: #b2; nnormalize; #H1; #H2; napply (asttype_destruct … H2) - ##| ##2: #b2; #n2; nnormalize; #H1; #H2; napply (asttype_destruct … H2) + ##| ##1: #b2; nnormalize; #H1; ndestruct (*napply (bool_destruct … H1)*) + ##| ##2: #st2; #n2; nnormalize; #H1; ndestruct (*napply (bool_destruct … H1)*) ##] - ##| ##4: #hh1; #tt1; #H; #H1; #t2; ncases t2; - ##[ ##3: #n2; ncases n2; - ##[ ##2: #hh2; #tt2; nchange with ((((eq_asttype hh1 hh2)⊗(bfold_right_neList2 ?? tt1 tt2)) = false) → ?); - #H2; napply (or2_elim ??? (andb_false2 … H2)); - ##[ ##1: #H3; nnormalize; #H4; napply (H hh2 H3); - napply (nelist_destruct_cons_cons_1 ast_type … (asttype_destruct_struct_struct … H4)) - ##| ##2: #H3; nnormalize; #H4; napply (H1 (AST_TYPE_STRUCT tt2) H3); - nrewrite > (nelist_destruct_cons_cons_2 ast_type … (asttype_destruct_struct_struct … H4)); - napply refl_eq - ##] - ##| ##1: #hh2; nnormalize; #H2; #H3; - napply (nelist_destruct_cons_nil ast_type … (asttype_destruct_struct_struct … H3)) + ##| ##4: #hh1; #ll1; #H; #H1; #t2; ncases t2; + ##[ ##3: #nl2; ncases nl2; + ##[ ##1: #hh2; nnormalize; #H2; ndestruct (*napply (bool_destruct … H2)*) + ##| ##2: #hh2; #ll2; #H2; nchange in H2:(%) with (((eq_asttype hh1 hh2)⊗(bfold_right_neList2 ? (λx,y.eq_asttype x y) ll1 ll2)) = true); + nrewrite > (H hh2 (andb_true_true_l … H2)); + nrewrite > (asttype_destruct_struct_struct ll1 ll2 (H1 (AST_TYPE_STRUCT ll2) (andb_true_true_r … H2))); + napply refl_eq ##] - ##| ##1: #b2; nnormalize; #H2; #H3; napply (asttype_destruct … H3) - ##| ##2: #b2; #n2; nnormalize; #H2; #H3; napply (asttype_destruct … H3) + ##| ##1: #b2; nnormalize; #H2; ndestruct (*napply (bool_destruct … H2)*) + ##| ##2: #st2; #n2; nnormalize; #H2; ndestruct (*napply (bool_destruct … H2)*) ##] ##] nqed. -nlemma neq_to_neqasttype : ∀t1,t2.t1 ≠ t2 → eq_asttype t1 t2 = false. - #t1; - napply (ast_type_index … t1); - ##[ ##1: #b1; #t2; ncases t2; - ##[ ##1: #b2; nchange with (? → (eq_astbasetype b1 b2 = false)); #H; - napply (neq_to_neqastbasetype b1 b2 ?); nnormalize; #H1; - napply H; nrewrite > H1; napply refl_eq - ##| ##2: #b2; #n2; nnormalize; #H; napply refl_eq - ##| ##3: #n2; nnormalize; #H; napply refl_eq - ##] - ##| ##2: #b1; #n1; #H; #t2; ncases t2; - ##[ ##2: #b2; #n2; nchange with (? → ((eq_asttype b1 b2)⊗(eq_nat n1 n2)) = false); #H1; - napply (or2_elim ??? (decidable_asttype b1 b2)); - ##[ ##2: #H2; nrewrite > (H b2 H2); nnormalize; napply refl_eq - ##| ##1: #H2; napply (or2_elim ??? (decidable_nat n1 n2)) - ##[ ##2: #H3; nrewrite > (neq_to_neqnat n1 n2 H3); - nrewrite > (andb_false2_2 (eq_asttype b1 b2)); - napply refl_eq - ##| ##1: #H3; nrewrite > H2 in H1:(%); nrewrite > H3; #H1; - nelim (H1 (refl_eq …)) - ##] - ##] - ##| ##1: #b2; nnormalize; #H1; napply refl_eq - ##| ##3: #n2; nnormalize; #H1; napply refl_eq - ##] - ##| ##3: #hh1; #H; #t2; ncases t2; - ##[ ##3: #n2; ncases n2; - ##[ ##1: #hh2; nchange with (? → (eq_asttype hh1 hh2 = false)); #H1; - napply (H hh2); nnormalize; #H2; nrewrite > H2 in H1:(%); - nnormalize; #H1; napply (H1 (refl_eq …)) - ##| ##2: #hh2; #tt2; nnormalize; #H1; napply refl_eq - ##] - ##| ##1: #b2; nnormalize; #H1; napply refl_eq - ##| ##2: #b2; #n2; nnormalize; #H1; napply refl_eq - ##] - ##| ##4: #hh1; #tt1; #H; #H1; #t2; ncases t2; - ##[ ##3: #n2; ncases n2; - ##[ ##2: #hh2; #tt2; nchange with (? → ((eq_asttype hh1 hh2)⊗(bfold_right_neList2 ?? tt1 tt2)) = false); - #H2; napply (or2_elim (hh1 ≠ hh2) (tt1 ≠ tt2) …); - ##[ ##2: #H3; nrewrite > (H hh2 H3); nnormalize; napply refl_eq - ##| ##3: #H3; nchange with (((eq_asttype hh1 hh2)⊗(eq_asttype (AST_TYPE_STRUCT tt1) (AST_TYPE_STRUCT tt2))) = false); - nrewrite > (H1 (AST_TYPE_STRUCT tt2) ?); - ##[ ##1: nrewrite > (andb_false2_2 (eq_asttype hh1 hh2)); napply refl_eq - ##| ##2: nnormalize; #H4; napply (H3 (asttype_destruct_struct_struct … H4)) - ##] - ##| ##1: napply (or2_elim ??? (decidable_asttype hh1 hh2)); - ##[ ##2: #H3; napply (or2_intro1 … H3) - ##| ##1: #H3; napply (or2_elim ??? (decidable_nelist ast_type decidable_asttype tt1 tt2)); - ##[ ##2: #H4; napply (or2_intro2 … H4) - ##| ##1: #H4; nrewrite > H3 in H2:(%); nrewrite > H4; #H2; - nelim (H2 (refl_eq …)) - ##] - ##] - ##] - ##| ##1: #hh2; nnormalize; #H2; napply refl_eq - ##] - ##| ##1: #b2; nnormalize; #H2; napply refl_eq - ##| ##2: #b2; #n2; nnormalize; #H2; napply refl_eq - ##] +nlemma neq_to_neqasttype : ∀n1,n2.n1 ≠ n2 → eq_asttype n1 n2 = false. + #n1; #n2; #H; + napply (neqtrue_to_eqfalse (eq_asttype n1 n2)); + napply (not_to_not (eq_asttype n1 n2 = true) (n1 = n2) ? H); + napply (eqasttype_to_eq n1 n2). +nqed. + +nlemma decidable_asttype : ∀x,y:ast_type.decidable (x = y). + #x; #y; nnormalize; + napply (or2_elim (eq_asttype x y = true) (eq_asttype x y = false) ? (decidable_bexpr ?)); + ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqasttype_to_eq … H)) + ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqasttype_to_neq … H)) + ##] +nqed. + +nlemma symmetric_eqasttype : symmetricT ast_type bool eq_asttype. + #n1; #n2; + napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_asttype n1 n2)); + ##[ ##1: #H; nrewrite > H; napply refl_eq + ##| ##2: #H; nrewrite > (neq_to_neqasttype n1 n2 H); + napply (symmetric_eq ? (eq_asttype n2 n1) false); + napply (neq_to_neqasttype n2 n1 (symmetric_neq ? n1 n2 H)) ##] nqed. @@ -485,8 +293,8 @@ nlemma isbastbasetype_to_isastbasetype : ∀ast.isb_ast_base_type ast = true → ncases ast; nnormalize; ##[ ##1: #t; #H; napply I - ##| ##2: #t; #n; #H; napply (bool_destruct … H) - ##| ##3: #t; #H; napply (bool_destruct … H) + ##| ##2: #t; #n; #H; ndestruct (*napply (bool_destruct … H)*) + ##| ##3: #t; #H; ndestruct (*napply (bool_destruct … H)*) ##] nqed. @@ -494,7 +302,7 @@ nlemma isntbastbasetype_to_isntastbasetype : ∀ast.isntb_ast_base_type ast = tr #ast; ncases ast; nnormalize; - ##[ ##1: #t; #H; napply (bool_destruct … H) + ##[ ##1: #t; #H; ndestruct (*napply (bool_destruct … H)*) ##| ##2: #t; #n; #H; napply I ##| ##3: #l; #H; napply I ##]