From: Ferruccio Guidi Date: Tue, 1 May 2018 16:34:07 +0000 (+0200) Subject: update in models and ground_2 X-Git-Tag: make_still_working~335 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=c52e807a10cac88866b61fa458936dc5c0f5ee70 update in models and ground_2 + model declaration completed + compatibility with veq, first results + some old files moved in etc for now --- diff --git a/matita/matita/contribs/lambdadelta/apps_2/etc/models/model.etc b/matita/matita/contribs/lambdadelta/apps_2/etc/models/model.etc new file mode 100644 index 000000000..51ea8d85b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/etc/models/model.etc @@ -0,0 +1,7 @@ + +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-. diff --git a/matita/matita/contribs/lambdadelta/apps_2/etc/models/model_cpr.etc b/matita/matita/contribs/lambdadelta/apps_2/etc/models/model_cpr.etc new file mode 100644 index 000000000..cc96e9954 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/etc/models/model_cpr.etc @@ -0,0 +1,54 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reduction/cpr.ma". +include "apps_2/models/model_drop.ma". + +(* MODEL ********************************************************************) + +(* Forward lemmas on context-sensitive parallel reduction for terms *********) + +lemma sound_fwd_cpr: ∀M. sound M → extensional M → + ∀sv,gv,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → + ∀lv. lv ∈ 〚L〛⦋M⦌{sv, gv} → 〚T1〛{sv, gv, lv} = 〚T2〛{sv, gv, lv}. +#M #H1M #H2M #sv #gv #G #L #T1 #T2 #H elim H -G -L -T1 -T2 // +[ #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #lv #Hlv >(m2 … H1M) + <(sound_fwd_lift … H1M H2M … HVW2) -HVW2 + lapply (sound_drop … HLK … Hlv) // -L -H2M #H + elim (li_inv_ldef … H) -H #v #HK #H + elim (lower_inv_raise_be … H) -H #H >H -H #Hlv + (m4 … H1M) >(m4 … H1M) -H1M (m6 … H1M) >(m6 … H1M) -H1M /3 width=1 by eq_f2/ + | -IHV12 >(m7 … H1M) >(m7 … H1M) -H1M /2 width=1 by/ + ] +| #G #L #V #U1 #U2 #T2 #_ #HTU2 #IHU12 #lv #Hlv >(m4 … H1M) + >IHU12 -IHU12 /2 width=1 by li_ldef/ + <(sound_fwd_lift … H1M H2M … HTU2) -H2M -HTU2 + /2 width=1 by sound_ti_eq_l/ +| #G #L #V #T1 #T2 #_ #IHT12 #lv #Hlv >(m7 … H1M) -H1M /2 width=1 by/ +| #a #G #L #V1 #V2 #W1 #w2 #T1 #T2 #_ #_ #_ #IHV12 #_ #IHT12 #lv #Hlv + >(m6 … H1M) >(m8 … H1M) >(m4 … H1M) >(m7 … H1M) -H1M + >IHV12 -IHV12 /3 width=1 by li_ldec/ +| #a #G #L #V1 #V2 #W2 #U1 #U2 #T1 #T2 #_ #HVW2 #_ #_ #IHV12 #IHU12 #IHT12 #lv #Hlv + >(m6 … H1M) >(m4 … H1M) >(m4 … H1M) >(m6 … H1M) + >IHV12 -IHV12 // (m1 … H1M) >(m1 … H1M) -H1M // +| #i #l #m #Hil #lv >(m2 … H1M) >(m2 … H1M) -H1M >lower_lt // +| #i #l #m #Hli #lv >(m2 … H1M) >(m2 … H1M) -H1M >lower_ge // +| #p #l #m #lv >(m3 … H1M) >(m3 … H1M) -H1M // +| #a * #V1 #V2 #T1 #T2 #l #m #_ #_ #IHV12 #IHT12 #lv + [ >(m4 … H1M) >(m4 … H1M) /3 width=1 by raise_lower_lt, sound_ti_eq_l/ + | @(mx … H2M) /3 width=1 by raise_lower_lt, sound_ti_eq_l/ + ] +| * #V1 #V2 #T1 #T2 #l #m #_ #_ #IHV12 #IHT12 #lv + [ >(m6 … H1M) >(m6 … H1M) /3 width=1 by eq_f2/ + | >(m7 … H1M) >(m7 … H1M) /2 width=1 by/ + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/apps_2/etc/models/model_lower.etc b/matita/matita/contribs/lambdadelta/apps_2/etc/models/model_lower.etc new file mode 100644 index 000000000..e99004e7b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/etc/models/model_lower.etc @@ -0,0 +1,181 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "apps_2/notation/models/fdrop_4.ma". +include "apps_2/models/model_veq.ma". +include "apps_2/models/model_raise.ma". + +(* MODEL ********************************************************************) + +definition lower: ∀M. nat → nat → evaluation M → evaluation M ≝ + λM,l,m,lv,i. tri … i l (lv i) (lv (i+m)) (lv (i+m)). + +interpretation "evaluation lower (models)" + 'FDrop M l m lv = (lower M l m lv). + +(* Basic properties *********************************************************) + +lemma lower_lt: ∀M,lv,l,m,i. i < l → (↓[l, m]⦋M⦌ lv) i = lv i. +/2 width=1 by tri_lt/ qed-. + +lemma lower_ge: ∀M,lv,l,m,i. l ≤ i → (↓[l, m]⦋M⦌ lv) i = lv (i+m). +#M #lv #l #m #i #Hli elim (le_to_or_lt_eq … Hli) -Hli #Hli destruct +[ /2 width=1 by tri_gt/ +| /2 width=1 by tri_eq/ +] +qed-. + +lemma lower_veq: ∀M,v1,v2. v1 ≐⦋M⦌ v2 → ∀l,m. ↓[l, m] v1 ≐ ↓[l, m] v2. +#m #v1 #v2 #Hv12 #l #m #i elim (lt_or_ge i l) #Hli +[ >lower_lt // >lower_lt // +| >lower_ge // >lower_ge // +] +qed. + +lemma lower_refl: ∀M,v,l. ↓[l, 0] v ≐⦋M⦌ v. +#M #v #l #i elim (lt_or_ge … i l) #Hil +[ >lower_lt // +| >lower_ge // +] +qed. + +(* Main properties **********************************************************) + +theorem lower_lower_le_sym: ∀M,v,l1,l2,m1,m2. l1 ≤ l2 → + ↓[l1, m1] ↓[l2+m1, m2] v ≐⦋M⦌ ↓[l2, m2] ↓[l1, m1] v. +#M #v #l1 #l2 #m1 #m2 #Hl12 #j elim (lt_or_ge … j l1) #Hjl1 +[ lapply (lt_to_le_to_lt … Hjl1 Hl12) -Hl12 #Hjl2 + >lower_lt // >lower_lt /2 width=3 by lt_to_le_to_lt/ + >lower_lt // >lower_lt // +| >lower_ge // elim (lt_or_ge … j l2) #Hjl2 -Hl12 + [ >lower_lt /2 width=1 by lt_minus_to_plus/ + >lower_lt // >lower_ge // + | >lower_ge /2 width=1 by monotonic_le_plus_l/ + >lower_ge // >lower_ge /2 width=1 by le_plus/ + ] +] +qed. + +lemma lower_lower_le: ∀M,v,l1,l2,m1,m2. l1 ≤ l2 → + ↓[l2, m2] ↓[l1, m1] v ≐⦋M⦌ ↓[l1, m1] ↓[l2+m1, m2] v. +/3 width=1 by lower_lower_le_sym, veq_sym/ qed-. + +(* Properties on raise ******************************************************) + +lemma lower_raise_lt: ∀M,v,d,l,m,i. i ≤ l → ↓[l+1, m] [i⬐d] v ≐⦋M⦌ [i⬐d] ↓[l, m] v. +#M #v #d #l #m #i #Hil #j elim (lt_or_eq_or_gt … j i) #Hij destruct +[ lapply (lt_to_le_to_lt … Hij Hil) -Hil #Hjl + >lower_lt /2 width=1 by le_S/ >raise_lt // >raise_lt // >lower_lt // +| >lower_lt /2 width=1 by le_S_S/ >raise_eq >raise_eq // +| lapply (ltn_to_ltO … Hij) #Hj + >raise_gt // elim (lt_or_ge … j (l+1)) #Hlj + [ -Hil >lower_lt // >lower_lt /2 width=2 by lt_plus_to_minus/ >raise_gt // + | >lower_ge // >lower_ge /2 width=1 by le_plus_to_minus_r/ + >raise_gt /2 width=1 by le_plus/ >plus_minus // + ] +] +qed. + +lemma raise_lower_lt: ∀M,v,d,l,m,i. i ≤ l → [i⬐d] ↓[l, m] v ≐⦋M⦌ ↓[l+1, m] [i⬐d] v. +/3 width=1 by lower_raise_lt, veq_sym/ qed. + +lemma lower_raise_be: ∀M,v,d,l,m,i. l ≤ i → i ≤ l + m → ↓[l, m+1] [i⬐d] v ≐⦋M⦌ ↓[l, m] v. +#M #v #d #l #m #i #Hli #Hilm #j elim (lt_or_ge … j l) #Hlj +[ lapply (lt_to_le_to_lt … Hlj Hli) -Hli -Hilm #Hij + >lower_lt // >lower_lt // >raise_lt // +| lapply (transitive_le … (j+m) Hilm ?) -Hli -Hilm /2 width=1 by monotonic_le_plus_l/ #Hijm + >lower_ge // >lower_ge // >raise_gt /2 width=1 by le_S_S/ +] +qed. + +lemma lower_raise_be_sym: ∀M,v,d,l,m,i. l ≤ i → i ≤ l + m → ↓[l, m] v ≐⦋M⦌ ↓[l, m+1] [i⬐d] v. +/3 width=1 by lower_raise_be, veq_sym/ qed. + +lemma lower_raise: ∀M,v,d,l. ↓[l, 1] [l⬐d] v ≐⦋M⦌ v. +/3 width=3 by lower_raise_be, veq_trans/ qed. + +lemma lower_raise_sym: ∀M,v,d,l. v ≐⦋M⦌ ↓[l, 1] [l⬐d] v. +/2 width=1 by veq_sym/ qed. + +lemma raise_lower: ∀M,v,i. [i⬐v i] ↓[i,1] v ≐⦋M⦌ v. +#M #V #i #j elim (lt_or_eq_or_gt j i) #Hij destruct +[ >raise_lt // >lower_lt // +| >raise_eq // +| >raise_gt // >lower_ge /2 width=1 by monotonic_pred/ + lower_lt // >raise_lt // >lower_lt // +| >lower_ge // >raise_eq // +| lapply (ltn_to_ltO … Hlj) #Hj + >lower_ge /2 width=1 by lt_to_le/ >raise_gt // + >lower_ge /4 width=1 by plus_minus, monotonic_pred, eq_f/ +] +qed. + +lemma raise_lower_be_sym: ∀M,v,l,m. [l⬐v (l+m)] ↓[l, m+1] v ≐⦋M⦌ ↓[l, m] v. +/3 width=1 by raise_lower_be, veq_sym/ qed. + +(* Forward lemmas on raise **************************************************) + +lemma lower_fwd_raise_be_S: ∀M,v1,v2,d,l,m. ↓[l, m] v1 ≐⦋M⦌ [l⬐d] v2 → + ↓[l, m+1] v1 ≐ v2. +#M #v1 #v2 #d #l #m #Hv12 #j elim (lt_or_ge j l) #Hlj +[ lapply (Hv12 j) -Hv12 + >lower_lt // >lower_lt // >raise_lt // +| lapply (Hv12 (j+1)) + >lower_ge /2 width=1 by le_S/ >lower_ge // >raise_gt /2 width=1 by le_S_S/ +] +qed-. + +lemma raise_fwd_lower_be_S: ∀M,v1,v2,d,l,m. [l⬐d] v2 ≐⦋M⦌ ↓[l, m] v1 → + v2 ≐ ↓[l, m+1] v1. +/3 width=2 by lower_fwd_raise_be_S, veq_sym/ qed-. + +lemma lower_fwd_raise_be_O: ∀M,v1,v2,d,l,m. ↓[l, m] v1 ≐⦋M⦌ [l⬐d] v2 → v1 (l+m) = d. +#M #v1 #v2 #d #l #m #Hv12 lapply (Hv12 l) +>lower_ge // >raise_eq // +qed-. + +lemma raise_fwd_lower_be_O: ∀M,v1,v2,d,l,m. [l⬐d] v2 ≐⦋M⦌ ↓[l, m] v1 → d = v1 (l+m). +/4 width=7 by lower_fwd_raise_be_O, veq_sym, sym_eq/ qed-. + +(* Inversion lemmas on raise ************************************************) + +lemma raise_inv_lower_lt: ∀M,v1,v2,d,l,m,i. i ≤ l → [i⬐d] v1 ≐⦋M⦌ ↓[l+1, m] v2 → + ∃∃v. v1 ≐ ↓[l, m] v & v2 ≐ [i⬐d] v. +#M #v1 #v2 #d #l #m #i #Hil #Hv12 +lapply (Hv12 i) >raise_eq >lower_lt /2 width=1 by le_S_S/ #H destruct +@(ex2_intro … (↓[i, 1] v2)) // +@(veq_trans … (↓[i, 1] ↓[l+1, m] v2)) +/3 width=3 by lower_lower_le_sym, lower_veq, veq_trans/ +qed-. + +lemma lower_inv_raise_lt: ∀M,v1,v2,d,l,m,i. i ≤ l → ↓[l+1, m] v2 ≐⦋M⦌ [i⬐d] v1 → + ∃∃v. v1 ≐ ↓[l, m] v & v2 ≐ [i⬐d] v. +/3 width=1 by raise_inv_lower_lt, veq_sym/ qed-. + +lemma lower_inv_raise_be: ∀M,v1,v2,d,l,m. ↓[l, m] v1 ≐⦋M⦌ [l⬐d] v2 → + v1 (l+m) = d ∧ ↓[l, m+1] v1 ≐ v2. +/3 width=2 by lower_fwd_raise_be_O, lower_fwd_raise_be_S, conj/ qed-. + +lemma raise_inv_lower_be: ∀M,v1,v2,d,l,m. [l⬐d] v2 ≐⦋M⦌ ↓[l, m] v1 → + d = v1 (l+m) ∧ v2 ≐ ↓[l, m+1] v1. +/3 width=2 by raise_fwd_lower_be_O, raise_fwd_lower_be_S, conj/ qed-. diff --git a/matita/matita/contribs/lambdadelta/apps_2/etc/models/model_nlift.etc b/matita/matita/contribs/lambdadelta/apps_2/etc/models/model_nlift.etc new file mode 100644 index 000000000..2c4e8eca1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/etc/models/model_nlift.etc @@ -0,0 +1,44 @@ +(**************************************************************************) +(* ___ *) +(* ||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/substitution/lift_neg.ma". +include "apps_2/models/model_sound.ma". + +(* MODEL ********************************************************************) + +lemma sound_ti_eq_nlift: ∀M. sound M → ∀sv,gv,U,lv1,lv2. + (∀i. (∀T. ⬆[i, 1]T ≡ U → ⊥) → lv1 i = lv2 i) → + 〚U〛⦋M⦌{sv, gv, lv1} = 〚U〛⦋M⦌{sv, gv, lv2}. +#M #HM #sv #gv #U elim U -U * [||| #a * | * ] +[ #k #lv1 #lv2 #H >(m1 … HM) >(m1 … HM) -HM // +| #i #lv1 #lv2 #H >(m2 … HM) >(m2 … HM) -HM + /3 width=7 by lift_inv_lref2_be/ +| #p #lv1 #lv2 #H >(m3 … HM) >(m3 … HM) -HM // +| #W #U #IHW #IHU #lv1 #lv2 #H >(m4 … HM) >(m4 … HM) + @IHU -IHU #i @(nat_ind_plus … i) -i + [ /5 width=9 by nlift_bind_sn/ + | #i #_ #H0 >raise_gt // >raise_gt // + /4 width=9 by nlift_bind_dx/ + ] +| #W #U #IHW #IHU #lv1 #lv2 #H @(m5 … HM) /5 width=9 by nlift_bind_sn/ + #d @IHU -IHU #i @(nat_ind_plus … i) -i // + #i #_ #H0 lapply (nlift_bind_dx … H0) -H0 + #H0 lapply (H i ?) -H /2 width=5 by/ -H0 #H + >raise_gt // >raise_gt // +| #W #U #IHW #IHU #lv1 #lv2 #H >(m6 … HM) >(m6 … HM) + /6 width=8 by nlift_flat_sn, nlift_flat_dx, eq_f2/ +| #W #U #_ #IHU #lv1 #lv2 #H >(m7 … HM) >(m7 … HM) + /5 width=8 by nlift_flat_dx/ +] +qed-. 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 c07d13022..90ab35238 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/model_props.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/model_props.ma @@ -12,12 +12,15 @@ (* *) (**************************************************************************) +include "ground_2/lib/functions.ma". include "apps_2/models/model_push.ma". (* MODEL ********************************************************************) record is_model (M): Prop ≝ { mq: reflexive … (sq M); + mr: replace_2 … (sq M) (sq M) (sq M); + mc: compatible_3 … (ap M) (sq M) (sq M) (sq M); ms: ∀gv,lv,s. ⟦⋆s⟧{M}[gv, lv] ≗ sv M s; ml: ∀gv,lv,i. ⟦#i⟧{M}[gv, lv] ≗ lv i; mg: ∀gv,lv,l. ⟦§l⟧{M}[gv, lv] ≗ gv l; @@ -35,3 +38,11 @@ record is_extensional (M): Prop ≝ { (∀d. ⟦T1⟧{M}[gv, ⫯[d]lv1] ≗ ⟦T2⟧{M}[gv, ⫯[d]lv2]) → ⟦ⓛ{p}W1.T1⟧[gv, lv1] ≗ ⟦ⓛ{p}W2.T2⟧[gv, lv2] }. + +(* Basic properties *********************************************************) + +lemma seq_sym (M): is_model M → symmetric … (sq M). +/3 width=5 by mr, mq/ qed-. + +lemma seq_trans (M): is_model M → Transitive … (sq M). +/3 width=5 by mr, mq/ qed-. diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma b/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma index a64dc2b19..11f07c404 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma @@ -27,10 +27,41 @@ interpretation "evaluation equivalence (model)" lemma veq_refl (M): is_model M → reflexive … (veq M). /2 width=1 by mq/ qed. + +lemma veq_repl (M): is_model M → + replace_2 … (veq M) (veq M) (veq M). +/2 width=5 by mr/ qed-. + +(* Properties with evaluation push ******************************************) + +lemma push_comp (M): ∀i. compatible_3 … (push M i) (sq M) (veq M) (veq M). +#m #i #d1 #d2 #Hd12 #lv1 #lv2 #HLv12 #j +elim (lt_or_eq_or_gt j i) #Hij destruct +[ >(push_lt … Hij) >(push_lt … Hij) // +| >(push_eq …) >(push_eq …) // +| >(push_gt … Hij) >(push_gt … Hij) // +] +qed. + +(* Inversion lemmas with evaluation push *************************************) + +axiom veq_inv_push_sn: ∀M,lv1,y2,d1,i. ⫯[i←d1]lv1 ≗{M} y2 → + ∃∃lv2,d2. lv1 ≗ lv2 & d1 ≗ d2 & ⫯[i←d2]lv2 = y2. (* -lemma veq_sym: ∀M. symmetric … (veq M). -// qed-. +#M #lv1 #y2 #d1 #i #H +*) +(* Properies with term interpretation ***************************************) -theorem veq_trans: ∀M. transitive … (veq M). -// qed-. -*) \ No newline at end of file +lemma ti_comp_l (M): is_model M → + ∀T,gv,lv1,lv2. lv1 ≗{M} lv2 → + ⟦T⟧[gv, lv1] ≗ ⟦T⟧[gv, lv2]. +#M #HM #T elim T -T * [||| #p * | * ] +[ /4 width=3 by seq_trans, seq_sym, ms/ +| /4 width=5 by seq_sym, ml, mr/ +| /4 width=3 by seq_trans, seq_sym, mg/ +| /5 width=5 by push_comp, seq_sym, md, mr/ +| /5 width=1 by push_comp, mi, mq/ +| /4 width=5 by seq_sym, ma, mc, mr/ +| /4 width=5 by seq_sym, me, mr/ +] +qed. diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/veq_li.ma b/matita/matita/contribs/lambdadelta/apps_2/models/veq_li.ma new file mode 100644 index 000000000..717a03911 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/models/veq_li.ma @@ -0,0 +1,36 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "apps_2/models/model_li.ma". +include "apps_2/models/veq.ma". + +(* EVALUATION EQUIVALENCE **************************************************) + +(* Properties with local environment interpretation *************************) + +lemma li_repl_back (M) (gv): is_model M → + ∀L,lv1. lv1 ϵ ⟦L⟧[gv] → + ∀lv2. lv1 ≗{M} lv2 → lv2 ϵ ⟦L⟧[gv]. +#M #gv #HM #L #lv1 #H elim H -L -lv1 // +[ #lv1 #d1 #K #V #_ #Hd #IH #y #H + elim (veq_inv_push_sn … H) -H #lv2 #d2 #Hlv12 #Hd12 #H destruct + /4 width=5 by li_abbr, ti_comp_l, mr/ +| #lv1 #d1 #K #W #_ #IH #y #H + elim (veq_inv_push_sn … H) -H #lv2 #d2 #Hlv12 #_ #H destruct + /3 width=1 by li_abst/ +| #lv1 #d1 #I #K #_ #IH #y #H + elim (veq_inv_push_sn … H) -H #lv2 #d2 #Hlv12 #_ #H destruct + /3 width=1 by li_unit/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/apps_2/notation/models/downspoon_3.ma b/matita/matita/contribs/lambdadelta/apps_2/notation/models/downspoon_3.ma new file mode 100644 index 000000000..434c98e7e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/notation/models/downspoon_3.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( ⫰[ break term 46 i ] break term 46 lv )" + non associative with precedence 46 + for @{ 'DownSpoon $M $d $lv }. + +notation > "hvbox( ⫰[ break term 46 i ] break term 46 lv )" + non associative with precedence 46 + for @{ 'DownSpoon ? $d $lv }. + +notation > "hvbox( ⫰{ term 46 M }[ break term 46 i ] break term 46 lv )" + non associative with precedence 46 + for @{ 'DownSpoon $M $d $lv }. 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 e7dc9c67e..4a5ab318a 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 @@ -9,6 +9,26 @@ table { ] } ] + class "orange" + [ { "models" * } { + [ { "denotational equivalence" * } { + [ "deq" + "( ? ⊢ ? ≗{?} ? )" * ] + } + ] + [ { "evaluation equivalence" * } { + [ "veq" + "( ? ≗{?} ? )" "veq_li" * ] + } + ] + [ { "model declaration" * } { + [ "model" + "( ? ≗{?} ? )" + "( ? @{?} ? )" + "( ⟦?⟧{?}[?,?] )" + "model_push" + "( ⫯{?}[?] )" + "( ⫯{?}[?←?] )" + "model_props" + "model_li" + "( ? ϵ ⟦?⟧{?}[?] )" + * ] + } + ] + } + ] (* class "yellow" [ { "MLTT1" * } { diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/functions.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/functions.ma index 64fbae2e1..4276e1a6c 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/functions.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/functions.ma @@ -16,6 +16,10 @@ include "ground_2/lib/relations.ma". (* FUNCTIONS ****************************************************************) -definition left_identity (A:Type[0]) (f): predicate A ≝ λi. ∀a:A. a = f i a. +definition left_identity (A) (f): predicate A ≝ λi. ∀a:A. a = f i a. -definition right_identity (A:Type[0]) (f): predicate A ≝ λi. ∀a:A. a = f a i. +definition right_identity (A) (f): predicate A ≝ λi. ∀a:A. a = f a i. + +definition compatible_3 (A) (B) (C): relation4 … (relation A) (relation B) (relation C) ≝ + λf,Sa,Sb,Sc. + ∀a1,a2. Sa a1 a2 → ∀b1,b2. Sb b1 b2 → Sc (f a1 b1) (f a2 b2). diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/relations.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/relations.ma index af10dbb89..7c63b469f 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/relations.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/relations.ma @@ -20,6 +20,9 @@ include "ground_2/lib/logic.ma". lemma insert_eq: ∀A,a. ∀Q1,Q2:predicate A. (∀a0. Q1 a0 → a = a0 → Q2 a0) → Q1 a → Q2 a. /2 width=1 by/ qed-. +definition replace_2 (A) (B): relation3 (relation2 A B) (relation A) (relation B) ≝ + λR,Sa,Sb. ∀a1,b1. R a1 b1 → ∀a2. Sa a1 a2 → ∀b2. Sb b1 b2 → R a2 b2. + (* Inclusion ****************************************************************) definition subR2 (S1) (S2): relation (relation2 S1 S2) ≝