From b0eb62e60a2fd73ba39c7a0df112f04131528602 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 10 Feb 2018 23:27:55 +0100 Subject: [PATCH] two cases of cpx_lfxs_conf_fle closed + advances on fle + one inversion lemma missing in lveq + one character missing in predefined virtuals --- .../lambdadelta/basic_2/etc/voids/fle.etc | 17 ++++ .../basic_2/rt_computation/lfpxs_etc.ma | 2 +- .../basic_2/rt_transition/cpx_etc.ma | 79 +++++++++++-------- .../lambdadelta/basic_2/static/fle.ma | 19 ----- .../lambdadelta/basic_2/static/fle_drops.ma | 35 +++++--- .../lambdadelta/basic_2/static/fle_fle.ma | 30 ++++--- .../lambdadelta/basic_2/static/fle_fqup.ma | 19 +++++ .../lambdadelta/basic_2/static/fle_lsubf.ma | 31 ++++++++ .../lambdadelta/basic_2/syntax/lveq.ma | 5 ++ .../lambdadelta/basic_2/syntax/lveq_length.ma | 12 +++ .../lambdadelta/basic_2/web/basic_2_src.tbl | 2 +- matita/matita/predefined_virtuals.ml | 2 +- 12 files changed, 181 insertions(+), 72 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/voids/fle.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/static/fle_lsubf.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/voids/fle.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/voids/fle.etc new file mode 100644 index 000000000..6bbb5cea8 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/voids/fle.etc @@ -0,0 +1,17 @@ +(* Basic inversion lemmas ***************************************************) + +fact fle_inv_voids_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊆ ⦃L2, T2⦄ → + ∀K1,K2,n1,n2. |K1| = |K2| → L1 = ⓧ*[n1]K1 → L2 = ⓧ*[n2]K2 → + ∃∃f1,f2. ⓧ*[n1]K1 ⊢ 𝐅*⦃T1⦄ ≡ f1 & ⓧ*[n2]K2 ⊢ 𝐅*⦃T2⦄ ≡ f2 & ⫱*[n1]f1 ⊆ ⫱*[n2]f2. +#L1 #L2 #T1 #T2 * -L1 -L2 +#f1 #f2 #L1 #L2 #n1 #n2 #Hf1 #Hf2 #HL12 #Hf12 #Y1 #Y2 #x1 #x2 #HY12 #H1 #H2 destruct +>H1 in Hf1; >H2 in Hf2; #Hf2 #Hf1 +@(ex3_2_intro … Hf1 Hf2) -Hf1 -Hf2 + +elim (voids_inj_length … H1) // -H -HL12 -HY #H1 #H2 destruct +/2 width=5 by ex3_2_intro/ +qed-. + +lemma fle_inv_voids_sn: ∀L1,L2,T1,T2,n. ⦃ⓧ*[n]L1, T1⦄ ⊆ ⦃L2, T2⦄ → |L1| = |L2| → + ∃∃f1,f2. ⓧ*[n]L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 & L2 ⊢ 𝐅*⦃T2⦄ ≡ f2 & ⫱*[n]f1 ⊆ f2. +/2 width=3 by fle_inv_voids_sn_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.ma index 05f1e7357..e70a8f596 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.ma @@ -8,7 +8,7 @@ lemma lfpxs_cpx_conf: ∀h,G. s_r_confluent1 … (cpx h G) (lfpxs h G). #h #G #L1 #T1 #T2 #HT12 #L2 #H elim (tc_lfxs_inv_lex_lfeq … H) -H #L #HL1 #HL2 lapply (lfxs_lex … HL1 T1) #H -elim (cpx_lfxs_conf_gen … HT12 … H) -HT12 -H // #_ #HT21 #_ +elim (cpx_lfxs_conf_fle … HT12 … H) -HT12 -H // #_ #HT21 #_ @(lfpxs_lpxs_lfeq … HL1) -HL1 @(fle_lfxs_trans … HL2) // qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_etc.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_etc.ma index 7a516ee46..d83d1f063 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_etc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_etc.ma @@ -14,25 +14,17 @@ include "basic_2/static/fle_drops.ma". include "basic_2/static/fle_fqup.ma". +include "basic_2/static/fle_lsubf.ma". include "basic_2/static/fle_fle.ma". -include "basic_2/static/lfxs.ma". +include "basic_2/static/lfxs_length.ma". include "basic_2/rt_transition/cpx.ma". -axiom fle_pair_sn: ∀L,V1,V2. ⦃L, V1⦄ ⊆ ⦃L, V2⦄ → - ∀I1,I2,T. ⦃L.ⓑ{I1}V1, T⦄ ⊆ ⦃L.ⓑ{I2}V2, T⦄. -(* -axiom fle_elim_flat: ∀L1,L2,V1,T2. ⦃L1, V1⦄ ⊆ ⦃L2, T2⦄ → ∀T1. ⦃L1, T1⦄ ⊆ ⦃L2, T2⦄ → - ∀I. ⦃L1, ⓕ{I}V1.T1⦄ ⊆ ⦃L2, T2⦄. - -axiom fle_elim_bind: - ∀p,I1,I2,J1,J2,L,V,W,T. ⦃L, ⓑ{p,I1}ⓕ{J1}V.W.T⦄ ⊆ ⦃L, ⓕ{J2}V.ⓑ{p,I2}W.T⦄. -*) (* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************) (* Properties with context-sensitive free variables *************************) (* Note: "⦃L2, T1⦄ ⊆ ⦃L0, T1⦄" may not hold *) -axiom cpx_lfxs_conf_gen: ∀R. c_reflexive … R → +axiom cpx_lfxs_conf_fle: ∀R. c_reflexive … R → ∀h,G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ⬈[h] T1 → ∀L2. L0 ⪤*[R, T0] L2 → ∧∧ ⦃L2, T0⦄ ⊆ ⦃L0, T0⦄ & ⦃L2, T1⦄ ⊆ ⦃L2, T0⦄ @@ -40,24 +32,40 @@ axiom cpx_lfxs_conf_gen: ∀R. c_reflexive … R → (* #R #HR #h #G #L0 #T0 @(fqup_wf_ind_eq (Ⓕ) … G L0 T0) -G -L0 -T0 #G #L #T #IH #G0 #L0 * * -[ #s #HG #HL #HT #X #HX #Y #_ destruct -IH +[ #s #HG #HL #HT #X #HX #Y #HY destruct -IH + lapply (lfxs_fwd_length … HY) -HY #H0 elim (cpx_inv_sort1 … HX) -HX #H destruct - /2 width=1 by and3_intro/ -| -| #l #HG #HL #HT #X #HX #Y #_ destruct -IH + /3 width=1 by fle_sort_length, and3_intro/ +| * [| #i ] #HG #HL #HT #X #HX #Y #HY destruct + [ elim (cpx_inv_zero1 … HX) -HX + [ #H destruct + elim (lfxs_inv_zero … HY) -HY * + [ #H1 #H2 destruct -IH /2 width=1 by and3_intro/ + | #I #K0 #K2 #V0 #V2 #HK02 #HV02 #H1 #H2 destruct + elim (IH … HK02) [4,5: /2 width=2 by fqu_fqup, fqu_lref_O/ ] + + lapply (lfxs_fwd_length … HY) -HY #H0 + /3 width=1 by fle_lref_length, and3_intro/ + | * #I0 #K0 #V0 #V1 #HLK0 #HV01 #HX + + elim (lfxs_inv_lref … HY) -HY // #HV0 #HT0 + +| #l #HG #HL #HT #X #HX #Y #HY destruct -IH + lapply (lfxs_fwd_length … HY) -HY #H0 >(cpx_inv_gref1 … HX) -X - /2 width=1 by and3_intro/ + /3 width=1 by fle_gref_length, and3_intro/ | #p #I #V0 #T0 #HG #HL #HT #X #HX #Y #HY destruct + lapply (lfxs_fwd_length … HY) #H0 elim (lfxs_inv_bind … V0 ? HY) -HY // #HV0 #HT0 elim (cpx_inv_bind1 … HX) -HX * [ #V1 #T1 #HV01 #HT01 #H destruct elim (IH … HV01 … HV0) -HV01 -HV0 // #H1V #H2V #H3V elim (IH … HT01 … HT0) -HT01 -HT0 -IH // #H1T #H2T #H3T - /5 width=4 by fle_pair_sn, fle_trans, fle_bind, and3_intro/ + /4 width=3 by fle_bind_eq, fle_fwd_pair_sn, and3_intro/ | #T #HT #HXT #H1 #H2 destruct elim (IH G0 … V0… V0 … HV0) -HV0 // #H1V #H2V #H3V elim (IH … HT … HT0) -HT -HT0 -IH // #H1T #H2T #H3T - /4 width=7 by fle_bind_dx, fle_trans, fle_bind, and3_intro/ + /3 width=5 by fle_bind, fle_inv_lifts_sn, and3_intro/ ] | #I #V0 #X0 #HG #HL #HT #X #HX #Y #HY destruct elim (lfxs_inv_flat … HY) -HY #HV0 #HX0 @@ -69,25 +77,32 @@ axiom cpx_lfxs_conf_gen: ∀R. c_reflexive … R → | #HX #H destruct elim (IH G0 … V0… V0 … HV0) -HV0 // #H1V #H2V #H3V elim (IH … HX … HX0) -HX -HX0 -IH // #H1T #H2T #H3T - /4 width=4 by fle_trans, fle_flat, and3_intro/ + /4 width=3 by fle_flat_sn, fle_flat_dx_dx, fle_flat_dx_sn, and3_intro/ | #HX #H destruct elim (IH … HX … HV0) -HX -HV0 // #H1V #H2V #H3V elim (IH G0 … X0… X0 … HX0) -HX0 -IH // #H1T #H2T #H3T - /4 width=4 by fle_trans, fle_flat, and3_intro/ + /4 width=3 by fle_flat_sn, fle_flat_dx_dx, fle_flat_dx_sn, and3_intro/ | #p #V1 #W0 #W1 #T0 #T1 #HV01 #HW01 #HT01 #H1 #H2 #H3 destruct elim (lfxs_inv_bind … W0 ? HX0) -HX0 // #HW0 #HT0 elim (IH … HV01 … HV0) -HV01 -HV0 // #H1V #H2V #H3V elim (IH … HW01 … HW0) -HW01 -HW0 // #H1W #H2W #H3W elim (IH … HT01 … HT0) -HT01 -HT0 -IH // #H1T #H2T #H3T - @and3_intro - [ /3 width=5 by fle_flat, fle_bind/ - | @(fle_trans) - [4: @(fle_flat … H2V) [2: @(fle_bind … H2T) // | skip | @Appl ] - |1,2: skip - | @(fle_trans) [3: @fle_elim_bind - - … H2T) // - - // |1,2: skip - | /2 width=1 by fle_bind_dx/ -*) + lapply (fle_fwd_pair_sn … H2T) -H2T #H2T + lapply (fle_fwd_pair_sn … H3T) -H3T #H3T + @and3_intro [ /3 width=5 by fle_flat, fle_bind/ ] (**) (* full auto too slow *) + @fle_bind_sn_ge /4 width=1 by fle_shift, fle_flat_sn, fle_flat_dx_dx, fle_flat_dx_sn, fle_bind_dx_sn/ + | #p #V1 #X1 #W0 #W1 #T0 #T1 #HV01 #HVX1 #HW01 #HT01 #H1 #H2 #H3 destruct + elim (lfxs_inv_bind … W0 ? HX0) -HX0 // #HW0 #HT0 + elim (IH … HV01 … HV0) -HV01 -HV0 // #H1V #H2V #H3V + elim (IH … HW01 … HW0) -HW01 -HW0 // #H1W #H2W #H3W + elim (IH … HT01 … HT0) -HT01 -HT0 -IH // #H1T #H2T #H3T + lapply (fle_fwd_pair_sn … H2T) -H2T #H2T + lapply (fle_fwd_pair_sn … H3T) -H3T #H3T + @and3_intro[ /3 width=5 by fle_flat, fle_bind/ ] (**) (* full auto too slow *) + @fle_bind_sn_ge // + [1,3: /3 width=1 by fle_flat_dx_dx, fle_bind_dx_sn/ + |2,4: /4 width=3 by fle_flat_sn, fle_flat_dx_sn, fle_flat_dx_dx, fle_shift, fle_lifts_sn/ + ] + ] +] +*) \ No newline at end of file diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/fle.ma b/matita/matita/contribs/lambdadelta/basic_2/static/fle.ma index 95d12b132..921c37b88 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/fle.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/fle.ma @@ -33,22 +33,3 @@ lemma fle_sort: ∀L,s1,s2. ⦃L, ⋆s1⦄ ⊆ ⦃L, ⋆s2⦄. lemma fle_gref: ∀L,l1,l2. ⦃L, §l1⦄ ⊆ ⦃L, §l2⦄. /3 width=8 by frees_gref, sle_refl, ex4_4_intro/ qed. - -(* Basic inversion lemmas ***************************************************) -(* -fact fle_inv_voids_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊆ ⦃L2, T2⦄ → - ∀K1,K2,n1,n2. |K1| = |K2| → L1 = ⓧ*[n1]K1 → L2 = ⓧ*[n2]K2 → - ∃∃f1,f2. ⓧ*[n1]K1 ⊢ 𝐅*⦃T1⦄ ≡ f1 & ⓧ*[n2]K2 ⊢ 𝐅*⦃T2⦄ ≡ f2 & ⫱*[n1]f1 ⊆ ⫱*[n2]f2. -#L1 #L2 #T1 #T2 * -L1 -L2 -#f1 #f2 #L1 #L2 #n1 #n2 #Hf1 #Hf2 #HL12 #Hf12 #Y1 #Y2 #x1 #x2 #HY12 #H1 #H2 destruct ->H1 in Hf1; >H2 in Hf2; #Hf2 #Hf1 -@(ex3_2_intro … Hf1 Hf2) -Hf1 -Hf2 - -elim (voids_inj_length … H1) // -H -HL12 -HY #H1 #H2 destruct -/2 width=5 by ex3_2_intro/ -qed-. - -lemma fle_inv_voids_sn: ∀L1,L2,T1,T2,n. ⦃ⓧ*[n]L1, T1⦄ ⊆ ⦃L2, T2⦄ → |L1| = |L2| → - ∃∃f1,f2. ⓧ*[n]L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 & L2 ⊢ 𝐅*⦃T2⦄ ≡ f2 & ⫱*[n]f1 ⊆ f2. -/2 width=3 by fle_inv_voids_sn_aux/ qed-. -*) \ No newline at end of file diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/fle_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/fle_drops.ma index 4ce02b60b..39bf29385 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/fle_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/fle_drops.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "basic_2/syntax/lveq_length.ma". include "basic_2/static/frees_drops.ma". include "basic_2/static/fle.ma". @@ -19,12 +20,28 @@ include "basic_2/static/fle.ma". (* Advanced properties ******************************************************) -lemma fle_bind_dx: ∀T,U. ⬆*[1] T ≡ U → - ∀p,I,L,V. ⦃L, T⦄ ⊆ ⦃L, ⓑ{p,I}V.U⦄. -#T #U #HTU #p #I #L #V -elim (frees_total L V) #f1 #Hf1 -elim (frees_total L T) #f2 #Hf2 -elim (sor_isfin_ex f1 f2) /3 width=3 by frees_fwd_isfin, isfin_tl/ #f #Hf #_ -lapply (sor_inv_sle_dx … Hf) #Hf0 -/6 width=8 by frees_lifts_SO, frees_bind, drops_refl, drops_drop, sle_tls, ex4_4_intro/ -qed. +lemma fle_lifts_sn: ∀T1,U1. ⬆*[1] T1 ≡ U1 → ∀L1,L2. |L2| ≤ |L1| → + ∀T2. ⦃L1, T1⦄ ⊆ ⦃L2, T2⦄ → ⦃L1.ⓧ, U1⦄ ⊆ ⦃L2, T2⦄. +#T1 #U1 #HTU1 #L1 #L2 #H1L #T2 +* #n #m #f #g #Hf #Hg #H2L #Hfg +lapply (lveq_length_fwd_dx … H2L ?) // -H1L #H destruct +lapply (frees_lifts_SO (Ⓣ) (L1.ⓧ) … HTU1 … Hf) +[ /3 width=4 by drops_refl, drops_drop/ ] -T1 #Hf +@(ex4_4_intro … Hf Hg) /2 width=4 by lveq_void_sn/ (**) (* explict constructor *) +qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma fle_inv_lifts_sn: ∀T1,U1. ⬆*[1] T1 ≡ U1 → + ∀I1,I2,L1,L2,V1,V2,U2. ⦃L1.ⓑ{I1}V1,U1⦄ ⊆ ⦃L2.ⓑ{I2}V2, U2⦄ → + ∀p. ⦃L1, T1⦄ ⊆ ⦃L2, ⓑ{p,I2}V2.U2⦄. +#T1 #U1 #HTU1 #I1 #I2 #L1 #L2 #V1 #V2 #U2 +* #n #m #f2 #g2 #Hf2 #Hg2 #HL #Hfg2 #p +elim (lveq_inv_pair_pair … HL) -HL #HL #H1 #H2 destruct +elim (frees_total L2 V2) #g1 #Hg1 +elim (sor_isfin_ex g1 (⫱g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_ +lapply (frees_inv_lifts_SO (Ⓣ) … Hf2 … HTU1) +[1,2: /3 width=4 by drops_refl, drops_drop/ ] -U1 #Hf2 +lapply (sor_inv_sle_dx … Hg) #H0g +/5 width=10 by frees_bind, sle_tl, sle_trans, ex4_4_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/fle_fle.ma b/matita/matita/contribs/lambdadelta/basic_2/static/fle_fle.ma index 4301456f5..0bd285aca 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/fle_fle.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/fle_fle.ma @@ -57,21 +57,33 @@ elim (lveq_inj … H1n1 … H1n2) -H1n2 #H1 #H2 destruct elim (sor_isfin_ex f1 f2) /2 width=3 by frees_fwd_isfin/ #f #Hf #_ /4 width=12 by frees_flat, sor_inv_sle, sor_tls, ex4_4_intro/ qed. -(* + +theorem fle_bind_eq: ∀L1,L2. |L1| = |L2| → ∀V1,V2. ⦃L1, V1⦄ ⊆ ⦃L2, V2⦄ → + ∀I2,T1,T2. ⦃L1.ⓧ, T1⦄ ⊆ ⦃L2.ⓑ{I2}V2, T2⦄ → + ∀p,I1. ⦃L1, ⓑ{p,I1}V1.T1⦄ ⊆ ⦃L2, ⓑ{p,I2}V2.T2⦄. +#L1 #L2 #HL #V1 #V2 +* #n1 #m1 #f1 #g1 #Hf1 #Hg1 #H1L #Hfg1 #I2 #T1 #T2 +* #n2 #m2 #f2 #g2 #Hf2 #Hg2 #H2L #Hfg2 #p #I1 +elim (lveq_inj_length … H1L) // #H1 #H2 destruct +elim (lveq_inj_length … H2L) // -HL -H2L #H1 #H2 destruct +elim (sor_isfin_ex f1 (⫱f2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #f #Hf #_ +elim (sor_isfin_ex g1 (⫱g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_ +/4 width=15 by frees_bind_void, frees_bind, monotonic_sle_sor, sle_tl, ex4_4_intro/ +qed. + theorem fle_bind: ∀L1,L2,V1,V2. ⦃L1, V1⦄ ⊆ ⦃L2, V2⦄ → ∀I1,I2,T1,T2. ⦃L1.ⓑ{I1}V1, T1⦄ ⊆ ⦃L2.ⓑ{I2}V2, T2⦄ → ∀p. ⦃L1, ⓑ{p,I1}V1.T1⦄ ⊆ ⦃L2, ⓑ{p,I2}V2.T2⦄. -#L1 #L2 #V1 #V2 #HV #I1 #I2 #T1 #T2 #HT #p -@fle_bind_sn -[ @fle_bind_dx_sn // -| @fle_bind_dx_dx - - +#L1 #L2 #V1 #V2 +* #n1 #m1 #f1 #g1 #Hf1 #Hg1 #H1L #Hfg1 #I1 #I2 #T1 #T2 +* #n2 #m2 #f2 #g2 #Hf2 #Hg2 #H2L #Hfg2 #p +elim (lveq_inv_pair_pair … H2L) -H2L #H2L #H1 #H2 destruct +elim (lveq_inj … H2L … H1L) -H1L #H1 #H2 destruct elim (sor_isfin_ex f1 (⫱f2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #f #Hf #_ elim (sor_isfin_ex g1 (⫱g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_ -/4 width=12 by frees_bind, monotonic_sle_sor, sle_tl, ex3_2_intro/ +/4 width=15 by frees_bind, monotonic_sle_sor, sle_tl, ex4_4_intro/ qed. -*) + theorem fle_flat: ∀L1,L2,V1,V2. ⦃L1, V1⦄ ⊆ ⦃L2, V2⦄ → ∀T1,T2. ⦃L1, T1⦄ ⊆ ⦃L2, T2⦄ → ∀I1,I2. ⦃L1, ⓕ{I1}V1.T1⦄ ⊆ ⦃L2, ⓕ{I2}V2.T2⦄. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/fle_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/static/fle_fqup.ma index 65237fbc1..c6d61ed91 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/fle_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/fle_fqup.ma @@ -26,6 +26,25 @@ elim (frees_total L T) #f #Hf /2 width=8 by sle_refl, ex4_4_intro/ qed. +lemma fle_sort_length: ∀L1,L2,s1,s2. |L1| = |L2| → ⦃L1, ⋆s1⦄ ⊆ ⦃L2, ⋆s2⦄. +/3 width=8 by lveq_length_eq, frees_sort, sle_refl, ex4_4_intro/ qed. + +lemma fle_gref_length: ∀L1,L2,l1,l2. |L1| = |L2| → ⦃L1, §l1⦄ ⊆ ⦃L2, §l2⦄. +/3 width=8 by lveq_length_eq, frees_gref, sle_refl, ex4_4_intro/ qed. + +lemma fle_shift: ∀L1,L2. |L1| = |L2| → + ∀I,T1,T2,V. ⦃L1.ⓧ, T1⦄ ⊆ ⦃L2.ⓑ{I}V, T2⦄ → + ∀p. ⦃L1.ⓧ, T1⦄ ⊆ ⦃L2, ⓑ{p,I}V.T2⦄. +#L1 #L2 #H1L #I #T1 #T2 #V +* #n #m #f2 #g2 #Hf2 #Hg2 #H2L #Hfg2 #p +elim (lveq_inj_length … H2L) // -H1L #H1 #H2 destruct +lapply (lveq_inv_bind … H2L) -H2L #HL +elim (frees_total L2 V) #g1 #Hg1 +elim (sor_isfin_ex g1 (⫱g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_ +lapply (sor_inv_sle_dx … Hg) #H0g +/4 width=10 by frees_bind, lveq_void_sn, sle_tl, sle_trans, ex4_4_intro/ +qed. + lemma fle_bind_dx_sn: ∀L1,L2,V1,V2. ⦃L1, V1⦄ ⊆ ⦃L2, V2⦄ → ∀p,I,T2. ⦃L1, V1⦄ ⊆ ⦃L2, ⓑ{p,I}V2.T2⦄. #L1 #L2 #V1 #V2 * #n1 #m1 #f1 #g1 #Hf1 #Hg1 #HL12 #Hfg1 #p #I #T2 diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/fle_lsubf.ma b/matita/matita/contribs/lambdadelta/basic_2/static/fle_lsubf.ma new file mode 100644 index 000000000..7f6af2eaf --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/fle_lsubf.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "basic_2/static/frees_fqup.ma". +include "basic_2/static/lsubf_lsubr.ma". +include "basic_2/static/fle.ma". + +(* FREE VARIABLES INCLUSION FOR RESTRICTED CLOSURES *************************) + +(* Advanced forward lemmas ***************************************************) + +lemma fle_fwd_pair_sn: ∀I1,I2,L1,L2,V1,V2,T1,T2. ⦃L1.ⓑ{I1}V1, T1⦄ ⊆ ⦃L2.ⓑ{I2}V2, T2⦄ → + ⦃L1.ⓧ, T1⦄ ⊆ ⦃L2.ⓑ{I2}V2, T2⦄. +#I1 #I2 #L1 #L2 #V1 #V2 #T1 #T2 * +#n1 #n2 #f1 #f2 #Hf1 #Hf2 #HL12 #Hf12 +elim (lveq_inv_pair_pair … HL12) -HL12 #HL12 #H1 #H2 destruct +elim (frees_total (L1.ⓧ) T1) #g1 #Hg1 +lapply (lsubr_lsubf … Hg1 … Hf1) -Hf1 /2 width=1 by lsubr_unit/ #Hfg1 +/5 width=10 by lsubf_fwd_sle, lveq_bind, sle_trans, ex4_4_intro/ (**) (* full auto too slow *) +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/lveq.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/lveq.ma index e19708385..524c2779b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/lveq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/lveq.ma @@ -94,6 +94,11 @@ lemma lveq_inv_succ: ∀L1,L2,n1,n2. L1 ≋ⓧ*[⫯n1, ⫯n2] L2 → ⊥. (* Advanced inversion lemmas ************************************************) +lemma lveq_inv_bind: ∀I1,I2,K1,K2. K1.ⓘ{I1} ≋ⓧ*[0, 0] K2.ⓘ{I2} → K1 ≋ⓧ*[0, 0] K2. +#I1 #I2 #K1 #K2 #H +elim (lveq_inv_zero … H) -H * [| #Z1 #Z2 #Y1 #Y2 #HY ] #H1 #H2 destruct // +qed-. + lemma lveq_inv_atom_atom: ∀n1,n2. ⋆ ≋ⓧ*[n1, n2] ⋆ → ∧∧ 0 = n1 & 0 = n2. * [2: #n1 ] * [2,4: #n2 ] #H [ elim (lveq_inv_succ … H) diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/lveq_length.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/lveq_length.ma index ab3445522..5c1f16f6f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/lveq_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/lveq_length.ma @@ -46,6 +46,18 @@ lemma lveq_fwd_length: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 → #K1 #K2 #n #_ * #H1 #H2 >length_bind /3 width=1 by minus_Sn_m, conj/ qed-. +lemma lveq_length_fwd_sn: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 → |L1| ≤ |L2| → 0 = n1. +#L1 #L2 #n1 #n2 #H #HL +elim (lveq_fwd_length … H) -H +>(eq_minus_O … HL) // +qed-. + +lemma lveq_length_fwd_dx: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 → |L2| ≤ |L1| → 0 = n2. +#L1 #L2 #n1 #n2 #H #HL +elim (lveq_fwd_length … H) -H +>(eq_minus_O … HL) // +qed-. + lemma lveq_inj_length: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 → |L1| = |L2| → ∧∧ 0 = n1 & 0 = n2. #L1 #L2 #n1 #n2 #H #HL 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 618d4550e..fb78039ee 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 @@ -184,7 +184,7 @@ table { } ] [ { "context-sensitive free variables" * } { - [ [ "inclusion for restricted closures" ] "fle ( ⦃?,?⦄ ⊆ ⦃?,?⦄ )" "fle_drops" + "fle_fqup" + "fle_fle" * ] + [ [ "inclusion for restricted closures" ] "fle ( ⦃?,?⦄ ⊆ ⦃?,?⦄ )" "fle_drops" + "fle_fqup" + "fle_lsubf" + "fle_fle" * ] [ [ "restricted refinement for lenvs" ] "lsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ )" "lsubf_lsubr" + "lsubf_frees" + "lsubf_lsubf" * ] [ [ "for terms" ] "frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )" "frees_drops" + "frees_fqup" + "frees_frees" * ] } diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml index d76dd9e6f..d5aa9b533 100644 --- a/matita/matita/predefined_virtuals.ml +++ b/matita/matita/predefined_virtuals.ml @@ -1539,7 +1539,7 @@ let predefined_classes = [ ["b"; "β"; "ß"; "𝕓"; "𝐛"; "𝛃"; "ⓑ"; ] ; ["B"; "ℶ"; "ℬ"; "𝔹"; "𝐁"; "Ⓑ"; ] ; ["c"; "𝕔"; "𝐜"; "ⓒ"; ] ; - ["C"; "ℭ"; "∁"; "𝐂"; "Ⓒ"; ] ; + ["C"; "ℭ"; "∁"; "𝐂"; "ℂ"; "Ⓒ"; ] ; ["d"; "δ"; "∂"; "𝕕"; "ⅆ"; "𝐝"; "𝛅"; "ⓓ"; ] ; ["D"; "Δ"; "𝔻"; "ⅅ"; "𝐃"; "𝚫"; "Ⓓ"; ] ; ["e"; "ɛ"; "ε"; "ϵ"; "Є"; "ℯ"; "𝕖"; "ⅇ"; "𝐞"; "𝛆"; "𝛜"; "ⓔ"; ] ; -- 2.39.2