From 928cfe1ebf2fbd31731c8851cdec70802596016d Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 16 Jan 2014 21:49:29 +0000 Subject: [PATCH] commit of the "relocation" component with the new definition of ldrop, the other components will be committed shortly ... --- .../contribs/lambdadelta/basic_2/names.txt | 5 +- .../basic_2/notation/relations/rdrop_5.ma | 19 + .../basic_2/notation/relations/rdropstar_4.ma | 19 + .../lambdadelta/basic_2/relocation/cpy.ma | 14 +- .../basic_2/relocation/cpy_lift.ma | 106 +++--- .../lambdadelta/basic_2/relocation/fqu.ma | 6 +- .../lambdadelta/basic_2/relocation/fquq.ma | 4 +- .../basic_2/relocation/fquq_alt.ma | 2 +- .../lambdadelta/basic_2/relocation/ldrop.ma | 356 ++++++++++-------- .../basic_2/relocation/ldrop_append.ma | 32 +- .../basic_2/relocation/ldrop_ldrop.ma | 190 +++++----- .../basic_2/relocation/ldrop_lpx_sn.ma | 62 +-- .../lambdadelta/basic_2/relocation/lsubr.ma | 38 +- .../basic_2/relocation/lsubr_lsubr.ma | 10 +- .../lambdadelta/basic_2/relocation/lsuby.ma | 18 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 4 +- .../contribs/lambdadelta/ground_2/lib/bool.ma | 30 ++ .../ground_2/notation/constructors/no_0.ma | 19 + .../ground_2/notation/constructors/yes_0.ma | 19 + 19 files changed, 564 insertions(+), 389 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/rdrop_5.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/rdropstar_4.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/lib/bool.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/constructors/no_0.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/constructors/yes_0.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/names.txt b/matita/matita/contribs/lambdadelta/basic_2/names.txt index 1bfe7ed6d..a9008510e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/names.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/names.txt @@ -28,7 +28,8 @@ l : term degree m,n : reserved: future use o : p,q : global reference position -r,s : +r : reduction kind parameter (true = ordinary, false = extended) +s : local dropping kind parameter (true = general, false = restricted) t,u : local reference position level (de Bruijn's) v,w : x,y,z : reserved: transient objet denoted by a small letter @@ -39,6 +40,8 @@ NAMING CONVENTIONS FOR CONSTRUCTORS 2: binary A: application to vector +F: boolean false +T: boolean true a: application b: binder diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rdrop_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rdrop_5.ma new file mode 100644 index 000000000..70d59f931 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rdrop_5.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⇩ [ term 46 s , break term 46 d , break term 46 e ] break term 46 L1 ≡ break term 46 L2 )" + non associative with precedence 45 + for @{ 'RDrop $s $d $e $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rdropstar_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rdropstar_4.ma new file mode 100644 index 000000000..94906922f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rdropstar_4.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⇩ * [ term 46 s , break term 46 e ] break term 46 L1 ≡ break term 46 L2 )" + non associative with precedence 45 + for @{ 'RDropStar $s $e $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma index 05b77349e..798b6eb79 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma @@ -25,7 +25,7 @@ include "basic_2/relocation/lsuby.ma". inductive cpy: ynat → ynat → relation4 genv lenv term term ≝ | cpy_atom : ∀I,G,L,d,e. cpy d e G L (⓪{I}) (⓪{I}) | cpy_subst: ∀I,G,L,K,V,W,i,d,e. d ≤ yinj i → i < d+e → - ⇩[0, i] L ≡ K.ⓑ{I}V → ⇧[0, i+1] V ≡ W → cpy d e G L (#i) W + ⇩[i] L ≡ K.ⓑ{I}V → ⇧[0, i+1] V ≡ W → cpy d e G L (#i) W | cpy_bind : ∀a,I,G,L,V1,V2,T1,T2,d,e. cpy d e G L V1 V2 → cpy (⫯d) e G (L.ⓑ{I}V2) T1 T2 → cpy d e G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2) @@ -39,7 +39,7 @@ interpretation "context-sensitive extended ordinary substritution (term)" (* Basic properties *********************************************************) -lemma lsuby_cpy_trans: ∀G,d,e. lsub_trans … (cpy d e G) (lsuby d e). +lemma lsuby_cpy_trans: ∀G,d,e. lsub_trans … (cpy d e G) (lsuby d e). #G #d #e #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2 -d -e [ // | #I #G #L1 #K1 #V #W #i #d #e #Hdi #Hide #HLK1 #HVW #L2 #HL12 @@ -53,7 +53,7 @@ lemma cpy_refl: ∀G,T,L,d,e. ⦃G, L⦄ ⊢ T ▶×[d, e] T. #G #T elim T -T // * /2 width=1 by cpy_bind, cpy_flat/ qed. -lemma cpy_full: ∀I,G,K,V,T1,L,d. ⇩[0, d] L ≡ K.ⓑ{I}V → +lemma cpy_full: ∀I,G,K,V,T1,L,d. ⇩[d] L ≡ K.ⓑ{I}V → ∃∃T2,T. ⦃G, L⦄ ⊢ T1 ▶×[d, 1] T2 & ⇧[d, 1] T ≡ T2. #I #G #K #V #T1 elim T1 -T1 [ * #i #L #d #HLK @@ -67,7 +67,7 @@ lemma cpy_full: ∀I,G,K,V,T1,L,d. ⇩[0, d] L ≡ K.ⓑ{I}V → | * [ #a ] #J #W1 #U1 #IHW1 #IHU1 #L #d #HLK elim (IHW1 … HLK) -IHW1 #W2 #W #HW12 #HW2 [ elim (IHU1 (L.ⓑ{J}W2) (d+1)) -IHU1 - /3 width=9 by cpy_bind, ldrop_ldrop, lift_bind, ex2_2_intro/ + /3 width=9 by cpy_bind, ldrop_drop, lift_bind, ex2_2_intro/ | elim (IHU1 … HLK) -IHU1 -HLK /3 width=8 by cpy_flat, lift_flat, ex2_2_intro/ ] @@ -186,7 +186,7 @@ qed-. fact cpy_inv_atom1_aux: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶×[d, e] T2 → ∀J. T1 = ⓪{J} → T2 = ⓪{J} ∨ ∃∃I,K,V,i. d ≤ yinj i & i < d + e & - ⇩[O, i] L ≡ K.ⓑ{I}V & + ⇩[i] L ≡ K.ⓑ{I}V & ⇧[O, i+1] V ≡ T2 & J = LRef i. #G #L #T1 #T2 #d #e * -G -L -T1 -T2 -d -e @@ -200,7 +200,7 @@ qed-. lemma cpy_inv_atom1: ∀I,G,L,T2,d,e. ⦃G, L⦄ ⊢ ⓪{I} ▶×[d, e] T2 → T2 = ⓪{I} ∨ ∃∃J,K,V,i. d ≤ yinj i & i < d + e & - ⇩[O, i] L ≡ K.ⓑ{J}V & + ⇩[i] L ≡ K.ⓑ{J}V & ⇧[O, i+1] V ≡ T2 & I = LRef i. /2 width=4 by cpy_inv_atom1_aux/ qed-. @@ -214,7 +214,7 @@ qed-. lemma cpy_inv_lref1: ∀G,L,T2,i,d,e. ⦃G, L⦄ ⊢ #i ▶×[d, e] T2 → T2 = #i ∨ ∃∃I,K,V. d ≤ i & i < d + e & - ⇩[O, i] L ≡ K.ⓑ{I}V & + ⇩[i] L ≡ K.ⓑ{I}V & ⇧[O, i+1] V ≡ T2. #G #L #T2 #i #d #e #H elim (cpy_inv_atom1 … H) -H /2 width=1 by or_introl/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_lift.ma index 85203f203..38ba768e8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_lift.ma @@ -20,13 +20,13 @@ include "basic_2/relocation/cpy.ma". (* Properties on relocation *************************************************) lemma cpy_lift_le: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶×[dt, et] T2 → - ∀L,U1,U2,d,e. ⇩[d, e] L ≡ K → + ∀L,U1,U2,s,d,e. ⇩[s, d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 → ⇧[d, e] T2 ≡ U2 → dt + et ≤ d → ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2. #G #K #T1 #T2 #dt #et #H elim H -G -K -T1 -T2 -dt -et -[ #I #G #K #dt #et #L #U1 #U2 #d #e #_ #H1 #H2 #_ +[ #I #G #K #dt #et #L #U1 #U2 #s #d #e #_ #H1 #H2 #_ >(lift_mono … H1 … H2) -H1 -H2 // -| #I #G #K #KV #V #W #i #dt #et #Hdti #Hidet #HKV #HVW #L #U1 #U2 #d #e #HLK #H #HWU2 #Hdetd +| #I #G #K #KV #V #W #i #dt #et #Hdti #Hidet #HKV #HVW #L #U1 #U2 #s #d #e #HLK #H #HWU2 #Hdetd lapply (ylt_yle_trans … Hdetd … Hidet) -Hdetd #Hid lapply (ylt_inv_inj … Hid) -Hid #Hid lapply (lift_inv_lref1_lt … H … Hid) -H #H destruct @@ -34,25 +34,25 @@ lemma cpy_lift_le: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶×[dt, et] T2 → elim (ldrop_trans_le … HLK … HKV) -K /2 width=2 by lt_to_le/ #X #HLK #H elim (ldrop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hid #K #Y #_ #HVY >(lift_mono … HVY … HVW) -Y -HVW #H destruct /2 width=5 by cpy_subst/ -| #a #I #G #K #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hdetd +| #a #I #G #K #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #s #d #e #HLK #H1 #H2 #Hdetd elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct - /4 width=6 by cpy_bind, ldrop_skip, yle_succ/ -| #G #I #K #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hdetd + /4 width=7 by cpy_bind, ldrop_skip, yle_succ/ +| #G #I #K #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #s #d #e #HLK #H1 #H2 #Hdetd elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct - /3 width=6 by cpy_flat/ + /3 width=7 by cpy_flat/ ] qed-. lemma cpy_lift_be: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶×[dt, et] T2 → - ∀L,U1,U2,d,e. ⇩[d, e] L ≡ K → + ∀L,U1,U2,s,d,e. ⇩[s, d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 → ⇧[d, e] T2 ≡ U2 → dt ≤ d → d ≤ dt + et → ⦃G, L⦄ ⊢ U1 ▶×[dt, et + e] U2. #G #K #T1 #T2 #dt #et #H elim H -G -K -T1 -T2 -dt -et -[ #I #G #K #dt #et #L #U1 #U2 #d #e #_ #H1 #H2 #_ #_ +[ #I #G #K #dt #et #L #U1 #U2 #s #d #e #_ #H1 #H2 #_ #_ >(lift_mono … H1 … H2) -H1 -H2 // -| #I #G #K #KV #V #W #i #dt #et #Hdti #Hidet #HKV #HVW #L #U1 #U2 #d #e #HLK #H #HWU2 #Hdtd #_ +| #I #G #K #KV #V #W #i #dt #et #Hdti #Hidet #HKV #HVW #L #U1 #U2 #s #d #e #HLK #H #HWU2 #Hdtd #_ elim (lift_inv_lref1 … H) -H * #Hid #H destruct [ -Hdtd lapply (ylt_yle_trans … (dt+et+e) … Hidet) // -Hidet #Hidete @@ -65,68 +65,68 @@ lemma cpy_lift_be: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶×[dt, et] T2 → lapply (transitive_le … Hdtd Hid) -Hdtd #Hdti lapply (lift_trans_be … HVW … HWU2 ? ?) -W /2 width=1 by le_S/ >plus_plus_comm_23 #HVU2 lapply (ldrop_trans_ge_comm … HLK … HKV ?) -K // -Hid - /4 width=5 by cpy_subst, monotonic_ylt_plus_dx, yle_plus_dx1_trans, yle_inj/ + /4 width=5 by cpy_subst, ldrop_inv_gen, monotonic_ylt_plus_dx, yle_plus_dx1_trans, yle_inj/ ] -| #a #I #G #K #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hdtd #Hddet +| #a #I #G #K #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #s #d #e #HLK #H1 #H2 #Hdtd #Hddet elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct - /4 width=6 by cpy_bind, ldrop_skip, yle_succ/ -| #I #G #K #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hdetd + /4 width=7 by cpy_bind, ldrop_skip, yle_succ/ +| #I #G #K #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #s #d #e #HLK #H1 #H2 #Hdetd elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct - /3 width=6 by cpy_flat/ + /3 width=7 by cpy_flat/ ] qed-. lemma cpy_lift_ge: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶×[dt, et] T2 → - ∀L,U1,U2,d,e. ⇩[d, e] L ≡ K → + ∀L,U1,U2,s,d,e. ⇩[s, d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 → ⇧[d, e] T2 ≡ U2 → d ≤ dt → ⦃G, L⦄ ⊢ U1 ▶×[dt+e, et] U2. #G #K #T1 #T2 #dt #et #H elim H -G -K -T1 -T2 -dt -et -[ #I #G #K #dt #et #L #U1 #U2 #d #e #_ #H1 #H2 #_ +[ #I #G #K #dt #et #L #U1 #U2 #s #d #e #_ #H1 #H2 #_ >(lift_mono … H1 … H2) -H1 -H2 // -| #I #G #K #KV #V #W #i #dt #et #Hdti #Hidet #HKV #HVW #L #U1 #U2 #d #e #HLK #H #HWU2 #Hddt +| #I #G #K #KV #V #W #i #dt #et #Hdti #Hidet #HKV #HVW #L #U1 #U2 #s #d #e #HLK #H #HWU2 #Hddt lapply (yle_trans … Hddt … Hdti) -Hddt #Hid elim (yle_inv_inj2 … Hid) -Hid #dd #Hddi #H0 destruct lapply (lift_inv_lref1_ge … H … Hddi) -H #H destruct lapply (lift_trans_be … HVW … HWU2 ? ?) -W /2 width=1 by le_S/ >plus_plus_comm_23 #HVU2 lapply (ldrop_trans_ge_comm … HLK … HKV ?) -K // -Hddi - /3 width=5 by cpy_subst, monotonic_ylt_plus_dx, monotonic_yle_plus_dx/ -| #a #I #G #K #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hddt + /3 width=5 by cpy_subst, ldrop_inv_gen, monotonic_ylt_plus_dx, monotonic_yle_plus_dx/ +| #a #I #G #K #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #s #d #e #HLK #H1 #H2 #Hddt elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct - /4 width=5 by cpy_bind, ldrop_skip, yle_succ/ -| #I #G #K #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hddt + /4 width=6 by cpy_bind, ldrop_skip, yle_succ/ +| #I #G #K #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #s #d #e #HLK #H1 #H2 #Hddt elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct - /3 width=5 by cpy_flat/ + /3 width=6 by cpy_flat/ ] qed-. (* Inversion lemmas on relocation *******************************************) lemma cpy_inv_lift1_le: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 → - ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → + ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → dt + et ≤ d → ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶×[dt, et] T2 & ⇧[d, e] T2 ≡ U2. #G #L #U1 #U2 #dt #et #H elim H -G -L -U1 -U2 -dt -et -[ * #i #G #L #dt #et #K #d #e #_ #T1 #H #_ +[ * #i #G #L #dt #et #K #s #d #e #_ #T1 #H #_ [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by ex2_intro/ | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3 by lift_lref_ge_minus, lift_lref_lt, ex2_intro/ | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by ex2_intro/ ] -| #I #G #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #d #e #HLK #T1 #H #Hdetd +| #I #G #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #s #d #e #HLK #T1 #H #Hdetd lapply (ylt_yle_trans … Hdetd … Hidet) -Hdetd #Hid lapply (ylt_inv_inj … Hid) -Hid #Hid lapply (lift_inv_lref2_lt … H … Hid) -H #H destruct elim (ldrop_conf_lt … HLK … HLKV) -L // #L #U #HKL #_ #HUV elim (lift_trans_le … HUV … HVW) -V // >minus_plus yplus_minus_assoc_inj /3 width=1 by monotonic_ylt_minus_dx, yle_inj/ ] -| #a #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #d #e #HLK #X #H #Hdtd #Hdedet +| #a #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #s #d #e #HLK #X #H #Hdtd #Hdedet elim (lift_inv_bind2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct elim (IHW12 … HLK … HVW1) -W1 // #V2 #HV12 #HVW2 elim (IHU12 … HTU1) -U1 - /3 width=5 by cpy_bind, ldrop_skip, lift_bind, yle_succ, ex2_intro/ -| #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #d #e #HLK #X #H #Hdtd #Hdedet + /3 width=6 by cpy_bind, ldrop_skip, lift_bind, yle_succ, ex2_intro/ +| #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #s #d #e #HLK #X #H #Hdtd #Hdedet elim (lift_inv_flat2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct elim (IHW12 … HLK … HVW1) -W1 // elim (IHU12 … HLK … HTU1) -U1 -HLK // @@ -174,16 +174,16 @@ lemma cpy_inv_lift1_be: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 qed-. lemma cpy_inv_lift1_ge: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 → - ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → - d + e ≤ dt → + ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → + yinj d + e ≤ dt → ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶×[dt-e, et] T2 & ⇧[d, e] T2 ≡ U2. #G #L #U1 #U2 #dt #et #H elim H -G -L -U1 -U2 -dt -et -[ * #i #G #L #dt #et #K #d #e #_ #T1 #H #_ +[ * #i #G #L #dt #et #K #s #d #e #_ #T1 #H #_ [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by ex2_intro/ | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3 by lift_lref_ge_minus, lift_lref_lt, ex2_intro/ | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by ex2_intro/ ] -| #I #G #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #d #e #HLK #T1 #H #Hdedt +| #I #G #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #s #d #e #HLK #T1 #H #Hdedt lapply (yle_trans … Hdedt … Hdti) #Hdei elim (yle_inv_plus_inj2 … Hdedt) -Hdedt #_ #Hedt elim (yle_inv_plus_inj2 … Hdei) #Hdie #Hei @@ -195,13 +195,13 @@ lemma cpy_inv_lift1_ge: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 [ /2 width=1 by monotonic_yle_minus_dx/ | yminus_succ1_inj /3 width=5 by cpy_bind, lift_bind, ex2_intro/ -| #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #d #e #HLK #X #H #Hdetd +| #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #s #d #e #HLK #X #H #Hdetd elim (lift_inv_flat2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct elim (IHW12 … HLK … HVW1) -W1 // elim (IHU12 … HLK … HTU1) -U1 -HLK /3 width=5 by cpy_flat, lift_flat, ex2_intro/ @@ -211,10 +211,10 @@ qed-. (* Advancd inversion lemmas on relocation ***********************************) lemma cpy_inv_lift1_ge_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 → - ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → - d ≤ dt → dt ≤ d + e → d + e ≤ dt + et → - ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶×[d, dt + et - (d + e)] T2 & ⇧[d, e] T2 ≡ U2. -#G #L #U1 #U2 #dt #et #HU12 #K #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet + ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → + d ≤ dt → dt ≤ yinj d + e → yinj d + e ≤ dt + et → + ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶×[d, dt + et - (yinj d + e)] T2 & ⇧[d, e] T2 ≡ U2. +#G #L #U1 #U2 #dt #et #HU12 #K #s #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet elim (cpy_split_up … HU12 (d + e)) -HU12 // -Hdedet #U #HU1 #HU2 lapply (cpy_weak … HU1 d e ? ?) -HU1 // [ >ymax_pre_sn_comm // ] -Hddt -Hdtde #HU1 lapply (cpy_inv_lift1_eq … HTU1 … HU1) -HU1 #HU1 destruct @@ -222,20 +222,20 @@ elim (cpy_inv_lift1_ge … HU2 … HLK … HTU1) -U -L /2 width=3 by ex2_intro/ qed-. lemma cpy_inv_lift1_be_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 → - ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → - dt ≤ d → dt + et ≤ d + e → + ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → + dt ≤ d → dt + et ≤ yinj d + e → ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶×[dt, d-dt] T2 & ⇧[d, e] T2 ≡ U2. -#G #L #U1 #U2 #dt #et #HU12 #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdetde +#G #L #U1 #U2 #dt #et #HU12 #K #s #d #e #HLK #T1 #HTU1 #Hdtd #Hdetde lapply (cpy_weak … HU12 dt (d+e-dt) ? ?) -HU12 // [ >ymax_pre_sn_comm /2 width=1 by yle_plus_dx1_trans/ ] -Hdetde #HU12 elim (cpy_inv_lift1_be … HU12 … HLK … HTU1) -U1 -L /2 width=3 by ex2_intro/ qed-. lemma cpy_inv_lift1_le_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 → - ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → - dt ≤ d → d ≤ dt + et → dt + et ≤ d + e → + ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → + dt ≤ d → d ≤ dt + et → dt + et ≤ yinj d + e → ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶×[dt, d - dt] T2 & ⇧[d, e] T2 ≡ U2. -#G #L #U1 #U2 #dt #et #HU12 #K #d #e #HLK #T1 #HTU1 #Hdtd #Hddet #Hdetde +#G #L #U1 #U2 #dt #et #HU12 #K #s #d #e #HLK #T1 #HTU1 #Hdtd #Hddet #Hdetde elim (cpy_split_up … HU12 d) -HU12 // #U #HU1 #HU2 elim (cpy_inv_lift1_le … HU1 … HLK … HTU1) -U1 [2: >ymax_pre_sn_comm // ] -Hdtd #T #HT1 #HTU diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fqu.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fqu.ma index 2058b25b7..46f274def 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fqu.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/fqu.ma @@ -25,7 +25,7 @@ inductive fqu: tri_relation genv lenv term ≝ | fqu_bind_dx: ∀a,I,G,L,V,T. fqu G L (ⓑ{a,I}V.T) G (L.ⓑ{I}V) T | fqu_flat_dx: ∀I,G,L,V,T. fqu G L (ⓕ{I}V.T) G L T | fqu_drop : ∀G,L,K,T,U,e. - ⇩[0, e+1] L ≡ K → ⇧[0, e+1] T ≡ U → fqu G L U G K T + ⇩[e+1] L ≡ K → ⇧[0, e+1] T ≡ U → fqu G L U G K T . interpretation @@ -35,12 +35,12 @@ interpretation (* Basic properties *********************************************************) lemma fqu_drop_lt: ∀G,L,K,T,U,e. 0 < e → - ⇩[0, e] L ≡ K → ⇧[0, e] T ≡ U → ⦃G, L, U⦄ ⊃ ⦃G, K, T⦄. + ⇩[e] L ≡ K → ⇧[0, e] T ≡ U → ⦃G, L, U⦄ ⊃ ⦃G, K, T⦄. #G #L #K #T #U #e #He >(plus_minus_m_m e 1) /2 width=3 by fqu_drop/ qed. lemma fqu_lref_S_lt: ∀I,G,L,V,i. 0 < i → ⦃G, L.ⓑ{I}V, #i⦄ ⊃ ⦃G, L, #(i-1)⦄. -/3 width=3 by fqu_drop, ldrop_ldrop, lift_lref_ge_minus/ +/3 width=3 by fqu_drop, ldrop_drop, lift_lref_ge_minus/ qed. (* Basic forward lemmas *****************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq.ma index de000da70..6601cb963 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq.ma @@ -24,7 +24,7 @@ inductive fquq: tri_relation genv lenv term ≝ | fquq_bind_dx: ∀a,I,G,L,V,T. fquq G L (ⓑ{a,I}V.T) G (L.ⓑ{I}V) T | fquq_flat_dx: ∀I,G, L,V,T. fquq G L (ⓕ{I}V.T) G L T | fquq_drop : ∀G,L,K,T,U,e. - ⇩[0, e] L ≡ K → ⇧[0, e] T ≡ U → fquq G L U G K T + ⇩[e] L ≡ K → ⇧[0, e] T ≡ U → fquq G L U G K T . interpretation @@ -37,7 +37,7 @@ lemma fquq_refl: tri_reflexive … fquq. /2 width=3 by fquq_drop/ qed. lemma fqu_fquq: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄. -#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 // /2 width=3 by fquq_drop/ +#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 /2 width=3 by fquq_drop/ qed. (* Basic forward lemmas *****************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq_alt.ma index 1d770dcc4..033959bea 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq_alt.ma @@ -30,7 +30,7 @@ lemma fquqa_refl: tri_reflexive … fquqa. // qed. lemma fquqa_drop: ∀G,L,K,T,U,e. - ⇩[0, e] L ≡ K → ⇧[0, e] T ≡ U → ⦃G, L, U⦄ ⊃⊃⸮ ⦃G, K, T⦄. + ⇩[e] L ≡ K → ⇧[0, e] T ≡ U → ⦃G, L, U⦄ ⊃⊃⸮ ⦃G, K, T⦄. #G #L #K #T #U #e #HLK #HTU elim (eq_or_gt e) /3 width=5 by fqu_drop_lt, or_introl/ #H destruct >(ldrop_inv_O2 … HLK) -L >(lift_inv_O2 … HTU) -T // diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma index ee4780d88..b26b7e95b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma @@ -12,8 +12,11 @@ (* *) (**************************************************************************) +include "ground_2/lib/bool.ma". include "ground_2/lib/lstar.ma". +include "basic_2/notation/relations/rdrop_5.ma". include "basic_2/notation/relations/rdrop_4.ma". +include "basic_2/notation/relations/rdrop_3.ma". include "basic_2/grammar/lenv_length.ma". include "basic_2/grammar/cl_restricted_weight.ma". include "basic_2/relocation/lift.ma". @@ -21,283 +24,307 @@ include "basic_2/relocation/lift.ma". (* BASIC SLICING FOR LOCAL ENVIRONMENTS *************************************) (* Basic_1: includes: drop_skip_bind *) -inductive ldrop: relation4 nat nat lenv lenv ≝ -| ldrop_atom : ∀d. ldrop d 0 (⋆) (⋆) -| ldrop_pair : ∀L,I,V. ldrop 0 0 (L. ⓑ{I} V) (L. ⓑ{I} V) -| ldrop_ldrop: ∀L1,L2,I,V,e. ldrop 0 e L1 L2 → ldrop 0 (e + 1) (L1. ⓑ{I} V) L2 -| ldrop_skip : ∀L1,L2,I,V1,V2,d,e. - ldrop d e L1 L2 → ⇧[d,e] V2 ≡ V1 → - ldrop (d + 1) e (L1. ⓑ{I} V1) (L2. ⓑ{I} V2) +inductive ldrop (s:bool): relation4 nat nat lenv lenv ≝ +| ldrop_atom: ∀d,e. (s = Ⓕ → e = 0) → ldrop s d e (⋆) (⋆) +| ldrop_pair: ∀I,L,V. ldrop s 0 0 (L.ⓑ{I}V) (L.ⓑ{I}V) +| ldrop_drop: ∀I,L1,L2,V,e. ldrop s 0 e L1 L2 → ldrop s 0 (e+1) (L1.ⓑ{I}V) L2 +| ldrop_skip: ∀I,L1,L2,V1,V2,d,e. + ldrop s d e L1 L2 → ⇧[d, e] V2 ≡ V1 → + ldrop s (d+1) e (L1.ⓑ{I}V1) (L2.ⓑ{I}V2) . interpretation - "basic slicing (local environment)" - 'RDrop d e L1 L2 = (ldrop d e L1 L2). + "basic slicing (local environment) abstract" + 'RDrop s d e L1 L2 = (ldrop s d e L1 L2). + +interpretation + "basic slicing (local environment) general" + 'RDrop d e L1 L2 = (ldrop true d e L1 L2). + +interpretation + "basic slicing (local environment) lget" + 'RDrop e L1 L2 = (ldrop false O e L1 L2). definition l_liftable: predicate (lenv → relation term) ≝ - λR. ∀K,T1,T2. R K T1 T2 → ∀L,d,e. ⇩[d, e] L ≡ K → + λR. ∀K,T1,T2. R K T1 T2 → ∀L,s,d,e. ⇩[s, d, e] L ≡ K → ∀U1. ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 → R L U1 U2. definition l_deliftable_sn: predicate (lenv → relation term) ≝ - λR. ∀L,U1,U2. R L U1 U2 → ∀K,d,e. ⇩[d, e] L ≡ K → + λR. ∀L,U1,U2. R L U1 U2 → ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → ∃∃T2. ⇧[d, e] T2 ≡ U2 & R K T1 T2. definition dropable_sn: predicate (relation lenv) ≝ - λR. ∀L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀L2. R L1 L2 → - ∃∃K2. R K1 K2 & ⇩[d, e] L2 ≡ K2. + λR. ∀L1,K1,s,d,e. ⇩[s, d, e] L1 ≡ K1 → ∀L2. R L1 L2 → + ∃∃K2. R K1 K2 & ⇩[s, d, e] L2 ≡ K2. definition dedropable_sn: predicate (relation lenv) ≝ - λR. ∀L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀K2. R K1 K2 → - ∃∃L2. R L1 L2 & ⇩[d, e] L2 ≡ K2. + λR. ∀L1,K1,s,d,e. ⇩[s, d, e] L1 ≡ K1 → ∀K2. R K1 K2 → + ∃∃L2. R L1 L2 & ⇩[s, d, e] L2 ≡ K2. definition dropable_dx: predicate (relation lenv) ≝ - λR. ∀L1,L2. R L1 L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 → - ∃∃K1. ⇩[0, e] L1 ≡ K1 & R K1 K2. + λR. ∀L1,L2. R L1 L2 → ∀K2,s,e. ⇩[s, 0, e] L2 ≡ K2 → + ∃∃K1. ⇩[s, 0, e] L1 ≡ K1 & R K1 K2. (* Basic inversion lemmas ***************************************************) -fact ldrop_inv_atom1_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → L1 = ⋆ → - L2 = ⋆ ∧ e = 0. -#d #e #L1 #L2 * -d -e -L1 -L2 -[ /2 width=1 by conj/ -| #L #I #V #H destruct -| #L1 #L2 #I #V #e #_ #H destruct -| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H destruct +fact ldrop_inv_atom1_aux: ∀L1,L2,s,d,e. ⇩[s, d, e] L1 ≡ L2 → L1 = ⋆ → + L2 = ⋆ ∧ (s = Ⓕ → e = 0). +#L1 #L2 #s #d #e * -L1 -L2 -d -e +[ /3 width=1 by conj/ +| #I #L #V #H destruct +| #I #L1 #L2 #V #e #_ #H destruct +| #I #L1 #L2 #V1 #V2 #d #e #_ #_ #H destruct ] qed-. (* Basic_1: was: drop_gen_sort *) -lemma ldrop_inv_atom1: ∀d,e,L2. ⇩[d, e] ⋆ ≡ L2 → L2 = ⋆ ∧ e = 0. +lemma ldrop_inv_atom1: ∀L2,s,d,e. ⇩[s, d, e] ⋆ ≡ L2 → L2 = ⋆ ∧ (s = Ⓕ → e = 0). /2 width=4 by ldrop_inv_atom1_aux/ qed-. -fact ldrop_inv_O1_pair1_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → d = 0 → - ∀K,I,V. L1 = K. ⓑ{I} V → - (e = 0 ∧ L2 = K. ⓑ{I} V) ∨ - (0 < e ∧ ⇩[d, e - 1] K ≡ L2). -#d #e #L1 #L2 * -d -e -L1 -L2 -[ #d #_ #K #I #V #H destruct -| #L #I #V #_ #K #J #W #HX destruct /3 width=1 by or_introl, conj/ -| #L1 #L2 #I #V #e #HL12 #_ #K #J #W #H destruct /3 width=1 by or_intror, conj/ -| #L1 #L2 #I #V1 #V2 #d #e #_ #_ >commutative_plus normalize #H destruct +fact ldrop_inv_O1_pair1_aux: ∀L1,L2,s,d,e. ⇩[s, d, e] L1 ≡ L2 → d = 0 → + ∀K,I,V. L1 = K.ⓑ{I}V → + (e = 0 ∧ L2 = K.ⓑ{I}V) ∨ + (0 < e ∧ ⇩[s, d, e-1] K ≡ L2). +#L1 #L2 #s #d #e * -L1 -L2 -d -e +[ #d #e #_ #_ #K #J #W #H destruct +| #I #L #V #_ #K #J #W #HX destruct /3 width=1 by or_introl, conj/ +| #I #L1 #L2 #V #e #HL12 #_ #K #J #W #H destruct /3 width=1 by or_intror, conj/ +| #I #L1 #L2 #V1 #V2 #d #e #_ #_ >commutative_plus normalize #H destruct ] qed-. -lemma ldrop_inv_O1_pair1: ∀e,K,I,V,L2. ⇩[0, e] K. ⓑ{I} V ≡ L2 → - (e = 0 ∧ L2 = K. ⓑ{I} V) ∨ - (0 < e ∧ ⇩[0, e - 1] K ≡ L2). +lemma ldrop_inv_O1_pair1: ∀I,K,L2,V,s,e. ⇩[s, 0, e] K. ⓑ{I} V ≡ L2 → + (e = 0 ∧ L2 = K.ⓑ{I}V) ∨ + (0 < e ∧ ⇩[s, 0, e-1] K ≡ L2). /2 width=3 by ldrop_inv_O1_pair1_aux/ qed-. -lemma ldrop_inv_pair1: ∀K,I,V,L2. ⇩[0, 0] K. ⓑ{I} V ≡ L2 → L2 = K. ⓑ{I} V. -#K #I #V #L2 #H +lemma ldrop_inv_pair1: ∀I,K,L2,V,s. ⇩[s, 0, 0] K.ⓑ{I}V ≡ L2 → L2 = K.ⓑ{I}V. +#I #K #L2 #V #s #H elim (ldrop_inv_O1_pair1 … H) -H * // #H destruct elim (lt_refl_false … H) qed-. (* Basic_1: was: drop_gen_drop *) -lemma ldrop_inv_ldrop1_lt: ∀e,K,I,V,L2. - ⇩[0, e] K. ⓑ{I} V ≡ L2 → 0 < e → ⇩[0, e - 1] K ≡ L2. -#e #K #I #V #L2 #H #He +lemma ldrop_inv_drop1_lt: ∀I,K,L2,V,s,e. + ⇩[s, 0, e] K.ⓑ{I}V ≡ L2 → 0 < e → ⇩[s, 0, e-1] K ≡ L2. +#I #K #L2 #V #s #e #H #He elim (ldrop_inv_O1_pair1 … H) -H * // #H destruct elim (lt_refl_false … He) qed-. -lemma ldrop_inv_ldrop1: ∀e,K,I,V,L2. - ⇩[0, e+1] K. ⓑ{I} V ≡ L2 → ⇩[0, e] K ≡ L2. -#e #K #I #V #L2 #H lapply (ldrop_inv_ldrop1_lt … H ?) -H // +lemma ldrop_inv_drop1: ∀I,K,L2,V,s,e. + ⇩[s, 0, e+1] K.ⓑ{I}V ≡ L2 → ⇩[s, 0, e] K ≡ L2. +#I #K #L2 #V #s #e #H lapply (ldrop_inv_drop1_lt … H ?) -H // qed-. -fact ldrop_inv_skip1_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → 0 < d → - ∀I,K1,V1. L1 = K1. ⓑ{I} V1 → - ∃∃K2,V2. ⇩[d - 1, e] K1 ≡ K2 & - ⇧[d - 1, e] V2 ≡ V1 & - L2 = K2. ⓑ{I} V2. -#d #e #L1 #L2 * -d -e -L1 -L2 -[ #d #_ #I #K #V #H destruct -| #L #I #V #H elim (lt_refl_false … H) -| #L1 #L2 #I #V #e #_ #H elim (lt_refl_false … H) -| #X #L2 #Y #Z #V2 #d #e #HL12 #HV12 #_ #I #L1 #V1 #H destruct /2 width=5 by ex3_2_intro/ +fact ldrop_inv_skip1_aux: ∀L1,L2,s,d,e. ⇩[s, d, e] L1 ≡ L2 → 0 < d → + ∀I,K1,V1. L1 = K1.ⓑ{I}V1 → + ∃∃K2,V2. ⇩[s, d-1, e] K1 ≡ K2 & + ⇧[d-1, e] V2 ≡ V1 & + L2 = K2.ⓑ{I}V2. +#L1 #L2 #s #d #e * -L1 -L2 -d -e +[ #d #e #_ #_ #J #K1 #W1 #H destruct +| #I #L #V #H elim (lt_refl_false … H) +| #I #L1 #L2 #V #e #_ #H elim (lt_refl_false … H) +| #I #L1 #L2 #V1 #V2 #d #e #HL12 #HV21 #_ #J #K1 #W1 #H destruct /2 width=5 by ex3_2_intro/ ] qed-. (* Basic_1: was: drop_gen_skip_l *) -lemma ldrop_inv_skip1: ∀d,e,I,K1,V1,L2. ⇩[d, e] K1. ⓑ{I} V1 ≡ L2 → 0 < d → - ∃∃K2,V2. ⇩[d - 1, e] K1 ≡ K2 & - ⇧[d - 1, e] V2 ≡ V1 & - L2 = K2. ⓑ{I} V2. +lemma ldrop_inv_skip1: ∀I,K1,V1,L2,s,d,e. ⇩[s, d, e] K1.ⓑ{I}V1 ≡ L2 → 0 < d → + ∃∃K2,V2. ⇩[s, d-1, e] K1 ≡ K2 & + ⇧[d-1, e] V2 ≡ V1 & + L2 = K2.ⓑ{I}V2. /2 width=3 by ldrop_inv_skip1_aux/ qed-. -lemma ldrop_inv_O1_pair2: ∀I,K,V,e,L1. ⇩[0, e] L1 ≡ K. ⓑ{I} V → - (e = 0 ∧ L1 = K. ⓑ{I} V) ∨ - ∃∃I1,K1,V1. ⇩[0, e - 1] K1 ≡ K. ⓑ{I} V & L1 = K1.ⓑ{I1}V1 & 0 < e. -#I #K #V #e * +lemma ldrop_inv_O1_pair2: ∀I,K,V,s,e,L1. ⇩[s, 0, e] L1 ≡ K.ⓑ{I}V → + (e = 0 ∧ L1 = K.ⓑ{I}V) ∨ + ∃∃I1,K1,V1. ⇩[s, 0, e-1] K1 ≡ K.ⓑ{I}V & L1 = K1.ⓑ{I1}V1 & 0 < e. +#I #K #V #s #e * [ #H elim (ldrop_inv_atom1 … H) -H #H destruct | #L1 #I1 #V1 #H elim (ldrop_inv_O1_pair1 … H) -H * [ #H1 #H2 destruct /3 width=1 by or_introl, conj/ - | /3 width=5/ + | /3 width=5 by ex3_3_intro, or_intror/ ] ] qed-. -fact ldrop_inv_skip2_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → 0 < d → - ∀I,K2,V2. L2 = K2. ⓑ{I} V2 → - ∃∃K1,V1. ⇩[d - 1, e] K1 ≡ K2 & - ⇧[d - 1, e] V2 ≡ V1 & - L1 = K1. ⓑ{I} V1. -#d #e #L1 #L2 * -d -e -L1 -L2 -[ #d #_ #I #K #V #H destruct -| #L #I #V #H elim (lt_refl_false … H) -| #L1 #L2 #I #V #e #_ #H elim (lt_refl_false … H) -| #L1 #X #Y #V1 #Z #d #e #HL12 #HV12 #_ #I #L2 #V2 #H destruct /2 width=5 by ex3_2_intro/ +fact ldrop_inv_skip2_aux: ∀L1,L2,s,d,e. ⇩[s, d, e] L1 ≡ L2 → 0 < d → + ∀I,K2,V2. L2 = K2.ⓑ{I}V2 → + ∃∃K1,V1. ⇩[s, d-1, e] K1 ≡ K2 & + ⇧[d-1, e] V2 ≡ V1 & + L1 = K1.ⓑ{I}V1. +#L1 #L2 #s #d #e * -L1 -L2 -d -e +[ #d #e #_ #_ #J #K2 #W2 #H destruct +| #I #L #V #H elim (lt_refl_false … H) +| #I #L1 #L2 #V #e #_ #H elim (lt_refl_false … H) +| #I #L1 #L2 #V1 #V2 #d #e #HL12 #HV21 #_ #J #K2 #W2 #H destruct /2 width=5 by ex3_2_intro/ ] qed-. (* Basic_1: was: drop_gen_skip_r *) -lemma ldrop_inv_skip2: ∀d,e,I,L1,K2,V2. ⇩[d, e] L1 ≡ K2. ⓑ{I} V2 → 0 < d → - ∃∃K1,V1. ⇩[d - 1, e] K1 ≡ K2 & ⇧[d - 1, e] V2 ≡ V1 & - L1 = K1. ⓑ{I} V1. +lemma ldrop_inv_skip2: ∀I,L1,K2,V2,s,d,e. ⇩[s, d, e] L1 ≡ K2.ⓑ{I}V2 → 0 < d → + ∃∃K1,V1. ⇩[s, d-1, e] K1 ≡ K2 & ⇧[d-1, e] V2 ≡ V1 & + L1 = K1.ⓑ{I}V1. /2 width=3 by ldrop_inv_skip2_aux/ qed-. (* Basic properties *********************************************************) +lemma ldrop_refl_atom_O2: ∀s,d. ⇩[s, d, O] ⋆ ≡ ⋆. +/2 width=1 by ldrop_atom/ qed. + (* Basic_1: was by definition: drop_refl *) -lemma ldrop_refl: ∀L,d. ⇩[d, 0] L ≡ L. +lemma ldrop_refl: ∀L,d,s. ⇩[s, d, 0] L ≡ L. #L elim L -L // -#L #I #V #IHL #d @(nat_ind_plus … d) -d /2 width=1 by ldrop_pair, ldrop_skip/ +#L #I #V #IHL #d #s @(nat_ind_plus … d) -d /2 width=1 by ldrop_pair, ldrop_skip/ qed. -lemma ldrop_ldrop_lt: ∀L1,L2,I,V,e. - ⇩[0, e - 1] L1 ≡ L2 → 0 < e → ⇩[0, e] L1. ⓑ{I} V ≡ L2. -#L1 #L2 #I #V #e #HL12 #He >(plus_minus_m_m e 1) /2 width=1 by ldrop_ldrop/ +lemma ldrop_drop_lt: ∀I,L1,L2,V,s,e. + ⇩[s, 0, e-1] L1 ≡ L2 → 0 < e → ⇩[s, 0, e] L1.ⓑ{I}V ≡ L2. +#I #L1 #L2 #V #s #e #HL12 #He >(plus_minus_m_m e 1) /2 width=1 by ldrop_drop/ qed. -lemma ldrop_skip_lt: ∀L1,L2,I,V1,V2,d,e. - ⇩[d - 1, e] L1 ≡ L2 → ⇧[d - 1, e] V2 ≡ V1 → 0 < d → - ⇩[d, e] L1. ⓑ{I} V1 ≡ L2. ⓑ{I} V2. -#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV21 #Hd >(plus_minus_m_m d 1) /2 width=1 by ldrop_skip/ +lemma ldrop_skip_lt: ∀I,L1,L2,V1,V2,s,d,e. + ⇩[s, d-1, e] L1 ≡ L2 → ⇧[d-1, e] V2 ≡ V1 → 0 < d → + ⇩[s, d, e] L1. ⓑ{I} V1 ≡ L2.ⓑ{I}V2. +#I #L1 #L2 #V1 #V2 #s #d #e #HL12 #HV21 #Hd >(plus_minus_m_m d 1) /2 width=1 by ldrop_skip/ qed. -lemma ldrop_O1_le: ∀e,L. e ≤ |L| → ∃K. ⇩[0, e] L ≡ K. -#e @(nat_ind_plus … e) -e /2 width=2/ +lemma ldrop_O1_le: ∀e,L. e ≤ |L| → ∃K. ⇩[e] L ≡ K. +#e @(nat_ind_plus … e) -e /2 width=2 by ex_intro/ #e #IHe * [ #H lapply (le_n_O_to_eq … H) -H >commutative_plus normalize #H destruct | #L #I #V normalize #H - elim (IHe L) -IHe /2 width=1/ -H /3 width=2 by ldrop_ldrop, ex_intro/ + elim (IHe L) -IHe /3 width=2 by ldrop_drop, monotonic_pred, ex_intro/ ] -qed. +qed-. -lemma ldrop_O1_lt: ∀L,e. e < |L| → ∃∃I,K,V. ⇩[0, e] L ≡ K.ⓑ{I}V. +lemma ldrop_O1_lt: ∀L,e. e < |L| → ∃∃I,K,V. ⇩[e] L ≡ K.ⓑ{I}V. #L elim L -L [ #e #H elim (lt_zero_false … H) | #L #I #V #IHL #e @(nat_ind_plus … e) -e /2 width=4 by ldrop_pair, ex1_3_intro/ #e #_ normalize #H - elim (IHL e) -IHL /3 width=4 by ldrop_ldrop, lt_plus_to_minus_r, lt_plus_to_lt_l, ex1_3_intro/ + elim (IHL e) -IHL /3 width=4 by ldrop_drop, lt_plus_to_minus_r, lt_plus_to_lt_l, ex1_3_intro/ ] +qed-. + +lemma ldrop_FT: ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ L2 → ⇩[Ⓣ, d, e] L1 ≡ L2. +#L1 #L2 #d #e #H elim H -L1 -L2 -d -e +/3 width=1 by ldrop_atom, ldrop_drop, ldrop_skip/ qed. +lemma ldrop_gen: ∀L1,L2,s,d,e. ⇩[Ⓕ, d, e] L1 ≡ L2 → ⇩[s, d, e] L1 ≡ L2. +#L1 #L2 * /2 width=1 by ldrop_FT/ +qed-. + +lemma ldrop_T: ∀L1,L2,s,d,e. ⇩[s, d, e] L1 ≡ L2 → ⇩[Ⓣ, d, e] L1 ≡ L2. +#L1 #L2 * /2 width=1 by ldrop_FT/ +qed-. + lemma l_liftable_LTC: ∀R. l_liftable R → l_liftable (LTC … R). #R #HR #K #T1 #T2 #H elim H -T2 -[ /3 width=9/ -| #T #T2 #_ #HT2 #IHT1 #L #d #e #HLK #U1 #HTU1 #U2 #HTU2 - elim (lift_total T d e) /4 width=11 by step/ +[ /3 width=10 by inj/ +| #T #T2 #_ #HT2 #IHT1 #L #s #d #e #HLK #U1 #HTU1 #U2 #HTU2 + elim (lift_total T d e) /4 width=12 by step/ ] -qed. +qed-. lemma l_deliftable_sn_LTC: ∀R. l_deliftable_sn R → l_deliftable_sn (LTC … R). #R #HR #L #U1 #U2 #H elim H -U2 -[ #U2 #HU12 #K #d #e #HLK #T1 #HTU1 +[ #U2 #HU12 #K #s #d #e #HLK #T1 #HTU1 elim (HR … HU12 … HLK … HTU1) -HR -L -U1 /3 width=3 by inj, ex2_intro/ -| #U #U2 #_ #HU2 #IHU1 #K #d #e #HLK #T1 #HTU1 +| #U #U2 #_ #HU2 #IHU1 #K #s #d #e #HLK #T1 #HTU1 elim (IHU1 … HLK … HTU1) -IHU1 -U1 #T #HTU #HT1 elim (HR … HU2 … HLK … HTU) -HR -L -U /3 width=5 by step, ex2_intro/ ] -qed. +qed-. lemma dropable_sn_TC: ∀R. dropable_sn R → dropable_sn (TC … R). -#R #HR #L1 #K1 #d #e #HLK1 #L2 #H elim H -L2 -[ #L2 #HL12 - elim (HR … HLK1 … HL12) -HR -L1 /3 width=3 by inj, ex2_intro/ -| #L #L2 #_ #HL2 * #K #HK1 #HLK - elim (HR … HLK … HL2) -HR -L /3 width=3 by step, ex2_intro/ +#R #HR #L1 #K1 #s #d #e #HLK1 #L2 #H elim H -L2 +[ #L2 #HL12 elim (HR … HLK1 … HL12) -HR -L1 + /3 width=3 by inj, ex2_intro/ +| #L #L2 #_ #HL2 * #K #HK1 #HLK elim (HR … HLK … HL2) -HR -L + /3 width=3 by step, ex2_intro/ ] -qed. +qed-. lemma dedropable_sn_TC: ∀R. dedropable_sn R → dedropable_sn (TC … R). -#R #HR #L1 #K1 #d #e #HLK1 #K2 #H elim H -K2 -[ #K2 #HK12 - elim (HR … HLK1 … HK12) -HR -K1 /3 width=3 by inj, ex2_intro/ -| #K #K2 #_ #HK2 * #L #HL1 #HLK - elim (HR … HLK … HK2) -HR -K /3 width=3 by step, ex2_intro/ +#R #HR #L1 #K1 #s #d #e #HLK1 #K2 #H elim H -K2 +[ #K2 #HK12 elim (HR … HLK1 … HK12) -HR -K1 + /3 width=3 by inj, ex2_intro/ +| #K #K2 #_ #HK2 * #L #HL1 #HLK elim (HR … HLK … HK2) -HR -K + /3 width=3 by step, ex2_intro/ ] -qed. +qed-. lemma dropable_dx_TC: ∀R. dropable_dx R → dropable_dx (TC … R). #R #HR #L1 #L2 #H elim H -L2 -[ #L2 #HL12 #K2 #e #HLK2 - elim (HR … HL12 … HLK2) -HR -L2 /3 width=3 by inj, ex2_intro/ -| #L #L2 #_ #HL2 #IHL1 #K2 #e #HLK2 - elim (HR … HL2 … HLK2) -HR -L2 #K #HLK #HK2 - elim (IHL1 … HLK) -L /3 width=5 by step, ex2_intro/ +[ #L2 #HL12 #K2 #s #e #HLK2 elim (HR … HL12 … HLK2) -HR -L2 + /3 width=3 by inj, ex2_intro/ +| #L #L2 #_ #HL2 #IHL1 #K2 #s #e #HLK2 elim (HR … HL2 … HLK2) -HR -L2 + #K #HLK #HK2 elim (IHL1 … HLK) -L + /3 width=5 by step, ex2_intro/ ] -qed. +qed-. lemma l_deliftable_sn_llstar: ∀R. l_deliftable_sn R → ∀l. l_deliftable_sn (llstar … R l). #R #HR #l #L #U1 #U2 #H @(lstar_ind_r … l U2 H) -l -U2 [ /2 width=3 by lstar_O, ex2_intro/ -| #l #U #U2 #_ #HU2 #IHU1 #K #d #e #HLK #T1 #HTU1 +| #l #U #U2 #_ #HU2 #IHU1 #K #s #d #e #HLK #T1 #HTU1 elim (IHU1 … HLK … HTU1) -IHU1 -U1 #T #HTU #HT1 elim (HR … HU2 … HLK … HTU) -HR -L -U /3 width=5 by lstar_dx, ex2_intro/ ] -qed. +qed-. (* Basic forvard lemmas *****************************************************) (* Basic_1: was: drop_S *) -lemma ldrop_fwd_ldrop2: ∀L1,I2,K2,V2,e. ⇩[O, e] L1 ≡ K2. ⓑ{I2} V2 → - ⇩[O, e + 1] L1 ≡ K2. +lemma ldrop_fwd_drop2: ∀L1,I2,K2,V2,s,e. ⇩[s, O, e] L1 ≡ K2. ⓑ{I2} V2 → + ⇩[s, O, e + 1] L1 ≡ K2. #L1 elim L1 -L1 -[ #I2 #K2 #V2 #e #H lapply (ldrop_inv_atom1 … H) -H * #H destruct -| #K1 #I1 #V1 #IHL1 #I2 #K2 #V2 #e #H +[ #I2 #K2 #V2 #s #e #H lapply (ldrop_inv_atom1 … H) -H * #H destruct +| #K1 #I1 #V1 #IHL1 #I2 #K2 #V2 #s #e #H elim (ldrop_inv_O1_pair1 … H) -H * #He #H - [ -IHL1 destruct /2 width=1/ - | @ldrop_ldrop >(plus_minus_m_m e 1) /2 width=3 by / + [ -IHL1 destruct /2 width=1 by ldrop_drop/ + | @ldrop_drop >(plus_minus_m_m e 1) /2 width=3 by/ ] ] qed-. -lemma ldrop_fwd_length: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → |L1| = |L2| + e. -#L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize /2 width=1 by / +lemma ldrop_fwd_length: ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ L2 → |L1| = |L2| + e. +#L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize /2 width=1 by/ qed-. -lemma ldrop_fwd_length_minus2: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → |L2| = |L1| - e. +lemma ldrop_fwd_length_minus2: ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ L2 → |L2| = |L1| - e. #L1 #L2 #d #e #H lapply (ldrop_fwd_length … H) -H /2 width=1 by plus_minus, le_n/ qed-. -lemma ldrop_fwd_length_minus4: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → e = |L1| - |L2|. +lemma ldrop_fwd_length_minus4: ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ L2 → e = |L1| - |L2|. #L1 #L2 #d #e #H lapply (ldrop_fwd_length … H) -H // qed-. -lemma ldrop_fwd_length_le2: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → e ≤ |L1|. +lemma ldrop_fwd_length_le2: ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ L2 → e ≤ |L1|. #L1 #L2 #d #e #H lapply (ldrop_fwd_length … H) -H // qed-. -lemma ldrop_fwd_length_le4: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → |L2| ≤ |L1|. +lemma ldrop_fwd_length_le4: ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ L2 → |L2| ≤ |L1|. #L1 #L2 #d #e #H lapply (ldrop_fwd_length … H) -H // qed-. lemma ldrop_fwd_length_lt2: ∀L1,I2,K2,V2,d,e. - ⇩[d, e] L1 ≡ K2. ⓑ{I2} V2 → e < |L1|. + ⇩[Ⓕ, d, e] L1 ≡ K2. ⓑ{I2} V2 → e < |L1|. #L1 #I2 #K2 #V2 #d #e #H lapply (ldrop_fwd_length … H) normalize in ⊢ (%→?); -I2 -V2 // qed-. -lemma ldrop_fwd_length_lt4: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → 0 < e → |L2| < |L1|. +lemma ldrop_fwd_length_lt4: ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ L2 → 0 < e → |L2| < |L1|. #L1 #L2 #d #e #H lapply (ldrop_fwd_length … H) -H /2 width=1 by lt_minus_to_plus_r/ qed-. -lemma ldrop_fwd_length_eq1: ∀L1,L2,K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 → +lemma ldrop_fwd_length_eq1: ∀L1,L2,K1,K2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 → |L1| = |L2| → |K1| = |K2|. #L1 #L2 #K1 #K2 #d #e #HLK1 #HLK2 #HL12 lapply (ldrop_fwd_length … HLK1) -HLK1 @@ -305,60 +332,85 @@ lapply (ldrop_fwd_length … HLK2) -HLK2 /2 width=2 by injective_plus_r/ qed-. -lemma ldrop_fwd_length_eq2: ∀L1,L2,K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 → +lemma ldrop_fwd_length_eq2: ∀L1,L2,K1,K2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 → |K1| = |K2| → |L1| = |L2|. #L1 #L2 #K1 #K2 #d #e #HLK1 #HLK2 #HL12 lapply (ldrop_fwd_length … HLK1) -HLK1 lapply (ldrop_fwd_length … HLK2) -HLK2 // qed-. -lemma ldrop_fwd_lw: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ♯{L2} ≤ ♯{L1}. -#L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize +lemma ldrop_fwd_lw: ∀L1,L2,s,d,e. ⇩[s, d, e] L1 ≡ L2 → ♯{L2} ≤ ♯{L1}. +#L1 #L2 #s #d #e #H elim H -L1 -L2 -d -e // normalize [ /2 width=3 by transitive_le/ -| #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12 +| #I #L1 #L2 #V1 #V2 #d #e #_ #HV21 #IHL12 >(lift_fwd_tw … HV21) -HV21 /2 width=1 by monotonic_le_plus_l/ ] qed-. -lemma ldrop_fwd_lw_lt: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → 0 < e → ♯{L2} < ♯{L1}. -#L1 #L2 #d #e #H elim H -L1 -L2 -d -e // -[ #L #I #V #H elim (lt_refl_false … H) -| #L1 #L2 #I #V #e #HL12 #_ #_ +lemma ldrop_fwd_lw_lt: ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ L2 → 0 < e → ♯{L2} < ♯{L1}. +#L1 #L2 #d #e #H elim H -L1 -L2 -d -e +[ #d #e #H >H -H // +| #I #L #V #H elim (lt_refl_false … H) +| #I #L1 #L2 #V #e #HL12 #_ #_ lapply (ldrop_fwd_lw … HL12) -HL12 #HL12 @(le_to_lt_to_lt … HL12) -HL12 // -| #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12 #H normalize in ⊢ (?%%); -I +| #I #L1 #L2 #V1 #V2 #d #e #_ #HV21 #IHL12 #H normalize in ⊢ (?%%); -I >(lift_fwd_tw … HV21) -V2 /3 by lt_minus_to_plus/ ] qed-. -lemma ldrop_fwd_rfw: ∀I,L,K,V,i. ⇩[O, i] L ≡ K.ⓑ{I}V → ♯{K, V} < ♯{L, #i}. +lemma ldrop_fwd_rfw: ∀I,L,K,V,i. ⇩[i] L ≡ K.ⓑ{I}V → ♯{K, V} < ♯{L, #i}. #I #L #K #V #i #HLK lapply (ldrop_fwd_lw … HLK) -HLK normalize in ⊢ (%→?%%); /2 width=1 by le_S_S/ qed-. (* Advanced inversion lemmas ************************************************) -fact ldrop_inv_O2_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → e = 0 → L1 = L2. -#d #e #L1 #L2 #H elim H -d -e -L1 -L2 +fact ldrop_inv_O2_aux: ∀L1,L2,s,d,e. ⇩[s, d, e] L1 ≡ L2 → e = 0 → L1 = L2. +#L1 #L2 #s #d #e #H elim H -L1 -L2 -d -e [ // | // -| #L1 #L2 #I #V #e #_ #_ >commutative_plus normalize #H destruct -| #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12 #H +| #I #L1 #L2 #V #e #_ #_ >commutative_plus normalize #H destruct +| #I #L1 #L2 #V1 #V2 #d #e #_ #HV21 #IHL12 #H >(IHL12 H) -L1 >(lift_inv_O2_aux … HV21 … H) -V2 -d -e // ] qed-. (* Basic_1: was: drop_gen_refl *) -lemma ldrop_inv_O2: ∀L1,L2,d. ⇩[d, 0] L1 ≡ L2 → L1 = L2. -/2 width=4 by ldrop_inv_O2_aux/ qed-. +lemma ldrop_inv_O2: ∀L1,L2,s,d. ⇩[s, d, 0] L1 ≡ L2 → L1 = L2. +/2 width=5 by ldrop_inv_O2_aux/ qed-. -lemma ldrop_inv_length_eq: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → |L1| = |L2| → e = 0. +lemma ldrop_inv_length_eq: ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ L2 → |L1| = |L2| → e = 0. #L1 #L2 #d #e #H #HL12 lapply (ldrop_fwd_length_minus4 … H) // qed-. -lemma ldrop_inv_refl: ∀L,d,e. ⇩[d, e] L ≡ L → e = 0. +lemma ldrop_inv_refl: ∀L,d,e. ⇩[Ⓕ, d, e] L ≡ L → e = 0. /2 width=5 by ldrop_inv_length_eq/ qed-. +fact ldrop_inv_FT_aux: ∀L1,L2,s,d,e. ⇩[s, d, e] L1 ≡ L2 → + ∀I,K,V. L2 = K.ⓑ{I}V → s = Ⓣ → d = 0 → + ⇩[Ⓕ, d, e] L1 ≡ K.ⓑ{I}V. +#L1 #L2 #s #d #e #H elim H -L1 -L2 -d -e +[ #d #e #_ #J #K #W #H destruct +| #I #L #V #J #K #W #H destruct // +| #I #L1 #L2 #V #e #_ #IHL12 #J #K #W #H1 #H2 destruct + /3 width=1 by ldrop_drop/ +| #I #L1 #L2 #V1 #V2 #d #e #_ #_ #_ #J #K #W #_ #_ + commutative_plus normalize #H destruct @@ -43,18 +44,17 @@ elim (ldrop_inv_O1_pair1 … H) -H * #H2e #HL12 destruct ] qed-. -lemma ldrop_O1_inv_append1_le: ∀K,L1,L2,e. ⇩[0, e] L1 @@ L2 ≡ K → e ≤ |L2| → - ∀K2. ⇩[0, e] L2 ≡ K2 → K = L1 @@ K2. +lemma ldrop_O1_inv_append1_le: ∀K,L1,L2,s,e. ⇩[s, 0, e] L1 @@ L2 ≡ K → e ≤ |L2| → + ∀K2. ⇩[s, 0, e] L2 ≡ K2 → K = L1 @@ K2. #K #L1 #L2 elim L2 -L2 normalize -[ #e #H1 #H2 #K2 #H3 - lapply (le_n_O_to_eq … H2) -H2 #H2 - elim (ldrop_inv_atom1 … H3) -H3 #H3 #_ destruct +[ #s #e #H1 #H2 #K2 #H3 lapply (le_n_O_to_eq … H2) -H2 + #H2 elim (ldrop_inv_atom1 … H3) -H3 #H3 #_ destruct >(ldrop_inv_O2 … H1) -H1 // -| #L2 #I #V #IHL2 #e @(nat_ind_plus … e) -e [ -IHL2 ] +| #L2 #I #V #IHL2 #s #e @(nat_ind_plus … e) -e [ -IHL2 ] [ #H1 #_ #K2 #H2 lapply (ldrop_inv_O2 … H1) -H1 #H1 lapply (ldrop_inv_O2 … H2) -H2 #H2 destruct // - | /4 width=6 by ldrop_inv_ldrop1, le_plus_to_le_r/ + | /4 width=7 by ldrop_inv_drop1, le_plus_to_le_r/ ] ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_ldrop.ma index ce3326a9d..77e7e5b59 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_ldrop.ma @@ -20,14 +20,14 @@ include "basic_2/relocation/ldrop.ma". (* Main properties **********************************************************) (* Basic_1: was: drop_mono *) -theorem ldrop_mono: ∀d,e,L,L1. ⇩[d, e] L ≡ L1 → - ∀L2. ⇩[d, e] L ≡ L2 → L1 = L2. -#d #e #L #L1 #H elim H -d -e -L -L1 -[ #d #L2 #H elim (ldrop_inv_atom1 … H) -H // -| #K #I #V #L2 #HL12 <(ldrop_inv_O2 … HL12) -L2 // -| #L #K #I #V #e #_ #IHLK #L2 #H - lapply (ldrop_inv_ldrop1 … H) -H /2 width=1 by/ -| #L #K1 #I #T #V1 #d #e #_ #HVT1 #IHLK1 #X #H +theorem ldrop_mono: ∀L,L1,s1,d,e. ⇩[s1, d, e] L ≡ L1 → + ∀L2,s2. ⇩[s2, d, e] L ≡ L2 → L1 = L2. +#L #L1 #s1 #d #e #H elim H -L -L1 -d -e +[ #d #e #He #L2 #s2 #H elim (ldrop_inv_atom1 … H) -H // +| #I #K #V #L2 #s2 #HL12 <(ldrop_inv_O2 … HL12) -L2 // +| #I #L #K #V #e #_ #IHLK #L2 #s2 #H + lapply (ldrop_inv_drop1 … H) -H /2 width=2 by/ +| #I #L #K1 #T #V1 #d #e #_ #HVT1 #IHLK1 #X #s2 #H elim (ldrop_inv_skip1 … H) -H // (lift_inj … HVT1 … HVT2) -HVT1 -HVT2 >(IHLK1 … HLK2) -IHLK1 -HLK2 // @@ -35,148 +35,154 @@ theorem ldrop_mono: ∀d,e,L,L1. ⇩[d, e] L ≡ L1 → qed-. (* Basic_1: was: drop_conf_ge *) -theorem ldrop_conf_ge: ∀d1,e1,L,L1. ⇩[d1, e1] L ≡ L1 → - ∀e2,L2. ⇩[0, e2] L ≡ L2 → d1 + e1 ≤ e2 → - ⇩[0, e2 - e1] L1 ≡ L2. -#d1 #e1 #L #L1 #H elim H -d1 -e1 -L -L1 // -[ #L #K #I #V #e #_ #IHLK #e2 #L2 #H #He2 - lapply (ldrop_inv_ldrop1_lt … H ?) -H /2 width=2 by ltn_to_ltO/ #HL2 +theorem ldrop_conf_ge: ∀L,L1,s1,d1,e1. ⇩[s1, d1, e1] L ≡ L1 → + ∀L2,s2,e2. ⇩[s2, 0, e2] L ≡ L2 → d1 + e1 ≤ e2 → + ⇩[s2, 0, e2 - e1] L1 ≡ L2. +#L #L1 #s1 #d1 #e1 #H elim H -L -L1 -d1 -e1 // +[ #d #e #_ #L2 #s2 #e2 #H #_ elim (ldrop_inv_atom1 … H) -H + #H #He destruct + @ldrop_atom #H >He // (**) (* explicit constructor *) +| #I #L #K #V #e #_ #IHLK #L2 #s2 #e2 #H #He2 + lapply (ldrop_inv_drop1_lt … H ?) -H /2 width=2 by ltn_to_ltO/ #HL2 minus_minus_comm /3 width=1 by monotonic_pred/ -| #L #K #I #V1 #V2 #d #e #_ #_ #IHLK #e2 #L2 #H #Hdee2 +| #I #L #K #V1 #V2 #d #e #_ #_ #IHLK #L2 #s2 #e2 #H #Hdee2 lapply (transitive_le 1 … Hdee2) // #He2 - lapply (ldrop_inv_ldrop1_lt … H ?) -H // -He2 #HL2 + lapply (ldrop_inv_drop1_lt … H ?) -H // -He2 #HL2 lapply (transitive_le (1 + e) … Hdee2) // #Hee2 - @ldrop_ldrop_lt >minus_minus_comm /3 width=1 by O, lt_minus_to_plus_r, monotonic_le_minus_r, monotonic_pred/ (**) (* explicit constructor *) + @ldrop_drop_lt >minus_minus_comm /3 width=1 by lt_minus_to_plus_r, monotonic_le_minus_r, monotonic_pred/ (**) (* explicit constructor *) ] qed. (* Note: apparently this was missing in basic_1 *) -theorem ldrop_conf_be: ∀L0,L1,d1,e1. ⇩[d1, e1] L0 ≡ L1 → - ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 → - ∃∃L. ⇩[0, d1 + e1 - e2] L2 ≡ L & ⇩[0, d1] L1 ≡ L. -#L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1 -[ #d1 #L2 #e2 #H #Hd1 #_ elim (ldrop_inv_atom1 … H) -H #H1 #H2 destruct - <(le_n_O_to_eq … Hd1) -d1 /2 width=3 by ldrop_atom, ex2_intro/ -| normalize #L #I #V #L2 #e2 #HL2 #_ #He2 +theorem ldrop_conf_be: ∀L0,L1,s1,d1,e1. ⇩[s1, d1, e1] L0 ≡ L1 → + ∀L2,e2. ⇩[e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 → + ∃∃L. ⇩[s1, 0, d1 + e1 - e2] L2 ≡ L & ⇩[d1] L1 ≡ L. +#L0 #L1 #s1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1 +[ #d1 #e1 #He1 #L2 #e2 #H #Hd1 #_ elim (ldrop_inv_atom1 … H) -H #H #He2 destruct + >(He2 ?) in Hd1; // -He2 #Hd1 <(le_n_O_to_eq … Hd1) -d1 + /4 width=3 by ldrop_atom, ex2_intro/ +| normalize #I #L #V #L2 #e2 #HL2 #_ #He2 lapply (le_n_O_to_eq … He2) -He2 #H destruct lapply (ldrop_inv_O2 … HL2) -HL2 #H destruct /2 width=3 by ldrop_pair, ex2_intro/ -| normalize #L0 #K0 #I #V1 #e1 #HLK0 #IHLK0 #L2 #e2 #H #_ #He21 +| normalize #I #L0 #K0 #V1 #e1 #HLK0 #IHLK0 #L2 #e2 #H #_ #He21 lapply (ldrop_inv_O1_pair1 … H) -H * * #He2 #HL20 - [ -IHLK0 -He21 destruct plus_plus_comm_23 #_ #_ #IHLK0 #L2 #e2 #H #Hd1e2 #He2de1 +| #I #L0 #K0 #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHLK0 #L2 #e2 #H #Hd1e2 #He2de1 elim (le_inv_plus_l … Hd1e2) #_ #He2 minus_le_minus_minus_comm /3 width=3 by ldrop_ldrop_lt, ex2_intro/ + >minus_le_minus_minus_comm /3 width=3 by ldrop_drop_lt, ex2_intro/ ] ] -qed. +qed-. +(* Note: with "s2", the conclusion parameter is "s1 ∨ s2" *) (* Basic_1: was: drop_trans_ge *) -theorem ldrop_trans_ge: ∀d1,e1,L1,L. ⇩[d1, e1] L1 ≡ L → - ∀e2,L2. ⇩[0, e2] L ≡ L2 → d1 ≤ e2 → ⇩[0, e1 + e2] L1 ≡ L2. -#d1 #e1 #L1 #L #H elim H -d1 -e1 -L1 -L // -[ /3 width=1/ -| #L1 #L2 #I #V1 #V2 #d #e #H_ #_ #IHL12 #e2 #L #H #Hde2 +theorem ldrop_trans_ge: ∀L1,L,s1,d1,e1. ⇩[s1, d1, e1] L1 ≡ L → + ∀L2,e2. ⇩[e2] L ≡ L2 → d1 ≤ e2 → ⇩[s1, 0, e1 + e2] L1 ≡ L2. +#L1 #L #s1 #d1 #e1 #H elim H -L1 -L -d1 -e1 +[ #d1 #e1 #He1 #L2 #e2 #H #_ elim (ldrop_inv_atom1 … H) -H + #H #He2 destruct /4 width=1 by ldrop_atom, eq_f2/ +| /2 width=1 by ldrop_gen/ +| /3 width=1 by ldrop_drop/ +| #I #L1 #L2 #V1 #V2 #d #e #_ #_ #IHL12 #L #e2 #H #Hde2 lapply (lt_to_le_to_lt 0 … Hde2) // #He2 lapply (lt_to_le_to_lt … (e + e2) He2 ?) // #Hee2 - lapply (ldrop_inv_ldrop1_lt … H ?) -H // #HL2 - @ldrop_ldrop_lt // >le_plus_minus /3 width=1 by monotonic_pred/ + lapply (ldrop_inv_drop1_lt … H ?) -H // #HL2 + @ldrop_drop_lt // >le_plus_minus /3 width=1 by monotonic_pred/ ] qed. (* Basic_1: was: drop_trans_le *) -theorem ldrop_trans_le: ∀d1,e1,L1,L. ⇩[d1, e1] L1 ≡ L → - ∀e2,L2. ⇩[0, e2] L ≡ L2 → e2 ≤ d1 → - ∃∃L0. ⇩[0, e2] L1 ≡ L0 & ⇩[d1 - e2, e1] L0 ≡ L2. -#d1 #e1 #L1 #L #H elim H -d1 -e1 -L1 -L -[ #d #e2 #L2 #H - elim (ldrop_inv_atom1 … H) -H /2 width=3 by ldrop_atom, ex2_intro/ -| #K #I #V #e2 #L2 #HL2 #H - lapply (le_n_O_to_eq … H) -H #H destruct /2 width=3 by ldrop_pair, ex2_intro/ -| #L1 #L2 #I #V #e #_ #IHL12 #e2 #L #HL2 #H - lapply (le_n_O_to_eq … H) -H #H destruct - elim (IHL12 … HL2) -IHL12 -HL2 // #L0 #H #HL0 - lapply (ldrop_inv_O2 … H) -H #H destruct /3 width=5 by ldrop_pair, ldrop_ldrop, ex2_intro/ -| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #IHL12 #e2 #L #H #He2d +theorem ldrop_trans_le: ∀L1,L,s1,d1,e1. ⇩[s1, d1, e1] L1 ≡ L → + ∀L2,s2,e2. ⇩[s2, 0, e2] L ≡ L2 → e2 ≤ d1 → + ∃∃L0. ⇩[s2, 0, e2] L1 ≡ L0 & ⇩[s1, d1 - e2, e1] L0 ≡ L2. +#L1 #L #s1 #d1 #e1 #H elim H -L1 -L -d1 -e1 +[ #d1 #e1 #He1 #L2 #s2 #e2 #H #_ elim (ldrop_inv_atom1 … H) -H + #H #He2 destruct /4 width=3 by ldrop_atom, ex2_intro/ +| #I #K #V #L2 #s2 #e2 #HL2 #H lapply (le_n_O_to_eq … H) -H + #H destruct /2 width=3 by ldrop_pair, ex2_intro/ +| #I #L1 #L2 #V #e #_ #IHL12 #L #s2 #e2 #HL2 #H lapply (le_n_O_to_eq … H) -H + #H destruct elim (IHL12 … HL2) -IHL12 -HL2 // + #L0 #H #HL0 lapply (ldrop_inv_O2 … H) -H #H destruct + /3 width=5 by ldrop_pair, ldrop_drop, ex2_intro/ +| #I #L1 #L2 #V1 #V2 #d #e #HL12 #HV12 #IHL12 #L #s2 #e2 #H #He2d elim (ldrop_inv_O1_pair1 … H) -H * [ -He2d -IHL12 #H1 #H2 destruct /3 width=5 by ldrop_pair, ldrop_skip, ex2_intro/ | -HL12 -HV12 #He2 #HL2 - elim (IHL12 … HL2) -L2 [ >minus_le_minus_minus_comm // /3 width=3 by ldrop_ldrop_lt, ex2_intro/ | /2 width=1 by monotonic_pred/ ] + elim (IHL12 … HL2) -L2 [ >minus_le_minus_minus_comm // /3 width=3 by ldrop_drop_lt, ex2_intro/ | /2 width=1 by monotonic_pred/ ] ] ] -qed. - -(* Basic_1: was: drop_conf_rev *) -axiom ldrop_div: ∀e1,L1,L. ⇩[0, e1] L1 ≡ L → ∀e2,L2. ⇩[0, e2] L2 ≡ L → - ∃∃L0. ⇩[0, e1] L0 ≡ L2 & ⇩[e1, e2] L0 ≡ L1. +qed-. (* Advanced properties ******************************************************) lemma l_liftable_llstar: ∀R. l_liftable R → ∀l. l_liftable (llstar … R l). #R #HR #l #K #T1 #T2 #H @(lstar_ind_r … l T2 H) -l -T2 -[ #L #d #e #_ #U1 #HTU1 #U2 #HTU2 -HR -K +[ #L #s #d #e #_ #U1 #HTU1 #U2 #HTU2 -HR -K >(lift_mono … HTU2 … HTU1) -T1 -U2 -d -e // -| #l #T #T2 #_ #HT2 #IHT1 #L #d #e #HLK #U1 #HTU1 #U2 #HTU2 - elim (lift_total T d e) /3 width=11 by lstar_dx/ +| #l #T #T2 #_ #HT2 #IHT1 #L #s #d #e #HLK #U1 #HTU1 #U2 #HTU2 + elim (lift_total T d e) /3 width=12 by lstar_dx/ ] -qed. +qed-. (* Basic_1: was: drop_conf_lt *) -lemma ldrop_conf_lt: ∀d1,e1,L,L1. ⇩[d1, e1] L ≡ L1 → - ∀e2,K2,I,V2. ⇩[0, e2] L ≡ K2. ⓑ{I} V2 → +lemma ldrop_conf_lt: ∀L,L1,s1,d1,e1. ⇩[s1, d1, e1] L ≡ L1 → + ∀I,K2,V2,s2,e2. ⇩[s2, 0, e2] L ≡ K2.ⓑ{I}V2 → e2 < d1 → let d ≝ d1 - e2 - 1 in - ∃∃K1,V1. ⇩[0, e2] L1 ≡ K1. ⓑ{I} V1 & - ⇩[d, e1] K2 ≡ K1 & ⇧[d, e1] V1 ≡ V2. -#d1 #e1 #L #L1 #H1 #e2 #K2 #I #V2 #H2 #He2d1 + ∃∃K1,V1. ⇩[s2, 0, e2] L1 ≡ K1.ⓑ{I}V1 & + ⇩[s1, d, e1] K2 ≡ K1 & ⇧[d, e1] V1 ≡ V2. +#L #L1 #s1 #d1 #e1 #H1 #I #K2 #V2 #s2 #e2 #H2 #He2d1 elim (ldrop_conf_le … H1 … H2) -L /2 width=2 by lt_to_le/ #K #HL1K #HK2 -elim (ldrop_inv_skip1 … HK2) -HK2 /2 width=1 by lt_plus_to_minus_r/ #K1 #V1 #HK21 #HV12 #H destruct /2 width=5 by ex3_2_intro/ -qed. +elim (ldrop_inv_skip1 … HK2) -HK2 /2 width=1 by lt_plus_to_minus_r/ +#K1 #V1 #HK21 #HV12 #H destruct /2 width=5 by ex3_2_intro/ +qed-. (* Note: apparently this was missing in basic_1 *) -lemma ldrop_trans_lt: ∀d1,e1,L1,L. ⇩[d1, e1] L1 ≡ L → - ∀e2,L2,I,V2. ⇩[0, e2] L ≡ L2.ⓑ{I}V2 → +lemma ldrop_trans_lt: ∀L1,L,s1,d1,e1. ⇩[s1, d1, e1] L1 ≡ L → + ∀I,L2,V2,s2,e2. ⇩[s2, 0, e2] L ≡ L2.ⓑ{I}V2 → e2 < d1 → let d ≝ d1 - e2 - 1 in - ∃∃L0,V0. ⇩[0, e2] L1 ≡ L0.ⓑ{I}V0 & - ⇩[d, e1] L0 ≡ L2 & ⇧[d, e1] V2 ≡ V0. -#d1 #e1 #L1 #L #HL1 #e2 #L2 #I #V2 #HL2 #Hd21 + ∃∃L0,V0. ⇩[s2, 0, e2] L1 ≡ L0.ⓑ{I}V0 & + ⇩[s1, d, e1] L0 ≡ L2 & ⇧[d, e1] V2 ≡ V0. +#L1 #L #s1 #d1 #e1 #HL1 #I #L2 #V2 #s2 #e2 #HL2 #Hd21 elim (ldrop_trans_le … HL1 … HL2) -L /2 width=1 by lt_to_le/ #L0 #HL10 #HL02 elim (ldrop_inv_skip2 … HL02) -HL02 /2 width=1 by lt_plus_to_minus_r/ #L #V1 #HL2 #HV21 #H destruct /2 width=5 by ex3_2_intro/ qed-. -lemma ldrop_trans_ge_comm: ∀d1,e1,e2,L1,L2,L. - ⇩[d1, e1] L1 ≡ L → ⇩[0, e2] L ≡ L2 → d1 ≤ e2 → - ⇩[0, e2 + e1] L1 ≡ L2. -#e1 #e1 #e2 >commutative_plus /2 width=5 by ldrop_trans_ge/ +lemma ldrop_trans_ge_comm: ∀L1,L,L2,s1,d1,e1,e2. + ⇩[s1, d1, e1] L1 ≡ L → ⇩[e2] L ≡ L2 → d1 ≤ e2 → + ⇩[s1, 0, e2 + e1] L1 ≡ L2. +#L1 #L #L2 #s1 #d1 #e1 #e2 +>commutative_plus /2 width=5 by ldrop_trans_ge/ qed. -lemma ldrop_conf_div: ∀I1,L,K,V1,e1. ⇩[0, e1] L ≡ K. ⓑ{I1} V1 → - ∀I2,V2,e2. ⇩[0, e2] L ≡ K. ⓑ{I2} V2 → +lemma ldrop_conf_div: ∀I1,L,K,V1,e1. ⇩[e1] L ≡ K.ⓑ{I1}V1 → + ∀I2,V2,e2. ⇩[e2] L ≡ K.ⓑ{I2}V2 → ∧∧ e1 = e2 & I1 = I2 & V1 = V2. #I1 #L #K #V1 #e1 #HLK1 #I2 #V2 #e2 #HLK2 elim (le_or_ge e1 e2) #He @@ -193,8 +199,8 @@ qed-. (* Advanced forward lemmas **************************************************) -lemma ldrop_fwd_be: ∀L,K,d,e,i. ⇩[d, e] L ≡ K → |K| ≤ i → i < d → |L| ≤ i. -#L #K #d #e #i #HLK #HK #Hd elim (lt_or_ge i (|L|)) // +lemma ldrop_fwd_be: ∀L,K,s,d,e,i. ⇩[s, d, e] L ≡ K → |K| ≤ i → i < d → |L| ≤ i. +#L #K #s #d #e #i #HLK #HK #Hd elim (lt_or_ge i (|L|)) // #HL elim (ldrop_O1_lt … HL) #I #K0 #V #HLK0 -HL elim (ldrop_conf_lt … HLK … HLK0) // -HLK -HLK0 -Hd #K1 #V1 #HK1 #_ #_ lapply (ldrop_fwd_length_lt2 … HK1) -I -K1 -V1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx_sn.ma index 5dafe7a58..0bf892c33 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx_sn.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx_sn.ma @@ -20,47 +20,53 @@ include "basic_2/relocation/ldrop.ma". (* Properties on sn pointwise extension *************************************) lemma lpx_sn_deliftable_dropable: ∀R. l_deliftable_sn R → dropable_sn (lpx_sn R). -#R #HR #L1 #K1 #d #e #H elim H -L1 -K1 -d -e -[ #d #X #H >(lpx_sn_inv_atom1 … H) -H /2 width=3/ -| #K1 #I #V1 #X #H - elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct /3 width=5/ -| #L1 #K1 #I #V1 #e #_ #IHLK1 #X #H - elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct - elim (IHLK1 … HL12) -L1 /3 width=3/ -| #L1 #K1 #I #V1 #W1 #d #e #HLK1 #HWV1 #IHLK1 #X #H +#R #HR #L1 #K1 #s #d #e #H elim H -L1 -K1 -d -e +[ #d #e #He #X #H >(lpx_sn_inv_atom1 … H) -H + /4 width=3 by ldrop_atom, lpx_sn_atom, ex2_intro/ +| #I #K1 #V1 #X #H elim (lpx_sn_inv_pair1 … H) -H + #L2 #V2 #HL12 #HV12 #H destruct + /3 width=5 by ldrop_pair, lpx_sn_pair, ex2_intro/ +| #I #L1 #K1 #V1 #e #_ #IHLK1 #X #H elim (lpx_sn_inv_pair1 … H) -H + #L2 #V2 #HL12 #HV12 #H destruct + elim (IHLK1 … HL12) -L1 /3 width=3 by ldrop_drop, ex2_intro/ +| #I #L1 #K1 #V1 #W1 #d #e #HLK1 #HWV1 #IHLK1 #X #H elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct elim (HR … HV12 … HLK1 … HWV1) -V1 - elim (IHLK1 … HL12) -L1 /3 width=5/ + elim (IHLK1 … HL12) -L1 /3 width=5 by ldrop_skip, lpx_sn_pair, ex2_intro/ ] qed-. lemma lpx_sn_liftable_dedropable: ∀R. (∀L. reflexive ? (R L)) → l_liftable R → dedropable_sn (lpx_sn R). -#R #H1R #H2R #L1 #K1 #d #e #H elim H -L1 -K1 -d -e -[ #d #X #H >(lpx_sn_inv_atom1 … H) -H /2 width=3/ -| #K1 #I #V1 #X #H - elim (lpx_sn_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=5/ -| #L1 #K1 #I #V1 #e #_ #IHLK1 #K2 #HK12 - elim (IHLK1 … HK12) -K1 /3 width=5/ -| #L1 #K1 #I #V1 #W1 #d #e #HLK1 #HWV1 #IHLK1 #X #H +#R #H1R #H2R #L1 #K1 #s #d #e #H elim H -L1 -K1 -d -e +[ #d #e #He #X #H >(lpx_sn_inv_atom1 … H) -H + /4 width=3 by ldrop_atom, lpx_sn_atom, ex2_intro/ +| #I #K1 #V1 #X #H elim (lpx_sn_inv_pair1 … H) -H + #K2 #V2 #HK12 #HV12 #H destruct + /3 width=5 by ldrop_pair, lpx_sn_pair, ex2_intro/ +| #I #L1 #K1 #V1 #e #_ #IHLK1 #K2 #HK12 elim (IHLK1 … HK12) -K1 + /3 width=5 by ldrop_drop, lpx_sn_pair, ex2_intro/ +| #I #L1 #K1 #V1 #W1 #d #e #HLK1 #HWV1 #IHLK1 #X #H elim (lpx_sn_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct elim (lift_total W2 d e) #V2 #HWV2 lapply (H2R … HW12 … HLK1 … HWV1 … HWV2) -W1 - elim (IHLK1 … HK12) -K1 /3 width=5/ + elim (IHLK1 … HK12) -K1 /3 width=5 by ldrop_skip, lpx_sn_pair, ex2_intro/ ] qed-. -fact lpx_sn_dropable_aux: ∀R,L2,K2,d,e. ⇩[d, e] L2 ≡ K2 → ∀L1. lpx_sn R L1 L2 → - d = 0 → ∃∃K1. ⇩[0, e] L1 ≡ K1 & lpx_sn R K1 K2. -#R #L2 #K2 #d #e #H elim H -L2 -K2 -d -e -[ #d #X #H >(lpx_sn_inv_atom2 … H) -H /2 width=3/ -| #K2 #I #V2 #X #H - elim (lpx_sn_inv_pair2 … H) -H #K1 #V1 #HK12 #HV12 #H destruct /3 width=5/ -| #L2 #K2 #I #V2 #e #_ #IHLK2 #X #H #_ - elim (lpx_sn_inv_pair2 … H) -H #L1 #V1 #HL12 #HV12 #H destruct - elim (IHLK2 … HL12) -L2 // /3 width=3/ -| #L2 #K2 #I #V2 #W2 #d #e #_ #_ #_ #L1 #_ - >commutative_plus normalize #H destruct +fact lpx_sn_dropable_aux: ∀R,L2,K2,s,d,e. ⇩[s, d, e] L2 ≡ K2 → ∀L1. lpx_sn R L1 L2 → + d = 0 → ∃∃K1. ⇩[s, 0, e] L1 ≡ K1 & lpx_sn R K1 K2. +#R #L2 #K2 #s #d #e #H elim H -L2 -K2 -d -e +[ #d #e #He #X #H >(lpx_sn_inv_atom2 … H) -H + /4 width=3 by ldrop_atom, lpx_sn_atom, ex2_intro/ +| #I #K2 #V2 #X #H elim (lpx_sn_inv_pair2 … H) -H + #K1 #V1 #HK12 #HV12 #H destruct + /3 width=5 by ldrop_pair, lpx_sn_pair, ex2_intro/ +| #I #L2 #K2 #V2 #e #_ #IHLK2 #X #H #_ elim (lpx_sn_inv_pair2 … H) -H + #L1 #V1 #HL12 #HV12 #H destruct + elim (IHLK2 … HL12) -L2 /3 width=3 by ldrop_drop, ex2_intro/ +| #I #L2 #K2 #V2 #W2 #d #e #_ #_ #_ #L1 #_ + yplus_O1 +| #I1 #I2 #L1 #L2 #V #e #HL12 #IHL12 #J2 #K2 #W #s #i #H #_ >yplus_O1 elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK1 [ -IHL12 | -HL12 ] [ #_ destruct -I2 >ypred_succ /2 width=4 by ldrop_pair, ex2_2_intro/ | lapply (ylt_inv_O1 i ?) /2 width=1 by ylt_inj/ #H yminus_succ yminus_succ yplus_succ1 #H lapply (ylt_inv_succ … H) -H - #Hide lapply (ldrop_inv_ldrop1_lt … HLK2 ?) -HLK2 /2 width=1 by ylt_O/ + #Hide lapply (ldrop_inv_drop1_lt … HLK2 ?) -HLK2 /2 width=1 by ylt_O/ #HLK1 elim (IHL12 … HLK1) -IHL12 -HLK1 yminus_SO2 - /4 width=4 by ylt_O, ldrop_ldrop_lt, ex2_2_intro/ + /4 width=4 by ylt_O, ldrop_drop_lt, ex2_2_intro/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index ceacb2e53..da58e39aa 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -222,7 +222,7 @@ table { } ] [ { "generic local env. slicing" * } { - [ "ldrops ( ⇩*[?] ? ≡ ? )" "ldrops_ldrop" + "ldrops_ldrops" * ] + [ "ldrops ( ⇩*[?,?] ? ≡ ? )" "ldrops_ldrop" + "ldrops_ldrops" * ] } ] [ { "generic term relocation" * } { @@ -260,7 +260,7 @@ table { } ] [ { "basic local env. slicing" * } { - [ "ldrop ( ⇩[?,?] ? ≡ ? )" "ldrop_append" + "ldrop_lpx_sn" + "ldrop_ldrop" * ] + [ "ldrop ( ⇩[?,?,?] ? ≡ ? )" "ldrop_append" + "ldrop_lpx_sn" + "ldrop_ldrop" * ] } ] [ { "basic term relocation" * } { diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/bool.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/bool.ma new file mode 100644 index 000000000..fed25ceda --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/bool.ma @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basics/bool.ma". +include "ground_2/notation/constructors/no_0.ma". +include "ground_2/notation/constructors/yes_0.ma". + +(* BOOLEAN PROPERTIES *******************************************************) + +interpretation "boolean false" 'no = false. + +interpretation "boolean true" 'yes = true. + +lemma orb_false_r: ∀b1,b2:bool. (b1 ∨ b2) = false → b1 = false ∧ b2 = false. +* normalize /2 width=1 by conj/ #b2 #H destruct +qed-. + +lemma commutative_orb: commutative … orb. +* * // qed. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/no_0.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/no_0.ma new file mode 100644 index 000000000..af692211e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/no_0.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation "Ⓕ" + non associative with precedence 55 + for @{'no}. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/yes_0.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/yes_0.ma new file mode 100644 index 000000000..c321749ae --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/yes_0.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation "Ⓣ" + non associative with precedence 55 + for @{'yes}. -- 2.39.2