notation and dependences bug fix

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_aaa.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_aaa.ma
index 537d5b235d9a0869c5cdf0dfa363bfef344564e4..f3863f38b81131dd91acb51d008ca0b1dd8cd3a7 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_aaa.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_aaa.ma
@@ -21,7 +21,7 @@ include "Basic_2/computation/lsubc.ma".
 
 axiom aacr_aaa_csubc: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
                         ∀L1,T,A. L1 ⊢ T ÷ A →
-                        ∀L2. L2 [RP] ⊑ L1 → {L2, T} [RP] ϵ 〚A〛.
+                        ∀L2. L2 [RP] ⊑ L1 → ⦃L2, T⦄ [RP] ϵ 〚A〛.
 (*
 #RR #RS #RP #H1RP #H2RP #L1 #T #A #H elim H -L1 -T -A
 [ #L #k #L2 #HL2

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_cr.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_cr.ma
index 699d997dd2acb594e19f912772c364d45e4ec13b..c45bc25914fbbef41fd70ef470ab1ce12b78a601 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_cr.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_cr.ma
@@ -88,11 +88,11 @@ axiom aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
   @(s7 … IHA … HL21) [2: @HA [2: 
 ]
 qed.
-*)  
+*)
 lemma aacr_abst: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
-                 ∀L,W,T,A,B. RP L W → 
-                 (∀V. {L, V} [RP] ϵ 〚B〛 → {L. 𝕓{Abbr}V, T} [RP] ϵ 〚A〛) →
-                 {L, 𝕓{Abst}W. T} [RP] ϵ 〚𝕔B. A〛.
+                 ∀L,W,T,A,B. RP L W →
+                 (∀V. ⦃L, V⦄ [RP] ϵ 〚B〛 → ⦃L. 𝕓{Abbr}V, T⦄ [RP] ϵ 〚A〛) →
+                              ⦃L, 𝕓{Abst}W. T⦄ [RP] ϵ 〚𝕔B. A〛.
 #RR #RS #RP #H1RP #H2RP #L #W #T #A #B #HW #HA #V #HB
 lapply (aacr_acr … H1RP H2RP A) #HCA
 lapply (aacr_acr … H1RP H2RP B) #HCB

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc.ma
index 9d38f25d7be95f2db7b89ff3c113fbb9d5dca41a..60320a22ae35437cfb5c449759b627096735f285 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc.ma
@@ -19,7 +19,7 @@ include "Basic_2/computation/acp_cr.ma".
 inductive lsubc (RP:lenv→predicate term): relation lenv ≝
 | lsubc_atom: lsubc RP (⋆) (⋆)
 | lsubc_pair: ∀I,L1,L2,V. lsubc RP L1 L2 → lsubc RP (L1. 𝕓{I} V) (L2. 𝕓{I} V)
-| lsubc_abbr: ∀L1,L2,V,W,A. {L1, V} [RP] ϵ 〚A〛 → {L2, W} [RP] ϵ 〚A〛 →
+| lsubc_abbr: ∀L1,L2,V,W,A. ⦃L1, V⦄ [RP] ϵ 〚A〛 → ⦃L2, W⦄ [RP] ϵ 〚A〛 →
               lsubc RP L1 L2 → lsubc RP (L1. 𝕓{Abbr} V) (L2. 𝕓{Abst} W)
 .
 

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/functional/subst.ma b/matita/matita/contribs/lambda_delta/Basic_2/functional/subst.ma
index 05f698ff8fb9931a7b5357efae2252d7b4541710..46d3117408a7f0b20832aba26b218df92a34b63b 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/functional/subst.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/functional/subst.ma
@@ -34,7 +34,7 @@ interpretation "functional core substitution" 'Subst V d T = (fsubst V d T).
 (* Main properties **********************************************************)
 
 theorem fsubst_delift: ∀K,V,T,L,d.
-                       ⇓[0, d] L ≡ K. 𝕓{Abbr} V → L ⊢ T [d, 1] ≡ ↓[d ← V] T.
+                       ⇓[0, d] L ≡ K. 𝕓{Abbr} V → L ⊢ T [d, 1] ≡ [d ← V] T.
 #K #V #T elim T -T
 [ * #i #L #d #HLK normalize in ⊢ (? ? ? ? ? %); /2 width=3/
   elim (lt_or_eq_or_gt i d) #Hid
@@ -49,7 +49,7 @@ qed.
 (* Main inversion properties ************************************************)
 
 theorem fsubst_inv_delift: ∀K,V,T1,L,T2,d. ⇓[0, d] L ≡ K. 𝕓{Abbr} V →
-                           L ⊢ T1 [d, 1] ≡ T2 → ↓[d ← V] T1 = T2.
+                           L ⊢ T1 [d, 1] ≡ T2 → [d ← V] T1 = T2.
 #K #V #T1 elim T1 -T1
 [ * #i #L #T2 #d #HLK #H
   [ -HLK >(delift_fwd_sort1 … H) -H //

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/aarity.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/aarity.ma
index 42354e7008f136d5e8bbb2805e82df779388b8b0..8062d8604cfc762b37a06a1ca26565521f7a5d88 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/aarity.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/aarity.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "Ground_2/list.ma".
+include "Ground_2/star.ma".
 include "Basic_2/notation.ma".
 
 (* ATOMIC ARITY *************************************************************)

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/item.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/item.ma
index 48ff1ec9acf8448c1f48773a571343c298f1e628..08e35083de29cb17f6826ca6d558aa94425e616e 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/item.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/item.ma
@@ -20,7 +20,7 @@
  * [ suggested invocation to start formal specifications with ]
  *)
 
-include "Ground_2/list.ma".
+include "Ground_2/arith.ma".
 include "Basic_2/notation.ma".
 
 (* ITEMS ********************************************************************)

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_vector.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_vector.ma
index 6c9ea1ce5dac632e3900a33ec426e18ac5a92249..01dec21029029b8422487c81fddbf73d92fd0f9d 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_vector.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_vector.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "Ground_2/list.ma".
 include "Basic_2/grammar/term.ma".
 
 (* TERMS ********************************************************************)

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma
index 49f126019c2d9040329062891733ce42f659fac6..36f9f765294632f4ee1df6ab3d9e24acad4f8b16 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma
@@ -218,18 +218,10 @@ notation "hvbox( L ⊢ ⇓ T )"
    non associative with precedence 45
    for @{ 'SN $L $T }.
 
-notation "hvbox( { L, break T } ϵ break 〚 A 〛 )"
-   non associative with precedence 45
-   for @{ 'InEInt $L $T $A }.
-
-notation "hvbox( { L, break T } break [ R ] ϵ break 〚 A 〛 )"
+notation "hvbox( ⦃ L, break T ⦄ break [ R ] ϵ break 〚 A 〛 )"
    non associative with precedence 45
    for @{ 'InEInt $R $L $T $A }.
 
-notation "hvbox( T1 ⊑ break T2 )"
-   non associative with precedence 45
-   for @{ 'CrSubEq $T1 $T2 }.
-
 notation "hvbox( T1 break [ R ] ⊑ break T2 )"
    non associative with precedence 45
    for @{ 'CrSubEq $T1 $R $T2 }.
@@ -237,10 +229,10 @@ notation "hvbox( T1 break [ R ] ⊑ break T2 )"
 (* Functional ***************************************************************)
 
 notation "hvbox( ↑ [ d , break e ] break T )"
-   non associative with precedence 80
+   non associative with precedence 55
    for @{ 'Lift $d $e $T }.
 
-notation "hvbox( ↓ [ d ← break V ] break T )"
-   non associative with precedence 80
+notation "hvbox( [ d ← break V ] break T )"
+   non associative with precedence 55
    for @{ 'Subst $V $d $T }.
 

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/static/sh.ma b/matita/matita/contribs/lambda_delta/Basic_2/static/sh.ma
index 1708b7970397af2e6b726e67f51ecfd34bcf8215..7edbfd2afafe168259ceb0965d8ed76cc7908f82 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/static/sh.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/static/sh.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "Ground_2/list.ma".
+include "Ground_2/arith.ma".
 
 (* SORT HIERARCHY ***********************************************************)
 

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops.ma
new file mode 100644 (file)
index 0000000..c6bb67e
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops.ma
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "Basic_2/substitution/ldrop.ma".
+include "Basic_2/unfold/lifts.ma".
+
+(* GENERIC LOCAL ENVIRONMENT SLICING ****************************************)
+
+inductive ldrops: list2 nat nat → relation lenv ≝
+| ldrops_nil : ∀L. ldrops ⟠ L L
+| ldrops_cons: ∀L1,L,L2,des,d,e.
+               ⇓[d,e] L1 ≡ L → ldrops des L L2 → ldrops ({d, e} :: des) L1 L2
+.
+
+interpretation "generic local environment slicing"
+   'RDrop des T1 T2 = (ldrops des T1 T2).

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts.ma
new file mode 100644 (file)
index 0000000..9994f44
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts.ma
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "Basic_2/substitution/lift_vector.ma".
+
+(* GENERIC RELOCATION *******************************************************)
+
+inductive lifts: list2 nat nat → relation term ≝
+| lifts_nil : ∀T. lifts ⟠ T T
+| lifts_cons: ∀T1,T,T2,des,d,e.
+              ⇑[d,e] T1 ≡ T → lifts des T T2 → lifts ({d, e} :: des) T1 T2
+.
+
+interpretation "generic relocation" 'RLift des T1 T2 = (lifts des T1 T2).

diff --git a/matita/matita/contribs/lambda_delta/Ground_2/list.ma b/matita/matita/contribs/lambda_delta/Ground_2/list.ma
index 846d1f804fa1bcab92836e62215fb75c2b34859f..78a2305ea8dee7982f27c57203775de0911700af 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Ground_2/list.ma
+++ b/matita/matita/contribs/lambda_delta/Ground_2/list.ma
@@ -13,13 +13,12 @@
 (**************************************************************************)
 
 include "Ground_2/arith.ma".
-include "Ground_2/notation.ma".
 
 (* LISTS ********************************************************************)
 
 inductive list (A:Type[0]) : Type[0] :=
   | nil : list A
-  | cons: A -> list A -> list A.
+  | cons: A → list A → list A.
 
 interpretation "nil (list)" 'Nil = (nil ?).
 
@@ -30,3 +29,11 @@ let rec all A (R:predicate A) (l:list A) on l ≝
   [ nil        ⇒ True
   | cons hd tl ⇒ R hd ∧ all A R tl
   ].
+
+inductive list2 (A1,A2:Type[0]) : Type[0] :=
+  | nil2 : list2 A1 A2
+  | cons2: A1 → A2 → list2 A1 A2 → list2 A1 A2.
+
+interpretation "nil (list of pairs)" 'Nil2 = (nil2 ? ?). (**) (* 'Nil causes unification error in aacr_abst *)
+
+interpretation "cons (list of pairs)" 'Cons hd1 hd2 tl = (cons2 ? ? hd1 hd2 tl).

diff --git a/matita/matita/contribs/lambda_delta/Ground_2/notation.ma b/matita/matita/contribs/lambda_delta/Ground_2/notation.ma
index 5238b0d132525c02155a6d41b7683cd8a6203359..0703963d238e6cf75b70bb29831dfc3c4ba31a37 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Ground_2/notation.ma
+++ b/matita/matita/contribs/lambda_delta/Ground_2/notation.ma
@@ -20,10 +20,18 @@ notation "hvbox( ◊ )"
   non associative with precedence 90
   for @{'Nil}.
 
-notation "hvbox( hd break :: tl )"
+notation "hvbox( hd :: break tl )"
   right associative with precedence 47
   for @{'Cons $hd $tl}.
 
-notation "hvbox( l1 break @ l2 )"
+notation "hvbox( l1 @ break l2 )"
   right associative with precedence 47
   for @{'Append $l1 $l2 }.
+
+notation "hvbox( ⟠ )"
+  non associative with precedence 90
+  for @{'Nil2}.
+
+notation "hvbox( { hd1 , break hd2 } :: break tl )"
+  non associative with precedence 45
+  for @{'Cons $hd1 $hd2 $tl}.

diff --git a/matita/matita/contribs/lambda_delta/Ground_2/star.ma b/matita/matita/contribs/lambda_delta/Ground_2/star.ma
index 56181da2f24ee45733ef5298c3db1f65f7a5d52e..ed35806424bbb2c0bca9ae9796fc8a3521eae9a7 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Ground_2/star.ma
+++ b/matita/matita/contribs/lambda_delta/Ground_2/star.ma
@@ -14,6 +14,7 @@
 
 include "basics/star.ma".
 include "Ground_2/xoa_props.ma".
+include "Ground_2/notation.ma".
 
 (* PROPERTIES OF RELATIONS **************************************************)