-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;
-
+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
|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/
| #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-.
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".
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 *)
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).
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 *)
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).
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
(* 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-.
(**************************************************************************)
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
].
(* 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.
(* *)
(**************************************************************************)
+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)
+
+
+
+<pippo in ⊢ (????%?); >(mf_comp … T) in ⊢ (????%?);
+[2: @@tm_vpush_vlift_join_O
+
+<pippo in ⊢ (????%?);
+
+lapply (HT (#0)) -HT #HT
+*)
+
+lemma tm_md (h) (p) (gv) (lv) (V) (T):
+ ⓓ{p}V.⟦T⟧{TM h}[⇡[0]gv,⇡[0←#0]lv] ≗{TM h} V⊕{TM h}[p]⟦T⟧{TM h}[gv,⫯{TM h}[0←V]lv].
+#h #p #gv #lv #V #T
+>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 ]
-*)
+].
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
+
(**************************************************************************)
(* ___ *)
(* ||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/
/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/ ]
(* 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
>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/
(* 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
>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
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 }.
class "yellow"
[ { "models" * } {
[ { "term model" * } {
- [ "tm" * ]
+ [ "tm" "tm_vpush" * ]
}
]
[ { "denotational equivalence" * } {
}
]
[ { "multiple evaluation push" * } {
- [ "vpushs" + "( ?⨁{?}[?]? ≘ ? )" "vpush_fold" * ]
+ [ "vpushs" + "( ?⨁{?}[?]? ≘ ? )" "vpushs_fold" * ]
}
]
[ { "evaluation equivalence" * } {
projects / helm.git / commitdiff