From aa1045fc70f4b7be41bd8c49402de64d05a865b1 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi <ferruccio.guidi@unibo.it> Date: Mon, 3 Mar 2014 22:59:18 +0000 Subject: [PATCH] some additions for the forthcoming presentation --- .../basic_2/reduction/lpr_ldrop.ma | 56 ++++++++++++++++--- 1 file changed, 49 insertions(+), 7 deletions(-) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_ldrop.ma index a0f04dd96..4156df6ea 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_ldrop.ma @@ -34,9 +34,9 @@ lemma lpr_ldrop_trans_O1: âG. dropable_dx (lpr G). (* Properties on context-sensitive parallel reduction for terms *************) -lemma fqu_cpr_trans: âG1,G2,L1,L2,T1,T2. â¦G1, L1, T1⦠â â¦G2, L2, T2⦠â - âU2. â¦G2, L2⦠⢠T2 â¡ U2 â - ââL,U1. â¦G1, L1⦠⢠⡠L & â¦G1, L⦠⢠T1 â¡ U1 & â¦G1, L, U1⦠â â¦G2, L2, U2â¦. +lemma fqu_cpr_trans_dx: âG1,G2,L1,L2,T1,T2. â¦G1, L1, T1⦠â â¦G2, L2, T2⦠â + âU2. â¦G2, L2⦠⢠T2 â¡ U2 â + ââL,U1. â¦G1, L1⦠⢠⡠L & â¦G1, L⦠⢠T1 â¡ U1 & â¦G1, L, U1⦠â â¦G2, L2, U2â¦. #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 /3 width=5 by fqu_lref_O, fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, lpr_pair, cpr_pair_sn, cpr_atom, cpr_bind, cpr_flat, ex3_2_intro/ #G #L #K #U #T #e #HLK #HUT #U2 #HU2 @@ -44,11 +44,53 @@ elim (lift_total U2 0 (e+1)) #T2 #HUT2 lapply (cpr_lift ⦠HU2 ⦠HLK ⦠HUT ⦠HUT2) -HU2 -HUT /3 width=9 by fqu_drop, ex3_2_intro/ qed-. -lemma fquq_cpr_trans: âG1,G2,L1,L2,T1,T2. â¦G1, L1, T1⦠â⸮ â¦G2, L2, T2⦠â - âU2. â¦G2, L2⦠⢠T2 â¡ U2 â - ââL,U1. â¦G1, L1⦠⢠⡠L & â¦G1, L⦠⢠T1 â¡ U1 & â¦G1, L, U1⦠â⸮ â¦G2, L2, U2â¦. +lemma fquq_cpr_trans_dx: âG1,G2,L1,L2,T1,T2. â¦G1, L1, T1⦠â⸮ â¦G2, L2, T2⦠â + âU2. â¦G2, L2⦠⢠T2 â¡ U2 â + ââL,U1. â¦G1, L1⦠⢠⡠L & â¦G1, L⦠⢠T1 â¡ U1 & â¦G1, L, U1⦠â⸮ â¦G2, L2, U2â¦. #G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 elim (fquq_inv_gen ⦠H) -H -[ #HT12 elim (fqu_cpr_trans ⦠HT12 ⦠HTU2) /3 width=5 by fqu_fquq, ex3_2_intro/ +[ #HT12 elim (fqu_cpr_trans_dx ⦠HT12 ⦠HTU2) /3 width=5 by fqu_fquq, ex3_2_intro/ +| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/ +] +qed-. + +lemma fqu_cpr_trans_sn: âG1,G2,L1,L2,T1,T2. â¦G1, L1, T1⦠â â¦G2, L2, T2⦠â + âU2. â¦G2, L2⦠⢠T2 â¡ U2 â + ââL,U1. â¦G1, L1⦠⢠⡠L & â¦G1, L1⦠⢠T1 â¡ U1 & â¦G1, L, U1⦠â â¦G2, L2, U2â¦. +#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 +/3 width=5 by fqu_lref_O, fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, lpr_pair, cpr_pair_sn, cpr_atom, cpr_bind, cpr_flat, ex3_2_intro/ +#G #L #K #U #T #e #HLK #HUT #U2 #HU2 +elim (lift_total U2 0 (e+1)) #T2 #HUT2 +lapply (cpr_lift ⦠HU2 ⦠HLK ⦠HUT ⦠HUT2) -HU2 -HUT /3 width=9 by fqu_drop, ex3_2_intro/ +qed-. + +lemma fquq_cpr_trans_sn: âG1,G2,L1,L2,T1,T2. â¦G1, L1, T1⦠â⸮ â¦G2, L2, T2⦠â + âU2. â¦G2, L2⦠⢠T2 â¡ U2 â + ââL,U1. â¦G1, L1⦠⢠⡠L & â¦G1, L1⦠⢠T1 â¡ U1 & â¦G1, L, U1⦠â⸮ â¦G2, L2, U2â¦. +#G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 elim (fquq_inv_gen ⦠H) -H +[ #HT12 elim (fqu_cpr_trans_sn ⦠HT12 ⦠HTU2) /3 width=5 by fqu_fquq, ex3_2_intro/ +| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/ +] +qed-. + +lemma fqu_lpr_trans: âG1,G2,L1,L2,T1,T2. â¦G1, L1, T1⦠â â¦G2, L2, T2⦠â + âK2. â¦G2, L2⦠⢠⡠K2 â + ââK1,T. â¦G1, L1⦠⢠⡠K1 & â¦G1, L1⦠⢠T1 â¡ T & â¦G1, K1, T⦠â â¦G2, K2, T2â¦. +#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 +/3 width=5 by fqu_lref_O, fqu_pair_sn, fqu_flat_dx, lpr_pair, ex3_2_intro/ +[ #a #I #G2 #L2 #V2 #T2 #X #H elim (lpr_inv_pair1 ⦠H) -H + #K2 #W2 #HLK2 #HVW2 #H destruct + /3 width=5 by fqu_fquq, cpr_pair_sn, fqu_bind_dx, ex3_2_intro/ +| #G #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #K2 #HK12 + elim (ldrop_lpr_trans ⦠HLK1 ⦠HK12) -HK12 + /3 width=7 by fqu_drop, ex3_2_intro/ +] +qed-. + +lemma fquq_lpr_trans: âG1,G2,L1,L2,T1,T2. â¦G1, L1, T1⦠â⸮ â¦G2, L2, T2⦠â + âK2. â¦G2, L2⦠⢠⡠K2 â + ââK1,T. â¦G1, L1⦠⢠⡠K1 & â¦G1, L1⦠⢠T1 â¡ T & â¦G1, K1, T⦠â⸮ â¦G2, K2, T2â¦. +#G1 #G2 #L1 #L2 #T1 #T2 #H #K2 #HLK2 elim (fquq_inv_gen ⦠H) -H +[ #HT12 elim (fqu_lpr_trans ⦠HT12 ⦠HLK2) /3 width=5 by fqu_fquq, ex3_2_intro/ | * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/ ] qed-. -- 2.39.2