From a28bc89ee87228140c6559e3dacfeaaf2ac70d1d Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 26 Dec 2011 19:54:26 +0000 Subject: [PATCH] notation and dependences bug fix --- .../Basic_2/computation/acp_aaa.ma | 2 +- .../Basic_2/computation/acp_cr.ma | 8 +++--- .../lambda_delta/Basic_2/computation/lsubc.ma | 2 +- .../lambda_delta/Basic_2/functional/subst.ma | 4 +-- .../lambda_delta/Basic_2/grammar/aarity.ma | 2 +- .../lambda_delta/Basic_2/grammar/item.ma | 2 +- .../Basic_2/grammar/term_vector.ma | 1 + .../contribs/lambda_delta/Basic_2/notation.ma | 16 +++-------- .../lambda_delta/Basic_2/static/sh.ma | 2 +- .../lambda_delta/Basic_2/unfold/ldrops.ma | 27 +++++++++++++++++++ .../lambda_delta/Basic_2/unfold/lifts.ma | 25 +++++++++++++++++ .../contribs/lambda_delta/Ground_2/list.ma | 11 ++++++-- .../lambda_delta/Ground_2/notation.ma | 12 +++++++-- .../contribs/lambda_delta/Ground_2/star.ma | 1 + 14 files changed, 88 insertions(+), 27 deletions(-) create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops.ma create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts.ma 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 537d5b235..f3863f38b 100644 --- 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 699d997dd..c45bc2591 100644 --- 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 9d38f25d7..60320a22a 100644 --- 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 05f698ff8..46d311740 100644 --- 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 42354e700..8062d8604 100644 --- 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 48ff1ec9a..08e35083d 100644 --- 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 6c9ea1ce5..01dec2102 100644 --- 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 49f126019..36f9f7652 100644 --- 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 1708b7970..7edbfd2af 100644 --- 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 index 000000000..c6bb67e79 --- /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 index 000000000..9994f44a2 --- /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 846d1f804..78a2305ea 100644 --- 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 5238b0d13..0703963d2 100644 --- 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 56181da2f..ed3580642 100644 --- 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 **************************************************) -- 2.39.2