- bug fix in notation precedences

- bug fix in the Makefile

diff --git a/matita/matita/contribs/lambda_delta/Makefile b/matita/matita/contribs/lambda_delta/Makefile
index 3e696b6b67bd0dae0cde666445cc46749693f0fa..7e267a2f31c6157d713f2c726ea6017ebd790f20 100644 (file)
--- 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/dsubst.ma b/matita/matita/contribs/lambda_delta/apps_2/functional/dsubst.ma
new file mode 100644 (file)
index 0000000..f584737
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/apps_2/functional/dsubst.ma
@@ -0,0 +1,75 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/unfold/delift_lift.ma".
+include "apps_2/functional/lift.ma".
+
+(* FUNCTIONAL DELIFTING SUBSTITUTION ****************************************)
+
+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} (fdsubst W d V). (fdsubst W (d+1) T)
+  | Flat2 I   ⇒ ⓕ{I} (fdsubst W d V). (fdsubst W d T)
+  ]
+].
+
+interpretation
+   "functional delifting substitution"
+   'DSubst V d T = (fdsubst V d T).
+
+(* Main properties **********************************************************)
+
+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
+  [ -HLK >(tri_lt ?????? Hid) /3 width=3/
+  | destruct >tri_eq /4 width=4 by tpss_strap2, tps_subst, le_n, ex2_1_intro/ (**) (* too slow without trace *)   
+  | -HLK >(tri_gt ?????? Hid) /3 width=3/
+  ]
+| * /3 width=1/ /4 width=1/
+]
+qed.
+
+(* Main inversion properties ************************************************)
+
+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 //
+  | elim (lt_or_eq_or_gt i d) #Hid normalize
+    [ -HLK >(delift_inv_lref1_lt … H) -H // /2 width=1/
+    | destruct
+      elim (delift_inv_lref1_be … H ? ?) -H // #K0 #V0 #V2 #HLK0
+      lapply (ldrop_mono … HLK0 … HLK) -HLK0 -HLK #H >minus_plus <minus_n_n #HV2 #HVT2 destruct
+      >(delift_inv_refl_O2 … HV2) -V >(flift_inv_lift … HVT2) -V2 //
+    | -HLK >(delift_inv_lref1_ge … H) -H // /2 width=1/
+    ]
+  | -HLK >(delift_inv_gref1 … H) -H //
+  ]
+| * [ #a ] #I #V1 #T1 #IHV1 #IHT1 #L #X #d #HLK #H
+  [ elim (delift_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+    <(IHV1 … HV12) -IHV1 -HV12 // <(IHT1 … HT12) -IHT1 -HT12 // /2 width=1/
+  | elim (delift_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+    <(IHV1 … HV12) -IHV1 -HV12 // <(IHT1 … HT12) -IHT1 -HT12 //
+  ]
+]
+qed-.

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 361350c688d580d5f85c45b6594392d7b561753c..bf05ea36a2765cbcd37e568bb8508380aebff48f 100644 (file)
--- 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 8a72746511c40700f7cf826e81d9701fb4082d46..1c60d6c18e4802730297b69182a67c8d6da9f752 100644 (file)
--- 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/apps_2/functional/subst.ma b/matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma
deleted file mode 100644 (file)
index e19af61..0000000
--- a/matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma
+++ /dev/null
@@ -1,73 +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 "basic_2/unfold/delift_lift.ma".
-include "apps_2/functional/lift.ma".
-
-(* CORE SUBSTITUTION ********************************************************)
-
-let rec fsubst 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)
-  ]
-].
-
-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. ⓓ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
-  [ -HLK >(tri_lt ?????? Hid) /3 width=3/
-  | destruct >tri_eq /4 width=4 by tpss_strap2, tps_subst, le_n, ex2_1_intro/ (**) (* too slow without trace *)   
-  | -HLK >(tri_gt ?????? Hid) /3 width=3/
-  ]
-| * /3 width=1/ /4 width=1/
-]
-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.
-#K #V #T1 elim T1 -T1
-[ * #i #L #T2 #d #HLK #H
-  [ -HLK >(delift_inv_sort1 … H) -H //
-  | elim (lt_or_eq_or_gt i d) #Hid normalize
-    [ -HLK >(delift_inv_lref1_lt … H) -H // /2 width=1/
-    | destruct
-      elim (delift_inv_lref1_be … H ? ?) -H // #K0 #V0 #V2 #HLK0
-      lapply (ldrop_mono … HLK0 … HLK) -HLK0 -HLK #H >minus_plus <minus_n_n #HV2 #HVT2 destruct
-      >(delift_inv_refl_O2 … HV2) -V >(flift_inv_lift … HVT2) -V2 //
-    | -HLK >(delift_inv_lref1_ge … H) -H // /2 width=1/
-    ]
-  | -HLK >(delift_inv_gref1 … H) -H //
-  ]
-| * [ #a ] #I #V1 #T1 #IHV1 #IHT1 #L #X #d #HLK #H
-  [ elim (delift_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
-    <(IHV1 … HV12) -IHV1 -HV12 // <(IHT1 … HT12) -IHT1 -HT12 // /2 width=1/
-  | elim (delift_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
-    <(IHV1 … HV12) -IHV1 -HV12 // <(IHT1 … HT12) -IHT1 -HT12 //
-  ]
-]
-qed-.

diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma
index eb59a9d8f9bbc2bd55953ca26839913ad5c4db4f..3ff8f21e555ec1a47cc980c76bf5585c50911562 100644 (file)
--- 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 ad3ab4a3d5dab681e6971977d0d3e078251275ec..8afc445b8f4343d68494ce3e774ebc8beb196c9c 100644 (file)
--- 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 (file)
index 4fc6195..0000000
--- 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.
-