(* Progetto FreeScale *)
(* *)
(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Ultima modifica: 05/08/2009 *)
+(* Sviluppo: 2008-2010 *)
(* *)
(* ********************************************************************** *)
(* 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 ].
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.
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 ].
##]
##]
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.
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);
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) ?));
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.
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.
#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
##]
projects / helm.git / blobdiff