From eae50cc815292d335df1c488a00b39ef98fa5870 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 29 Nov 2012 16:53:26 +0000 Subject: [PATCH] - bug fix in notation precedences - bug fix in the Makefile --- matita/matita/contribs/lambda_delta/Makefile | 2 +- .../apps_2/functional/{subst.ma => dsubst.ma} | 20 ++- .../lambda_delta/apps_2/functional/lift.ma | 3 +- .../apps_2/functional/notation.ma | 10 +- .../contribs/lambda_delta/basic_2/notation.ma | 156 +++++++++--------- .../contribs/lambda_delta/ground_2/arith.ma | 31 +++- .../contribs/lambda_delta/ground_2/tri.ma | 44 ----- 7 files changed, 125 insertions(+), 141 deletions(-) rename matita/matita/contribs/lambda_delta/apps_2/functional/{subst.ma => dsubst.ma} (81%) delete mode 100644 matita/matita/contribs/lambda_delta/ground_2/tri.ma diff --git a/matita/matita/contribs/lambda_delta/Makefile b/matita/matita/contribs/lambda_delta/Makefile index 3e696b6b6..7e267a2f3 100644 --- a/matita/matita/contribs/lambda_delta/Makefile +++ b/matita/matita/contribs/lambda_delta/Makefile @@ -7,7 +7,7 @@ MAC_DIR = ../../../components/binaries/mac MAC = mac.native XOA_CONF = ground_2/xoa.conf.xml -XOA_TARGETS = ground_2/xoa_natation.ma ground_2/xoa.ma +XOA_TARGETS = ground_2/xoa_notation.ma ground_2/xoa.ma ORIG = . ./orig.sh diff --git a/matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma b/matita/matita/contribs/lambda_delta/apps_2/functional/dsubst.ma similarity index 81% rename from matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma rename to matita/matita/contribs/lambda_delta/apps_2/functional/dsubst.ma index e19af6108..f5847371c 100644 --- a/matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma +++ b/matita/matita/contribs/lambda_delta/apps_2/functional/dsubst.ma @@ -15,26 +15,28 @@ include "basic_2/unfold/delift_lift.ma". include "apps_2/functional/lift.ma". -(* CORE SUBSTITUTION ********************************************************) +(* FUNCTIONAL DELIFTING SUBSTITUTION ****************************************) -let rec fsubst W d U on U ≝ match U with +let rec fdsubst W d U on U ≝ match U with [ TAtom I ⇒ match I with [ Sort _ ⇒ U | LRef i ⇒ tri … i d (#i) (↑[0, i] W) (#(i-1)) | GRef _ ⇒ U ] | TPair I V T ⇒ match I with - [ Bind2 a I ⇒ ⓑ{a,I} (fsubst W d V). (fsubst W (d+1) T) - | Flat2 I ⇒ ⓕ{I} (fsubst W d V). (fsubst W d T) + [ Bind2 a I ⇒ ⓑ{a,I} (fdsubst W d V). (fdsubst W (d+1) T) + | Flat2 I ⇒ ⓕ{I} (fdsubst W d V). (fdsubst W d T) ] ]. -interpretation "functional core substitution" 'Subst V d T = (fsubst V d T). +interpretation + "functional delifting substitution" + 'DSubst V d T = (fdsubst V d T). (* Main properties **********************************************************) -theorem fsubst_delift: ∀K,V,T,L,d. - ⇩[0, d] L ≡ K. ⓓV → L ⊢ ▼*[d, 1] T ≡ [d ← V] T. +theorem fdsubst_delift: ∀K,V,T,L,d. + ⇩[0, d] L ≡ K. ⓓV → L ⊢ ▼*[d, 1] T ≡ [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 @@ -48,8 +50,8 @@ qed. (* Main inversion properties ************************************************) -theorem fsubst_inv_delift: ∀K,V,T1,L,T2,d. ⇩[0, d] L ≡ K. ⓓV → - L ⊢ ▼*[d, 1] T1 ≡ T2 → [d ← V] T1 = T2. +theorem fdsubst_inv_delift: ∀K,V,T1,L,T2,d. ⇩[0, d] L ≡ K. ⓓV → + L ⊢ ▼*[d, 1] T1 ≡ T2 → [d ⬐ V] T1 = T2. #K #V #T1 elim T1 -T1 [ * #i #L #T2 #d #HLK #H [ -HLK >(delift_inv_sort1 … H) -H // diff --git a/matita/matita/contribs/lambda_delta/apps_2/functional/lift.ma b/matita/matita/contribs/lambda_delta/apps_2/functional/lift.ma index 361350c68..bf05ea36a 100644 --- a/matita/matita/contribs/lambda_delta/apps_2/functional/lift.ma +++ b/matita/matita/contribs/lambda_delta/apps_2/functional/lift.ma @@ -12,11 +12,10 @@ (* *) (**************************************************************************) -include "ground_2/tri.ma". include "basic_2/substitution/lift.ma". include "apps_2/functional/notation.ma". -(* RELOCATION ***************************************************************) +(* FUNCTIONAL RELOCATION ****************************************************) let rec flift d e U on U ≝ match U with [ TAtom I ⇒ match I with diff --git a/matita/matita/contribs/lambda_delta/apps_2/functional/notation.ma b/matita/matita/contribs/lambda_delta/apps_2/functional/notation.ma index 8a7274651..1c60d6c18 100644 --- a/matita/matita/contribs/lambda_delta/apps_2/functional/notation.ma +++ b/matita/matita/contribs/lambda_delta/apps_2/functional/notation.ma @@ -14,13 +14,13 @@ (* NOTATION FOR THE "functional" COMPONENT ********************************) -notation "hvbox( ↑ [ d , break e ] break term 60 T )" - non associative with precedence 60 +notation "hvbox( ↑ [ term 46 d , break term 46 e ] break term 46 T )" + non associative with precedence 46 for @{ 'Lift $d $e $T }. -notation "hvbox( [ d ← break V ] break term 60 T )" - non associative with precedence 60 - for @{ 'Subst $V $d $T }. +notation "hvbox( [ term 46 d ⬐ break term 46 V ] break term 46 T )" + non associative with precedence 46 + for @{ 'DSubst $V $d $T }. notation "hvbox( T1 ⇨ break term 46 T2 )" non associative with precedence 45 diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma index eb59a9d8f..3ff8f21e5 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/notation.ma @@ -20,7 +20,7 @@ notation "⓪" non associative with precedence 90 for @{ 'Item0 }. -notation "hvbox( ⓪ { I } )" +notation "hvbox( ⓪ { term 46 I } )" non associative with precedence 90 for @{ 'Item0 $I }. @@ -44,27 +44,27 @@ notation "hvbox( ② term 55 T1 . break term 55 T )" non associative with precedence 55 for @{ 'SnItem2 $T1 $T }. -notation "hvbox( ② { I } break term 55 T1 . break term 55 T )" +notation "hvbox( ② { term 46 I } break term 55 T1 . break term 55 T )" non associative with precedence 55 for @{ 'SnItem2 $I $T1 $T }. -notation "hvbox( ⓑ { a , I } break term 55 T1 . break term 55 T )" +notation "hvbox( ⓑ { term 46 a , term 46 I } break term 55 T1 . break term 55 T )" non associative with precedence 55 for @{ 'SnBind2 $a $I $T1 $T }. -notation "hvbox( + ⓑ { I } break term 55 T1 . break term 55 T )" +notation "hvbox( + ⓑ { term 46 I } break term 55 T1 . break term 55 T )" non associative with precedence 55 for @{ 'SnBind2Pos $I $T1 $T }. -notation "hvbox( - ⓑ { I } break term 55 T1 . break term 55 T )" +notation "hvbox( - ⓑ { term 46 I } break term 55 T1 . break term 55 T )" non associative with precedence 55 for @{ 'SnBind2Neg $I $T1 $T }. -notation "hvbox( ⓕ { I } break term 55 T1 . break term 55 T )" +notation "hvbox( ⓕ { term 46 I } break term 55 T1 . break term 55 T )" non associative with precedence 55 for @{ 'SnFlat2 $I $T1 $T }. -notation "hvbox( ⓓ { a } term 55 T1 . break term 55 T2 )" +notation "hvbox( ⓓ { term 46 a } term 55 T1 . break term 55 T2 )" non associative with precedence 55 for @{ 'SnAbbr $a $T1 $T2 }. @@ -76,7 +76,7 @@ notation "hvbox( - ⓓ term 55 T1 . break term 55 T2 )" non associative with precedence 55 for @{ 'SnAbbrNeg $T1 $T2 }. -notation "hvbox( ⓛ { a } term 55 T1 . break term 55 T2 )" +notation "hvbox( ⓛ { term 46 a } term 55 T1 . break term 55 T2 )" non associative with precedence 55 for @{ 'SnAbst $a $T1 $T2 }. @@ -88,11 +88,11 @@ notation "hvbox( - ⓛ term 55 T1 . break term 55 T2 )" non associative with precedence 55 for @{ 'SnAbstNeg $T1 $T2 }. -notation "hvbox( ⓐ term 55 T1 . break term 55 T2 )" +notation "hvbox( ⓐ term 55 T1 . break term 55 T2 )" non associative with precedence 55 for @{ 'SnAppl $T1 $T2 }. -notation "hvbox( ⓝ term 55 T1 . break term 55 T2 )" +notation "hvbox( ⓝ term 55 T1 . break term 55 T2 )" non associative with precedence 55 for @{ 'SnCast $T1 $T2 }. @@ -100,11 +100,11 @@ notation "hvbox( Ⓐ term 55 T1 . break term 55 T )" non associative with precedence 55 for @{ 'SnApplV $T1 $T }. -notation > "hvbox( T . break ②{ I } break term 47 T1 )" +notation > "hvbox( T . break ②{ term 46 I } break term 47 T1 )" non associative with precedence 46 for @{ 'DxBind2 $T $I $T1 }. -notation "hvbox( T . break ⓑ { I } break term 48 T1 )" +notation "hvbox( T . break ⓑ { term 46 I } break term 48 T1 )" non associative with precedence 47 for @{ 'DxBind2 $T $I $T1 }. @@ -116,19 +116,19 @@ notation "hvbox( T1 . break ⓛ T2 )" left associative with precedence 49 for @{ 'DxAbst $T1 $T2 }. -notation "hvbox( T . break ④ { I } break { T1 , break T2 , break T3 } )" +notation "hvbox( T . break ④ { term 46 I } break { term 46 T1 , break term 46 T2 , break term 46 T3 } )" non associative with precedence 50 for @{ 'DxItem4 $T $I $T1 $T2 $T3 }. -notation "hvbox( # { x } )" +notation "hvbox( # { term 46 x } )" non associative with precedence 90 for @{ 'Weight $x }. -notation "hvbox( # { x , break y } )" +notation "hvbox( # { term 46 x , break term 46 y } )" non associative with precedence 90 for @{ 'Weight $x $y }. -notation "hvbox( 𝐒 ⦃ T ⦄ )" +notation "hvbox( 𝐒 ⦃ term 46 T ⦄ )" non associative with precedence 45 for @{ 'Simple $T }. @@ -142,41 +142,41 @@ notation "hvbox( T1 ≃ break term 46 T2 )" (* Substitution *************************************************************) -notation "hvbox( ⇧ [ d , break e ] break term 46 T1 ≡ break term 46 T2 )" +notation "hvbox( ⇧ [ term 46 d , break term 46 e ] break term 46 T1 ≡ break term 46 T2 )" non associative with precedence 45 for @{ 'RLift $d $e $T1 $T2 }. -notation "hvbox( T1 break ≼ [ d , break e ] break term 46 T2 )" +notation "hvbox( T1 break ≼ [ term 46 d , break term 46 e ] break term 46 T2 )" non associative with precedence 45 for @{ 'SubEq $T1 $d $e $T2 }. -notation "hvbox( ≽ [ d , break e ] break term 46 T2 )" +notation "hvbox( ≽ [ term 46 d , break term 46 e ] break term 46 T2 )" non associative with precedence 45 for @{ 'SubEqBottom $d $e $T2 }. -notation "hvbox( ⇩ [ e ] break term 46 L1 ≡ break term 46 L2 )" +notation "hvbox( ⇩ [ term 46 e ] break term 46 L1 ≡ break term 46 L2 )" non associative with precedence 45 for @{ 'RDrop $e $L1 $L2 }. -notation "hvbox( ⇩ [ d , break e ] break term 46 L1 ≡ break term 46 L2 )" +notation "hvbox( ⇩ [ term 46 d , break term 46 e ] break term 46 L1 ≡ break term 46 L2 )" non associative with precedence 45 for @{ 'RDrop $d $e $L1 $L2 }. -notation "hvbox( ⦃ L1, break T1 ⦄ ⧁ break ⦃ L2 , break T2 ⦄ )" +notation "hvbox( ⦃ term 46 L1, break term 46 T1 ⦄ ⧁ break ⦃ term 46 L2 , break term 46 T2 ⦄ )" non associative with precedence 45 for @{ 'RestSupTerm $L1 $T1 $L2 $T2 }. -notation "hvbox( L ⊢ break ⌘ ⦃ T ⦄ ≡ break term 46 k )" +notation "hvbox( L ⊢ break ⌘ ⦃ term 46 T ⦄ ≡ break term 46 k )" non associative with precedence 45 for @{ 'ICM $L $T $k }. -notation "hvbox( L ⊢ break term 46 T1 break ▶ [ d , break e ] break term 46 T2 )" +notation "hvbox( L ⊢ break term 46 T1 break ▶ [ term 46 d , break term 46 e ] break term 46 T2 )" non associative with precedence 45 for @{ 'PSubst $L $T1 $d $e $T2 }. (* Unfold *******************************************************************) -notation "hvbox( @ ⦃ T1 , break f ⦄ ≡ break term 46 T2 )" +notation "hvbox( @ ⦃ term 46 T1 , break term 46 f ⦄ ≡ break term 46 T2 )" non associative with precedence 45 for @{ 'RAt $T1 $f $T2 }. @@ -184,55 +184,55 @@ notation "hvbox( T1 ▭ break term 46 T2 ≡ break term 46 T )" non associative with precedence 45 for @{ 'RMinus $T1 $T2 $T }. -notation "hvbox( ⇧ * [ e ] break term 46 T1 ≡ break term 46 T2 )" +notation "hvbox( ⇧ * [ term 46 e ] break term 46 T1 ≡ break term 46 T2 )" non associative with precedence 45 for @{ 'RLiftStar $e $T1 $T2 }. -notation "hvbox( ⇩ * [ e ] break term 46 L1 ≡ break term 46 L2 )" +notation "hvbox( ⇩ * [ term 46 e ] break term 46 L1 ≡ break term 46 L2 )" non associative with precedence 45 for @{ 'RDropStar $e $L1 $L2 }. -notation "hvbox( ⦃ L1, break T1 ⦄ ⧁ + break ⦃ L2 , break T2 ⦄ )" +notation "hvbox( ⦃ term 46 L1, break term 46 T1 ⦄ ⧁ + break ⦃ term 46 L2 , break term 46 T2 ⦄ )" non associative with precedence 45 for @{ 'RestSupTermPlus $L1 $T1 $L2 $T2 }. -notation "hvbox( ⦃ L1, break T1 ⦄ ⧁ * break ⦃ L2 , break T2 ⦄ )" +notation "hvbox( ⦃ term 46 L1, break term 46 T1 ⦄ ⧁ * break ⦃ term 46 L2 , break term 46 T2 ⦄ )" non associative with precedence 45 for @{ 'RestSupTermStar $L1 $T1 $L2 $T2 }. -notation "hvbox( T1 break ▶ * [ d , break e ] break term 46 T2 )" +notation "hvbox( T1 break ▶ * [ term 46 d , break term 46 e ] break term 46 T2 )" non associative with precedence 45 for @{ 'PSubstStar $T1 $d $e $T2 }. -notation "hvbox( L ⊢ break term 46 T1 break ▶ * [ d , break e ] break term 46 T2 )" +notation "hvbox( L ⊢ break term 46 T1 break ▶ * [ term 46 d , break term 46 e ] break term 46 T2 )" non associative with precedence 45 for @{ 'PSubstStar $L $T1 $d $e $T2 }. -notation "hvbox( L ⊢ break term 46 T1 break ▶ ▶ * [ d , break e ] break term 46 T2 )" +notation "hvbox( L ⊢ break term 46 T1 break ▶ ▶ * [ term 46 d , break term 46 e ] break term 46 T2 )" non associative with precedence 45 for @{ 'PSubstStarAlt $L $T1 $d $e $T2 }. -notation "hvbox( T1 break ⊢ ▶ * [ d , break e ] break term 46 T2 )" +notation "hvbox( T1 break ⊢ ▶ * [ term 46 d , break term 46 e ] break term 46 T2 )" non associative with precedence 45 for @{ 'PSubstStarSn $T1 $d $e $T2 }. -notation "hvbox( T1 break ⊢ ▶ ▶ * [ d , break e ] break term 46 T2 )" +notation "hvbox( T1 break ⊢ ▶ ▶ * [ term 46 d , break term 46 e ] break term 46 T2 )" non associative with precedence 45 for @{ 'PSubstStarSnAlt $T1 $d $e $T2 }. -notation "hvbox( ▼ * [ d , break e ] break term 46 T1 ≡ break term 46 T2 )" +notation "hvbox( ▼ * [ term 46 d , break term 46 e ] break term 46 T1 ≡ break term 46 T2 )" non associative with precedence 45 for @{ 'TSubst $T1 $d $e $T2 }. -notation "hvbox( L ⊢ break ▼ * [ d , break e ] break term 46 T1 ≡ break term 46 T2 )" +notation "hvbox( L ⊢ break ▼ * [ term 46 d , break term 46 e ] break term 46 T1 ≡ break term 46 T2 )" non associative with precedence 45 for @{ 'TSubst $L $T1 $d $e $T2 }. -notation "hvbox( ▼ ▼ * [ d , break e ] break term 46 T1 ≡ break term 46 T2 )" +notation "hvbox( ▼ ▼ * [ term 46 d , break term 46 e ] break term 46 T1 ≡ break term 46 T2 )" non associative with precedence 45 for @{ 'TSubstAlt $T1 $d $e $T2 }. -notation "hvbox( L ⊢ break ▼ ▼ * [ d , break e ] break term 46 T1 ≡ break term 46 T2 )" +notation "hvbox( L ⊢ break ▼ ▼ * [ term 46 d , break term 46 e ] break term 46 T1 ≡ break term 46 T2 )" non associative with precedence 45 for @{ 'TSubstAlt $L $T1 $d $e $T2 }. @@ -246,7 +246,7 @@ notation "hvbox( T1 ⁝ ⊑ break term 46 T2 )" non associative with precedence 45 for @{ 'CrSubEqA $T1 $T2 }. -notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T ÷ break term 46 A )" +notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T ÷ break term 46 A )" non associative with precedence 45 for @{ 'BinaryArity $h $L $T $A }. @@ -254,11 +254,11 @@ notation "hvbox( h ⊢ break term 46 L1 ÷ ⊑ break term 46 L2 )" non associative with precedence 45 for @{ 'CrSubEqB $h $L1 $L2 }. -notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 • break [ g , break l ] break term 46 T2 )" +notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 • break [ term 46 g , break term 46 l ] break term 46 T2 )" non associative with precedence 45 for @{ 'StaticType $h $g $l $L $T1 $T2 }. -notation "hvbox( h ⊢ break term 46 L1 • ⊑ [ g ] break term 46 L2 )" +notation "hvbox( h ⊢ break term 46 L1 • ⊑ [ term 46 g ] break term 46 L2 )" non associative with precedence 45 for @{ 'CrSubEqS $h $g $L1 $L2 }. @@ -270,45 +270,45 @@ notation "hvbox( L1 ⊢ ⧫ * break term 46 T ≡ break term 46 L2 )" (* Reducibility *************************************************************) -notation "hvbox( L ⊢ break 𝐑 ⦃ T ⦄ )" +notation "hvbox( L ⊢ break 𝐑 ⦃ term 46 T ⦄ )" non associative with precedence 45 for @{ 'Reducible $L $T }. -notation "hvbox( L ⊢ break 𝐈 ⦃ T ⦄ )" +notation "hvbox( L ⊢ break 𝐈 ⦃ term 46 T ⦄ )" non associative with precedence 45 for @{ 'NotReducible $L $T }. -notation "hvbox( L ⊢ break 𝐍 ⦃ T ⦄ )" +notation "hvbox( L ⊢ break 𝐍 ⦃ term 46 T ⦄ )" non associative with precedence 45 for @{ 'Normal $L $T }. (* this might be removed *) -notation "hvbox( 𝐇𝐑 ⦃ T ⦄ )" +notation "hvbox( 𝐇𝐑 ⦃ term 46 T ⦄ )" non associative with precedence 45 for @{ 'HdReducible $T }. (* this might be removed *) -notation "hvbox( L ⊢ break 𝐇𝐑 ⦃ T ⦄ )" +notation "hvbox( L ⊢ break 𝐇𝐑 ⦃ term 46 T ⦄ )" non associative with precedence 45 for @{ 'HdReducible $L $T }. (* this might be removed *) -notation "hvbox( 𝐇𝐈 ⦃ T ⦄ )" +notation "hvbox( 𝐇𝐈 ⦃ term 46 T ⦄ )" non associative with precedence 45 for @{ 'NotHdReducible $T }. (* this might be removed *) -notation "hvbox( L ⊢ break 𝐇𝐈 ⦃ T ⦄ )" +notation "hvbox( L ⊢ break 𝐇𝐈 ⦃ term 46 T ⦄ )" non associative with precedence 45 for @{ 'NotHdReducible $L $T }. (* this might be removed *) -notation "hvbox( 𝐇𝐍 ⦃ T ⦄ )" +notation "hvbox( 𝐇𝐍 ⦃ term 46 T ⦄ )" non associative with precedence 45 for @{ 'HdNormal $T }. (* this might be removed *) -notation "hvbox( L ⊢ break 𝐇𝐍 ⦃ T ⦄ )" +notation "hvbox( L ⊢ break 𝐇𝐍 ⦃ term 46 T ⦄ )" non associative with precedence 45 for @{ 'HdNormal $L $T }. @@ -320,23 +320,23 @@ notation "hvbox( L ⊢ break term 46 T1 ➡ break term 46 T2 )" non associative with precedence 45 for @{ 'PRed $L $T1 $T2 }. -notation "hvbox( ⦃ L1 ⦄ ➡ break ⦃ L2 ⦄ )" +notation "hvbox( ⦃ term 46 L1 ⦄ ➡ break ⦃ term 46 L2 ⦄ )" non associative with precedence 45 for @{ 'FocalizedPRed $L1 $L2 }. -notation "hvbox( ⦃ L1, break T1 ⦄ ➡ break ⦃ L2 , break T2 ⦄ )" +notation "hvbox( ⦃ term 46 L1, break term 46 T1 ⦄ ➡ break ⦃ term 46 L2 , break term 46 T2 ⦄ )" non associative with precedence 45 for @{ 'FocalizedPRed $L1 $T1 $L2 $T2 }. -notation "hvbox( L ⊢ break ⦃ L1, break T1 ⦄ ➡ break ⦃ L2 , break T2 ⦄ )" +notation "hvbox( L ⊢ break ⦃ term 46 L1, break term 46 T1 ⦄ ➡ break ⦃ term 46 L2 , break term 46 T2 ⦄ )" non associative with precedence 45 for @{ 'FocalizedPRed $L $L1 $T1 $L2 $T2 }. -notation "hvbox( ⦃ L1 ⦄ ➡ ➡ break ⦃ L2 ⦄ )" +notation "hvbox( ⦃ term 46 L1 ⦄ ➡ ➡ break ⦃ term 46 L2 ⦄ )" non associative with precedence 45 for @{ 'FocalizedPRedAlt $L1 $L2 }. -notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 • ➡ break [ g ] break term 46 T2 )" +notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 • ➡ break [ term 46 g ] break term 46 T2 )" non associative with precedence 45 for @{ 'XPRed $h $g $L $T1 $T2 }. @@ -354,23 +354,23 @@ notation "hvbox( T1 ➡ ➡ * break term 46 T2 )" non associative with precedence 45 for @{ 'PRedStarAlt $T1 $T2 }. -notation "hvbox( ⦃ L1 ⦄ ➡ * break ⦃ L2 ⦄ )" +notation "hvbox( ⦃ term 46 L1 ⦄ ➡ * break ⦃ term 46 L2 ⦄ )" non associative with precedence 45 for @{ 'FocalizedPRedStar $L1 $L2 }. -notation "hvbox( ⦃ L1 , T1 ⦄ ➡ * break ⦃ L2 , T2 ⦄ )" +notation "hvbox( ⦃ term 46 L1 , term 46 T1 ⦄ ➡ * break ⦃ term 46 L2 , term 46 T2 ⦄ )" non associative with precedence 45 for @{ 'FocalizedPRedStar $L1 $T1 $L2 $T2 }. -notation "hvbox( ⦃ L1 ⦄ ➡ ➡ * break ⦃ L2 ⦄ )" +notation "hvbox( ⦃ term 46 L1 ⦄ ➡ ➡ * break ⦃ term 46 L2 ⦄ )" non associative with precedence 45 for @{ 'FocalizedPRedStarAlt $L1 $L2 }. -notation "hvbox( ⦃ L1 , T1 ⦄ ➡ ➡ * break ⦃ L2 , T2 ⦄ )" +notation "hvbox( ⦃ term 46 L1 , term 46 T1 ⦄ ➡ ➡ * break ⦃ term 46 L2 , term 46 T2 ⦄ )" non associative with precedence 45 for @{ 'FocalizedPRedStarAlt $L1 $T1 $L2 $T2 }. -notation "hvbox( L ⊢ break term 46 T1 ➡ * break 𝐍 ⦃ T2 ⦄ )" +notation "hvbox( L ⊢ break term 46 T1 ➡ * break 𝐍 ⦃ Tterm 46 2 ⦄ )" non associative with precedence 45 for @{ 'PEval $L $T1 $T2 }. @@ -386,19 +386,19 @@ notation "hvbox( L ⊢ ⬊ ⬊ * break term 46 T )" non associative with precedence 45 for @{ 'SNAlt $L $T }. -notation "hvbox( ⦃ L, break T ⦄ ϵ break [ R ] break 〚 A 〛 )" +notation "hvbox( ⦃ term 46 L, break term 46 T ⦄ ϵ break [ term 46 R ] break 〚term 46 A 〛 )" non associative with precedence 45 for @{ 'InEInt $R $L $T $A }. -notation "hvbox( T1 ⊑ break [ R ] break term 46 T2 )" +notation "hvbox( T1 ⊑ break [ term 46 R ] break term 46 T2 )" non associative with precedence 45 for @{ 'CrSubEq $T1 $R $T2 }. -notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 • ➡ * break [ g ] break term 46 T2 )" +notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 • ➡ * break [ term 46 g ] break term 46 T2 )" non associative with precedence 45 for @{ 'XPRedStar $h $g $L $T1 $T2 }. -notation "hvbox( ⦃ h , break L ⦄ ⊢ • ⬊ * break [ g ] break term 46 T2 )" +notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ • ⬊ * break [ term 46 g ] break term 46 T2 )" non associative with precedence 45 for @{ 'XSN $h $g $L $T }. @@ -408,19 +408,19 @@ notation "hvbox( L ⊢ break term 46 T1 ⬌ break term 46 T2 )" non associative with precedence 45 for @{ 'PConv $L $T1 $T2 }. -notation "hvbox( ⦃ L1 ⦄ ⬌ break ⦃ L2 ⦄ )" +notation "hvbox( ⦃ term 46 L1 ⦄ ⬌ break ⦃ term 46 L2 ⦄ )" non associative with precedence 45 for @{ 'FocalizedPConv $L1 $L2 }. -notation "hvbox( ⦃ L1 , break T1 ⦄ ⬌ break ⦃ L2 , break T2 ⦄ )" +notation "hvbox( ⦃ term 46 L1 , break term 46 T1 ⦄ ⬌ break ⦃ term 46 L2 , break term 46 T2 ⦄ )" non associative with precedence 45 for @{ 'FocalizedPConv $L1 $T1 $L2 $T2 }. -notation "hvbox( ⦃ L1 ⦄ ⬌ ⬌ break ⦃ L2 ⦄ )" +notation "hvbox( ⦃ term 46 L1 ⦄ ⬌ ⬌ break ⦃ term 46 L2 ⦄ )" non associative with precedence 45 for @{ 'FocalizedPConvAlt $L1 $L2 }. -notation "hvbox( ⦃ L1 , break T1 ⦄ ⬌ ⬌ break ⦃ L2 , break T2 ⦄ )" +notation "hvbox( ⦃ term 46 L1 , break term 46 T1 ⦄ ⬌ ⬌ break ⦃ term 46 L2 , break term 46 T2 ⦄ )" non associative with precedence 45 for @{ 'FocalizedPConvAlt $L1 $T1 $L2 $T2 }. @@ -430,46 +430,46 @@ notation "hvbox( L ⊢ break term 46 T1 ⬌* break term 46 T2 )" non associative with precedence 45 for @{ 'PConvStar $L $T1 $T2 }. -notation "hvbox( h ⊢ break term 46 L1 ⊢ • ⊑ [ g ] break term 46 L2 )" +notation "hvbox( h ⊢ break term 46 L1 ⊢ • ⊑ [ term 46 g ] break term 46 L2 )" non associative with precedence 45 for @{ 'CrSubEqSE $h $g $L1 $L2 }. -notation "hvbox( ⦃ L1 ⦄ ⬌ * break ⦃ L2 ⦄ )" +notation "hvbox( ⦃ term 46 L1 ⦄ ⬌ * break ⦃ term 46 L2 ⦄ )" non associative with precedence 45 for @{ 'FocalizedPConvStar $L1 $L2 }. -notation "hvbox( ⦃ L1 , break T1 ⦄ ⬌ * break ⦃ L2 , break T2 ⦄ )" +notation "hvbox( ⦃ term 46 L1 , break term 46 T1 ⦄ ⬌ * break ⦃ term 46 L2 , break term 46 T2 ⦄ )" non associative with precedence 45 for @{ 'FocalizedPConvStar $L1 $T1 $L2 $T2 }. -notation "hvbox( ⦃ L1 ⦄ ⬌ ⬌ * break ⦃ L2 ⦄ )" +notation "hvbox( ⦃ term 46 L1 ⦄ ⬌ ⬌ * break ⦃ term 46 L2 ⦄ )" non associative with precedence 45 for @{ 'FocalizedPConvStarAlt $L1 $L2 }. -notation "hvbox( ⦃ L1 , break T1 ⦄ ⬌ ⬌ * break ⦃ L2 , break T2 ⦄ )" +notation "hvbox( ⦃ term 46 L1 , break term 46 T1 ⦄ ⬌ ⬌ * break ⦃ term 46 L2 , break term 46 T2 ⦄ )" non associative with precedence 45 for @{ 'FocalizedPConvStarAlt $L1 $T1 $L2 $T2 }. (* Dynamic typing ***********************************************************) -notation "hvbox( ⦃ h , break L ⦄ ⊩ break term 46 T : break [ g ] )" +notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊩ break term 46 T : break [ term 46 g ] )" non associative with precedence 45 for @{ 'NativeValid $h $g $L $T }. -notation "hvbox( h ⊢ break term 46 L1 ⊩ : ⊑ [ g ] break term 46 L2 )" +notation "hvbox( h ⊢ break term 46 L1 ⊩ : ⊑ [ term 46 g ] break term 46 L2 )" non associative with precedence 45 for @{ 'CrSubEqV $h $g $L1 $L2 }. -notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 : break term 46 T2 )" +notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 : break term 46 T2 )" non associative with precedence 45 for @{ 'NativeType $h $L $T1 $T2 }. -notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 : : break term 46 T2 )" +notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 : : break term 46 T2 )" non associative with precedence 45 for @{ 'NativeTypeAlt $h $L $T1 $T2 }. (* Higher order dynamic typing **********************************************) -notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 : * break term 46 T2 )" +notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 : * break term 46 T2 )" non associative with precedence 45 for @{ 'NativeTypeStar $h $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambda_delta/ground_2/arith.ma b/matita/matita/contribs/lambda_delta/ground_2/arith.ma index ad3ab4a3d..8afc445b8 100644 --- a/matita/matita/contribs/lambda_delta/ground_2/arith.ma +++ b/matita/matita/contribs/lambda_delta/ground_2/arith.ma @@ -44,7 +44,7 @@ lemma arith_h1: ∀a1,a2,b,c1. c1 ≤ a1 → c1 ≤ b → #a1 #a2 #b #c1 #H1 #H2 >plus_minus // /2 width=1/ qed. -(* inversion & forward lemmas ***********************************************) +(* Inversion & forward lemmas ***********************************************) axiom eq_nat_dec: ∀n1,n2:nat. Decidable (n1 = n2). @@ -80,7 +80,7 @@ qed-. lemma plus_xySz_x_false: ∀z,x,y. x + y + S z = x → ⊥. /2 width=4 by le_plus_xySz_x_false/ qed-. -(* iterators ****************************************************************) +(* Iterators ****************************************************************) (* Note: see also: lib/arithemetcs/bigops.ma *) let rec iter (n:nat) (B:Type[0]) (op: B → B) (nil: B) ≝ @@ -98,3 +98,30 @@ qed. lemma iter_n_Sm: ∀B:Type[0]. ∀f:B→B. ∀b,l. f^l (f b) = f (f^l b). #B #f #b #l elim l -l normalize // qed. + +(* Trichotomy operator ******************************************************) + +(* Note: this is "if eqb n1 n2 then a2 else if leb n1 n2 then a1 else a3" *) +let rec tri (A:Type[0]) n1 n2 a1 a2 a3 on n1 : A ≝ + match n1 with + [ O ⇒ match n2 with [ O ⇒ a2 | S n2 ⇒ a1 ] + | S n1 ⇒ match n2 with [ O ⇒ a3 | S n2 ⇒ tri A n1 n2 a1 a2 a3 ] + ]. + +lemma tri_lt: ∀A,a1,a2,a3,n2,n1. n1 < n2 → tri A n1 n2 a1 a2 a3 = a1. +#A #a1 #a2 #a3 #n2 elim n2 -n2 +[ #n1 #H elim (lt_zero_false … H) +| #n2 #IH #n1 elim n1 -n1 // /3 width=1/ +] +qed. + +lemma tri_eq: ∀A,a1,a2,a3,n. tri A n n a1 a2 a3 = a2. +#A #a1 #a2 #a3 #n elim n -n normalize // +qed. + +lemma tri_gt: ∀A,a1,a2,a3,n1,n2. n2 < n1 → tri A n1 n2 a1 a2 a3 = a3. +#A #a1 #a2 #a3 #n1 elim n1 -n1 +[ #n2 #H elim (lt_zero_false … H) +| #n1 #IH #n2 elim n2 -n2 // /3 width=1/ +] +qed. diff --git a/matita/matita/contribs/lambda_delta/ground_2/tri.ma b/matita/matita/contribs/lambda_delta/ground_2/tri.ma deleted file mode 100644 index 4fc619565..000000000 --- a/matita/matita/contribs/lambda_delta/ground_2/tri.ma +++ /dev/null @@ -1,44 +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/arith.ma". - -(* TRICOTOMY FUNCTION *******************************************************) - -let rec tri (A:Type[0]) m n a b c on m : A ≝ - match m with - [ O ⇒ match n with [ O ⇒ b | S n ⇒ a ] - | S m ⇒ match n with [ O ⇒ c | S n ⇒ tri A m n a b c ] - ]. - -(* Basic properties *********************************************************) - -lemma tri_lt: ∀A,a,b,c,n,m. m < n → tri A m n a b c = a. -#A #a #b #c #n elim n -n -[ #m #H elim (lt_zero_false … H) -| #n #IH #m elim m -m // /3 width=1/ -] -qed. - -lemma tri_eq: ∀A,a,b,c,m. tri A m m a b c = b. -#A #a #b #c #m elim m -m normalize // -qed. - -lemma tri_gt: ∀A,a,b,c,m,n. n < m → tri A m n a b c = c. -#A #a #b #c #m elim m -m -[ #n #H elim (lt_zero_false … H) -| #m #IH #n elim n -n // /3 width=1/ -] -qed. - -- 2.39.2