From baccd5a2f3b79c295b1f9444575bfb351577634e Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 7 Aug 2011 20:44:42 +0000 Subject: [PATCH] - cpr is now defined and the cpr_flat propery is proved! (it did not hold in the first version of the calculus because cpr (aka pr2) was badly designed). - relocation properties of tpr closed! - fixed bug in drop (base case was too restrictive) - some refactoring --- matita/matita/lib/lambda-delta/notation.ma | 12 +- .../matita/lib/lambda-delta/reduction/cpr.ma | 53 +++++++ .../reduction/{lpr_defs.ma => lpr.ma} | 2 +- .../reduction/{tpr_defs.ma => tpr.ma} | 2 +- .../lib/lambda-delta/reduction/tpr_lift.ma | 102 ++++++++++++++ .../lib/lambda-delta/reduction/tpr_main.ma | 130 ------------------ .../lib/lambda-delta/reduction/tpr_pts.ma | 2 +- .../lib/lambda-delta/reduction/tpr_tpr.ma | 2 +- .../substitution/{drop_defs.ma => drop.ma} | 40 ++++-- .../{drop_main.ma => drop_drop.ma} | 21 ++- .../substitution/{leq_defs.ma => leq.ma} | 0 .../substitution/{lift_defs.ma => lift.ma} | 19 +++ .../{lift_main.ma => lift_lift.ma} | 21 +-- .../lambda-delta/substitution/lift_weight.ma | 2 +- .../substitution/{pts_defs.ma => pts.ma} | 2 +- .../lib/lambda-delta/substitution/pts_lift.ma | 8 +- .../matita/lib/lambda-delta/syntax/length.ma | 22 +++ matita/matita/lib/lambda-delta/xoa.conf.xml | 2 +- .../lib/lambda-delta/{xoa_defs.ma => xoa.ma} | 0 matita/matita/lib/lambda-delta/xoa_props.ma | 2 +- 20 files changed, 258 insertions(+), 186 deletions(-) create mode 100644 matita/matita/lib/lambda-delta/reduction/cpr.ma rename matita/matita/lib/lambda-delta/reduction/{lpr_defs.ma => lpr.ma} (97%) rename matita/matita/lib/lambda-delta/reduction/{tpr_defs.ma => tpr.ma} (99%) create mode 100644 matita/matita/lib/lambda-delta/reduction/tpr_lift.ma delete mode 100644 matita/matita/lib/lambda-delta/reduction/tpr_main.ma rename matita/matita/lib/lambda-delta/substitution/{drop_defs.ma => drop.ma} (82%) rename matita/matita/lib/lambda-delta/substitution/{drop_main.ma => drop_drop.ma} (87%) rename matita/matita/lib/lambda-delta/substitution/{leq_defs.ma => leq.ma} (100%) rename matita/matita/lib/lambda-delta/substitution/{lift_defs.ma => lift.ma} (90%) rename matita/matita/lib/lambda-delta/substitution/{lift_main.ma => lift_lift.ma} (88%) rename matita/matita/lib/lambda-delta/substitution/{pts_defs.ma => pts.ma} (98%) create mode 100644 matita/matita/lib/lambda-delta/syntax/length.ma rename matita/matita/lib/lambda-delta/{xoa_defs.ma => xoa.ma} (100%) diff --git a/matita/matita/lib/lambda-delta/notation.ma b/matita/matita/lib/lambda-delta/notation.ma index 86e31894c..375d06abc 100644 --- a/matita/matita/lib/lambda-delta/notation.ma +++ b/matita/matita/lib/lambda-delta/notation.ma @@ -11,7 +11,7 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -(* *****************************************************************) +(* Syntax *******************************************************************) notation "hvbox( ⋆ )" non associative with precedence 90 @@ -36,7 +36,11 @@ notation "hvbox( 𝕗 { I } break (term 90 T1) . break (term 90 T) )" notation "hvbox( T . break 𝕓 { I } break (term 90 T1) )" non associative with precedence 89 for @{ 'DBind $T $I $T1 }. - +(* +notation "hvbox( | L | )" + non associative with precedence 70 + for @{ 'Length $L }. +*) notation "hvbox( # term 90 x )" non associative with precedence 90 for @{ 'Weight $x }. @@ -45,7 +49,7 @@ notation "hvbox( # [ x , break y ] )" non associative with precedence 90 for @{ 'Weight $x $y }. -(* substitution *************************************************************) +(* Substitution *************************************************************) notation "hvbox( T1 break [ d , break e ] ≈ break T2 )" non associative with precedence 45 @@ -63,7 +67,7 @@ notation "hvbox( L ⊢ break term 90 T1 break [ d , break e ] ≫ break T2 )" non associative with precedence 45 for @{ 'PSubst $L $T1 $d $e $T2 }. -(* reduction ****************************************************************) +(* Reduction ****************************************************************) notation "hvbox( T1 ⇒ break T2 )" non associative with precedence 45 diff --git a/matita/matita/lib/lambda-delta/reduction/cpr.ma b/matita/matita/lib/lambda-delta/reduction/cpr.ma new file mode 100644 index 000000000..80ccfd947 --- /dev/null +++ b/matita/matita/lib/lambda-delta/reduction/cpr.ma @@ -0,0 +1,53 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| This file is distributed under the terms of the + \ / GNU General Public License Version 2 + \ / + V_______________________________________________________________ *) + +include "lambda-delta/syntax/length.ma". +include "lambda-delta/reduction/tpr.ma". + +(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************) + +definition cpr: lenv → term → term → Prop ≝ + λL,T1,T2. ∃∃T. T1 ⇒ T & L ⊢ T [0, |L|] ≫ T2. + +interpretation + "context-sensitive parallel reduction (term)" + 'PRed L T1 T2 = (cpr L T1 T2). + +(* Basic properties *********************************************************) + +lemma cpr_pr: ∀T1,T2. T1 ⇒ T2 → ∀L. L ⊢ T1 ⇒ T2. +/2/ qed. + +axiom cpr_pts: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → L ⊢ T1 ⇒ T2. + +lemma cpr_refl: ∀L,T. L ⊢ T ⇒ T. +/2/ qed. + +(* NOTE: new property *) +lemma cpr_flat: ∀I,L,V1,V2,T1,T2. + L ⊢ V1 ⇒ V2 → L ⊢ T1 ⇒ T2 → L ⊢ 𝕗{I} V1. T1 ⇒ 𝕗{I} V2. T2. +#I #L #V1 #V2 #T1 #T2 * #V #HV1 #HV2 * /3 width=5/ +qed. + +axiom cpr_delta: ∀L,K,V0,V,i. + ↓[0, i] L ≡ K. 𝕓{Abbr} V0 → ↑[0, i + 1] V0 ≡ V → L ⊢ #i ⇒ V. +(* +#L #K #V0 #V #i #HLK #HV0 +@ex2_1_intro [2: // |1: skip ] +@pts_subst [4,6,7,8: // |1,2,3: skip |5: +*) + +lemma cpr_cast: ∀L,V,T1,T2. + L ⊢ T1 ⇒ T2 → L ⊢ 𝕗{Cast} V. T1 ⇒ T2. +#L #V #T1 #T2 * /3/ +qed. + +(* Basic inversion lemmas ***************************************************) diff --git a/matita/matita/lib/lambda-delta/reduction/lpr_defs.ma b/matita/matita/lib/lambda-delta/reduction/lpr.ma similarity index 97% rename from matita/matita/lib/lambda-delta/reduction/lpr_defs.ma rename to matita/matita/lib/lambda-delta/reduction/lpr.ma index 8adec5ca5..92f77215c 100644 --- a/matita/matita/lib/lambda-delta/reduction/lpr_defs.ma +++ b/matita/matita/lib/lambda-delta/reduction/lpr.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "lambda-delta/reduction/tpr_defs.ma". +include "lambda-delta/reduction/tpr.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************) diff --git a/matita/matita/lib/lambda-delta/reduction/tpr_defs.ma b/matita/matita/lib/lambda-delta/reduction/tpr.ma similarity index 99% rename from matita/matita/lib/lambda-delta/reduction/tpr_defs.ma rename to matita/matita/lib/lambda-delta/reduction/tpr.ma index cb9609951..3145ccaa5 100644 --- a/matita/matita/lib/lambda-delta/reduction/tpr_defs.ma +++ b/matita/matita/lib/lambda-delta/reduction/tpr.ma @@ -9,7 +9,7 @@ \ / V_______________________________________________________________ *) -include "lambda-delta/substitution/pts_defs.ma". +include "lambda-delta/substitution/pts.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) diff --git a/matita/matita/lib/lambda-delta/reduction/tpr_lift.ma b/matita/matita/lib/lambda-delta/reduction/tpr_lift.ma new file mode 100644 index 000000000..d639f7119 --- /dev/null +++ b/matita/matita/lib/lambda-delta/reduction/tpr_lift.ma @@ -0,0 +1,102 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "lambda-delta/substitution/pts_lift.ma". +include "lambda-delta/reduction/tpr.ma". + +(* Relocation properties ****************************************************) + +lemma tpr_lift: ∀T1,T2. T1 ⇒ T2 → + ∀d,e,U1. ↑[d, e] T1 ≡ U1 → ∀U2. ↑[d, e] T2 ≡ U2 → U1 ⇒ U2. +#T1 #T2 #H elim H -H T1 T2 +[ #k #d #e #U1 #HU1 #U2 #HU2 + lapply (lift_mono … HU1 … HU2) -HU1 #H destruct -U1; + lapply (lift_inv_sort1 … HU2) -HU2 #H destruct -U2 // +| #i #d #e #U1 #HU1 #U2 #HU2 + lapply (lift_mono … HU1 … HU2) -HU1 #H destruct -U1; + lapply (lift_inv_lref1 … HU2) * * #Hid #H destruct -U2 // +| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2 + elim (lift_inv_bind1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct -X1; + elim (lift_inv_bind1 … HX2) -HX2 #W2 #U2 #HVW2 #HTU2 #HX2 destruct -X2 /3/ +| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2 + elim (lift_inv_flat1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct -X1; + elim (lift_inv_flat1 … HX2) -HX2 #W2 #U2 #HVW2 #HTU2 #HX2 destruct -X2 /3/ +| #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2 + elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct -X1; + elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct -X; + elim (lift_inv_bind1 … HX2) -HX2 #V3 #T3 #HV23 #HT23 #HX2 destruct -X2 /3/ +| #V1 #V2 #T1 #T2 #T0 #HV12 #HT12 #HT2 #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2 + elim (lift_inv_bind1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct -X1; + elim (lift_inv_bind1 … HX2) -HX2 #W2 #U0 #HVW2 #HTU0 #HX2 destruct -X2; + elim (lift_total T2 (d + 1) e) #U2 #HTU2 + @tpr_delta + [4: @(pts_lift_le … HT2 … HTU2 HTU0 ?) /2/ |1: skip |2: /2/ |3: /2/ ] (**) (*/3. is too slow *) +| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #d #e #X1 #HX1 #X2 #HX2 + elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct -X1; + elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct -X; + elim (lift_inv_bind1 … HX2) -HX2 #W3 #X #HW23 #HX #HX2 destruct -X2; + elim (lift_inv_flat1 … HX) -HX #V3 #T3 #HV3 #HT23 #HX destruct -X; + elim (lift_trans_ge … HV2 … HV3 ?) -HV2 HV3 V // /3/ +| #V #T #T1 #T2 #HT1 #_ #IHT12 #d #e #X #HX #T0 #HT20 + elim (lift_inv_bind1 … HX) -HX #V3 #T3 #_ #HT3 #HX destruct -X; + elim (lift_trans_ge … HT1 … HT3 ?) -HT1 HT3 T // /3 width=6/ +| #V #T1 #T2 #_ #IHT12 #d #e #X #HX #T #HT2 + elim (lift_inv_flat1 … HX) -HX #V0 #T0 #_ #HT0 #HX destruct -X /3/ +] +qed. + +lemma tpr_inv_lift: ∀T1,T2. T1 ⇒ T2 → + ∀d,e,U1. ↑[d, e] U1 ≡ T1 → + ∃∃U2. ↑[d, e] U2 ≡ T2 & U1 ⇒ U2. +#T1 #T2 #H elim H -H T1 T2 +[ #k #d #e #U1 #HU1 + lapply (lift_inv_sort2 … HU1) -HU1 #H destruct -U1 /2/ +| #i #d #e #U1 #HU1 + lapply (lift_inv_lref2 … HU1) -HU1 * * #Hid #H destruct -U1 /3/ +| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X #HX + elim (lift_inv_bind2 … HX) -HX #V0 #T0 #HV01 #HT01 #HX destruct -X; + elim (IHV12 … HV01) -IHV12 HV01; + elim (IHT12 … HT01) -IHT12 HT01 /3 width=5/ +| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X #HX + elim (lift_inv_flat2 … HX) -HX #V0 #T0 #HV01 #HT01 #HX destruct -X; + elim (IHV12 … HV01) -IHV12 HV01; + elim (IHT12 … HT01) -IHT12 HT01 /3 width=5/ +| #V1 #V2 #W1 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X #HX + elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct -X; + elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct -Y; + elim (IHV12 … HV01) -IHV12 HV01; + elim (IHT12 … HT01) -IHT12 HT01 /3 width=5/ +| #V1 #V2 #T1 #T2 #T0 #_ #_ #HT20 #IHV12 #IHT12 #d #e #X #HX + elim (lift_inv_bind2 … HX) -HX #W1 #U1 #HWV1 #HUT1 #HX destruct -X; + elim (IHV12 … HWV1) -IHV12 HWV1 #W2 #HWV2 #HW12 + elim (IHT12 … HUT1) -IHT12 HUT1 #U2 #HUT2 #HU12 + elim (pts_inv_lift1_le … HT20 … HUT2 ?) -HT20 HUT2 // [3: /2 width=5/ |2: skip ] #U0 #HU20 #HUT0 + @ex2_1_intro [2: /2/ |1: skip |3: /2/ ] (**) (* /3 width=5/ is slow *) +| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #d #e #X #HX + elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct -X; + elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct -Y; + elim (IHV12 … HV01) -IHV12 HV01 #V3 #HV32 #HV03 + elim (IHW12 … HW01) -IHW12 HW01 #W3 #HW32 #HW03 + elim (IHT12 … HT01) -IHT12 HT01 #T3 #HT32 #HT03 + elim (lift_trans_le … HV32 … HV2 ?) -HV32 HV2 V2 // #V2 #HV32 #HV2 + @ex2_1_intro [2: /3/ |1: skip |3: /2/ ] (**) (* /4 width=5/ is slow *) +| #V #T #T1 #T2 #HT1 #_ #IHT12 #d #e #X #HX + elim (lift_inv_bind2 … HX) -HX #V0 #T0 #_ #HT0 #H destruct -X; + elim (lift_div_le … HT1 … HT0 ?) -HT1 HT0 T // #T #HT0 #HT1 + elim (IHT12 … HT1) -IHT12 HT1 /3 width=5/ +| #V #T1 #T2 #_ #IHT12 #d #e #X #HX + elim (lift_inv_flat2 … HX) -HX #V0 #T0 #_ #HT01 #H destruct -X; + elim (IHT12 … HT01) -IHT12 HT01 /3/ +] +qed. diff --git a/matita/matita/lib/lambda-delta/reduction/tpr_main.ma b/matita/matita/lib/lambda-delta/reduction/tpr_main.ma deleted file mode 100644 index 1d5d7d713..000000000 --- a/matita/matita/lib/lambda-delta/reduction/tpr_main.ma +++ /dev/null @@ -1,130 +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 "lambda-delta/substitution/lift_main.ma". -include "lambda-delta/substitution/drop_main.ma". -*) -include "lambda-delta/reduction/tpr_defs.ma". - -axiom tpr_lift: ∀T1,T2. T1 ⇒ T2 → - ∀d,e,U1. ↑[d, e] T1 ≡ U1 → ∀U2. ↑[d, e] T2 ≡ U2 → U1 ⇒ U2. -(* -#L #T1 #T2 #H elim H -H L T1 T2 -[ #L #k #d #e #K #_ #U1 #HU1 #U2 #HU2 - lapply (lift_mono … HU1 … HU2) -HU1 #H destruct -U1; - lapply (lift_inv_sort1 … HU2) -HU2 #H destruct -U2 // -| #L #i #d #e #K #_ #U1 #HU1 #U2 #HU2 - lapply (lift_mono … HU1 … HU2) -HU1 #H destruct -U1; - lapply (lift_inv_lref1 … HU2) * * #Hid #H destruct -U2 // -| #L #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HKL #X1 #HX1 #X2 #HX2 - elim (lift_inv_bind1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct -X1; - elim (lift_inv_bind1 … HX2) -HX2 #W2 #U2 #HVW2 #HTU2 #HX2 destruct -X2 - /5 width=5/ -| #L #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HKL #X1 #HX1 #X2 #HX2 - elim (lift_inv_flat1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct -X1; - elim (lift_inv_flat1 … HX2) -HX2 #W2 #U2 #HVW2 #HTU2 #HX2 destruct -X2 - /3 width=5/ -| #L #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HKL #X1 #HX1 #X2 #HX2 - elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct -X1; - elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct -X; - elim (lift_inv_bind1 … HX2) -HX2 #V3 #T3 #HV23 #HT23 #HX2 destruct -X2 - /5 width=5/ -| #L #K0 #V1 #V2 #V0 #i #HLK0 #HV12 #HV20 #IHV12 #d #e #K #HKL #X #HX #V3 #HV03 - lapply (lift_inv_lref1 … HX) -HX * * #Hid #H destruct -X; - [ -HV12; - elim (lift_trans_ge … HV20 … HV03 ?) -HV20 HV03 V0 // #V0 #HV20 #HV03 - elim (drop_trans_le … HKL … HLK0 ?) -HKL HLK0 L /2/ #L #HKL #HLK0 - elim (drop_inv_skip2 … HLK0 ?) -HLK0 /2/ #K1 #V #HK10 #HV #H destruct -L; - @pr_delta [4,6: // |1,2,3: skip |5: /2 width=5/] (**) (* /2 width=5/ *) - | -IHV12; - lapply (lift_trans_be … HV20 … HV03 ? ?) -HV20 HV03 V0 /2/ #HV23 - lapply (drop_trans_ge … HKL … HLK0 ?) -HKL HLK0 L // -Hid #HKK0 - @pr_delta /width=6/ - ] -| #L #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #d #e #K #HKL #X1 #HX1 #X2 #HX2 - elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct -X1; - elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct -X; - elim (lift_inv_bind1 … HX2) -HX2 #W3 #X #HW23 #HX #HX2 destruct -X2; - elim (lift_inv_flat1 … HX) -HX #V3 #T3 #HV3 #HT23 #HX destruct -X; - lapply (lift_trans_ge … HV2 … HV3 ?) -HV2 HV3 V // * #V #HV2 #HV3 - @pr_theta /3 width=5/ -| #L #V #T #T1 #T2 #HT1 #_ #IHT12 #d #e #K #HKL #X #HX #T0 #HT20 - elim (lift_inv_bind1 … HX) -HX #V3 #T3 #_ #HT3 #HX destruct -X; - lapply (lift_trans_ge … HT1 … HT3 ?) -HT1 HT3 T // * #T #HT1 #HT3 - @pr_zeta [2: // |1:skip | /2 width=5/] (**) (* /2 width=5/ *) -| #L #V #T1 #T2 #_ #IHT12 #d #e #K #HKL #X #HX #T #HT2 - elim (lift_inv_flat1 … HX) -HX #V0 #T0 #_ #HT0 #HX destruct -X; - @pr_tau /2 width=5/ -] -qed. -*) -axiom tpr_inv_lift: ∀T1,T2. T1 ⇒ T2 → - ∀d,e,U1. ↑[d, e] U1 ≡ T1 → - ∃∃U2. ↑[d, e] U2 ≡ T2 & U1 ⇒ U2. -(* -#L #T1 #T2 #H elim H -H L T1 T2 -[ #L #k #d #e #K #_ #U1 #HU1 - lapply (lift_inv_sort2 … HU1) -HU1 #H destruct -U1 /2/ -| #L #i #d #e #K #_ #U1 #HU1 - lapply (lift_inv_lref2 … HU1) -HU1 * * #Hid #H destruct -U1 /3/ -| #L #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HLK #X #HX - elim (lift_inv_bind2 … HX) -HX #V0 #T0 #HV01 #HT01 #HX destruct -X; - elim (IHV12 … HLK … HV01) -IHV12 #V3 #HV32 #HV03 - elim (IHT12 … HT01) -IHT12 HT01 [2,3: -HV32 HV03 /3/] -HLK HV01 /3 width=5/ -| #L #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HLK #X #HX - elim (lift_inv_flat2 … HX) -HX #V0 #T0 #HV01 #HT01 #HX destruct -X; - elim (IHV12 … HLK … HV01) -IHV12 HV01 #V3 #HV32 #HV03 - elim (IHT12 … HLK … HT01) -IHT12 HT01 HLK /3 width=5/ -| #L #V1 #V2 #W1 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HLK #X #HX - elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct -X; - elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct -Y; - elim (IHV12 … HLK … HV01) -IHV12 HV01 #V3 #HV32 #HV03 - elim (IHT12 … HT01) -IHT12 HT01 - [3: -HV32 HV03 @(drop_skip … HLK) /2/ |2: skip ] (**) (* /3 width=5/ is too slow *) - -HLK HW01 - /3 width=5/ -| #L #K0 #V1 #V2 #V0 #i #HLK0 #HV12 #HV20 #IHV12 #d #e #K #HLK #X #HX - lapply (lift_inv_lref2 … HX) -HX * * #Hid #HX destruct -X; - [ -HV12; - elim (drop_conf_lt … HLK … HLK0 Hid) -HLK HLK0 L #L #V3 #HKL #HK0L #HV31 - elim (IHV12 … HK0L … HV31) -IHV12 HK0L HV31 #V4 #HV42 #HV34 - elim (lift_trans_le … HV42 … HV20 ?) -HV42 HV20 V2 // #V2 #HV42 - >arith5 // -Hid #HV20 - @(ex2_1_intro … V2) /2 width=6/ (**) (* /3 width=8/ is slow *) - | -IHV12; - lapply (drop_conf_ge … HLK … HLK0 Hid) -HLK HLK0 L #HK - elim (lift_free … HV20 d (i - e + 1) ? ? ?) -HV20 /2/ - >arith3 /2/ -Hid /3 width=8/ (**) (* just /3 width=8/ is a bit slow *) - ] -| #L #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #d #e #K #HLK #X #HX - elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct -X; - elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct -Y; - elim (IHV12 ? ? ? HLK ? HV01) -IHV12 HV01 #V3 #HV32 #HV03 - elim (IHW12 ? ? ? HLK ? HW01) -IHW12 #W3 #HW32 #HW03 - elim (IHT12 … HT01) -IHT12 HT01 - [3: -HV2 HV32 HV03 HW32 HW03 @(drop_skip … HLK) /2/ |2: skip ] (**) (* /3/ is too slow *) - -HLK HW01 #T3 #HT32 #HT03 - elim (lift_trans_le … HV32 … HV2 ?) -HV32 HV2 V2 // #V2 #HV32 #HV2 - @(ex2_1_intro … (𝕓{Abbr}W3.𝕗{Appl}V2.T3)) /3/ (**) (* /4/ loops *) -| #L #V #T #T1 #T2 #HT1 #_ #IHT12 #d #e #K #HLK #X #HX - elim (lift_inv_bind2 … HX) -HX #V0 #T0 #_ #HT0 #H destruct -X; - elim (lift_div_le … HT1 … HT0 ?) -HT1 HT0 T // #T #HT0 #HT1 - elim (IHT12 … HLK … HT1) -IHT12 HLK HT1 /3 width=5/ -| #L #V #T1 #T2 #_ #IHT12 #d #e #K #HLK #X #HX - elim (lift_inv_flat2 … HX) -HX #V0 #T0 #_ #HT01 #H destruct -X; - elim (IHT12 … HLK … HT01) -IHT12 HLK HT01 /3/ -] -qed. -*) \ No newline at end of file diff --git a/matita/matita/lib/lambda-delta/reduction/tpr_pts.ma b/matita/matita/lib/lambda-delta/reduction/tpr_pts.ma index ea6b8027b..f8a41f025 100644 --- a/matita/matita/lib/lambda-delta/reduction/tpr_pts.ma +++ b/matita/matita/lib/lambda-delta/reduction/tpr_pts.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "lambda-delta/reduction/lpr_defs.ma". +include "lambda-delta/reduction/lpr.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) diff --git a/matita/matita/lib/lambda-delta/reduction/tpr_tpr.ma b/matita/matita/lib/lambda-delta/reduction/tpr_tpr.ma index 53ad09398..b5743ddd1 100644 --- a/matita/matita/lib/lambda-delta/reduction/tpr_tpr.ma +++ b/matita/matita/lib/lambda-delta/reduction/tpr_tpr.ma @@ -11,7 +11,7 @@ include "lambda-delta/substitution/lift_weight.ma". include "lambda-delta/substitution/pts_pts.ma". -include "lambda-delta/reduction/tpr_main.ma". +include "lambda-delta/reduction/tpr_lift.ma". include "lambda-delta/reduction/tpr_pts.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) diff --git a/matita/matita/lib/lambda-delta/substitution/drop_defs.ma b/matita/matita/lib/lambda-delta/substitution/drop.ma similarity index 82% rename from matita/matita/lib/lambda-delta/substitution/drop_defs.ma rename to matita/matita/lib/lambda-delta/substitution/drop.ma index 51c657615..d192c84dc 100644 --- a/matita/matita/lib/lambda-delta/substitution/drop_defs.ma +++ b/matita/matita/lib/lambda-delta/substitution/drop.ma @@ -9,13 +9,14 @@ \ / V_______________________________________________________________ *) -include "lambda-delta/substitution/leq_defs.ma". -include "lambda-delta/substitution/lift_defs.ma". +include "lambda-delta/substitution/leq.ma". +include "lambda-delta/substitution/lift.ma". (* DROPPING *****************************************************************) inductive drop: lenv → nat → nat → lenv → Prop ≝ -| drop_refl: ∀L. drop L 0 0 L +| drop_sort: ∀d,e. drop (⋆) d e (⋆) +| drop_comp: ∀L1,L2,I,V. drop L1 0 0 L2 → drop (L1. 𝕓{I} V) 0 0 (L2. 𝕓{I} V) | drop_drop: ∀L1,L2,I,V,e. drop L1 0 e L2 → drop (L1. 𝕓{I} V) 0 (e + 1) L2 | drop_skip: ∀L1,L2,I,V1,V2,d,e. drop L1 d e L2 → ↑[d,e] V2 ≡ V1 → @@ -27,11 +28,13 @@ interpretation "dropping" 'RDrop L1 d e L2 = (drop L1 d e L2). (* Basic inversion lemmas ***************************************************) lemma drop_inv_refl_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 → e = 0 → L1 = L2. -#d #e #L1 #L2 * -d e L1 L2 +#d #e #L1 #L2 #H elim H -H d e L1 L2 [ // -| #L1 #L2 #I #V #e #_ #_ #H +| #L1 #L2 #I #V #_ #IHL12 #H1 #H2 + >(IHL12 H1 H2) -IHL12 H1 H2 L1 // +| #L1 #L2 #I #V #e #_ #_ #_ #H elim (plus_S_eq_O_false … H) -| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H +| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #_ #H elim (plus_S_eq_O_false … H) ] qed. @@ -40,24 +43,26 @@ lemma drop_inv_refl: ∀L1,L2. ↓[0, 0] L1 ≡ L2 → L1 = L2. /2 width=5/ qed. lemma drop_inv_sort1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → L1 = ⋆ → - ∧∧ L2 = ⋆ & d = 0 & e = 0. + L2 = ⋆. #d #e #L1 #L2 * -d e L1 L2 -[ /2/ +[ // +| #L1 #L2 #I #V #_ #H destruct | #L1 #L2 #I #V #e #_ #H destruct | #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H destruct ] qed. -lemma drop_inv_sort1: ∀d,e,L2. ↓[d, e] ⋆ ≡ L2 → - ∧∧ L2 = ⋆ & d = 0 & e = 0. -/2/ qed. +lemma drop_inv_sort1: ∀d,e,L2. ↓[d, e] ⋆ ≡ L2 → L2 = ⋆. +/2 width=5/ qed. lemma drop_inv_O1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 → ∀K,I,V. L1 = K. 𝕓{I} V → (e = 0 ∧ L2 = K. 𝕓{I} V) ∨ (0 < e ∧ ↓[d, e - 1] K ≡ L2). #d #e #L1 #L2 * -d e L1 L2 -[ /3/ +[ #d #e #_ #K #I #V #H destruct +| #L1 #L2 #I #V #HL12 #H #K #J #W #HX destruct -L1 I V + >(drop_inv_refl … HL12) -HL12 K /3/ | #L1 #L2 #I #V #e #HL12 #_ #K #J #W #H destruct -L1 I V /3/ | #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H elim (plus_S_eq_O_false … H) ] @@ -81,7 +86,8 @@ lemma drop_inv_skip2_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d → ↑[d - 1, e] V2 ≡ V1 & L1 = K1. 𝕓{I} V1. #d #e #L1 #L2 * -d e L1 L2 -[ #L #H elim (lt_refl_false … H) +[ #d #e #_ #I #K #V #H destruct +| #L1 #L2 #I #V #_ #H elim (lt_refl_false … H) | #L1 #L2 #I #V #e #_ #H elim (lt_refl_false … H) | #L1 #X #Y #V1 #Z #d #e #HL12 #HV12 #_ #I #L2 #V2 #H destruct -X Y Z; /2 width=5/ @@ -95,6 +101,10 @@ lemma drop_inv_skip2: ∀d,e,I,L1,K2,V2. ↓[d, e] L1 ≡ K2. 𝕓{I} V2 → 0 < (* Basic properties *********************************************************) +lemma drop_refl: ∀L. ↓[0, 0] L ≡ L. +#L elim L -L /2/ +qed. + lemma drop_drop_lt: ∀L1,L2,I,V,e. ↓[0, e - 1] L1 ≡ L2 → 0 < e → ↓[0, e] L1. 𝕓{I} V ≡ L2. #L1 #L2 #I #V #e #HL12 #He >(plus_minus_m_m e 1) /2/ @@ -103,7 +113,7 @@ qed. lemma drop_fwd_drop2: ∀L1,I2,K2,V2,e. ↓[O, e] L1 ≡ K2. 𝕓{I2} V2 → ↓[O, e + 1] L1 ≡ K2. #L1 elim L1 -L1 -[ #I2 #K2 #V2 #e #H elim (drop_inv_sort1 … H) -H #H destruct +[ #I2 #K2 #V2 #e #H lapply (drop_inv_sort1 … H) -H #H destruct | #K1 #I1 #V1 #IHL1 #I2 #K2 #V2 #e #H elim (drop_inv_O1 … H) -H * #He #H [ -IHL1; destruct -e K2 I2 V2 /2/ @@ -119,7 +129,7 @@ lemma drop_leq_drop1: ∀L1,L2,d,e. L1 [d, e] ≈ L2 → ↓[0, i] L2 ≡ K2. 𝕓{I} V. #L1 #L2 #d #e #H elim H -H L1 L2 d e [ #d #e #I #K1 #V #i #H - elim (drop_inv_sort1 … H) -H #H destruct + lapply (drop_inv_sort1 … H) -H #H destruct | #L1 #L2 #I1 #I2 #V1 #V2 #_ #_ #I #K1 #V #i #_ #_ #H elim (lt_zero_false … H) | #L1 #L2 #I #V #e #HL12 #IHL12 #J #K1 #W #i #H #_ #Hie diff --git a/matita/matita/lib/lambda-delta/substitution/drop_main.ma b/matita/matita/lib/lambda-delta/substitution/drop_drop.ma similarity index 87% rename from matita/matita/lib/lambda-delta/substitution/drop_main.ma rename to matita/matita/lib/lambda-delta/substitution/drop_drop.ma index 575f25401..96fd0db51 100644 --- a/matita/matita/lib/lambda-delta/substitution/drop_main.ma +++ b/matita/matita/lib/lambda-delta/substitution/drop_drop.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "lambda-delta/substitution/drop_defs.ma". +include "lambda-delta/substitution/drop.ma". (* DROPPING *****************************************************************) @@ -22,7 +22,10 @@ lemma drop_conf_ge: ∀d1,e1,L,L1. ↓[d1, e1] L ≡ L1 → ∀e2,L2. ↓[0, e2] L ≡ L2 → d1 + e1 ≤ e2 → ↓[0, e2 - e1] L1 ≡ L2. #d1 #e1 #L #L1 #H elim H -H d1 e1 L L1 -[ // +[ #d #e #e2 #L2 #H + >(drop_inv_sort1 … H) -H L2 // +| #K1 #K2 #I #V #HK12 #_ #e2 #L2 #H #_ (drop_inv_sort1 … H) -H L2 /2/ +| #K1 #K2 #I #V #HK12 #_ #e2 #L2 #HL2 #H + >(drop_inv_refl … HK12) -HK12 K1; lapply (le_O_to_eq_O … H) -H #H destruct -e2 /2/ | #L1 #L2 #I #V #e #_ #IHL12 #e2 #L #HL2 #H lapply (le_O_to_eq_O … H) -H #H destruct -e2; @@ -76,7 +84,10 @@ qed. lemma drop_trans_ge: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L → ∀e2,L2. ↓[0, e2] L ≡ L2 → d1 ≤ e2 → ↓[0, e1 + e2] L1 ≡ L2. #d1 #e1 #L1 #L #H elim H -H d1 e1 L1 L -[ // +[ #d #e #e2 #L2 #H + >(drop_inv_sort1 … H) -H L2 // +| #K1 #K2 #I #V #HK12 #_ #e2 #L2 #H #_ normalize + >(drop_inv_refl … HK12) -HK12 K1 // | /3/ | #L1 #L2 #I #V1 #V2 #d #e #H_ #_ #IHL12 #e2 #L #H #Hde2 lapply (lt_to_le_to_lt 0 … Hde2) // #He2 diff --git a/matita/matita/lib/lambda-delta/substitution/leq_defs.ma b/matita/matita/lib/lambda-delta/substitution/leq.ma similarity index 100% rename from matita/matita/lib/lambda-delta/substitution/leq_defs.ma rename to matita/matita/lib/lambda-delta/substitution/leq.ma diff --git a/matita/matita/lib/lambda-delta/substitution/lift_defs.ma b/matita/matita/lib/lambda-delta/substitution/lift.ma similarity index 90% rename from matita/matita/lib/lambda-delta/substitution/lift_defs.ma rename to matita/matita/lib/lambda-delta/substitution/lift.ma index 71d438d68..a5b15e110 100644 --- a/matita/matita/lib/lambda-delta/substitution/lift_defs.ma +++ b/matita/matita/lib/lambda-delta/substitution/lift.ma @@ -53,6 +53,25 @@ lemma lift_total: ∀T1,d,e. ∃T2. ↑[d,e] T1 ≡ T2. ] qed. +lemma lift_split: ∀d1,e2,T1,T2. ↑[d1, e2] T1 ≡ T2 → ∀d2,e1. + d1 ≤ d2 → d2 ≤ d1 + e1 → e1 ≤ e2 → + ∃∃T. ↑[d1, e1] T1 ≡ T & ↑[d2, e2 - e1] T ≡ T2. +#d1 #e2 #T1 #T2 #H elim H -H d1 e2 T1 T2 +[ /3/ +| #i #d1 #e2 #Hid1 #d2 #e1 #Hd12 #_ #_ + lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2 /4/ +| #i #d1 #e2 #Hid1 #d2 #e1 #_ #Hd21 #He12 + lapply (transitive_le …(i+e1) Hd21 ?) /2/ -Hd21 #Hd21 + <(arith_d1 i e2 e1) // /3/ +| #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12 + elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b + elim (IHT (d2+1) … ? ? He12) /3 width = 5/ +| #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12 + elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b + elim (IHT d2 … ? ? He12) /3 width = 5/ +] +qed. + (* Basic inversion lemmas ***************************************************) lemma lift_inv_refl_aux: ∀d,e,T1,T2. ↑[d, e] T1 ≡ T2 → e = 0 → T1 = T2. diff --git a/matita/matita/lib/lambda-delta/substitution/lift_main.ma b/matita/matita/lib/lambda-delta/substitution/lift_lift.ma similarity index 88% rename from matita/matita/lib/lambda-delta/substitution/lift_main.ma rename to matita/matita/lib/lambda-delta/substitution/lift_lift.ma index 26680f364..4281046cb 100644 --- a/matita/matita/lib/lambda-delta/substitution/lift_main.ma +++ b/matita/matita/lib/lambda-delta/substitution/lift_lift.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "lambda-delta/substitution/lift_defs.ma". +include "lambda-delta/substitution/lift.ma". (* RELOCATION ***************************************************************) @@ -63,25 +63,6 @@ lemma lift_div_le: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → ] qed. -lemma lift_free: ∀d1,e2,T1,T2. ↑[d1, e2] T1 ≡ T2 → ∀d2,e1. - d1 ≤ d2 → d2 ≤ d1 + e1 → e1 ≤ e2 → - ∃∃T. ↑[d1, e1] T1 ≡ T & ↑[d2, e2 - e1] T ≡ T2. -#d1 #e2 #T1 #T2 #H elim H -H d1 e2 T1 T2 -[ /3/ -| #i #d1 #e2 #Hid1 #d2 #e1 #Hd12 #_ #_ - lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2 /4/ -| #i #d1 #e2 #Hid1 #d2 #e1 #_ #Hd21 #He12 - lapply (transitive_le …(i+e1) Hd21 ?) /2/ -Hd21 #Hd21 - <(arith_d1 i e2 e1) // /3/ -| #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12 - elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b - elim (IHT (d2+1) … ? ? He12) /3 width = 5/ -| #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12 - elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b - elim (IHT d2 … ? ? He12) /3 width = 5/ -] -qed. - lemma lift_mono: ∀d,e,T,U1. ↑[d,e] T ≡ U1 → ∀U2. ↑[d,e] T ≡ U2 → U1 = U2. #d #e #T #U1 #H elim H -H d e T U1 [ #k #d #e #X #HX diff --git a/matita/matita/lib/lambda-delta/substitution/lift_weight.ma b/matita/matita/lib/lambda-delta/substitution/lift_weight.ma index 934e22054..eafa00705 100644 --- a/matita/matita/lib/lambda-delta/substitution/lift_weight.ma +++ b/matita/matita/lib/lambda-delta/substitution/lift_weight.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "lambda-delta/syntax/weight.ma". -include "lambda-delta/substitution/lift_defs.ma". +include "lambda-delta/substitution/lift.ma". (* RELOCATION ***************************************************************) diff --git a/matita/matita/lib/lambda-delta/substitution/pts_defs.ma b/matita/matita/lib/lambda-delta/substitution/pts.ma similarity index 98% rename from matita/matita/lib/lambda-delta/substitution/pts_defs.ma rename to matita/matita/lib/lambda-delta/substitution/pts.ma index 111052f69..ac962355e 100644 --- a/matita/matita/lib/lambda-delta/substitution/pts_defs.ma +++ b/matita/matita/lib/lambda-delta/substitution/pts.ma @@ -9,7 +9,7 @@ \ / V_______________________________________________________________ *) -include "lambda-delta/substitution/drop_defs.ma". +include "lambda-delta/substitution/drop.ma". (* PARTIAL TELESCOPIC SUBSTITUTION ******************************************) diff --git a/matita/matita/lib/lambda-delta/substitution/pts_lift.ma b/matita/matita/lib/lambda-delta/substitution/pts_lift.ma index 9d1cdc378..8cd477738 100644 --- a/matita/matita/lib/lambda-delta/substitution/pts_lift.ma +++ b/matita/matita/lib/lambda-delta/substitution/pts_lift.ma @@ -9,9 +9,9 @@ \ / V_______________________________________________________________ *) -include "lambda-delta/substitution/lift_main.ma". -include "lambda-delta/substitution/drop_main.ma". -include "lambda-delta/substitution/pts_defs.ma". +include "lambda-delta/substitution/lift_lift.ma". +include "lambda-delta/substitution/drop_drop.ma". +include "lambda-delta/substitution/pts.ma". (* PARTIAL TELESCOPIC SUBSTITUTION ******************************************) @@ -115,7 +115,7 @@ lemma pts_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 → <(arith_h1 ? ? ? e ? ?) in HV1 // #HV1 lapply (lift_inv_lref2_ge … H … Hdei) -H #H destruct -T1; lapply (drop_conf_ge … HLK … HLKV ?) -HLK HLKV L // #HKV - elim (lift_free … HV12 d (i - e + 1) ? ? ?) -HV12; [2,3,4: normalize /2/ ] -Hdei >arith_e2 // #V0 #HV10 #HV02 + elim (lift_split … HV12 d (i - e + 1) ? ? ?) -HV12; [2,3,4: normalize /2/ ] -Hdei >arith_e2 // #V0 #HV10 #HV02 @ex2_1_intro [2: @pts_subst [4: /2/ |6,7,8: // |1,2,3: skip |5: @arith5 // ] |1: skip diff --git a/matita/matita/lib/lambda-delta/syntax/length.ma b/matita/matita/lib/lambda-delta/syntax/length.ma new file mode 100644 index 000000000..91e1bd78c --- /dev/null +++ b/matita/matita/lib/lambda-delta/syntax/length.ma @@ -0,0 +1,22 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| This file is distributed under the terms of the + \ / GNU General Public License Version 2 + \ / + V_______________________________________________________________ *) + +include "lambda-delta/syntax/lenv.ma". + +(* LENGTH *******************************************************************) + +(* the length of a local environment *) +let rec length L ≝ match L with +[ LSort ⇒ 0 +| LPair L _ _ ⇒ length L + 1 +]. + +interpretation "length (local environment)" 'card L = (length L). diff --git a/matita/matita/lib/lambda-delta/xoa.conf.xml b/matita/matita/lib/lambda-delta/xoa.conf.xml index 6eebcc64e..3330813ae 100644 --- a/matita/matita/lib/lambda-delta/xoa.conf.xml +++ b/matita/matita/lib/lambda-delta/xoa.conf.xml @@ -11,7 +11,7 @@
lib/lambda-delta - xoa_defs + xoa xoa_notation basics/pts.ma 2 1 diff --git a/matita/matita/lib/lambda-delta/xoa_defs.ma b/matita/matita/lib/lambda-delta/xoa.ma similarity index 100% rename from matita/matita/lib/lambda-delta/xoa_defs.ma rename to matita/matita/lib/lambda-delta/xoa.ma diff --git a/matita/matita/lib/lambda-delta/xoa_props.ma b/matita/matita/lib/lambda-delta/xoa_props.ma index 967656716..f07bc89be 100644 --- a/matita/matita/lib/lambda-delta/xoa_props.ma +++ b/matita/matita/lib/lambda-delta/xoa_props.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "lambda-delta/xoa_notation.ma". -include "lambda-delta/xoa_defs.ma". +include "lambda-delta/xoa.ma". lemma ex2_1_comm: ∀A0. ∀P0,P1:A0→Prop. (∃∃x0. P0 x0 & P1 x0) → ∃∃x0. P1 x0 & P0 x0. #A0 #P0 #P1 * /2/ -- 2.39.2