X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Fdrops.ma;h=1fc24f51e56e63b193c619a26c8c9436c8164131;hb=50997cb3042073d58c2a16885ef0c82217367e63;hp=a38d5c7a56d765a68f573e1b5066dc193d9424a7;hpb=11792b819aba3f464e63cb8f7834cac1652e372a;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma index a38d5c7a5..1fc24f51e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma @@ -12,11 +12,12 @@ (* *) (**************************************************************************) +include "ground_2/relocation/rtmap_isfin.ma". include "basic_2/notation/relations/rdropstar_4.ma". -include "basic_2/grammar/lenv.ma". +include "basic_2/relocation/lreq.ma". include "basic_2/relocation/lifts.ma". -(* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************) +(* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************) (* Basic_1: includes: drop_skip_bind drop1_skip_bind *) (* Basic_2A1: includes: drop_atom drop_pair drop_drop drop_skip @@ -48,9 +49,20 @@ definition d_deliftable2_sn: predicate (lenv → relation term) ≝ ∃∃T2. ⬆*[f] T2 ≡ U2 & R K T1 T2. definition dropable_sn: predicate (rtmap → relation lenv) ≝ - λR. ∀L1,K1,c,f. ⬇*[c, f] L1 ≡ K1 → ∀L2,u2. R u2 L1 L2 → - ∀u1. f ⊚ u1 ≡ u2 → - ∃∃K2. R u1 K1 K2 & ⬇*[c, f] L2 ≡ K2. + λR. ∀L1,K1,c,f. ⬇*[c, f] L1 ≡ K1 → ∀L2,f2. R f2 L1 L2 → + ∀f1. f ⊚ f1 ≡ f2 → + ∃∃K2. R f1 K1 K2 & ⬇*[c, f] L2 ≡ K2. + +definition dropable_dx: predicate (rtmap → relation lenv) ≝ + λR. ∀L1,L2,f2. R f2 L1 L2 → + ∀K2,c,f. ⬇*[c, f] L2 ≡ K2 → 𝐔⦃f⦄ → + ∀f1. f ⊚ f1 ≡ f2 → + ∃∃K1. ⬇*[c, f] L1 ≡ K1 & R f1 K1 K2. + +definition dedropable_sn: predicate (rtmap → relation lenv) ≝ + λR. ∀L1,K1,c,f. ⬇*[c, f] L1 ≡ K1 → ∀K2,f1. R f1 K1 K2 → + ∀f2. f ⊚ f1 ≡ f2 → + ∃∃L2. R f2 L1 L2 & ⬇*[c, f] L2 ≡ K2 & L1 ≡[f] L2. (* Basic inversion lemmas ***************************************************) @@ -117,18 +129,18 @@ lemma drops_inv_skip2: ∀I,X,K2,V2,c,f. ⬇*[c, ↑f] X ≡ K2.ⓑ{I}V2 → (* Basic properties *********************************************************) -lemma drops_eq_repl_back: ∀L1,L2,c. eq_stream_repl_back … (λf. ⬇*[c, f] L1 ≡ L2). +lemma drops_eq_repl_back: ∀L1,L2,c. eq_repl_back … (λf. ⬇*[c, f] L1 ≡ L2). #L1 #L2 #c #f1 #H elim H -L1 -L2 -f1 [ /4 width=3 by drops_atom, isid_eq_repl_back/ -| #I #L1 #L2 #V #f1 #_ #IH #f2 #H elim (next_inv_sn … H) -H - /3 width=1 by drops_drop/ -| #I #L1 #L2 #V1 #v2 #f1 #_ #HV #IH #f2 #H elim (push_inv_sn … H) -H +| #I #L1 #L2 #V #f1 #_ #IH #f2 #H elim (eq_inv_nx … H) -H + /3 width=3 by drops_drop/ +| #I #L1 #L2 #V1 #v2 #f1 #_ #HV #IH #f2 #H elim (eq_inv_px … H) -H /3 width=3 by drops_skip, lifts_eq_repl_back/ ] qed-. -lemma drops_eq_repl_fwd: ∀L1,L2,c. eq_stream_repl_fwd … (λf. ⬇*[c, f] L1 ≡ L2). -#L1 #L2 #c @eq_stream_repl_sym /2 width=3 by drops_eq_repl_back/ (**) (* full auto fails *) +lemma drops_eq_repl_fwd: ∀L1,L2,c. eq_repl_fwd … (λf. ⬇*[c, f] L1 ≡ L2). +#L1 #L2 #c @eq_repl_sym /2 width=3 by drops_eq_repl_back/ (**) (* full auto fails *) qed-. (* Basic_2A1: includes: drop_refl *) @@ -156,6 +168,15 @@ qed-. (* Basic forward lemmas *****************************************************) +(* Basic_1: includes: drop_gen_refl *) +(* Basic_2A1: includes: drop_inv_O2 *) +lemma drops_fwd_isid: ∀L1,L2,c,f. ⬇*[c, f] L1 ≡ L2 → 𝐈⦃f⦄ → L1 = L2. +#L1 #L2 #c #f #H elim H -L1 -L2 -f // +[ #I #L1 #L2 #V #f #_ #_ #H elim (isid_inv_next … H) // +| /5 width=5 by isid_inv_push, lifts_fwd_isid, eq_f3, sym_eq/ +] +qed-. + fact drops_fwd_drop2_aux: ∀X,Y,c,f2. ⬇*[c, f2] X ≡ Y → ∀I,K,V. Y = K.ⓑ{I}V → ∃∃f1,f. 𝐈⦃f1⦄ & f2 ⊚ ⫯f1 ≡ f & ⬇*[c, f] X ≡ K. #X #Y #c #f2 #H elim H -X -Y -f2 @@ -163,12 +184,10 @@ fact drops_fwd_drop2_aux: ∀X,Y,c,f2. ⬇*[c, f2] X ≡ Y → ∀I,K,V. Y = K. | #I #L1 #L2 #V #f2 #_ #IHL #J #K #W #H elim (IHL … H) -IHL /3 width=7 by after_next, ex3_2_intro, drops_drop/ | #I #L1 #L2 #V1 #V2 #f2 #HL #_ #_ #J #K #W #H destruct - lapply (isid_after_dx 𝐈𝐝 f2 ?) /3 width=9 by after_push, ex3_2_intro, drops_drop/ + lapply (isid_after_dx 𝐈𝐝 … f2) /3 width=9 by after_push, ex3_2_intro, drops_drop/ ] qed-. -(* Basic_1: includes: drop_S *) -(* Basic_2A1: includes: drop_fwd_drop2 *) lemma drops_fwd_drop2: ∀I,X,K,V,c,f2. ⬇*[c, f2] X ≡ K.ⓑ{I}V → ∃∃f1,f. 𝐈⦃f1⦄ & f2 ⊚ ⫯f1 ≡ f & ⬇*[c, f] X ≡ K. /2 width=5 by drops_fwd_drop2_aux/ qed-. @@ -176,17 +195,20 @@ lemma drops_fwd_drop2: ∀I,X,K,V,c,f2. ⬇*[c, f2] X ≡ K.ⓑ{I}V → lemma drops_after_fwd_drop2: ∀I,X,K,V,c,f2. ⬇*[c, f2] X ≡ K.ⓑ{I}V → ∀f1,f. 𝐈⦃f1⦄ → f2 ⊚ ⫯f1 ≡ f → ⬇*[c, f] X ≡ K. #I #X #K #V #c #f2 #H #f1 #f #Hf1 #Hf elim (drops_fwd_drop2 … H) -H -#g1 #g #Hg1 #Hg #HK lapply (after_mono … Hg Hf ??) -Hg -Hf -/3 width=3 by drops_eq_repl_back, isid_inv_eq_repl, next_eq_repl/ +#g1 #g #Hg1 #Hg #HK lapply (after_mono_eq … Hg … Hf ??) -Hg -Hf +/3 width=5 by drops_eq_repl_back, isid_inv_eq_repl, eq_next/ qed-. -(* Basic_1: includes: drop_gen_refl *) -(* Basic_2A1: includes: drop_inv_O2 *) -lemma drops_fwd_isid: ∀L1,L2,c,f. ⬇*[c, f] L1 ≡ L2 → 𝐈⦃f⦄ → L1 = L2. -#L1 #L2 #c #f #H elim H -L1 -L2 -f // -[ #I #L1 #L2 #V #f #_ #_ #H elim (isid_inv_next … H) -| /5 width=3 by isid_inv_push, lifts_fwd_isid, eq_f3, sym_eq/ -] +(* Basic_1: was: drop_S *) +(* Basic_2A1: was: drop_fwd_drop2 *) +lemma drops_isuni_fwd_drop2: ∀I,X,K,V,c,f. 𝐔⦃f⦄ → ⬇*[c, f] X ≡ K.ⓑ{I}V → ⬇*[c, ⫯f] X ≡ K. +/3 width=7 by drops_after_fwd_drop2, after_isid_isuni/ qed-. + +(* forward lemmas with test for finite colength *****************************) + +lemma drops_fwd_isfin: ∀L1,L2,f. ⬇*[Ⓣ, f] L1 ≡ L2 → 𝐅⦃f⦄. +#L1 #L2 #f #H elim H -L1 -L2 -f +/3 width=1 by isfin_next, isfin_push, isfin_isid/ qed-. (* Basic_2A1: removed theorems 14: