(* 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 eq_to_eqastbasetype : ∀n1,n2.n1 = n2 → eq_astbasetype n1 n2 = true.
#n1; #n2; #H;
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)
+ ##| ##*: #H; ndestruct (*napply (bool_destruct … 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 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.
##[ ##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: #st2; #n2; nnormalize; #H; ndestruct (*napply (bool_destruct … H)*)
+ ##| ##3: #nl2; nnormalize; #H; ndestruct (*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)
+ ##| ##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: #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)
+ ##| ##2: #hh2; #ll2; nnormalize; #H1; ndestruct (*napply (bool_destruct … H1)*)
##]
- ##| ##1: #b2; nnormalize; #H1; napply (bool_destruct … H1)
- ##| ##2: #st2; #n2; nnormalize; #H1; napply (bool_destruct … H1)
+ ##| ##1: #b2; nnormalize; #H1; ndestruct (*napply (bool_destruct … H1)*)
+ ##| ##2: #st2; #n2; nnormalize; #H1; ndestruct (*napply (bool_destruct … H1)*)
##]
##| ##4: #hh1; #ll1; #H; #H1; #t2; ncases t2;
##[ ##3: #nl2; ncases nl2;
- ##[ ##1: #hh2; nnormalize; #H2; napply (bool_destruct … H2)
+ ##[ ##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; napply (bool_destruct … H2)
- ##| ##2: #st2; #n2; nnormalize; #H2; napply (bool_destruct … H2)
+ ##| ##1: #b2; nnormalize; #H2; ndestruct (*napply (bool_destruct … H2)*)
+ ##| ##2: #st2; #n2; nnormalize; #H2; ndestruct (*napply (bool_destruct … H2)*)
##]
##]
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
##]