From: Ferruccio Guidi Date: Sat, 21 Jul 2018 19:28:59 +0000 (+0200) Subject: update in apps_2 X-Git-Tag: make_still_working~295 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=cc600ed1e115d5566947288d532a1e89d989227f update in apps_2 + the model is now aware of polarized abbreviation + the term model is on its way --- diff --git a/matita/matita/contribs/lambdadelta/apps_2/etc/models/model.etc b/matita/matita/contribs/lambdadelta/apps_2/etc/models/model.etc index 51ea8d85b..98f74ff50 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/etc/models/model.etc +++ b/matita/matita/contribs/lambdadelta/apps_2/etc/models/model.etc @@ -1,7 +1,6 @@ -lemma pippo: ∀M,v1,v2,d,i. [i⬐d] v1 ≐⦋M⦌ v2 → v1 ≐⦋M⦌ ↓[i,1] v2. -#M #v1 #v2 #d #i #H #j elim (lt_or_ge … j i) #Hij -[ >lower_lt // <(H j) >raise_lt // -| >lower_ge // <(H (j+1)) >raise_gt /2 width=1 by le_S_S/ -] -qed-. +(* Note: sort evaluation *) + sv: nat → dd; + +(* Note: interpretation: sort *) + ms: ∀gv,lv,s. ⟦⋆s⟧{M}[gv, lv] ≗ sv M s; diff --git a/matita/matita/contribs/lambdadelta/apps_2/etc/models/vdrop_old.etc b/matita/matita/contribs/lambdadelta/apps_2/etc/models/vdrop_old.etc index 5a857fbb1..d7dd140ac 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/etc/models/vdrop_old.etc +++ b/matita/matita/contribs/lambdadelta/apps_2/etc/models/vdrop_old.etc @@ -1,4 +1,9 @@ - +lemma pippo: ∀M,v1,v2,d,i. [i⬐d] v1 ≐⦋M⦌ v2 → v1 ≐⦋M⦌ ↓[i,1] v2. +#M #v1 #v2 #d #i #H #j elim (lt_or_ge … j i) #Hij +[ >lower_lt // <(H j) >raise_lt // +| >lower_ge // <(H (j+1)) >raise_gt /2 width=1 by le_S_S/ +] +qed-. lemma vdrop_refl: ∀M,v,l. ↓[l, 0] v ≐⦋M⦌ v. #M #v #l #i elim (lt_or_ge … i l) #Hil diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/deq_cpr.ma b/matita/matita/contribs/lambdadelta/apps_2/models/deq_cpr.ma index c0d19aefc..32d65f5f5 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/deq_cpr.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/deq_cpr.ma @@ -39,7 +39,8 @@ lemma cpr_fwd_deq (h) (M): is_model M → is_extensional M → |5: /2 width=2 by lifts_SO_fwd_vpush/ | skip ] -U >vpush_gt /3 width=5 by ml, mq, mr/ | #p * #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #gv #lv #Hlv - [ @(mq … H1M) [4,5: /3 width=2 by seq_sym, md/ |1,2: skip ] -p + [ @(mq … H1M) [4,5: /3 width=2 by seq_sym, md/ |1,2: skip ] + @mc [3:|*: /2 width=1 by/ ] -p @(seq_trans … H1M) [2: @IHT /2 width=1 by li_abbr/ | skip ] -T1 /4 width=1 by ti_comp, vpush_comp, (* 2x *) veq_refl/ | /4 width=1 by li_abst, mx/ @@ -53,27 +54,31 @@ lemma cpr_fwd_deq (h) (M): is_model M → is_extensional M → | #G #L #V #U1 #U2 #T2 #_ #IH #HTU2 #gv #lv #Hlv @(mq … H1M) [4: /3 width=2 by seq_sym, md/ | skip - |3: /3 width=1 by li_abbr/ | skip ] -L -U1 + |3: @(seq_trans … H1M) [2: @mz // | skip ] + /3 width=1 by li_abbr/ + |2: skip ] -L -U1 /3 width=1 by lifts_SO_fwd_vpush, seq_sym/ | #G #L #V #T1 #T2 #_ #IH #gv #lv #Hlv @(seq_trans … H1M) [2: @(me … H1M) | skip ] /2 width=1 by/ | #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV #_ #IHT #gv #lv #Hlv @(mq … H1M) [4,5: /3 width=2 by seq_sym, ma, md/ |1,2: skip ] - @(mq … H1M) - [4: /3 width=2 by seq_sym, mb/ | skip - |5: @IHT /2 width=1 by li_abst/ | skip ] -T2 + @(seq_trans … H1M) [3:|*: /2 width=2 by mb/ ] + @mc // -p [ /4 width=5 by seq_trans, seq_sym, me/ ] + @(seq_trans … H1M) [2: @IHT /2 width=1 by li_abst/ | skip ] -T1 @ti_comp /2 width=1 by veq_refl/ @vpush_comp /2 width=1 by veq_refl/ - @(mq … H1M) [4,5: /3 width=2 by seq_sym, me/ |1,2: skip ] -L -V1 - /2 width=1 by mr/ + /4 width=5 by seq_trans, seq_sym, me/ | #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV #IHW #IHT #HV2 #gv #lv #Hlv @(mq … H1M) [4,5: /3 width=2 by seq_sym, ma, md/ |1,2: skip ] - @(seq_trans … H1M) [3: /3 width=1 by seq_sym, ma/ | skip ] - @mp // [ @(seq_trans … H1M) /3 width=3 by lifts_SO_fwd_vpush/ ] -V1 -V -V2 @(mq … H1M) - [4: /3 width=2 by seq_sym, md/ | skip - |3: @IHT /2 width=1 by li_abbr/ | skip ] -T1 + [4: /4 width=2 by seq_sym, md, mp/ |1: skip + |5: /4 width=2 by seq_sym, ma, mc/ |2: skip + ] + @(seq_trans … H1M) [2: @mh // | skip ] + @mc [3:|*: /2 width=1 by mr/ ] + @mp [3:|*: /2 width=1 by lifts_SO_fwd_vpush/ ] + @(seq_trans … H1M) [2: @IHT /2 width=1 by li_abbr/ | skip ] -T1 /4 width=1 by ti_comp, vpush_comp, (* 2x *) veq_refl/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/model.ma b/matita/matita/contribs/lambdadelta/apps_2/models/model.ma index 290c3e4c6..8901e2d71 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/model.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/model.ma @@ -14,6 +14,7 @@ include "ground_2/notation/relations/ringeq_3.ma". include "apps_2/notation/models/at_3.ma". +include "apps_2/notation/models/oplus_4.ma". include "apps_2/notation/models/wbrackets_4.ma". include "static_2/syntax/term.ma". @@ -26,6 +27,8 @@ record model: Type[1] ≝ { sq: relation2 dd dd; (* Note: sort evaluation *) sv: nat → dd; +(* Note: conjunction *) + co: bool → dd → dd → dd; (* Note: application *) ap: dd → dd → dd; (* Note: term interperpretation *) @@ -38,6 +41,9 @@ interpretation "structural equivalence (model)" interpretation "application (model)" 'At M d1 d2 = (ap M d1 d2). +interpretation "conjunction (model)" + 'OPlus M p d1 d2 = (co M p d1 d2). + interpretation "term interpretation (model)" 'WBrackets M gv lv T = (ti M gv lv T). diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/model_props.ma b/matita/matita/contribs/lambdadelta/apps_2/models/model_props.ma index 346917ff8..b3acfc262 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/model_props.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/model_props.ma @@ -21,6 +21,8 @@ record is_model (M): Prop ≝ { mr: reflexive … (sq M); (* Note: equivalence: compatibility *) mq: replace_2 … (sq M) (sq M) (sq M); +(* Note: conjunction: compatibility *) + mc: ∀p. compatible_3 … (co M p) (sq M) (sq M) (sq M); (* Note: application: compatibility *) mp: compatible_3 … (ap M) (sq M) (sq M) (sq M); (* Note: interpretation: sort *) @@ -29,27 +31,36 @@ record is_model (M): Prop ≝ { ml: ∀gv,lv,i. ⟦#i⟧{M}[gv, lv] ≗ lv i; (* Note: interpretation: global reference *) mg: ∀gv,lv,l. ⟦§l⟧{M}[gv, lv] ≗ gv l; -(* Note: interpretation: local δ-equivalence *) - md: ∀gv,lv,p,V,T. ⟦ⓓ{p}V.T⟧{M}[gv, lv] ≗ ⟦T⟧[gv, ⫯[0←⟦V⟧[gv, lv]]lv]; -(* Note: interpretation: intensional abstraction *) - mi: ∀gv1,gv2,lv1,lv2,p,W,T. ⟦W⟧{M}[gv1, lv1] ≗ ⟦W⟧{M}[gv2, lv2] → +(* Note: interpretation: intensional binder *) + mi: ∀p,gv1,gv2,lv1,lv2,W,T. ⟦W⟧{M}[gv1, lv1] ≗ ⟦W⟧{M}[gv2, lv2] → (∀d. ⟦T⟧{M}[gv1, ⫯[0←d]lv1] ≗ ⟦T⟧{M}[gv2, ⫯[0←d]lv2]) → ⟦ⓛ{p}W.T⟧[gv1, lv1] ≗ ⟦ⓛ{p}W.T⟧[gv2, lv2]; +(* Note: interpretation: abbreviation *) + md: ∀p,gv,lv,V,T. ⟦ⓓ{p}V.T⟧{M}[gv, lv] ≗ ⟦V⟧[gv, lv] ⊕[p] ⟦T⟧[gv, ⫯[0←⟦V⟧[gv, lv]]lv]; (* Note: interpretation: application *) ma: ∀gv,lv,V,T. ⟦ⓐV.T⟧{M}[gv, lv] ≗ ⟦V⟧[gv, lv] @ ⟦T⟧[gv, lv]; +(* Note: interpretation: ζ-equivalence *) + mz: ∀d1,d2. d1 ⊕{M}[Ⓣ] d2 ≗ d2; (* Note: interpretation: ϵ-equivalence *) me: ∀gv,lv,W,T. ⟦ⓝW.T⟧{M}[gv, lv] ≗ ⟦T⟧[gv, lv]; (* Note: interpretation: β-requivalence *) - mb: ∀gv,lv,d,p,W,T. d @ ⟦ⓛ{p}W.T⟧{M}[gv, lv] ≗ ⟦T⟧[gv, ⫯[0←d]lv] + mb: ∀p,gv,lv,d,W,T. d @ ⟦ⓛ{p}W.T⟧{M}[gv, lv] ≗ d ⊕[p] ⟦T⟧[gv, ⫯[0←d]lv]; +(* Note: interpretation: θ-requivalence *) + mh: ∀p,d1,d2,d3. d1 @ (d2 ⊕{M}[p] d3) ≗ d2 ⊕[p] (d1 @ d3) }. record is_extensional (M): Prop ≝ { (* Note: interpretation: extensional abstraction *) - mx: ∀gv1,gv2,lv1,lv2,p,W1,W2,T1,T2. ⟦W1⟧{M}[gv1, lv1] ≗ ⟦W2⟧{M}[gv2, lv2] → + mx: ∀p,gv1,gv2,lv1,lv2,W1,W2,T1,T2. ⟦W1⟧{M}[gv1, lv1] ≗ ⟦W2⟧{M}[gv2, lv2] → (∀d. ⟦T1⟧{M}[gv1, ⫯[0←d]lv1] ≗ ⟦T2⟧{M}[gv2, ⫯[0←d]lv2]) → ⟦ⓛ{p}W1.T1⟧[gv1, lv1] ≗ ⟦ⓛ{p}W2.T2⟧[gv2, lv2] }. +record is_injective (M): Prop ≝ { +(* Note: conjunction: injectivity *) + mj: ∀d1,d3,d2,d4. d1 ⊕[Ⓕ] d2 ≗{M} d3 ⊕[Ⓕ] d4 → d2 ≗ d4 +}. + (* Basic properties *********************************************************) lemma seq_sym (M): is_model M → symmetric … (sq M). @@ -64,6 +75,12 @@ lemma seq_canc_sn (M): is_model M → left_cancellable … (sq M). lemma seq_canc_dx (M): is_model M → right_cancellable … (sq M). /3 width=3 by seq_trans, seq_sym/ qed-. +lemma co_inv_dx (M): is_model M → is_injective M → + ∀p,d1,d3,d2,d4. d1⊕[p]d2 ≗{M} d3⊕[p]d4 → d2 ≗ d4. +#M #H1M #H2M * #d1 #d3 #d2 #d4 #Hd +/3 width=5 by mj, mz, mq/ +qed-. + lemma ti_lref_vpush_eq (M): is_model M → ∀gv,lv,d,i. ⟦#i⟧[gv,⫯[i←d]lv] ≗{M} d. #M #HM #gv #lv #d #i @@ -80,10 +97,20 @@ qed. (* Basic Forward lemmas *****************************************************) -lemma ti_fwd_mx_dx (M): is_model M → - ∀gv1,gv2,lv1,lv2,p,W1,W2,T1,T2. - ⟦ⓛ{p}W1.T1⟧[gv1, lv1] ≗ ⟦ⓛ{p}W2.T2⟧[gv2, lv2] → - ∀d. ⟦T1⟧{M}[gv1, ⫯[0←d]lv1] ≗ ⟦T2⟧{M}[gv2, ⫯[0←d]lv2]. -#M #HM #gv1 #gv2 #lv1 #lv2 #p #W1 #W2 #T1 #T2 #H12 #d -@(mq … HM) /3 width=5 by mb, mp, mr/ +lemma ti_fwd_mx_dx (M): is_model M → is_injective M → + ∀p,gv1,gv2,lv1,lv2,W1,W2,T1,T2. + ⟦ⓛ{p}W1.T1⟧[gv1,lv1] ≗ ⟦ⓛ{p}W2.T2⟧[gv2,lv2] → + ∀d. ⟦T1⟧{M}[gv1,⫯[0←d]lv1] ≗ ⟦T2⟧{M}[gv2,⫯[0←d]lv2]. +#M #H1M #H2M #p #gv1 #gv2 #lv1 #lv2 #W1 #W2 #T1 #T2 #H12 #d +@(co_inv_dx … p d d) +/4 width=5 by mb, mp, mq, mr/ +qed-. + +lemma ti_fwd_abbr_dx (M): is_model M → is_injective M → + ∀p,gv1,gv2,lv1,lv2,V1,V2,T1,T2. + ⟦ⓓ{p}V1.T1⟧[gv1,lv1] ≗ ⟦ⓓ{p}V2.T2⟧[gv2,lv2] → + ⟦T1⟧{M}[gv1,⫯[0←⟦V1⟧[gv1,lv1]]lv1] ≗ ⟦T2⟧{M}[gv2,⫯[0←⟦V2⟧[gv2,lv2]]lv2]. +#M #H1M #H2M #p #gv1 #gv2 #lv1 #lv2 #V1 #V2 #T1 #T2 #H12 +@(co_inv_dx … p (⟦V1⟧[gv1,lv1]) (⟦V2⟧[gv2,lv2])) +/3 width=5 by md, mq/ qed-. diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/tm.ma b/matita/matita/contribs/lambdadelta/apps_2/models/tm.ma index 2a630c592..a0f7b84d1 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/tm.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/tm.ma @@ -13,54 +13,28 @@ (**************************************************************************) include "basic_2/rt_equivalence/cpcs.ma". -include "apps_2/functional/flifts_basic.ma". +include "apps_2/functional/mf.ma". include "apps_2/models/model.ma". -include "apps_2/notation/models/dotteduparrow_2.ma". -include "apps_2/notation/models/dotteduparrow_3.ma". (* TERM MODEL ***************************************************************) definition tm_dd ≝ term. -definition tm_evaluation ≝ nat → tm_dd. - definition tm_sq (h) (T1) (T2) ≝ ⦃⋆, ⋆⦄ ⊢ T1 ⬌*[h] T2. definition tm_sv (s) ≝ ⋆s. -definition tm_ap (V) (T) ≝ ⓐV.T. - -definition tm_vlift (j) (gv): tm_evaluation ≝ λi. ↑[j,1](gv i). - -interpretation "lift (term model evaluation)" - 'DottedUpArrow i gv = (tm_vlift i gv). - -definition tm_vpush (j) (T) (lv): tm_evaluation ≝ - λi. tri … i j (lv i) T (↑[j,1](lv (↓i))). - -interpretation "push (term model evaluation)" - 'DottedUpArrow i d lv = (tm_vpush i d lv). +definition tm_co (p) (V) (T) ≝ ⓓ{p}V.(↑[1]T). -rec definition tm_ti gv lv T on T ≝ match T with -[ TAtom I ⇒ match I with - [ Sort _ ⇒ T - | LRef i ⇒ lv i - | GRef l ⇒ gv l - ] -| TPair I V T ⇒ match I with - [ Bind2 _ _ ⇒ TPair I (tm_ti gv lv V) (tm_ti (⇡[0]gv) (⇡[0←#0]lv) T) - | Flat2 _ ⇒ TPair I (tm_ti gv lv V) (tm_ti gv lv T) - ] -]. - -definition tm_lc: tm_evaluation ≝ λi.#i. +definition tm_ap (V) (T) ≝ ⓐV.T. -definition tm_gc: tm_evaluation ≝ λl.§l. +definition tm_ti (gv) (lv) (T) ≝ ●[gv,lv]T. definition TM (h): model ≝ mk_model … . [ @tm_dd -| @(tm_sq h) |6,7: skip +| @(tm_sq h) |7,8: skip | @tm_sv +| @tm_co | @tm_ap | @tm_ti ]. @@ -68,17 +42,11 @@ defined-. (* Basic properties *********************************************************) -lemma tm_vlift_rw (j) (gv): ∀i. (⇡[j]gv) i = ↑[j,1](gv i). +lemma tm_co_rw (h) (p) (V) (T): V⊕{TM h}[p]T = ⓓ{p}V.(↑[1]T). // qed. -lemma tm_vpush_lt (lv) (j) (T): ∀i. i < j → (⇡[j←T]lv) i = lv i. -/2 width=1 by tri_lt/ qed-. - -lemma tm_vpush_eq: ∀lv,T,i. (⇡[i←T]lv) i = T. -/2 width=1 by tri_eq/ qed. - -lemma tm_vpush_gt: ∀lv,T,j,i. j < i → (⇡[j←T]lv) i = ↑[j,1](lv (↓i)). -/2 width=1 by tri_gt/ qed-. +lemma tm_ti_sort (h) (gv) (lv): ∀s. ⟦⋆s⟧{TM h}[gv,lv] = sv … s. +// qed. lemma tm_ti_lref (h): ∀gv,lv,i. ⟦#i⟧{TM h}[gv,lv] = lv i. // qed. diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/tm_props.ma b/matita/matita/contribs/lambdadelta/apps_2/models/tm_props.ma index 260d2415a..280bd8e51 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/tm_props.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/tm_props.ma @@ -12,43 +12,72 @@ (* *) (**************************************************************************) +include "basic_2/rt_equivalence/cpcs_drops.ma". include "basic_2/rt_equivalence/cpcs_cpcs.ma". +include "apps_2/functional/mf_lifts.ma". +include "apps_2/functional/mf_cpr.ma". include "apps_2/models/model_props.ma". -include "apps_2/models/tm.ma". +include "apps_2/models/tm_vpush.ma". (* TERM MODEL ***************************************************************) -lemma tm_md (h): ∀T,V,gv,lv. ⟦+ⓓV.T⟧[gv,lv] ≗{TM h} ⟦T⟧[gv,⫯[O←⟦V⟧[gv,lv]]lv]. -#h #T elim T * -[ /4 width=3 by cpc_cpcs, cpm_zeta, or_introl/ -| #i #V #gv #lv - elim (eq_or_gt i) #Hi destruct - [ elim (lifts_total (⟦V⟧[gv,lv]) (𝐔❴1❵)) #W #HVW - >tm_ti_lref >vpush_eq - >tm_ti_bind >tm_ti_lref >tm_vpush_eq - /5 width=3 by cpc_cpcs, cpm_zeta, cpm_delta, or_introl/ - | >tm_ti_lref >vpush_gt // - >tm_ti_bind >tm_ti_lref >tm_vpush_gt // - /4 width=3 by cpc_cpcs, cpm_zeta, or_introl/ - ] -| #l #V #gv #lv - >tm_ti_bind >tm_ti_gref >tm_ti_gref - /4 width=3 by cpc_cpcs, cpm_zeta, or_introl/ -| #p #I #W #T #IHW #IHT #V #gv #lv - >tm_ti_bind in ⊢ (???%); +lemma cpcs_repl (h) (G) (L): replace_2 … (cpcs h G L) (cpcs h G L) (cpcs h G L). +/3 width=5 by cpcs_trans, cpcs_sym/ qed-. (* - - >tm_ti_bind >tm_ti_bind - @cpc_cpcs @or_introl - @cpm_bind - - /4 width=3 by cpc_cpcs, cpm_zeta, or_introl/ +lemma pippo (h) (gv) (lv) (T): ●[gv,lv]T = ⟦T⟧{TM h}[gv,lv]. +// qed. + +lemma tm_mi (h) (gv1) (gv2) (lv1) (lv2) (p) (W) (T): + ⟦W⟧[gv1,lv1] ≗{TM h} ⟦W⟧[gv2,lv2] → + (∀d. ⟦T⟧[gv1,⫯[0←d]lv1] ≗ ⟦T⟧[gv2,⫯[0←d]lv2]) → + ⟦ⓛ{p}W.T⟧[gv1,lv1] ≗ ⟦ⓛ{p}W.T⟧[gv2,lv2]. +#h #gv1 #gv2 #lv1 #lv2 #p #W #T #HW #HT +>tm_ti_bind >tm_ti_bind +@(cpcs_bind1 … HW) + + + +(mf_comp … T) in ⊢ (????%?); +[2: @@tm_vpush_vlift_join_O + +tm_co_rw >(mf_lifts_basic_SO_dx T 0) +>(mf_comp … T) in ⊢ (???%); +[2: @tm_vpush_vlift_join_O |4: @exteq_refl |3,5: skip ] +/6 width=4 by mf_delta_drops, cpcs_bind1, cpc_cpcs, drops_refl, or_introl/ +qed. + +lemma tm_mz (h) (V) (T): V ⊕[Ⓣ] T ≗{TM h} T. +/4 width=3 by cpc_cpcs, cpm_zeta, or_introl/ qed. + +lemma tm_me (h) (gv) (lv) (U) (T): + ⟦ⓝU.T⟧[gv,lv] ≗{TM h} ⟦T⟧[gv,lv]. +/4 width=1 by cpc_cpcs, cpm_eps, or_introl/ qed. + +lemma tm_mb (h) (p) (gv) (lv) (d) (W) (T): + d@⟦ⓛ{p}W.T⟧[gv,lv] ≗{TM h} d⊕[p]⟦T⟧[gv,⫯[0←d]lv]. +#h #p #gv #lv #d #W #T +@cpcs_repl [5: @tm_md |4: /4 width=2 by cpc_cpcs, cpm_beta, or_intror/ |1,2: skip ] +/5 width=1 by cpcs_bind1, cpc_cpcs, cpm_eps, or_introl/ +qed. + +lemma ti_mh (h) (p) (d1) (d2) (d3): + d1@(d2⊕[p]d3) ≗{TM h} d2⊕[p](d1@d3). +/4 width=3 by cpc_cpcs, cpm_theta, or_introl/ qed. definition is_tm (h): is_model (TM h) ≝ mk_is_model …. // -[ +[ @cpcs_repl +| #p #V1 #V2 #HV #T1 #T2 #HT + @(cpcs_bind1 … HV) @(cpcs_lifts_bi … HT) + /2 width=5 by drops_drop/ +| #V1 #V2 #HV #T1 #T2 #HT + @(cpcs_flat … HV … HT) | -| #gv #lv #p #V #T - @cpcs_cprs_dx - @cprs_step_sn - [2: @cpm_bind // | skip ] -*) +]. diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/tm_vpush.ma b/matita/matita/contribs/lambdadelta/apps_2/models/tm_vpush.ma new file mode 100644 index 000000000..e1f086da0 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/models/tm_vpush.ma @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "ground_2/lib/exteq.ma". +include "apps_2/models/model_vpush.ma". +include "apps_2/models/tm.ma". + +(* TERM MODEL ***************************************************************) + +(* Properties with push for model evaluation ********************************) + +lemma tm_vpush_vlift_join_O (h) (v) (T): ⇡[0]⫯{TM h}[0←T]v ≐ ⇡[0←↑[1]T]v. +#h #v #T #i +elim (eq_or_gt i) #Hi destruct +[ >mf_vpush_eq >mf_vlift_rw >vpush_eq // +| >mf_vpush_gt // >mf_vlift_rw >vpush_gt // +] +qed. diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma b/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma index a351e2003..4d3d16c1e 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma @@ -1,3 +1,4 @@ + (**************************************************************************) (* ___ *) (* ||M|| *) @@ -87,7 +88,7 @@ lemma ti_comp (M): is_model M → [ /4 width=5 by seq_trans, seq_sym, ms/ | /4 width=5 by seq_sym, ml, mq/ | /4 width=3 by seq_trans, seq_sym, mg/ -| /5 width=5 by vpush_comp, seq_sym, md, mq/ +| /6 width=5 by vpush_comp, seq_sym, md, mc, mq/ | /5 width=1 by vpush_comp, mi, mr/ | /4 width=5 by seq_sym, ma, mp, mq/ | /4 width=5 by seq_sym, me, mq/ diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/veq_lifts.ma b/matita/matita/contribs/lambdadelta/apps_2/models/veq_lifts.ma index 943f8f5af..d7a225140 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/veq_lifts.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/veq_lifts.ma @@ -40,6 +40,7 @@ fact lifts_fwd_vpush_aux (M): is_model M → is_extensional M → /2 width=1 by mr/ | #f #p * #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #m #Hm #gv #lv #d destruct [ @(mq … H1M) [4,5: /3 width=2 by seq_sym, md/ |1,2: skip ] + @mc [3:|*: /2 width=1 by/ ] @(seq_trans … H1M) [3: @ti_comp // | skip ] [1,2: /2 width=2 by veq_refl/ ] diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/vpushs_fold.ma b/matita/matita/contribs/lambdadelta/apps_2/models/vpushs_fold.ma index 7f5eacc47..59f9b3e84 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/vpushs_fold.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/vpushs_fold.ma @@ -20,9 +20,9 @@ include "apps_2/models/vpushs.ma". (* Properties with fold for restricted closures *****************************) lemma vpushs_fold (M): is_model M → is_extensional M → - ∀L,T1,T2,gv,lv. - (∀v. L ⨁[gv] lv ≘ v → ⟦T1⟧[gv, v] ≗ ⟦T2⟧[gv, v]) → - ⟦L+T1⟧[gv, lv] ≗{M} ⟦L+T2⟧[gv, lv]. + ∀L,T1,T2,gv,lv. + (∀v. L ⨁[gv] lv ≘ v → ⟦T1⟧[gv, v] ≗ ⟦T2⟧[gv, v]) → + ⟦L+T1⟧[gv, lv] ≗{M} ⟦L+T2⟧[gv, lv]. #M #H1M #H2M #L elim L -L [| #K * [| * ]] [ #T1 #T2 #gv #lv #H12 >fold_atom >fold_atom @@ -34,7 +34,7 @@ lemma vpushs_fold (M): is_model M → is_extensional M → >fold_pair >fold_pair @IH -IH #v #Hv @(mq … H1M) [3:|*: /3 width=2 by seq_sym, md/ ] - /4 width=1 by vpushs_abbr, mr/ + /4 width=1 by vpushs_abbr, mc, mr/ | #W #IH #T1 #T2 #gv #lv #H12 >fold_pair >fold_pair /5 width=1 by vpushs_abst, mx, mr/ @@ -43,10 +43,10 @@ qed. (* Inversion lemmas with fold for restricted closures ***********************) -lemma vpushs_inv_fold (M): is_model M → - ∀L,T1,T2,gv,lv. ⟦L+T1⟧[gv, lv] ≗{M} ⟦L+T2⟧[gv, lv] → - ∀v. L ⨁[gv] lv ≘ v → ⟦T1⟧[gv, v] ≗ ⟦T2⟧[gv, v]. -#M #HM #L elim L -L [| #K * [| * ]] +lemma vpushs_inv_fold (M): is_model M → is_injective M → + ∀L,T1,T2,gv,lv. ⟦L+T1⟧[gv, lv] ≗{M} ⟦L+T2⟧[gv, lv] → + ∀v. L ⨁[gv] lv ≘ v → ⟦T1⟧[gv, v] ≗ ⟦T2⟧[gv, v]. +#M #H1M #H2M #L elim L -L [| #K * [| * ]] [ #T1 #T2 #gv #lv >fold_atom >fold_atom #H12 #v #H lapply (vpushs_inv_atom … H) -H // #Hv @@ -60,7 +60,8 @@ lemma vpushs_inv_fold (M): is_model M → >fold_pair >fold_pair #H12 #y #H elim (vpushs_inv_abbr … H) -H // #v #Hlv #Hv lapply (IH … H12 … Hlv) -IH -H12 -Hlv #H12 - /4 width=7 by ti_comp, veq_refl, md, mq/ + @(mq … H1M) [4,5: @(ti_comp … Hv) /3 width=2 by veq_refl/ |1,2: skip ] + /4 width=7 by ti_comp, ti_fwd_abbr_dx, veq_refl, mq/ | #W #IH #T1 #T2 #gv #lv >fold_pair >fold_pair #H12 #y #H elim (vpushs_inv_abst … H) -H // #v #d #Hlv #Hv diff --git a/matita/matita/contribs/lambdadelta/apps_2/notation/models/oplus_4.ma b/matita/matita/contribs/lambdadelta/apps_2/notation/models/oplus_4.ma new file mode 100644 index 000000000..6d5a64356 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/notation/models/oplus_4.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "models" COMPONENT **************************************) + +notation < "hvbox( d1 ⊕[ break term 46 p ] break term 46 d2 )" + non associative with precedence 47 + for @{ 'OPlus $M $p $d1 $d2 }. + +notation > "hvbox( d1 ⊕[ break term 46 p ] break term 46 d2 )" + non associative with precedence 47 + for @{ 'OPlus ? $p $d1 $d2 }. + +notation > "hvbox( d1 ⊕{ break term 46 M }[ break term 46 p ] break term 46 d2 )" + non associative with precedence 47 + for @{ 'OPlus $M $p $d1 $d2 }. diff --git a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl index 6010578f4..1966269f1 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl @@ -12,7 +12,7 @@ table { class "yellow" [ { "models" * } { [ { "term model" * } { - [ "tm" * ] + [ "tm" "tm_vpush" * ] } ] [ { "denotational equivalence" * } { @@ -24,7 +24,7 @@ table { } ] [ { "multiple evaluation push" * } { - [ "vpushs" + "( ?⨁{?}[?]? ≘ ? )" "vpush_fold" * ] + [ "vpushs" + "( ?⨁{?}[?]? ≘ ? )" "vpushs_fold" * ] } ] [ { "evaluation equivalence" * } {