From: Ferruccio Guidi Date: Wed, 11 Jul 2018 10:54:33 +0000 (+0200) Subject: update in static_2 and app_2 X-Git-Tag: make_still_working~300 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=41b61472d2c475e0f69e3dfc85539da3ad2bac1e update in static_2 and app_2 + advances on the support for models + tentative definition of shift (incomplete because unary binders are missing in terms) + minor updates and corrections --- diff --git a/helm/www/lambdadelta/download/lambda_talk_1s.pdf b/helm/www/lambdadelta/download/lambda_talk_1s.pdf new file mode 100644 index 000000000..5831950c5 Binary files /dev/null and b/helm/www/lambdadelta/download/lambda_talk_1s.pdf differ diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile index 073dc33a2..9d87f9909 100644 --- a/matita/matita/contribs/lambdadelta/Makefile +++ b/matita/matita/contribs/lambdadelta/Makefile @@ -32,8 +32,8 @@ WWW := ../../../../helm/www/lambdadelta TAGS := all xoa xoa2 orig elim deps top leaf stats tbls trim contrib clean \ www up-html -PACKAGES := ground_2 basic_2 static_2 apps_2 alpha_1 -XPACKAGES := ground_2 basic_2 +PACKAGES := ground_2 static_2 basic_2 apps_2 alpha_1 +XPACKAGES := ground_2 static_2 basic_2 LDWS := $(shell find -name "*.ldw.xml") TBLS := $(shell find -name "*.tbl") diff --git a/matita/matita/contribs/lambdadelta/apps_2/etc/models/downspoon_3.etc b/matita/matita/contribs/lambdadelta/apps_2/etc/models/downspoon_3.etc new file mode 100644 index 000000000..a0e2b5fc3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/etc/models/downspoon_3.etc @@ -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 $i $lv }. + +notation > "hvbox( ⫰[ break term 46 i ] break term 46 lv )" + non associative with precedence 46 + for @{ 'DownSpoon ? $i $lv }. + +notation > "hvbox( ⫰{ term 46 M }[ break term 46 i ] break term 46 lv )" + non associative with precedence 46 + for @{ 'DownSpoon $M $i $lv }. diff --git a/matita/matita/contribs/lambdadelta/apps_2/etc/models/model_ext.etc b/matita/matita/contribs/lambdadelta/apps_2/etc/models/model_ext.etc new file mode 100644 index 000000000..8c6e9d7c8 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/etc/models/model_ext.etc @@ -0,0 +1,78 @@ + +include "ground_2/lib/exteq.ma". +include "apps_2/models/model_li.ma". +include "apps_2/models/vdrop.ma". + +lemma vlift_ext (M): ∀i. compatible_3 … (vlift M i) (eq …) (exteq …) (exteq …). +#M #i #d1 #d2 #Hd12 #lv1 #lv2 #HLv12 #j +elim (lt_or_eq_or_gt j i) #Hij destruct +[ >vlift_lt // >vlift_lt // +| >vlift_eq >vlift_eq // +| >vlift_gt // >vlift_gt // +] +qed. + +lemma vdrop_ext (M): ∀i. compatible_2 … (vdrop M i) (exteq …) (exteq …). +#M #i #lv1 #lv2 #Hlv12 #j elim (lt_or_ge j i) #Hji +[ >vdrop_lt // >vdrop_lt // +| >vdrop_ge // >vdrop_ge // +] +qed. + +lemma vlift_vdrop_eq (M): ∀lv,i. lv ≐{?,dd M} ⫯[i←lv i]⫰[i]lv. +#M #lv #i #j elim (lt_or_eq_or_gt j i) #Hji destruct +[ >vlift_lt // >vdrop_lt // +| >vlift_eq // +| >vlift_gt // >vdrop_ge /2 width=1 by monotonic_pred/ + <(lt_succ_pred … Hji) // +] +qed. + +axiom vdrop_vlift_eq: ∀M,lv,d,i. lv ≐{?,dd M} ⫰[i]⫯[i←d]lv. +(* +#M #lv #d #i #j elim (lt_or_eq_or_gt j i) #Hji destruct +*) + +lemma ext_inv_vlift_sn (M): ∀lv1,y,i,d. ⫯[i←d]lv1 ≐{?,dd M} y → + ∧∧ d = y i & lv1 ≐ ⫰[i]y. +#M #lv1 #y #i #d #H @conj +[ lapply (H i) -H >vlift_eq // +| @exteq_trans [2: @(vdrop_vlift_eq … d i) | skip ] + @vdrop_ext // +] +qed-. + +lemma ext_inv_vlift_sn (M): ∀lv1,y,i,d. ⫯[i←d]lv1 ≐{?,dd M} y → + ∃∃lv2. lv1 ≐ lv2 & ⫯[i←d]lv2 = y. + +lemma li_repl (M) (gv): ∀lv1,L. lv1 ϵ ⟦L⟧{M}[gv] → + ∀lv2. lv1 ≐ lv2 → lv2 ϵ ⟦L⟧{M}[gv]. +#M #gv #lv1 #L #H elim H -lv1 -L +[ // +| +| #lv1 #d #K #W #_ #IH #y #H + + + + +lemma ext_veq (M): is_model M → + ∀lv1,lv2. lv1 ≐ lv2 → lv1 ≗{M} lv2. +/2 width=1 by mr/ qed. + +lemma veq_repl_exteq (M): is_model M → + replace_2 … (veq M) (exteq …) (exteq …). +/2 width=5 by mq/ qed-. + +lemma exteq_veq_trans (M): ∀lv1,lv. lv1 ≐ lv → + ∀lv2. lv ≗{M} lv2 → lv1 ≗ lv2. +// qed-. + +lemma ti_ext_l (M): is_model M → + ∀T,gv,lv1,lv2. lv1 ≐ lv2 → + ⟦T⟧[gv, lv1] ≗{M} ⟦T⟧[gv, lv2]. +/3 width=1 by ti_comp_l, ext_veq/ qed. + +lemma valign_ext (M) (l): compatible_2 … (valign M l) (exteq …) (exteq …). +#M #l #lv1 #lv2 #HLv12 #i +>valign_rw >valign_rw // +qed. diff --git a/matita/matita/contribs/lambdadelta/apps_2/etc/models/model_gi.etc b/matita/matita/contribs/lambdadelta/apps_2/etc/models/model_gi.etc new file mode 100644 index 000000000..1c354a621 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/etc/models/model_gi.etc @@ -0,0 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "static_2/syntax/genv.ma". + +(* GLOBAL ENVIRONMENT INTERPRETATION ***************************************) diff --git a/matita/matita/contribs/lambdadelta/apps_2/etc/models/model_valign.etc b/matita/matita/contribs/lambdadelta/apps_2/etc/models/model_valign.etc new file mode 100644 index 000000000..aafa0c097 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/etc/models/model_valign.etc @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||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/functions.ma". +include "ground_2/lib/exteq.ma". +include "apps_2/models/model.ma". + +(* MODEL ********************************************************************) + +definition valign (M) (l): evaluation M → evaluation M ≝ + λlv,i. ⫯[l](lv i). + +interpretation "alignment (model evaluation)" + 'UpSpoon M l lv = (valign M l lv). + +(* Basic properties *********************************************************) + +lemma valign_rw (M) (l) (lv): ∀i. (⫯{M}[l]lv) i = ⫯[l](lv i). +// qed. diff --git a/matita/matita/contribs/lambdadelta/apps_2/etc/models/uparrow_3.etc b/matita/matita/contribs/lambdadelta/apps_2/etc/models/uparrow_3.etc new file mode 100644 index 000000000..2a953eb67 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/etc/models/uparrow_3.etc @@ -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( ↑[ term 46 f ] break term 70 d )" + non associative with precedence 70 + for @{ 'UpArrow $M $f $d }. + +notation > "hvbox( ↑[ term 46 f ] break term 70 d )" + non associative with precedence 70 + for @{ 'UpArrow ? $f $d }. + +notation > "hvbox( ↑{ term 46 M }[ break term 46 f ] break term 70 d )" + non associative with precedence 70 + for @{ 'UpArrow $M $f $d }. diff --git a/matita/matita/contribs/lambdadelta/apps_2/etc/models/upspoon_3.etc b/matita/matita/contribs/lambdadelta/apps_2/etc/models/upspoon_3.etc new file mode 100644 index 000000000..a12cbbfb3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/etc/models/upspoon_3.etc @@ -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 d ] break term 46 lv )" + non associative with precedence 46 + for @{ 'UpSpoon $M $d $lv }. + +notation > "hvbox( ⫯[ break term 46 d ] break term 46 lv )" + non associative with precedence 46 + for @{ 'UpSpoon ? $d $lv }. + +notation > "hvbox( ⫯{ term 46 M }[ break term 46 d ] break term 46 lv )" + non associative with precedence 46 + for @{ 'UpSpoon $M $d $lv }. diff --git a/matita/matita/contribs/lambdadelta/apps_2/etc/models/valign.etc b/matita/matita/contribs/lambdadelta/apps_2/etc/models/valign.etc new file mode 100644 index 000000000..c8b4df01a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/etc/models/valign.etc @@ -0,0 +1,22 @@ +include "apps_2/notation/models/upspoon_3.ma". + + al: nat → dd → dd; (* alignment *) + +interpretation "alignment (model)" + 'UpSpoon M i d = (al M i d). + +(* Note: lift: compatibility *) + mf: compatible_3 … (al M) (eq …) (sq M) (sq M); +(* Note: lift: swap *) + mw: ∀l1,l2,d. l2 ≤ l1 → ⫯[l2]⫯[l1]d ≗{M} ⫯[↑l1]⫯[l2]d; +(* Note: lift: sort evaluation *) + mv: ∀l,s. ⫯[l](sv M s) ≗ sv M s; + +theorem valign_swap (M): is_model M → + ∀l1,l2. l2 ≤ l1 → + ∀lv:evaluation …. ⫯[l2]⫯[l1]lv ≗{M} ⫯[↑l1]⫯[l2]lv. +/2 width=1 by mw/ qed. + +lemma valign_comp (M): is_model M → + ∀l. compatible_2 … (valign M l) (veq M) (veq M). +/2 width=1 by mf/ qed-. diff --git a/matita/matita/contribs/lambdadelta/apps_2/etc/models/vdrop.etc b/matita/matita/contribs/lambdadelta/apps_2/etc/models/vdrop.etc index 5a857fbb1..e15ac254a 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/etc/models/vdrop.etc +++ b/matita/matita/contribs/lambdadelta/apps_2/etc/models/vdrop.etc @@ -1,138 +1,37 @@ - - -lemma vdrop_refl: ∀M,v,l. ↓[l, 0] v ≐⦋M⦌ v. -#M #v #l #i elim (lt_or_ge … i l) #Hil -[ >vdrop_lt // -| >vdrop_ge // -] -qed. - -(* Main properties **********************************************************) - -theorem vdrop_vdrop_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 - >vdrop_lt // >vdrop_lt /2 width=3 by lt_to_le_to_lt/ - >vdrop_lt // >vdrop_lt // -| >vdrop_ge // elim (lt_or_ge … j l2) #Hjl2 -Hl12 - [ >vdrop_lt /2 width=1 by lt_minus_to_plus/ - >vdrop_lt // >vdrop_ge // - | >vdrop_ge /2 width=1 by monotonic_le_plus_l/ - >vdrop_ge // >vdrop_ge /2 width=1 by le_plus/ - ] -] -qed. - -lemma vdrop_vdrop_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 vdrop_vdrop_le_sym, veq_sym/ qed-. - -(* Properties on raise ******************************************************) - -lemma vdrop_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 - >vdrop_lt /2 width=1 by le_S/ >raise_lt // >raise_lt // >vdrop_lt // -| >vdrop_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 >vdrop_lt // >vdrop_lt /2 width=2 by lt_plus_to_minus/ >raise_gt // - | >vdrop_ge // >vdrop_ge /2 width=1 by le_plus_to_minus_r/ - >raise_gt /2 width=1 by le_plus/ >plus_minus // - ] -] -qed. - -lemma raise_vdrop_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 vdrop_raise_lt, veq_sym/ qed. - -lemma vdrop_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 - >vdrop_lt // >vdrop_lt // >raise_lt // -| lapply (transitive_le … (j+m) Hilm ?) -Hli -Hilm /2 width=1 by monotonic_le_plus_l/ #Hijm - >vdrop_ge // >vdrop_ge // >raise_gt /2 width=1 by le_S_S/ -] -qed. - -lemma vdrop_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 vdrop_raise_be, veq_sym/ qed. - -lemma vdrop_raise: ∀M,v,d,l. ↓[l, 1] [l⬐d] v ≐⦋M⦌ v. -/3 width=3 by vdrop_raise_be, veq_trans/ qed. - -lemma vdrop_raise_sym: ∀M,v,d,l. v ≐⦋M⦌ ↓[l, 1] [l⬐d] v. -/2 width=1 by veq_sym/ qed. - -lemma raise_vdrop: ∀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 // >vdrop_lt // -| >raise_eq // -| >raise_gt // >vdrop_ge /2 width=1 by monotonic_pred/ - vdrop_lt // >raise_lt // >vdrop_lt // -| >vdrop_ge // >raise_eq // -| lapply (ltn_to_ltO … Hlj) #Hj - >vdrop_ge /2 width=1 by lt_to_le/ >raise_gt // - >vdrop_ge /4 width=1 by plus_minus, monotonic_pred, eq_f/ -] -qed. - -lemma raise_vdrop_be_sym: ∀M,v,l,m. [l⬐v (l+m)] ↓[l, m+1] v ≐⦋M⦌ ↓[l, m] v. -/3 width=1 by raise_vdrop_be, veq_sym/ qed. - -(* Forward lemmas on raise **************************************************) - -lemma vdrop_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 - >vdrop_lt // >vdrop_lt // >raise_lt // -| lapply (Hv12 (j+1)) - >vdrop_ge /2 width=1 by le_S/ >vdrop_ge // >raise_gt /2 width=1 by le_S_S/ +(**************************************************************************) +(* ___ *) +(* ||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/functions.ma". +include "apps_2/notation/models/downspoon_3.ma". +include "apps_2/models/model.ma". + +(* EVALUATION DROP **********************************************************) + +definition vdrop (M): nat → evaluation M → evaluation M ≝ + λj,lv,i. tri … i j (lv i) (lv (↑i)) (lv (↑i)). + +interpretation "drop (model evaluation)" + 'DownSpoon M i lv = (vdrop M i lv). + +(* Basic properties *********************************************************) + +lemma vdrop_lt (M): ∀lv,j,i. i < j → (⫰{M}[j] lv) i = lv i. +/2 width=1 by tri_lt/ qed-. + +lemma vdrop_ge (M): ∀lv,j,i. j ≤ i → (⫰{M}[j] lv) i = lv (↑i). +#M #lv #j #i #Hji elim (le_to_or_lt_eq … Hji) -Hji #Hji destruct +[ /2 width=1 by tri_gt/ +| /2 width=1 by tri_eq/ ] qed-. - -lemma raise_fwd_vdrop_be_S: ∀M,v1,v2,d,l,m. [l⬐d] v2 ≐⦋M⦌ ↓[l, m] v1 → - v2 ≐ ↓[l, m+1] v1. -/3 width=2 by vdrop_fwd_raise_be_S, veq_sym/ qed-. - -lemma vdrop_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) ->vdrop_ge // >raise_eq // -qed-. - -lemma raise_fwd_vdrop_be_O: ∀M,v1,v2,d,l,m. [l⬐d] v2 ≐⦋M⦌ ↓[l, m] v1 → d = v1 (l+m). -/4 width=7 by vdrop_fwd_raise_be_O, veq_sym, sym_eq/ qed-. - -(* Inversion lemmas on raise ************************************************) - -lemma raise_inv_vdrop_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 >vdrop_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 vdrop_vdrop_le_sym, vdrop_veq, veq_trans/ -qed-. - -lemma vdrop_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_vdrop_lt, veq_sym/ qed-. - -lemma vdrop_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 vdrop_fwd_raise_be_O, vdrop_fwd_raise_be_S, conj/ qed-. - -lemma raise_inv_vdrop_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_vdrop_be_O, raise_fwd_vdrop_be_S, conj/ qed-. 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 new file mode 100644 index 000000000..5a857fbb1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/etc/models/vdrop_old.etc @@ -0,0 +1,138 @@ + + +lemma vdrop_refl: ∀M,v,l. ↓[l, 0] v ≐⦋M⦌ v. +#M #v #l #i elim (lt_or_ge … i l) #Hil +[ >vdrop_lt // +| >vdrop_ge // +] +qed. + +(* Main properties **********************************************************) + +theorem vdrop_vdrop_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 + >vdrop_lt // >vdrop_lt /2 width=3 by lt_to_le_to_lt/ + >vdrop_lt // >vdrop_lt // +| >vdrop_ge // elim (lt_or_ge … j l2) #Hjl2 -Hl12 + [ >vdrop_lt /2 width=1 by lt_minus_to_plus/ + >vdrop_lt // >vdrop_ge // + | >vdrop_ge /2 width=1 by monotonic_le_plus_l/ + >vdrop_ge // >vdrop_ge /2 width=1 by le_plus/ + ] +] +qed. + +lemma vdrop_vdrop_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 vdrop_vdrop_le_sym, veq_sym/ qed-. + +(* Properties on raise ******************************************************) + +lemma vdrop_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 + >vdrop_lt /2 width=1 by le_S/ >raise_lt // >raise_lt // >vdrop_lt // +| >vdrop_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 >vdrop_lt // >vdrop_lt /2 width=2 by lt_plus_to_minus/ >raise_gt // + | >vdrop_ge // >vdrop_ge /2 width=1 by le_plus_to_minus_r/ + >raise_gt /2 width=1 by le_plus/ >plus_minus // + ] +] +qed. + +lemma raise_vdrop_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 vdrop_raise_lt, veq_sym/ qed. + +lemma vdrop_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 + >vdrop_lt // >vdrop_lt // >raise_lt // +| lapply (transitive_le … (j+m) Hilm ?) -Hli -Hilm /2 width=1 by monotonic_le_plus_l/ #Hijm + >vdrop_ge // >vdrop_ge // >raise_gt /2 width=1 by le_S_S/ +] +qed. + +lemma vdrop_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 vdrop_raise_be, veq_sym/ qed. + +lemma vdrop_raise: ∀M,v,d,l. ↓[l, 1] [l⬐d] v ≐⦋M⦌ v. +/3 width=3 by vdrop_raise_be, veq_trans/ qed. + +lemma vdrop_raise_sym: ∀M,v,d,l. v ≐⦋M⦌ ↓[l, 1] [l⬐d] v. +/2 width=1 by veq_sym/ qed. + +lemma raise_vdrop: ∀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 // >vdrop_lt // +| >raise_eq // +| >raise_gt // >vdrop_ge /2 width=1 by monotonic_pred/ + vdrop_lt // >raise_lt // >vdrop_lt // +| >vdrop_ge // >raise_eq // +| lapply (ltn_to_ltO … Hlj) #Hj + >vdrop_ge /2 width=1 by lt_to_le/ >raise_gt // + >vdrop_ge /4 width=1 by plus_minus, monotonic_pred, eq_f/ +] +qed. + +lemma raise_vdrop_be_sym: ∀M,v,l,m. [l⬐v (l+m)] ↓[l, m+1] v ≐⦋M⦌ ↓[l, m] v. +/3 width=1 by raise_vdrop_be, veq_sym/ qed. + +(* Forward lemmas on raise **************************************************) + +lemma vdrop_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 + >vdrop_lt // >vdrop_lt // >raise_lt // +| lapply (Hv12 (j+1)) + >vdrop_ge /2 width=1 by le_S/ >vdrop_ge // >raise_gt /2 width=1 by le_S_S/ +] +qed-. + +lemma raise_fwd_vdrop_be_S: ∀M,v1,v2,d,l,m. [l⬐d] v2 ≐⦋M⦌ ↓[l, m] v1 → + v2 ≐ ↓[l, m+1] v1. +/3 width=2 by vdrop_fwd_raise_be_S, veq_sym/ qed-. + +lemma vdrop_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) +>vdrop_ge // >raise_eq // +qed-. + +lemma raise_fwd_vdrop_be_O: ∀M,v1,v2,d,l,m. [l⬐d] v2 ≐⦋M⦌ ↓[l, m] v1 → d = v1 (l+m). +/4 width=7 by vdrop_fwd_raise_be_O, veq_sym, sym_eq/ qed-. + +(* Inversion lemmas on raise ************************************************) + +lemma raise_inv_vdrop_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 >vdrop_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 vdrop_vdrop_le_sym, vdrop_veq, veq_trans/ +qed-. + +lemma vdrop_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_vdrop_lt, veq_sym/ qed-. + +lemma vdrop_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 vdrop_fwd_raise_be_O, vdrop_fwd_raise_be_S, conj/ qed-. + +lemma raise_inv_vdrop_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_vdrop_be_O, raise_fwd_vdrop_be_S, conj/ qed-. diff --git a/matita/matita/contribs/lambdadelta/apps_2/etc/models/vdrop_vlift.etc b/matita/matita/contribs/lambdadelta/apps_2/etc/models/vdrop_vlift.etc new file mode 100644 index 000000000..0316fa161 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/etc/models/vdrop_vlift.etc @@ -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 "apps_2/models/model_vlift.ma". +include "apps_2/models/vdrop.ma". + +(* EVALUATION DROP **********************************************************) + +(* Advanced properties with evaluation evaluation lift **********************) + +lemma vlift_vdrop_eq (M): ∀lv,i. lv ≐{?,dd M} ⫯[i←lv i]⫰[i]lv. +#M #lv #i #j elim (lt_or_eq_or_gt j i) #Hji destruct +[ >vlift_lt // >vdrop_lt // +| >vlift_eq // +| >vlift_gt // >vdrop_ge /2 width=1 by monotonic_pred/ + <(lt_succ_pred … Hji) // +] +qed. diff --git a/matita/matita/contribs/lambdadelta/apps_2/etc/models/veq_li.etc b/matita/matita/contribs/lambdadelta/apps_2/etc/models/veq_li.etc new file mode 100644 index 000000000..f696a44d3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/etc/models/veq_li.etc @@ -0,0 +1,38 @@ +(**************************************************************************) +(* ___ *) +(* ||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_vdrop.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_vlift_sn … H) -H #lv2 #d2 #Hlv12 #Hd12 #Hy + /5 width=5 by li_repl, li_abbr, ti_comp_l, mq/ +| #lv1 #d1 #K #W #_ #IH #y #H + elim (veq_inv_vlift_sn … H) -H #lv2 #d2 #Hlv12 #_ #Hy + /4 width=3 by li_repl, li_abst/ +| #lv1 #d1 #I #K #_ #IH #y #H + elim (veq_inv_vlift_sn … H) -H #lv2 #d2 #Hlv12 #_ #Hy + /4 width=3 by li_repl, li_unit/ +| #lv1 #lv #L #_ #Hlv1 #IH #lv2 #Hlv2 + @IH /2 width=3 by exteq_veq_trans/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/apps_2/etc/models/veq_vdrop.etc b/matita/matita/contribs/lambdadelta/apps_2/etc/models/veq_vdrop.etc new file mode 100644 index 000000000..78b97950c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/etc/models/veq_vdrop.etc @@ -0,0 +1,42 @@ +(**************************************************************************) +(* ___ *) +(* ||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/vdrop_vlift.ma". +include "apps_2/models/veq.ma". + +(* EVALUATION EQUIVALENCE ***************************************************) + +(* Properties with evaluation drop ******************************************) + +lemma vdrop_comp (M): ∀i. compatible_2 … (vdrop M i) (veq M) (veq M). +#M #i #lv1 #lv2 #Hlv12 #j elim (lt_or_ge j i) #Hji +[ >vdrop_lt // >vdrop_lt // +| >vdrop_ge // >vdrop_ge // +] +qed. + +(* Advanced inversion lemmas with evaluation evaluation lift ****************) + +lemma veq_inv_vlift_sn (M): ∀lv1,y2,d1,i. ⫯[i←d1]lv1 ≗{M} y2 → + ∃∃lv2,d2. lv1 ≗ lv2 & d1 ≗ d2 & ⫯[i←d2]lv2 ≐ y2. +#M #lv1 #y2 #d1 #i #H +@(ex3_2_intro) +[5: @exteq_sym @vlift_vdrop_eq |1,2: skip +| #j elim (lt_or_ge j i) #Hji + [ lapply (H j) -H >vlift_lt // >vdrop_lt // + | lapply (H (↑j)) -H >vlift_gt /2 width=1 by monotonic_le_plus_l/ >vdrop_ge // + ] +| lapply (H i) >vlift_eq // +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/deq.ma b/matita/matita/contribs/lambdadelta/apps_2/models/deq.ma index 8de93a606..5d0f2d324 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/deq.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/deq.ma @@ -13,9 +13,8 @@ (**************************************************************************) include "apps_2/notation/models/ringeq_5.ma". -include "apps_2/models/model_gi.ma". -include "apps_2/models/model_li.ma". -include "apps_2/models/model_props.ma". +include "apps_2/models/li.ma". +include "static_2/syntax/genv.ma". (* DENOTATIONAL EQUIVALENCE ************************************************) @@ -29,7 +28,7 @@ interpretation "denotational equivalence (model)" lemma deq_refl (M): is_model M → ∀G,L. reflexive … (deq M G L). -/2 width=1 by mq/ qed. +/2 width=1 by mr/ qed. (* lemma veq_sym: ∀M. symmetric … (veq M). // qed-. 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 74124719e..6acf720cb 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/deq_cpr.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/deq_cpr.ma @@ -25,50 +25,55 @@ lemma cpr_fwd_deq (h) (M): is_model M → is_extensional M → #h #M #H1M #H2M #G #L #T1 #T2 #H @(cpr_ind … H) -G -L -T1 -T2 [ /2 width=2 by deq_refl/ | #G #K #V1 #V2 #W2 #_ #IH #HVW2 #gv #v #H - elim (li_inv_abbr … H) -H #lv #d #HK #Hd #H - @(mr … H1M) [4,5: @(ti_ext_l … H1M … H) |1,2: skip ] -v - lapply (lifts_SO_fwd_vlift … gv H1M H2M … HVW2 lv d) -HVW2 #HVW2 - @(seq_trans … H1M … HVW2) -W2 - @(seq_trans … H1M) [3: @IH // | skip ] -G -K -V2 - @(seq_canc_dx … H1M … Hd) -V1 /2 width=1 by ti_lref_vlift_eq/ + elim (li_inv_abbr … H) -H // #lv #HK #H + @(mq … H1M) [4,5: @(ti_comp … H) /2 width=2 by veq_refl/ |1,2: skip ] -v + @(mq … H1M) + [4: /3 width=1 by seq_sym, ml/ | skip + |5: /2 width=2 by lifts_SO_fwd_vlift/ | skip ] -W2 + >vlift_eq /2 width=1 by/ | #I #G #K #T #U #i #_ #IH #HTU #gv #v #H - elim (li_fwd_bind … H) -H #lv #d #HK #H - @(mr … H1M) [4,5: @(ti_ext_l … H1M … H) |1,2: skip ] -v - lapply (lifts_SO_fwd_vlift … gv H1M H2M … HTU lv d) -HTU #HTU - @(seq_trans … H1M … HTU) -U - @(seq_trans … H1M) [3: @IH // | skip ] -G -K -T - /2 width=1 by ti_lref_vlift_gt/ + elim (li_fwd_bind … H) // -H #lv #d #HK #H + @(mq … H1M) [4,5: @(ti_comp … H) /2 width=2 by veq_refl/ |1,2: skip ] -v + @(mq … H1M) + [4: /3 width=1 by seq_sym, ml/ | skip + |5: /2 width=2 by lifts_SO_fwd_vlift/ | skip ] -U + >vlift_gt /3 width=5 by ml, mq, mr/ | #p * #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #gv #lv #Hlv - [ @(mr … H1M) [4,5: @(seq_sym … H1M) @(md … H1M) |1,2: skip ] -p - @(seq_trans … H1M) [3: @IHT /3 width=1 by li_abbr/ | skip ] -T2 - /4 width=1 by ti_comp_l, veq_refl, vlift_comp/ - | @(mx … H2M) /3 width=1 by li_abst/ + [ @(mq … H1M) [4,5: /3 width=2 by seq_sym, md/ |1,2: skip ] -p + @(seq_trans … H1M) [2: @IHT /2 width=1 by li_abbr/ | skip ] -T1 + /4 width=1 by ti_comp, vlift_comp, (* 2x *) veq_refl/ + | /4 width=1 by li_abst, mx/ ] | * #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #gv #lv #Hlv - [ @(mr … H1M) [4,5: @(seq_sym … H1M) @(ma … H1M) |1,2: skip ] - /3 width=1 by mc/ - | @(mr … H1M) [4,5: @(seq_sym … H1M) @(me … H1M) |1,2: skip ] + [ @(mq … H1M) [4,5: /3 width=2 by seq_sym, ma/ |1,2: skip ] + /3 width=1 by mp/ + | @(mq … H1M) [4,5: /3 width=2 by seq_sym, me/ |1,2: skip ] /2 width=1 by/ ] | #G #L #V #U1 #U2 #T2 #_ #IH #HTU2 #gv #lv #Hlv - @(seq_trans … H1M) [2: @(md … H1M) | skip ] - @(seq_trans … H1M) [2: @IH /3 width=1 by li_abbr, veq_refl/ | skip ] -G -L -U1 + @(mq … H1M) + [4: /3 width=2 by seq_sym, md/ | skip + |3: /3 width=1 by li_abbr/ | skip ] -L -U1 /3 width=1 by lifts_SO_fwd_vlift, 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 - @(mr … H1M) [4,5: @(seq_sym … H1M) [ @(ma … H1M) | @(md … H1M) ] |1,2: skip ] - @(seq_trans … H1M) [3: @IHT /2 width=1 by li_abst/ | skip ] -T2 - @(mr … H1M) [4,5: @(seq_sym … H1M) [ @(mb … H1M) | @(ti_comp_l … H1M) ] |1,2: skip ] - [2: @vlift_comp [2: @(me … H1M) |4: @(veq_refl … H1M) |1,3: skip ] | skip ] - /4 width=1 by ti_comp_l, veq_refl, vlift_comp/ + @(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 + @ti_comp /2 width=1 by veq_refl/ + @vlift_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/ | #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV #IHW #IHT #HV2 #gv #lv #Hlv - @(mr … H1M) [4,5: @(seq_sym … H1M) [ @(ma … H1M) | @(md … H1M) ] |1,2: skip ] - @(mr … H1M) [4,5: @(seq_sym … H1M) [ @(mc … H1M) | @(ma … H1M) ] |1,2: skip ] - [2: @IHV // |4: @(md … H1M) |1,3: skip ] -p -V1 - @(mc … H1M) [ /2 width=1 by lifts_SO_fwd_vlift/ ] -V -V2 - @(seq_trans … H1M) [2: @IHT /3 width=1 by li_abbr, veq_refl/ | skip ] -T1 - /4 width=1 by ti_comp_l, veq_refl, vlift_comp/ + @(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_vlift/ ] -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 width=1 by ti_comp, vlift_comp, (* 2x *) veq_refl/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/li.ma b/matita/matita/contribs/lambdadelta/apps_2/models/li.ma new file mode 100644 index 000000000..f0f2c0f63 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/models/li.ma @@ -0,0 +1,124 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "static_2/syntax/lenv.ma". +include "apps_2/models/veq.ma". +include "apps_2/notation/models/inwbrackets_4.ma". + +(* LOCAL ENVIRONMENT INTERPRETATION ****************************************) + +inductive li (M) (gv): relation2 lenv (evaluation M) ≝ +| li_atom: ∀lv. li M gv (⋆) lv +| li_abbr: ∀lv,d,L,V. li M gv L lv → ⟦V⟧[gv, lv] = d → li M gv (L.ⓓV) (⫯[0←d]lv) +| li_abst: ∀lv,d,L,W. li M gv L lv → li M gv (L.ⓛW) (⫯[0←d]lv) +| li_unit: ∀lv,d,I,L. li M gv L lv → li M gv (L.ⓤ{I}) (⫯[0←d]lv) +| li_veq : ∀lv1,lv2,L. li M gv L lv1 → lv1 ≗ lv2 → li M gv L lv2 +. + +interpretation "local environment interpretation (model)" + 'InWBrackets M gv L lv = (li M gv L lv). + +(* Basic inversion lemmas ***************************************************) + +fact li_inv_abbr_aux (M) (gv): is_model M → + ∀v,Y. v ϵ ⟦Y⟧{M}[gv] → ∀L,V. Y = L.ⓓV → + ∃∃lv. lv ϵ ⟦L⟧[gv] & ⫯[0←⟦V⟧[gv,lv]]lv ≗ v. +#M #gv #HM #v #Y #H elim H -v -Y +[ #lv #K #W #H destruct +| #lv #d #L #V #HL #HV #_ #K #W #H destruct + /3 width=3 by veq_refl, ex2_intro/ +| #lv #d #L #V #_ #_ #K #W #H destruct +| #lv #d #I #L #_ #_ #K #W #H destruct +| #lv1 #lv2 #L #_ #Hlv12 #IH #K #W #H destruct + elim IH -IH [|*: // ] #lv #HK #HW + /3 width=5 by veq_trans, ex2_intro/ +] +qed-. + +lemma li_inv_abbr (M) (gv): is_model M → + ∀v,L,V. v ϵ ⟦L.ⓓV⟧{M}[gv] → + ∃∃lv. lv ϵ ⟦L⟧[gv] & ⫯[0←⟦V⟧[gv,lv]]lv ≗ v. +/2 width=3 by li_inv_abbr_aux/ qed-. + +fact li_inv_abst_aux (M) (gv): is_model M → + ∀v,Y. v ϵ ⟦Y⟧{M}[gv] → ∀L,W. Y = L.ⓛW → + ∃∃lv,d. lv ϵ ⟦L⟧[gv] & ⫯[0←d]lv ≗ v. +#M #gv #HM #v #Y #H elim H -v -Y +[ #lv #K #U #H destruct +| #lv #d #L #V #_ #_ #_ #K #U #H destruct +| #lv #d #L #V #HL #_ #K #U #H destruct + /3 width=4 by veq_refl, ex2_2_intro/ +| #lv #d #I #L #_ #_ #K #U #H destruct +| #lv1 #lv2 #L #_ #Hlv12 #IH #K #U #H destruct + elim IH -IH [|*: // ] #lv #d #HK #Hlv + /3 width=6 by veq_trans, ex2_2_intro/ +] +qed-. + +lemma li_inv_abst (M) (gv): is_model M → + ∀v,L,W. v ϵ ⟦L.ⓛW⟧{M}[gv] → + ∃∃lv,d. lv ϵ ⟦L⟧[gv] & ⫯[0←d]lv ≗ v. +/2 width=4 by li_inv_abst_aux/ qed-. + +fact li_inv_unit_aux (M) (gv): is_model M → + ∀v,Y. v ϵ ⟦Y⟧{M}[gv] → ∀I,L. Y = L.ⓤ{I} → + ∃∃lv,d. lv ϵ ⟦L⟧[gv] & ⫯[0←d]lv ≗ v. +#M #gv #HM #v #Y #H elim H -v -Y +[ #lv #J #K #H destruct +| #lv #d #L #V #_ #_ #_ #J #K #H destruct +| #lv #d #L #V #_ #_ #J #K #H destruct +| #lv #d #I #L #HL #_ #J #K #H destruct + /3 width=4 by veq_refl, ex2_2_intro/ +| #lv1 #lv2 #L #_ #Hlv12 #IH #J #K #H destruct + elim IH -IH [|*: // ] #lv #d #HK #Hlv + /3 width=6 by veq_trans, ex2_2_intro/ +] +qed-. + +lemma li_inv_unit (M) (gv): is_model M → + ∀v,I,L. v ϵ ⟦L.ⓤ{I}⟧{M}[gv] → + ∃∃lv,d. lv ϵ ⟦L⟧[gv] & ⫯[0←d]lv ≗ v. +/2 width=4 by li_inv_unit_aux/ qed-. + +(* Advanced forward lemmas **************************************************) + +lemma li_fwd_bind (M) (gv): is_model M → + ∀v,I,L. v ϵ ⟦L.ⓘ{I}⟧{M}[gv] → + ∃∃lv,d. lv ϵ ⟦L⟧[gv] & ⫯[0←d]lv ≗ v. +#M #gv #HM #v * [ #I | * #V ] #L #H +[ /2 width=2 by li_inv_unit/ +| elim (li_inv_abbr … H) // -H #lv #HL #Hv + /2 width=4 by ex2_2_intro/ +| /2 width=2 by li_inv_abst/ +] +qed-. + +(* Basic_properties *********************************************************) + +lemma li_repl (M) (L): is_model M -> + replace_2 … (λgv.li M gv L) (veq …) (veq …). +#M #L #HM #gv1 #lv1 #H elim H -L -lv1 +[ #lv1 #gv2 #Hgv #lv2 #Hlv /2 width=1 by li_atom/ +| #lv1 #d #K #V #_ #Hd #IH #gv2 #Hgv #lv2 #Hlv destruct + @li_veq [2: /4 width=4 by li_abbr, veq_refl/ | skip ] -IH + @(veq_canc_sn … Hlv) -Hlv // + /4 width=1 by ti_comp, vlift_comp, (* 2x *) veq_refl/ +| #lv1 #d #K #W #_ #IH #gv2 #Hgv #lv2 #Hlv + @li_veq /4 width=3 by li_abst, veq_refl/ +| #lv1 #d #I #K #_ #IH #gv2 #Hgv #lv2 #Hlv + @li_veq /4 width=3 by li_unit, veq_refl/ +| #lv1 #lv #L #_ #Hlv1 #IH #gv2 #Hgv #lv2 #Hlv + /3 width=3 by veq_trans/ +] +qed. diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/model.ma b/matita/matita/contribs/lambdadelta/apps_2/models/model.ma index 86c624e1b..290c3e4c6 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/model.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/model.ma @@ -20,11 +20,16 @@ include "static_2/syntax/term.ma". (* MODEL ********************************************************************) record model: Type[1] ≝ { - dd: Type[0]; (* denotations domain *) - sq: relation2 dd dd; (* structural equivalence *) - sv: nat → dd; (* sort evaluation *) - ap: dd → dd → dd; (* application *) - ti: (nat → dd) → (nat → dd) → term → dd (* term interperpretation *) +(* Note: denotations domain *) + dd: Type[0]; +(* Note: structural equivalence *) + sq: relation2 dd dd; +(* Note: sort evaluation *) + sv: nat → dd; +(* Note: application *) + ap: dd → dd → dd; +(* Note: term interperpretation *) + ti: (nat → dd) → (nat → dd) → term → dd }. interpretation "structural equivalence (model)" diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/model_gi.ma b/matita/matita/contribs/lambdadelta/apps_2/models/model_gi.ma deleted file mode 100644 index 1c354a621..000000000 --- a/matita/matita/contribs/lambdadelta/apps_2/models/model_gi.ma +++ /dev/null @@ -1,17 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 "static_2/syntax/genv.ma". - -(* GLOBAL ENVIRONMENT INTERPRETATION ***************************************) diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/model_li.ma b/matita/matita/contribs/lambdadelta/apps_2/models/model_li.ma deleted file mode 100644 index 6be3c60c6..000000000 --- a/matita/matita/contribs/lambdadelta/apps_2/models/model_li.ma +++ /dev/null @@ -1,95 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 "static_2/syntax/lenv.ma". -include "apps_2/models/model_vlift.ma". -include "apps_2/notation/models/inwbrackets_4.ma". - -(* LOCAL ENVIRONMENT INTERPRETATION ****************************************) - -inductive li (M) (gv): relation2 lenv (evaluation M) ≝ -| li_atom: ∀lv. li M gv (⋆) lv -| li_abbr: ∀lv,d,L,V. li M gv L lv → ⟦V⟧[gv, lv] ≗ d → li M gv (L.ⓓV) (⫯[d]lv) -| li_abst: ∀lv,d,L,W. li M gv L lv → li M gv (L.ⓛW) (⫯[d]lv) -| li_unit: ∀lv,d,I,L. li M gv L lv → li M gv (L.ⓤ{I}) (⫯[d]lv) -| li_repl: ∀lv1,lv2,L. li M gv L lv1 → lv1 ≐ lv2 → li M gv L lv2 -. - -interpretation "local environment interpretation (model)" - 'InWBrackets M gv L lv = (li M gv L lv). - -(* Basic inversion lemmas ***************************************************) - -fact li_inv_abbr_aux (M) (gv): ∀v,Y. v ϵ ⟦Y⟧{M}[gv] → ∀L,V. Y = L.ⓓV → - ∃∃lv,d. lv ϵ ⟦L⟧{M}[gv] & ⟦V⟧{M}[gv, lv] ≗ d & ⫯{M}[d]lv ≐ v. -#M #gv #v #Y #H elim H -v -Y -[ #lv #K #W #H destruct -| #lv #d #L #V #HL #HV #_ #K #W #H destruct /2 width=5 by ex3_2_intro/ -| #lv #d #L #V #_ #_ #K #W #H destruct -| #lv #d #I #L #_ #_ #K #W #H destruct -| #lv1 #lv2 #L #_ #Hlv12 #IH #K #W #H destruct - elim IH -IH [|*: // ] #lv #d #HK #HW #Hlv - /3 width=5 by exteq_trans, ex3_2_intro/ -] -qed-. - -lemma li_inv_abbr (M) (gv): ∀v,L,V. v ϵ ⟦L.ⓓV⟧{M}[gv] → - ∃∃lv,d. lv ϵ ⟦L⟧{M}[gv] & ⟦V⟧{M}[gv, lv] ≗ d & ⫯{M}[d]lv ≐ v. -/2 width=3 by li_inv_abbr_aux/ qed-. - -fact li_inv_abst_aux (M) (gv): ∀v,Y. v ϵ ⟦Y⟧{M}[gv] → ∀L,W. Y = L.ⓛW → - ∃∃lv,d. lv ϵ ⟦L⟧{M}[gv] & ⫯{M}[d]lv ≐ v. -#M #gv #v #Y #H elim H -v -Y -[ #lv #K #U #H destruct -| #lv #d #L #V #_ #_ #_ #K #U #H destruct -| #lv #d #L #V #HL #_ #K #U #H destruct /2 width=4 by ex2_2_intro/ -| #lv #d #I #L #_ #_ #K #U #H destruct -| #lv1 #lv2 #L #_ #Hlv12 #IH #K #U #H destruct - elim IH -IH [|*: // ] #lv #d #HK #Hlv - /3 width=4 by exteq_trans, ex2_2_intro/ -] -qed-. - -lemma li_inv_abst (M) (gv): ∀v,L,W. v ϵ ⟦L.ⓛW⟧{M}[gv] → - ∃∃lv,d. lv ϵ ⟦L⟧{M}[gv] & ⫯{M}[d]lv ≐ v. -/2 width=4 by li_inv_abst_aux/ qed-. - -fact li_inv_unit_aux (M) (gv): ∀v,Y. v ϵ ⟦Y⟧{M}[gv] → ∀I,L. Y = L.ⓤ{I} → - ∃∃lv,d. lv ϵ ⟦L⟧{M}[gv] & ⫯{M}[d]lv ≐ v. -#M #gv #v #Y #H elim H -v -Y -[ #lv #J #K #H destruct -| #lv #d #L #V #_ #_ #_ #J #K #H destruct -| #lv #d #L #V #_ #_ #J #K #H destruct -| #lv #d #I #L #HL #_ #J #K #H destruct /2 width=4 by ex2_2_intro/ -| #lv1 #lv2 #L #_ #Hlv12 #IH #J #K #H destruct - elim IH -IH [|*: // ] #lv #d #HK #Hlv - /3 width=4 by exteq_trans, ex2_2_intro/ -] -qed-. - -lemma li_inv_unit (M) (gv): ∀v,I,L. v ϵ ⟦L.ⓤ{I}⟧{M}[gv] → - ∃∃lv,d. lv ϵ ⟦L⟧{M}[gv] & ⫯{M}[d]lv ≐ v. -/2 width=4 by li_inv_unit_aux/ qed-. - -(* Advanced forward lemmas **************************************************) - -lemma li_fwd_bind (M) (gv): ∀v,I,L. v ϵ ⟦L.ⓘ{I}⟧{M}[gv] → - ∃∃lv,d. lv ϵ ⟦L⟧{M}[gv] & ⫯{M}[d]lv ≐ v. -#m #gv #v * [ #I | * #V ] #L #H -[ @(li_inv_unit … H) -| elim (li_inv_abbr … H) -H #lv #d #Hl #_ #Hv - /2 width=4 by ex2_2_intro/ -| @(li_inv_abst … H) -] -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 073d5db62..26a347832 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/model_props.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/model_props.ma @@ -17,34 +17,46 @@ include "apps_2/models/model_vlift.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); +(* Note: equivalence: reflexivity *) + mr: reflexive … (sq M); +(* Note: equivalence: compatibility *) + mq: replace_2 … (sq M) (sq M) (sq M); +(* Note: application: compatibility *) + mp: compatible_3 … (ap M) (sq M) (sq M) (sq M); +(* Note: interpretation: sort *) ms: ∀gv,lv,s. ⟦⋆s⟧{M}[gv, lv] ≗ sv M s; +(* Note: interpretation: local reference *) ml: ∀gv,lv,i. ⟦#i⟧{M}[gv, lv] ≗ lv i; +(* Note: interpretation: global reference *) mg: ∀gv,lv,l. ⟦§l⟧{M}[gv, lv] ≗ gv l; - md: ∀gv,lv,p,V,T. ⟦ⓓ{p}V.T⟧{M}[gv, lv] ≗ ⟦T⟧[gv, ⫯[⟦V⟧[gv, lv]]lv]; - mi: ∀gv,lv1,lv2,p,W,T. ⟦W⟧{M}[gv, lv1] ≗ ⟦W⟧{M}[gv, lv2] → - (∀d. ⟦T⟧{M}[gv, ⫯[d]lv1] ≗ ⟦T⟧{M}[gv, ⫯[d]lv2]) → - ⟦ⓛ{p}W.T⟧[gv, lv1] ≗ ⟦ⓛ{p}W.T⟧[gv, lv2]; +(* 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] → + (∀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: application *) ma: ∀gv,lv,V,T. ⟦ⓐV.T⟧{M}[gv, lv] ≗ ⟦V⟧[gv, lv] @ ⟦T⟧[gv, lv]; +(* Note: interpretation: ϵ-equivalence *) me: ∀gv,lv,W,T. ⟦ⓝW.T⟧{M}[gv, lv] ≗ ⟦T⟧[gv, lv]; - mb: ∀gv,lv,d,p,W,T. d @ ⟦ⓛ{p}W.T⟧{M}[gv, lv] ≗ ⟦T⟧[gv, ⫯[d]lv] +(* Note: interpretation: β-requivalence *) + mb: ∀gv,lv,d,p,W,T. d @ ⟦ⓛ{p}W.T⟧{M}[gv, lv] ≗ ⟦T⟧[gv, ⫯[0←d]lv] }. record is_extensional (M): Prop ≝ { - mx: ∀gv,lv1,lv2,p,W1,W2,T1,T2. ⟦W1⟧{M}[gv, lv1] ≗ ⟦W2⟧{M}[gv, lv2] → - (∀d. ⟦T1⟧{M}[gv, ⫯[d]lv1] ≗ ⟦T2⟧{M}[gv, ⫯[d]lv2]) → - ⟦ⓛ{p}W1.T1⟧[gv, lv1] ≗ ⟦ⓛ{p}W2.T2⟧[gv, lv2] +(* Note: interpretation: extensional abstraction *) + mx: ∀gv1,gv2,lv1,lv2,p,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] }. (* Basic properties *********************************************************) lemma seq_sym (M): is_model M → symmetric … (sq M). -/3 width=5 by mr, mq/ qed-. +/3 width=5 by mq, mr/ qed-. lemma seq_trans (M): is_model M → Transitive … (sq M). -/3 width=5 by mr, mq/ qed-. +/3 width=5 by mq, mr/ qed-. lemma seq_canc_sn (M): is_model M → left_cancellable … (sq M). /3 width=3 by seq_trans, seq_sym/ qed-. @@ -56,12 +68,22 @@ lemma ti_lref_vlift_eq (M): is_model M → ∀gv,lv,d,i. ⟦#i⟧[gv,⫯[i←d]lv] ≗{M} d. #M #HM #gv #lv #d #i @(seq_trans … HM) [2: @ml // | skip ] ->vlift_eq /2 width=1 by mq/ +>vlift_eq /2 width=1 by mr/ qed. lemma ti_lref_vlift_gt (M): is_model M → - ∀gv,lv,d,i. ⟦#(↑i)⟧[gv,⫯[d]lv] ≗{M} ⟦#i⟧[gv,lv]. + ∀gv,lv,d,i. ⟦#(↑i)⟧[gv,⫯[0←d]lv] ≗{M} ⟦#i⟧[gv,lv]. #M #HM #gv #lv #d #i -@(mr … HM) [4,5: @(seq_sym … HM) @(ml … HM) |1,2: skip ] ->vlift_gt /2 width=1 by mq/ +@(mq … HM) [4,5: @(seq_sym … HM) /2 width=2 by ml/ |1,2: skip ] +>vlift_gt /2 width=1 by mr/ 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/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/model_vlift.ma b/matita/matita/contribs/lambdadelta/apps_2/models/model_vlift.ma index 29bd2e67f..bb2d5c7c9 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/model_vlift.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/model_vlift.ma @@ -13,22 +13,16 @@ (**************************************************************************) include "ground_2/lib/functions.ma". -include "ground_2/lib/exteq.ma". include "apps_2/notation/models/upspoon_4.ma". -include "apps_2/notation/models/upspoon_3.ma". include "apps_2/models/model.ma". - (* MODEL ********************************************************************) definition vlift (M): nat → dd M → evaluation M → evaluation M ≝ λj,d,lv,i. tri … i j (lv i) d (lv (↓i)). -interpretation "generic lift (model evaluation)" - 'UpSpoon M i d lv = (vlift M i d lv). - interpretation "lift (model evaluation)" - 'UpSpoon M d lv = (vlift M O d lv). + 'UpSpoon M i d lv = (vlift M i d lv). (* Basic properties *********************************************************) @@ -40,12 +34,3 @@ lemma vlift_eq (M): ∀lv,d,i. (⫯{M}[i←d] lv) i = d. lemma vlift_gt (M): ∀lv,d,j,i. j < i → (⫯{M}[j←d] lv) i = lv (↓i). /2 width=1 by tri_gt/ qed-. - -lemma vlift_ext (M): ∀i. compatible_3 … (vlift M i) (eq …) (exteq …) (exteq …). -#m #i #d1 #d2 #Hd12 #lv1 #lv2 #HLv12 #j -elim (lt_or_eq_or_gt j i) #Hij destruct -[ >vlift_lt // >vlift_lt // -| >vlift_eq >vlift_eq // -| >vlift_gt // >vlift_gt // -] -qed. diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/vdrop.ma b/matita/matita/contribs/lambdadelta/apps_2/models/vdrop.ma deleted file mode 100644 index f0d72d4e2..000000000 --- a/matita/matita/contribs/lambdadelta/apps_2/models/vdrop.ma +++ /dev/null @@ -1,49 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/functions.ma". -include "ground_2/lib/exteq.ma". -include "ground_2/notation/functions/downspoon_2.ma". -include "apps_2/notation/models/downspoon_3.ma". -include "apps_2/models/model.ma". - -(* EVALUATION DROP **********************************************************) - -definition vdrop (M): nat → evaluation M → evaluation M ≝ - λj,lv,i. tri … i j (lv i) (lv (↑i)) (lv (↑i)). - -interpretation "generic drop (model evaluation)" - 'DownSpoon M i lv = (vdrop M i lv). - -interpretation "drop (model evaluation)" - 'DownSpoon M lv = (vdrop M O lv). - -(* Basic properties *********************************************************) - -lemma vdrop_lt (M): ∀lv,j,i. i < j → (⫰{M}[j] lv) i = lv i. -/2 width=1 by tri_lt/ qed-. - -lemma vdrop_ge (M): ∀lv,j,i. j ≤ i → (⫰{M}[j] lv) i = lv (↑i). -#M #lv #j #i #Hji elim (le_to_or_lt_eq … Hji) -Hji #Hji destruct -[ /2 width=1 by tri_gt/ -| /2 width=1 by tri_eq/ -] -qed-. - -lemma vdrop_ext (M): ∀i. compatible_2 … (vdrop M i) (exteq …) (exteq …). -#M #i #lv1 #lv2 #Hlv12 #j elim (lt_or_ge j i) #Hji -[ >vdrop_lt // >vdrop_lt // -| >vdrop_ge // >vdrop_ge // -] -qed. diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/vdrop_vlift.ma b/matita/matita/contribs/lambdadelta/apps_2/models/vdrop_vlift.ma deleted file mode 100644 index 0316fa161..000000000 --- a/matita/matita/contribs/lambdadelta/apps_2/models/vdrop_vlift.ma +++ /dev/null @@ -1,29 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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_vlift.ma". -include "apps_2/models/vdrop.ma". - -(* EVALUATION DROP **********************************************************) - -(* Advanced properties with evaluation evaluation lift **********************) - -lemma vlift_vdrop_eq (M): ∀lv,i. lv ≐{?,dd M} ⫯[i←lv i]⫰[i]lv. -#M #lv #i #j elim (lt_or_eq_or_gt j i) #Hji destruct -[ >vlift_lt // >vdrop_lt // -| >vlift_eq // -| >vlift_gt // >vdrop_ge /2 width=1 by monotonic_pred/ - <(lt_succ_pred … Hji) // -] -qed. diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma b/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma index e784d3b7a..7f6e8b789 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma @@ -14,7 +14,7 @@ include "apps_2/models/model_props.ma". -(* EVALUATION EQUIVALENCE **************************************************) +(* EVALUATION EQUIVALENCE ***************************************************) definition veq (M): relation (evaluation M) ≝ λv1,v2. ∀d. v1 d ≗ v2 d. @@ -26,11 +26,11 @@ interpretation "evaluation equivalence (model)" lemma veq_refl (M): is_model M → reflexive … (veq M). -/2 width=1 by mq/ qed. +/2 width=1 by mr/ qed. lemma veq_repl (M): is_model M → replace_2 … (veq M) (veq M) (veq M). -/2 width=5 by mr/ qed-. +/2 width=5 by mq/ qed-. lemma veq_sym (M): is_model M → symmetric … (veq M). /3 width=5 by veq_repl, veq_refl/ qed-. @@ -38,39 +38,39 @@ lemma veq_sym (M): is_model M → symmetric … (veq M). lemma veq_trans (M): is_model M → Transitive … (veq M). /3 width=5 by veq_repl, veq_refl/ qed-. -(* Properties with extebsional equivalence **********************************) +lemma veq_canc_sn (M): is_model M → left_cancellable … (veq M). +/3 width=3 by veq_trans, veq_sym/ qed-. -lemma ext_veq (M): is_model M → - ∀lv1,lv2. lv1 ≐ lv2 → lv1 ≗{M} lv2. -/2 width=1 by mq/ qed. +lemma veq_canc_dx (M): is_model M → right_cancellable … (veq M). +/3 width=3 by veq_trans, veq_sym/ qed-. -lemma veq_repl_exteq (M): is_model M → - replace_2 … (veq M) (exteq …) (exteq …). -/2 width=5 by mr/ qed-. +(* Properties with evaluation lift ******************************************) -lemma exteq_veq_trans (M): ∀lv1,lv. lv1 ≐ lv → - ∀lv2. lv ≗{M} lv2 → lv1 ≗ lv2. -// qed-. - -(* Properties with evaluation evaluation lift *******************************) - -theorem vlift_swap (M): ∀i1,i2. i1 ≤ i2 → - ∀lv,d1,d2. ⫯[i1←d1] ⫯[i2←d2] lv ≐{?,dd M} ⫯[↑i2←d2] ⫯[i1←d1] lv. -#M #i1 #i2 #Hi12 #lv #d1 #d2 #j +theorem vlift_swap (M): is_model M → + ∀i1,i2. i1 ≤ i2 → + ∀lv,d1,d2. ⫯[i1←d1] ⫯[i2←d2] lv ≗{M} ⫯[↑i2←d2] ⫯[i1←d1] lv. +#M #HM #i1 #i2 #Hi12 #lv #d1 #d2 #j elim (lt_or_eq_or_gt j i1) #Hji1 destruct -[ >vlift_lt // >vlift_lt /2 width=3 by lt_to_le_to_lt/ - >vlift_lt /3 width=3 by lt_S, lt_to_le_to_lt/ >vlift_lt // -| >vlift_eq >vlift_lt /2 width=1 by monotonic_le_plus_l/ >vlift_eq // +[ lapply (lt_to_le_to_lt … Hji1 Hi12) #Hji2 + >vlift_lt // >vlift_lt // >vlift_lt /2 width=1 by lt_S/ >vlift_lt // + /2 width=1 by veq_refl/ +| >vlift_eq >vlift_lt /2 width=1 by monotonic_le_plus_l/ >vlift_eq + /2 width=1 by mr/ | >vlift_gt // elim (lt_or_eq_or_gt (↓j) i2) #Hji2 destruct [ >vlift_lt // >vlift_lt /2 width=1 by lt_minus_to_plus/ >vlift_gt // - | >vlift_eq <(lt_succ_pred … Hji1) >vlift_eq // - | >vlift_gt // >vlift_gt /2 width=1 by lt_minus_to_plus_r/ >vlift_gt /2 width=3 by le_to_lt_to_lt/ + /2 width=1 by veq_refl/ + | >vlift_eq <(lt_succ_pred … Hji1) >vlift_eq + /2 width=1 by mr/ + | lapply (le_to_lt_to_lt … Hi12 Hji2) #Hi1j + >vlift_gt // >vlift_gt /2 width=1 by lt_minus_to_plus_r/ >vlift_gt // + /2 width=1 by veq_refl/ ] ] -qed-. +qed. -lemma vlift_comp (M): ∀i. compatible_3 … (vlift M i) (sq M) (veq M) (veq M). -#m #i #d1 #d2 #Hd12 #lv1 #lv2 #HLv12 #j +lemma vlift_comp (M): is_model M → + ∀i. compatible_3 … (vlift M i) (sq M) (veq M) (veq M). +#M #HM #i #d1 #d2 #Hd12 #lv1 #lv2 #HLv12 #j elim (lt_or_eq_or_gt j i) #Hij destruct [ >vlift_lt // >vlift_lt // | >vlift_eq >vlift_eq // @@ -80,21 +80,16 @@ qed-. (* Properies with term interpretation ***************************************) -lemma ti_comp_l (M): is_model M → - ∀T,gv,lv1,lv2. lv1 ≗{M} lv2 → - ⟦T⟧[gv, lv1] ≗ ⟦T⟧[gv, lv2]. +lemma ti_comp (M): is_model M → + ∀T,gv1,gv2. gv1 ≗ gv2 → ∀lv1,lv2. lv1 ≗ lv2 → + ⟦T⟧[gv1, lv1] ≗{M} ⟦T⟧[gv2, 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=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 vlift_comp, seq_sym, md, mr/ -| /5 width=1 by vlift_comp, mi, mq/ -| /4 width=5 by seq_sym, ma, mc, mr/ -| /4 width=5 by seq_sym, me, mr/ +| /5 width=5 by vlift_comp, seq_sym, md, mq/ +| /5 width=1 by vlift_comp, mi, mr/ +| /4 width=5 by seq_sym, ma, mp, mq/ +| /4 width=5 by seq_sym, me, mq/ ] qed. - -lemma ti_ext_l (M): is_model M → - ∀T,gv,lv1,lv2. lv1 ≐ lv2 → - ⟦T⟧[gv, lv1] ≗{M} ⟦T⟧[gv, lv2]. -/3 width=1 by ti_comp_l, ext_veq/ 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 deleted file mode 100644 index 8fa8d90d7..000000000 --- a/matita/matita/contribs/lambdadelta/apps_2/models/veq_li.ma +++ /dev/null @@ -1,38 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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_vdrop.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_vlift_sn … H) -H #lv2 #d2 #Hlv12 #Hd12 #Hy - /5 width=5 by li_repl, li_abbr, ti_comp_l, mr/ -| #lv1 #d1 #K #W #_ #IH #y #H - elim (veq_inv_vlift_sn … H) -H #lv2 #d2 #Hlv12 #_ #Hy - /4 width=3 by li_repl, li_abst/ -| #lv1 #d1 #I #K #_ #IH #y #H - elim (veq_inv_vlift_sn … H) -H #lv2 #d2 #Hlv12 #_ #Hy - /4 width=3 by li_repl, li_unit/ -| #lv1 #lv #L #_ #Hlv1 #IH #lv2 #Hlv2 - @IH /2 width=3 by exteq_veq_trans/ -] -qed-. 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 905b1a336..dc83b79b1 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/veq_lifts.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/veq_lifts.ma @@ -20,42 +20,51 @@ include "apps_2/models/veq.ma". (* Forward lemmas with generic relocation ***********************************) -fact lifts_fwd_vlift_aux (M) (gv): is_model M → is_extensional M → - ∀f,T1,T2. ⬆*[f] T1 ≘ T2 → ∀m. 𝐁❴m,1❵ = f → - ∀lv,d. ⟦T1⟧[gv, lv] ≗{M} ⟦T2⟧[gv, ⫯[m←d]lv]. -#M #gv #H1M #H2M #f #T1 #T2 #H elim H -f -T1 -T2 -[ /4 width=3 by seq_trans, seq_sym, ms/ -| #f #i1 #i2 #Hi12 #m #Hm #lv #d destruct - @(mr … H1M) [4,5: @(seq_sym … H1M) @(ml … H1M) |1,2: skip ] +fact lifts_fwd_vlift_aux (M): is_model M → is_extensional M → + ∀f,T1,T2. ⬆*[f] T1 ≘ T2 → ∀m. 𝐁❴m,1❵ = f → + ∀gv,lv,d. ⟦T1⟧[gv, lv] ≗{M} ⟦T2⟧[gv, ⫯[m←d]lv]. +#M #H1M #H2M #f #T1 #T2 #H elim H -f -T1 -T2 +[ #f #s #m #Hf #gv #lv #d + @(mq … H1M) [4,5: /3 width=2 by seq_sym, ms/ |1,2: skip ] + /2 width=1 by mr/ +| #f #i1 #i2 #Hi12 #m #Hm #gv #lv #d destruct + @(mq … H1M) [4,5: /3 width=2 by seq_sym, ml/ |1,2: skip ] elim (lt_or_ge i1 m) #Hi1 [ lapply (at_basic_inv_lt … Hi12) -Hi12 // #H destruct - >vlift_lt /2 width=1 by mq/ + >vlift_lt /2 width=1 by mr/ | lapply (at_basic_inv_ge … Hi12) -Hi12 // #H destruct - >vlift_gt /2 width=1 by mq, le_S_S/ + >vlift_gt /2 width=1 by mr, le_S_S/ ] -| /4 width=3 by seq_trans, seq_sym, mg/ -| #f #p * #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #m #Hm #lv #d destruct - [ @(mr … H1M) [4,5: @(seq_sym … H1M) @(md … H1M) |1,2: skip ] +| #f #l #m #Hf #gv #lv #d + @(mq … H1M) [4,5: /3 width=2 by seq_sym, mg/ |1,2: skip ] + /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 ] @(seq_trans … H1M) - [2: @(ti_comp_l … H1M) | skip ] - [2: @(vlift_comp … lv lv) | skip ] - [3: /2 width=1 by veq_refl/ ] - [2: @(IHV … d) // | skip ] - @(seq_trans … H1M) [2: @(IHT (↑m) … d) // | skip ] - /4 width=1 by seq_sym, ti_ext_l, vlift_swap/ - | @mx /2 width=1 by/ #d0 @(seq_trans … H1M) - [3: @(seq_sym … H1M) @(ti_ext_l … H1M) | skip ] - [2: @vlift_swap // | skip ] + [3: @ti_comp // | skip ] + [1,2: /2 width=2 by veq_refl/ ] + [2: @(vlift_comp … H1M) | skip ] + [1,2: /2 width=2 by/ |3,4: /2 width=2 by veq_refl/ ] -IHV + @(seq_trans … H1M) + [3: @ti_comp // | skip ] + [1,2: /2 width=2 by veq_refl/ ] + [2: @veq_sym // @vlift_swap // | skip ] + /2 width=1 by/ + | @mx // [ /2 width=1 by/ ] -IHV #d0 + @(seq_trans … H1M) + [3: @ti_comp // | skip ] + [1,2: /2 width=2 by veq_refl/ ] + [2: @veq_sym // @vlift_swap // | skip ] /2 width=1 by/ ] -| #f * #V1 #v2 #T1 #T2 #_ #_ #IHV #IHT #m #Hm #lv #d - [ /4 width=5 by seq_sym, ma, mc, mr/ - | /4 width=5 by seq_sym, me, mr/ +| #f * #V1 #v2 #T1 #T2 #_ #_ #IHV #IHT #m #Hm #gv #lv #d + [ /4 width=5 by seq_sym, ma, mp, mq/ + | /4 width=5 by seq_sym, me, mq/ ] ] qed-. lemma lifts_SO_fwd_vlift (M) (gv): is_model M → is_extensional M → ∀T1,T2. ⬆*[1] T1 ≘ T2 → - ∀lv,d. ⟦T1⟧[gv, lv] ≗{M} ⟦T2⟧[gv, ⫯[d]lv]. + ∀lv,d. ⟦T1⟧[gv, lv] ≗{M} ⟦T2⟧[gv, ⫯[0←d]lv]. /2 width=3 by lifts_fwd_vlift_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/veq_vdrop.ma b/matita/matita/contribs/lambdadelta/apps_2/models/veq_vdrop.ma deleted file mode 100644 index ae3175310..000000000 --- a/matita/matita/contribs/lambdadelta/apps_2/models/veq_vdrop.ma +++ /dev/null @@ -1,42 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/vdrop_vlift.ma". -include "apps_2/models/veq.ma". - -(* EVALUATION EQUIVALENCE **************************************************) - -(* Properties with evaluation drop ******************************************) - -lemma vdrop_comp (M): ∀i. compatible_2 … (vdrop M i) (veq M) (veq M). -#M #i #lv1 #lv2 #Hlv12 #j elim (lt_or_ge j i) #Hji -[ >vdrop_lt // >vdrop_lt // -| >vdrop_ge // >vdrop_ge // -] -qed. - -(* Advanced inversion lemmas with evaluation evaluation lift ****************) - -lemma veq_inv_vlift_sn (M): ∀lv1,y2,d1,i. ⫯[i←d1]lv1 ≗{M} y2 → - ∃∃lv2,d2. lv1 ≗ lv2 & d1 ≗ d2 & ⫯[i←d2]lv2 ≐ y2. -#M #lv1 #y2 #d1 #i #H -@(ex3_2_intro) -[5: @exteq_sym @vlift_vdrop_eq |1,2: skip -| #j elim (lt_or_ge j i) #Hji - [ lapply (H j) -H >vlift_lt // >vdrop_lt // - | lapply (H (↑j)) -H >vlift_gt /2 width=1 by monotonic_le_plus_l/ >vdrop_ge // - ] -| lapply (H i) >vlift_eq // -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/vlifts.ma b/matita/matita/contribs/lambdadelta/apps_2/models/vlifts.ma new file mode 100644 index 000000000..81321cdac --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/models/vlifts.ma @@ -0,0 +1,125 @@ +(**************************************************************************) +(* ___ *) +(* ||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/roplus_5.ma". +include "static_2/syntax/lenv.ma". +include "apps_2/models/veq.ma". + +(* MULTIPLE LIFT FOR MODEL EVALUATIONS **************************************) + +inductive vlifts (M) (gv) (lv): relation2 lenv (evaluation M) ≝ +| vlifts_atom: vlifts M gv lv (⋆) lv +| vlifts_abbr: ∀v,d,K,V. vlifts M gv lv K v → ⟦V⟧[gv, v] = d → vlifts M gv lv (K.ⓓV) (⫯[0←d]v) +| vlifts_abst: ∀v,d,K,V. vlifts M gv lv K v → vlifts M gv lv (K.ⓛV) (⫯[0←d]v) +| vlifts_unit: ∀v,d,I,K. vlifts M gv lv K v → vlifts M gv lv (K.ⓤ{I}) (⫯[0←d]v) +| vlifts_repl: ∀v1,v2,L. vlifts M gv lv L v1 → v1 ≗ v2 → vlifts M gv lv L v2 +. + +interpretation "multiple lift (model evaluation)" + 'ROPlus M gv L lv v = (vlifts M gv lv L v). + +(* Basic inversion lemmas ***************************************************) + +fact vlifts_inv_atom_aux (M) (gv) (lv): is_model M → + ∀v,L. L ⨁{M}[gv] lv ≘ v → + ⋆ = L → lv ≗ v. +#M #gv #lv #HM #v #L #H elim H -v -L +[ #_ /2 width=1 by veq_refl/ +| #v #d #K #V #_ #_ #_ #H destruct +| #v #d #K #V #_ #_ #H destruct +| #v #d #I #K #_ #_ #H destruct +| #v1 #v2 #L #_ #Hv12 #IH #H destruct + /3 width=3 by veq_trans/ +] +qed-. + +lemma vlifts_inv_atom (M) (gv) (lv): is_model M → + ∀v. ⋆ ⨁{M}[gv] lv ≘ v → lv ≗ v. +/2 width=4 by vlifts_inv_atom_aux/ qed-. + +fact vlifts_inv_abbr_aux (M) (gv) (lv): is_model M → + ∀y,L. L ⨁{M}[gv] lv ≘ y → + ∀K,V. K.ⓓV = L → + ∃∃v. K ⨁[gv] lv ≘ v & ⫯[0←⟦V⟧[gv, v]]v ≗ y. +#M #gv #lv #HM #y #L #H elim H -y -L +[ #Y #X #H destruct +| #v #d #K #V #Hv #Hd #_ #Y #X #H destruct + /3 width=3 by veq_refl, ex2_intro/ +| #v #d #K #V #_ #_ #Y #X #H destruct +| #v #d #I #K #_ #_ #Y #X #H destruct +| #v1 #v2 #L #_ #Hv12 #IH #Y #X #H destruct + elim IH -IH [|*: // ] #v #Hv #Hv1 + /3 width=5 by veq_trans, ex2_intro/ +] +qed-. + +lemma vlifts_inv_abbr (M) (gv) (lv): is_model M → + ∀y,K,V. K.ⓓV ⨁{M}[gv] lv ≘ y → + ∃∃v. K ⨁[gv] lv ≘ v & ⫯[0←⟦V⟧[gv, v]]v ≗ y. +/2 width=3 by vlifts_inv_abbr_aux/ qed-. + +fact vlifts_inv_abst_aux (M) (gv) (lv): is_model M → + ∀y,L. L ⨁{M}[gv] lv ≘ y → + ∀K,W. K.ⓛW = L → + ∃∃v,d. K ⨁[gv] lv ≘ v & ⫯[0←d]v ≗ y. +#M #gv #lv #HM #y #L #H elim H -y -L +[ #Y #X #H destruct +| #v #d #K #V #_ #_ #_ #Y #X #H destruct +| #v #d #K #V #Hv #_ #Y #X #H destruct + /3 width=4 by veq_refl, ex2_2_intro/ +| #v #d #I #K #_ #_ #Y #X #H destruct +| #v1 #v2 #L #_ #Hv12 #IH #Y #X #H destruct + elim IH -IH [|*: // ] #v #d #Hv #Hv1 + /3 width=6 by veq_trans, ex2_2_intro/ +] +qed-. + +lemma vlifts_inv_abst (M) (gv) (lv): is_model M → + ∀y,K,W. K.ⓛW ⨁{M}[gv] lv ≘ y → + ∃∃v,d. K ⨁[gv] lv ≘ v & ⫯[0←d]v ≗ y. +/2 width=4 by vlifts_inv_abst_aux/ qed-. + +fact vlifts_inv_unit_aux (M) (gv) (lv): is_model M → + ∀y,L. L ⨁{M}[gv] lv ≘ y → + ∀I,K. K.ⓤ{I} = L → + ∃∃v,d. K ⨁[gv] lv ≘ v & ⫯[0←d]v ≗ y. +#M #gv #lv #HM #y #L #H elim H -y -L +[ #Z #Y #H destruct +| #v #d #K #V #_ #_ #_ #Z #Y #H destruct +| #v #d #K #V #_ #_ #Z #Y #H destruct +| #v #d #I #K #Hv #_ #Z #Y #H destruct + /3 width=4 by veq_refl, ex2_2_intro/ +| #v1 #v2 #L #_ #Hv12 #IH #Z #Y #H destruct + elim IH -IH [|*: // ] #v #d #Hv #Hv1 + /3 width=6 by veq_trans, ex2_2_intro/ +] +qed-. + +lemma vlifts_inv_unit (M) (gv) (lv): is_model M → + ∀y,I,K. K.ⓤ{I} ⨁{M}[gv] lv ≘ y → + ∃∃v,d. K ⨁[gv] lv ≘ v & ⫯[0←d]v ≗ y. +/2 width=4 by vlifts_inv_unit_aux/ qed-. + +(* Basic forward lemmas *****************************************************) + +lemma vlifts_fwd_bind (M) (gv) (lv): is_model M → + ∀y,I,K. K.ⓘ{I} ⨁{M}[gv] lv ≘ y → + ∃∃v,d. K ⨁[gv] lv ≘ v & ⫯[0←d]v ≗ y. +#M #gv #lv #HM #y * [ #I | * #V ] #L #H +[ /2 width=2 by vlifts_inv_unit/ +| elim (vlifts_inv_abbr … H) // -H #v #HL #Hv + /2 width=4 by ex2_2_intro/ +| /2 width=2 by vlifts_inv_abst/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/vlifts_shift.ma b/matita/matita/contribs/lambdadelta/apps_2/models/vlifts_shift.ma new file mode 100644 index 000000000..a324d3cf4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/models/vlifts_shift.ma @@ -0,0 +1,70 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "static_2/syntax/shift.ma". +include "apps_2/models/vlifts.ma". + +(* MULTIPLE LIFT FOR MODEL EVALUATIONS **************************************) + +(* Properties with shift for restricted closures ****************************) + +lemma vlifts_shift (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]. +#M #H1M #H2M #L elim L -L [| #K * [| * ]] +[ #T1 #T2 #gv #lv #H12 + >shift_atom >shift_atom + /4 width=1 by vlifts_atom, veq_refl/ +| #I #IH #T1 #T2 #gv #lv #H12 + >shift_unit >shift_unit + /5 width=1 by vlifts_unit, mx, mr/ +| #V #IH #T1 #T2 #gv #lv #H12 + >shift_pair >shift_pair + @IH -IH #v #Hv + @(mq … H1M) [3:|*: /3 width=2 by seq_sym, md/ ] + /4 width=1 by vlifts_abbr, mr/ +| #W #IH #T1 #T2 #gv #lv #H12 + >shift_pair >shift_pair + /5 width=1 by vlifts_abst, mx, mr/ +] +qed. + +(* Inversion lemmas with shift for restricted closures **********************) + +lemma vlifts_inv_shift (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 * [| * ]] +[ #T1 #T2 #gv #lv + >shift_atom >shift_atom #H12 #v #H + lapply (vlifts_inv_atom … H) -H // #Hv + /4 width=7 by ti_comp, veq_refl, mq/ +| #I #IH #T1 #T2 #gv #lv + >shift_unit >shift_unit #H12 #y #H + elim (vlifts_inv_unit … H) -H // #v #d #Hlv #Hv + lapply (IH … H12 … Hlv) -IH -H12 -Hlv #H12 + /4 width=7 by ti_comp, ti_fwd_mx_dx, veq_refl, mq/ +| #V #IH #T1 #T2 #gv #lv + >shift_pair >shift_pair #H12 #y #H + elim (vlifts_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/ +| #W #IH #T1 #T2 #gv #lv + >shift_pair >shift_pair #H12 #y #H + elim (vlifts_inv_abst … H) -H // #v #d #Hlv #Hv + lapply (IH … H12 … Hlv) -IH -H12 -Hlv #H12 + /4 width=7 by ti_comp, ti_fwd_mx_dx, veq_refl, mq/ +] +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 deleted file mode 100644 index a0e2b5fc3..000000000 --- a/matita/matita/contribs/lambdadelta/apps_2/notation/models/downspoon_3.ma +++ /dev/null @@ -1,27 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 $i $lv }. - -notation > "hvbox( ⫰[ break term 46 i ] break term 46 lv )" - non associative with precedence 46 - for @{ 'DownSpoon ? $i $lv }. - -notation > "hvbox( ⫰{ term 46 M }[ break term 46 i ] break term 46 lv )" - non associative with precedence 46 - for @{ 'DownSpoon $M $i $lv }. diff --git a/matita/matita/contribs/lambdadelta/apps_2/notation/models/roplus_5.ma b/matita/matita/contribs/lambdadelta/apps_2/notation/models/roplus_5.ma new file mode 100644 index 000000000..149ea8540 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/notation/models/roplus_5.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( L ⨁[ break term 46 gv ] break term 46 lv ≘ break term 46 v )" + non associative with precedence 45 + for @{ 'ROPlus $M $gv $L $lv $v }. + +notation > "hvbox( L ⨁[ break term 46 gv ] break term 46 lv ≘ break term 46 v )" + non associative with precedence 45 + for @{ 'ROPlus ? $gv $L $lv $v }. + +notation > "hvbox( L ⨁{ break term 46 M }[ break term 46 gv ] break term 46 lv ≘ break term 46 v )" + non associative with precedence 45 + for @{ 'ROPlus $M $gv $L $lv $v }. diff --git a/matita/matita/contribs/lambdadelta/apps_2/notation/models/upspoon_3.ma b/matita/matita/contribs/lambdadelta/apps_2/notation/models/upspoon_3.ma deleted file mode 100644 index a12cbbfb3..000000000 --- a/matita/matita/contribs/lambdadelta/apps_2/notation/models/upspoon_3.ma +++ /dev/null @@ -1,27 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 d ] break term 46 lv )" - non associative with precedence 46 - for @{ 'UpSpoon $M $d $lv }. - -notation > "hvbox( ⫯[ break term 46 d ] break term 46 lv )" - non associative with precedence 46 - for @{ 'UpSpoon ? $d $lv }. - -notation > "hvbox( ⫯{ term 46 M }[ break term 46 d ] break term 46 lv )" - non associative with precedence 46 - for @{ 'UpSpoon $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 6f9d8a2e7..236ec0c5c 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 @@ -15,20 +15,22 @@ table { [ "deq" + "( ? ⊢ ? ≗{?} ? )" "deq_cpr" * ] } ] - [ { "evaluation equivalence" * } { - [ "veq" + "( ? ≗{?} ? )" "veq_vdrop" "veq_li" "veq_lifts" * ] + [ { "local environment interpretation" * } { + [ "li" + "( ? ϵ ⟦?⟧{?}[?] )" "li_vlifts" * ] } ] - [ { "evaluation drop" * } { - [ "vdrop" + "( ⫰{?}? )" + "( ⫰{?}[?]? )" "vdrop_vlift" * ] + [ { "multiple evaluation lift" * } { + [ "vlifts" + "( ?⨁{?}[?]? ≘ ? )" "vlifts_shift" * ] + } + ] + [ { "evaluation equivalence" * } { + [ "veq" + "( ? ≗{?} ? )" "veq_lifts" * ] } ] [ { "model declaration" * } { [ "model" + "( ? ≗{?} ? )" + "( ? @{?} ? )" + "( ⟦?⟧{?}[?,?] )" - "model_vlift" + "( ⫯{?}[?]? )" + "( ⫯{?}[?←?]? )" + "model_vlift" + "( ⫯{?}[?←?]? )" "model_props" - "model_li" + "( ? ϵ ⟦?⟧{?}[?] )" - "model_gi" * ] } ] @@ -71,3 +73,9 @@ class "top" { * } class "capitalize italic" { 0 } class "italic" { 1 } +(* + [ { "evaluation drop" * } { + [ "vdrop" + "( ⫰{?}? )" + "( ⫰{?}[?]? )" "vdrop_vlift" * ] + } + ] +*) diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/shift.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/shift.ma new file mode 100644 index 000000000..0c40a310b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/shift.ma @@ -0,0 +1,38 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "static_2/syntax/lenv.ma". + +(* SHIFT FOR RESTRICTED CLOSURES ********************************************) + +rec definition shift L T on L ≝ match L with +[ LAtom ⇒ T +| LBind L I ⇒ match I with + [ BUnit _ ⇒ shift L (-ⓛ⋆0.T) + | BPair I V ⇒ shift L (-ⓑ{I}V.T) + ] +]. + +interpretation "shift (restricted closure)" 'plus L T = (shift L T). + +(* Basic properties *********************************************************) + +lemma shift_atom: ∀T. ⋆ + T = T. +// qed. + +lemma shift_unit: ∀I,L,T. L.ⓤ{I}+T = L+(-ⓛ⋆0.T). +// qed. + +lemma shift_pair: ∀I,L,V,T. (L.ⓑ{I}V)+T = L+(-ⓑ{I}V.T). +// qed. diff --git a/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl b/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl index 740b3482e..6a2e3859e 100644 --- a/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl @@ -103,6 +103,7 @@ table { } ] [ { "append" * } { + [ [ "for restricted closures" ] "shift" + "( ? + ? )" "shift_append" * ] [ [ "for lenvs" ] "append" + "( ? + ? )" "append_length" * ] } ] diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml index 02a5c2269..9c1715d39 100644 --- a/matita/matita/predefined_virtuals.ml +++ b/matita/matita/predefined_virtuals.ml @@ -1510,7 +1510,7 @@ let predefined_classes = [ [":"; "⁝"; ]; ["."; "•"; "◦"; ]; ["#"; "♯"; "⋕"; "⧣"; "⧤"; "⌘"; ]; - ["+"; "⨭"; "⨮"; "⊕"; "⊞"; ]; + ["+"; "⨭"; "⨮"; "⨁"; "⊕"; "⊞"; ]; ["-"; "÷"; "⊢"; "⊩"; "⧟"; "⊟"; ]; ["="; "≝"; "≡"; "≘"; "≗"; "≐"; "≑"; "≛"; "≚"; "≙"; "⌆"; "⧦"; "⊜"; "≋"; "⩳"; "≅"; "⩬"; "≂"; "≃"; "≈"; ]; ["→"; "↦"; "⇝"; "⤞"; "⇾"; "⤍"; "⤏"; "⤳"; ] ;