]> matita.cs.unibo.it Git - helm.git/commitdiff
update in static_2 and app_2
authorFerruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Wed, 11 Jul 2018 10:54:33 +0000 (12:54 +0200)
committerFerruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Wed, 11 Jul 2018 10:54:33 +0000 (12:54 +0200)
+ advances on the support for models
+ tentative definition of shift (incomplete because unary binders are missing in terms)
+ minor updates and corrections

37 files changed:
helm/www/lambdadelta/download/lambda_talk_1s.pdf [new file with mode: 0644]
matita/matita/contribs/lambdadelta/Makefile
matita/matita/contribs/lambdadelta/apps_2/etc/models/downspoon_3.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/apps_2/etc/models/model_ext.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/apps_2/etc/models/model_gi.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/apps_2/etc/models/model_valign.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/apps_2/etc/models/uparrow_3.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/apps_2/etc/models/upspoon_3.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/apps_2/etc/models/valign.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/apps_2/etc/models/vdrop.etc
matita/matita/contribs/lambdadelta/apps_2/etc/models/vdrop_old.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/apps_2/etc/models/vdrop_vlift.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/apps_2/etc/models/veq_li.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/apps_2/etc/models/veq_vdrop.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/apps_2/models/deq.ma
matita/matita/contribs/lambdadelta/apps_2/models/deq_cpr.ma
matita/matita/contribs/lambdadelta/apps_2/models/li.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/apps_2/models/model.ma
matita/matita/contribs/lambdadelta/apps_2/models/model_gi.ma [deleted file]
matita/matita/contribs/lambdadelta/apps_2/models/model_li.ma [deleted file]
matita/matita/contribs/lambdadelta/apps_2/models/model_props.ma
matita/matita/contribs/lambdadelta/apps_2/models/model_vlift.ma
matita/matita/contribs/lambdadelta/apps_2/models/vdrop.ma [deleted file]
matita/matita/contribs/lambdadelta/apps_2/models/vdrop_vlift.ma [deleted file]
matita/matita/contribs/lambdadelta/apps_2/models/veq.ma
matita/matita/contribs/lambdadelta/apps_2/models/veq_li.ma [deleted file]
matita/matita/contribs/lambdadelta/apps_2/models/veq_lifts.ma
matita/matita/contribs/lambdadelta/apps_2/models/veq_vdrop.ma [deleted file]
matita/matita/contribs/lambdadelta/apps_2/models/vlifts.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/apps_2/models/vlifts_shift.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/apps_2/notation/models/downspoon_3.ma [deleted file]
matita/matita/contribs/lambdadelta/apps_2/notation/models/roplus_5.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/apps_2/notation/models/upspoon_3.ma [deleted file]
matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl
matita/matita/contribs/lambdadelta/static_2/syntax/shift.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl
matita/matita/predefined_virtuals.ml

diff --git a/helm/www/lambdadelta/download/lambda_talk_1s.pdf b/helm/www/lambdadelta/download/lambda_talk_1s.pdf
new file mode 100644 (file)
index 0000000..5831950
Binary files /dev/null and b/helm/www/lambdadelta/download/lambda_talk_1s.pdf differ
index 073dc33a2b640d6b971c771f546e7c4c6503fe3f..9d87f9909be37dc50abc38a8e6dabffc49a57cc0 100644 (file)
@@ -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 (file)
index 0000000..a0e2b5f
--- /dev/null
@@ -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 (file)
index 0000000..8c6e9d7
--- /dev/null
@@ -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 (file)
index 0000000..1c354a6
--- /dev/null
@@ -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 (file)
index 0000000..aafa0c0
--- /dev/null
@@ -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 (file)
index 0000000..2a953eb
--- /dev/null
@@ -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 (file)
index 0000000..a12cbbf
--- /dev/null
@@ -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 (file)
index 0000000..c8b4df0
--- /dev/null
@@ -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-.
index 5a857fbb18100add93281751c1f8603c2b069f1a..e15ac254a9363867a3f87d8bde95c45ae59d64d0 100644 (file)
-
-
-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/
-  <plus_minus_m_m /2 width=2 by ltn_to_ltO/
-]
-qed.
-
-lemma raise_vdrop_sym: ∀M,v,i. v ≐⦋M⦌ [i⬐v i] ↓[i,1] v.
-/3 width=1 by raise_vdrop, veq_sym/ qed.
-
-lemma raise_vdrop_be: ∀M,v,l,m. ↓[l, m] v ≐⦋M⦌ [l⬐v (l+m)] ↓[l, m+1] v.
-#M #v #l #m #j elim (lt_or_eq_or_gt j l) #Hlj destruct
-[ >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 (file)
index 0000000..5a857fb
--- /dev/null
@@ -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/
+  <plus_minus_m_m /2 width=2 by ltn_to_ltO/
+]
+qed.
+
+lemma raise_vdrop_sym: ∀M,v,i. v ≐⦋M⦌ [i⬐v i] ↓[i,1] v.
+/3 width=1 by raise_vdrop, veq_sym/ qed.
+
+lemma raise_vdrop_be: ∀M,v,l,m. ↓[l, m] v ≐⦋M⦌ [l⬐v (l+m)] ↓[l, m+1] v.
+#M #v #l #m #j elim (lt_or_eq_or_gt j l) #Hlj destruct
+[ >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 (file)
index 0000000..0316fa1
--- /dev/null
@@ -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 (file)
index 0000000..f696a44
--- /dev/null
@@ -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 (file)
index 0000000..78b9795
--- /dev/null
@@ -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-.
index 8de93a606782d76b8c6afbbca2ab9c7c204dc201..5d0f2d324ef315cfaa1c3259e074bf5da94a3edc 100644 (file)
@@ -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-.
index 74124719e6eb355d28045ccacd8fda08fde6af55..6acf720cbb99889881c8a4d00e46c6317bbe6e5a 100644 (file)
@@ -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 (file)
index 0000000..f0f2c0f
--- /dev/null
@@ -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.
index 86c624e1bd26fcad3d629811420609a664e1e306..290c3e4c6b6abbf06df1221aa97d615d5de13fd3 100644 (file)
@@ -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 (file)
index 1c354a6..0000000
+++ /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 (file)
index 6be3c60..0000000
+++ /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-.
index 073d5db6278a04b2b831af10fbe4d0c9f22ddf57..26a34783265df483e696b21e10fac459e7c709f2 100644 (file)
@@ -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-.
index 29bd2e67f65b8fc6ddfdb951e7fa69ca639e01dc..bb2d5c7c90ad8445756c012929b083abbdce3652 100644 (file)
 (**************************************************************************)
 
 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 (file)
index f0d72d4..0000000
+++ /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 (file)
index 0316fa1..0000000
+++ /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.
index e784d3b7a8148c05e71034929822171fbfb9af43..7f6e8b78979d5f9e61055435b218f6e569ccc3a6 100644 (file)
@@ -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 (file)
index 8fa8d90..0000000
+++ /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-.
index 905b1a33650f710a58d9f301a01e099aa5086809..dc83b79b1ac1d22edb22635bb5aafd0a14a02ee0 100644 (file)
@@ -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 (file)
index ae31753..0000000
+++ /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 (file)
index 0000000..81321cd
--- /dev/null
@@ -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 (file)
index 0000000..a324d3c
--- /dev/null
@@ -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 (file)
index a0e2b5f..0000000
+++ /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 (file)
index 0000000..149ea85
--- /dev/null
@@ -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 (file)
index a12cbbf..0000000
+++ /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 }.
index 6f9d8a2e7860a03e7610bfed3385274f953cdbd4..236ec0c5c67f54ada08e655b0dbcabe853572004 100644 (file)
@@ -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 (file)
index 0000000..0c40a31
--- /dev/null
@@ -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.
index 740b3482e9b87219d9684c877185139c7206c0c5..6a2e3859ef7ca4483a228827ea8a4342b48e9f29 100644 (file)
@@ -103,6 +103,7 @@ table {
           }
         ]
         [ { "append" * } {
+             [ [ "for restricted closures" ] "shift" + "( ? + ? )" "shift_append" * ]
              [ [ "for lenvs" ] "append" + "( ? + ? )" "append_length" * ]
           }
         ]
index 02a5c226998cf2db2d032370d45219c133f591a6..9c1715d39135b5c26eb5522aeb4f286f1ca6c401 100644 (file)
@@ -1510,7 +1510,7 @@ let predefined_classes = [
  [":"; "⁝"; ];
  ["."; "•"; "◦"; ];
  ["#"; "♯"; "⋕"; "⧣"; "⧤"; "⌘"; ];
- ["+"; "⨭"; "⨮"; "⊕"; "⊞"; ];
+ ["+"; "⨭"; "⨮"; "â¨\81"; "â\8a\95"; "â\8a\9e"; ];
  ["-"; "÷"; "⊢"; "⊩"; "⧟"; "⊟"; ];
  ["="; "≝"; "≡"; "≘"; "≗"; "≐"; "≑"; "≛"; "≚"; "≙"; "⌆"; "⧦"; "⊜"; "≋"; "⩳"; "≅"; "⩬"; "≂"; "≃"; "≈"; ];  
  ["→"; "↦"; "⇝"; "⤞"; "⇾"; "⤍"; "⤏"; "⤳"; ] ;