From 2976c347e18717e691825ebdf73a5ce941c57d1b Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 3 May 2018 22:27:36 +0200 Subject: [PATCH] update in ground_2 and models + bug fixed in local environment interpretation extensional equality of evaluations allows to prove a lemma --- .../apps_2/etc/models/model_lower.etc | 181 ------------------ .../lambdadelta/apps_2/etc/models/vdrop.etc | 138 +++++++++++++ .../lambdadelta/apps_2/models/model_li.ma | 46 +++-- .../lambdadelta/apps_2/models/model_props.ma | 3 +- .../models/{model_push.ma => model_vlift.ma} | 30 ++- .../lambdadelta/apps_2/models/vdrop.ma | 49 +++++ .../lambdadelta/apps_2/models/vdrop_vlift.ma | 29 +++ .../contribs/lambdadelta/apps_2/models/veq.ma | 29 +-- .../lambdadelta/apps_2/models/veq_li.ma | 16 +- .../lambdadelta/apps_2/models/veq_vdrop.ma | 42 ++++ .../lambdadelta/apps_2/web/apps_2_src.tbl | 8 +- .../lambdadelta/ground_2/lib/arith.ma | 4 + .../lambdadelta/ground_2/lib/exteq.ma | 39 ++++ .../lambdadelta/ground_2/lib/functions.ma | 4 + .../ground_2/notation/relations/doteq_4.ma | 27 +++ .../lambdadelta/ground_2/web/ground_2_src.tbl | 2 +- 16 files changed, 413 insertions(+), 234 deletions(-) delete mode 100644 matita/matita/contribs/lambdadelta/apps_2/etc/models/model_lower.etc create mode 100644 matita/matita/contribs/lambdadelta/apps_2/etc/models/vdrop.etc rename matita/matita/contribs/lambdadelta/apps_2/models/{model_push.ma => model_vlift.ma} (61%) create mode 100644 matita/matita/contribs/lambdadelta/apps_2/models/vdrop.ma create mode 100644 matita/matita/contribs/lambdadelta/apps_2/models/vdrop_vlift.ma create mode 100644 matita/matita/contribs/lambdadelta/apps_2/models/veq_vdrop.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/lib/exteq.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/relations/doteq_4.ma 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 deleted file mode 100644 index e99004e7b..000000000 --- a/matita/matita/contribs/lambdadelta/apps_2/etc/models/model_lower.etc +++ /dev/null @@ -1,181 +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/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/vdrop.etc b/matita/matita/contribs/lambdadelta/apps_2/etc/models/vdrop.etc new file mode 100644 index 000000000..5a857fbb1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/etc/models/vdrop.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/models/model_li.ma b/matita/matita/contribs/lambdadelta/apps_2/models/model_li.ma index 07266f8d3..8d59fe006 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/model_li.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/model_li.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/syntax/lenv.ma". -include "apps_2/models/model_push.ma". +include "apps_2/models/model_vlift.ma". include "apps_2/notation/models/inwbrackets_4.ma". (* LOCAL ENVIRONMENT INTERPRETATION ****************************************) @@ -23,6 +23,7 @@ inductive li (M) (gv): relation2 lenv (evaluation M) ≝ | 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)" @@ -31,43 +32,52 @@ interpretation "local environment interpretation (model)" (* 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 * -v -Y + ∃∃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 +| #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. + ∃∃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 * -v -Y + ∃∃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 +| #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. + ∃∃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 * -v -Y + ∃∃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 #L #V #_ #J #K #H destruct -| #lv #d #I #L #HL #J #K #H destruct /2 width=4 by ex2_2_intro/ +| #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. + ∃∃lv,d. lv ϵ ⟦L⟧{M}[gv] & ⫯{M}[d]lv ≐ v. /2 width=4 by li_inv_unit_aux/ 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 90ab35238..863e3d063 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/model_props.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/model_props.ma @@ -12,8 +12,7 @@ (* *) (**************************************************************************) -include "ground_2/lib/functions.ma". -include "apps_2/models/model_push.ma". +include "apps_2/models/model_vlift.ma". (* MODEL ********************************************************************) diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/model_push.ma b/matita/matita/contribs/lambdadelta/apps_2/models/model_vlift.ma similarity index 61% rename from matita/matita/contribs/lambdadelta/apps_2/models/model_push.ma rename to matita/matita/contribs/lambdadelta/apps_2/models/model_vlift.ma index acf96a0cc..29bd2e67f 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/model_push.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/model_vlift.ma @@ -12,28 +12,40 @@ (* *) (**************************************************************************) +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 push (M): nat → dd M → evaluation M → evaluation M ≝ - λj,d,lv,i. tri … i j (lv i) d (lv (↓i)). +definition vlift (M): nat → dd M → evaluation M → evaluation M ≝ + λj,d,lv,i. tri … i j (lv i) d (lv (↓i)). -interpretation "generic push (model evaluation)" - 'UpSpoon M i d lv = (push M i d lv). +interpretation "generic lift (model evaluation)" + 'UpSpoon M i d lv = (vlift M i d lv). -interpretation "push (model evaluation)" - 'UpSpoon M d lv = (push M O d lv). +interpretation "lift (model evaluation)" + 'UpSpoon M d lv = (vlift M O d lv). (* Basic properties *********************************************************) -lemma push_lt: ∀M,lv,d,j,i. i < j → (⫯{M}[j←d] lv) i = lv i. +lemma vlift_lt (M): ∀lv,d,j,i. i < j → (⫯{M}[j←d] lv) i = lv i. /2 width=1 by tri_lt/ qed-. -lemma push_eq: ∀M,lv,d,i. (⫯{M}[i←d] lv) i = d. +lemma vlift_eq (M): ∀lv,d,i. (⫯{M}[i←d] lv) i = d. /2 width=1 by tri_eq/ qed-. -lemma push_gt: ∀M,lv,d,j,i. j < i → (⫯{M}[j←d] lv) i = lv (↓i). +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 new file mode 100644 index 000000000..f0d72d4e2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/models/vdrop.ma @@ -0,0 +1,49 @@ +(**************************************************************************) +(* ___ *) +(* ||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 new file mode 100644 index 000000000..0316fa161 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/models/vdrop_vlift.ma @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "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 11f07c404..47d4a1b74 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma @@ -32,24 +32,25 @@ 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 ext_veq (M): is_model M → + ∀lv1,lv2. lv1 ≐ lv2 → lv1 ≗{M} lv2. +/2 width=1 by mq/ qed. + +lemma exteq_veq_trans (M): ∀lv1,lv. lv1 ≐ lv → + ∀lv2. lv ≗{M} lv2 → lv1 ≗ lv2. +// qed-. -lemma push_comp (M): ∀i. compatible_3 … (push M i) (sq M) (veq M) (veq M). +(* Properties with evaluation evaluation lift *******************************) + +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 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) // +[ >(vlift_lt … Hij) >(vlift_lt … Hij) // +| >(vlift_eq …) >(vlift_eq …) // +| >(vlift_gt … Hij) >(vlift_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. -(* -#M #lv1 #y2 #d1 #i #H -*) (* Properies with term interpretation ***************************************) lemma ti_comp_l (M): is_model M → @@ -59,8 +60,8 @@ lemma ti_comp_l (M): is_model M → [ /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/ +| /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/ ] diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/veq_li.ma b/matita/matita/contribs/lambdadelta/apps_2/models/veq_li.ma index 717a03911..8fa8d90d7 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/veq_li.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/veq_li.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "apps_2/models/model_li.ma". -include "apps_2/models/veq.ma". +include "apps_2/models/veq_vdrop.ma". (* EVALUATION EQUIVALENCE **************************************************) @@ -24,13 +24,15 @@ lemma li_repl_back (M) (gv): is_model M → ∀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/ + 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_push_sn … H) -H #lv2 #d2 #Hlv12 #_ #H destruct - /3 width=1 by li_abst/ + 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_push_sn … H) -H #lv2 #d2 #Hlv12 #_ #H destruct - /3 width=1 by li_unit/ + 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_vdrop.ma b/matita/matita/contribs/lambdadelta/apps_2/models/veq_vdrop.ma new file mode 100644 index 000000000..ae3175310 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/models/veq_vdrop.ma @@ -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/web/apps_2_src.tbl b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl index 4a5ab318a..3388f4350 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 @@ -16,12 +16,16 @@ table { } ] [ { "evaluation equivalence" * } { - [ "veq" + "( ? ≗{?} ? )" "veq_li" * ] + [ "veq" + "( ? ≗{?} ? )" "veq_vdrop" "veq_li" * ] + } + ] + [ { "evaluation drop" * } { + [ "vdrop" + "( ⫰{?}? )" + "( ⫰{?}[?]? )" "vdrop_vlift" * ] } ] [ { "model declaration" * } { [ "model" + "( ? ≗{?} ? )" + "( ? @{?} ? )" + "( ⟦?⟧{?}[?,?] )" - "model_push" + "( ⫯{?}[?] )" + "( ⫯{?}[?←?] )" + "model_vlift" + "( ⫯{?}[?]? )" + "( ⫯{?}[?←?]? )" "model_props" "model_li" + "( ? ϵ ⟦?⟧{?}[?] )" * ] diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma index 9135ff24d..6f018ea25 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma @@ -62,6 +62,10 @@ lemma plus_minus_minus_be: ∀x,y,z. y ≤ z → z ≤ x → (x - z) + (z - y) = #x #z #y #Hzy #Hyx >plus_minus // >commutative_plus >plus_minus // qed-. +lemma lt_succ_pred: ∀m,n. n < m → m = ↑↓m. +#m #n #Hm >S_pred /2 width=2 by ltn_to_ltO/ +qed-. + fact plus_minus_minus_be_aux: ∀i,x,y,z. y ≤ z → z ≤ x → i = z - y → x - z + i = x - y. /2 width=1 by plus_minus_minus_be/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/exteq.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/exteq.ma new file mode 100644 index 000000000..4e4152ff3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/exteq.ma @@ -0,0 +1,39 @@ +(**************************************************************************) +(* ___ *) +(* ||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/notation/relations/doteq_4.ma". +include "ground_2/lib/relations.ma". + +(* EXTENSIONAL EQUIVALENCE **************************************************) + +definition exteq (A,B:Type[0]): relation (A → B) ≝ + λf1,f2. ∀a. f1 a = f2 a. + +interpretation "extensional equivalence" + 'DotEq A B f1 f2 = (exteq A B f1 f2). + +(* Basic_properties *********************************************************) + +lemma exteq_refl (A) (B): reflexive … (exteq A B). +// qed. + +lemma exteq_repl (A) (B): replace_2 … (exteq A B) (exteq A B) (exteq A B). +// qed-. + +lemma exteq_sym (A) (B): symmetric … (exteq A B). +/2 width=1 by exteq_repl/ qed-. + +lemma exteq_trans (A) (B): Transitive … (exteq A B). +/2 width=1 by exteq_repl/ qed-. + diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/functions.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/functions.ma index 4276e1a6c..4977504b9 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/functions.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/functions.ma @@ -20,6 +20,10 @@ definition left_identity (A) (f): predicate A ≝ λi. ∀a:A. a = f i a. definition right_identity (A) (f): predicate A ≝ λi. ∀a:A. a = f a i. +definition compatible_2 (A) (B): relation3 … (relation A) (relation B) ≝ + λf,Sa,Sb. + ∀a1,a2. Sa a1 a2 → Sb (f a1) (f a2). + 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/notation/relations/doteq_4.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/doteq_4.ma new file mode 100644 index 000000000..f3a39a720 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/doteq_4.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation < "hvbox( f1 ≐ break term 46 f2 )" + non associative with precedence 45 + for @{ 'DotEq $A $B $f1 $f2 }. + +notation > "hvbox( f1 ≐ break term 46 f2 )" + non associative with precedence 45 + for @{ 'DotEq ? ? $f1 $f2 }. + +notation > "hvbox( f1 ≐{ break term 46 A, break term 46 B } break term 46 f2 )" + non associative with precedence 45 + for @{ 'DotEq $A $B $f1 $f2 }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl index 65846a1b5..1cd156ab1 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl @@ -55,7 +55,7 @@ table { [ "stream ( ? ⨮{?} ? )" "stream_eq ( ? ≗{?} ? )" "stream_hdtl ( ⫰{?}? )" "stream_tls ( ⫰*{?}[?]? )" * ] [ "list ( ◊ ) ( ? ⨮{?} ? ) ( |?| )" "list2 ( ◊ ) ( {?,?} ⨮{?,?} ? ) ( |?| )" * ] [ "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? ) ( ↑? ) ( ↓? ) ( ? ∨ ? ) ( ? ∧ ? )" * ] - [ "logic ( ⊥ ) ( ⊤ )" "relations ( ? ⊆ ? )" "functions" "star" "ltc" * ] + [ "logic ( ⊥ ) ( ⊤ )" "relations ( ? ⊆ ? )" "functions" "exteq ( ? ≐{?,?} ? )" "star" "ltc" * ] } ] } -- 2.39.2