From 6f29b61aeae23efb412ac48ab747d63bcedcacd6 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 24 Jul 2011 12:23:53 +0000 Subject: [PATCH] - sone refactoring - notation fix - telescopic substitution replaced by parallel substitution - context-free parallel reduction added --- matita/matita/lib/lambda-delta/ground.ma | 1 - matita/matita/lib/lambda-delta/notation.ma | 12 +- .../thin_main.ma => reduction/lpr_defs.ma} | 35 +++--- .../lib/lambda-delta/reduction/pr_defs.ma | 81 ------------- .../lib/lambda-delta/reduction/pr_pr.ma | 41 ++++++- .../lib/lambda-delta/reduction/tpr_defs.ma | 74 ++++++++++++ .../lambda-delta/substitution/drop_defs.ma | 34 +++--- .../lambda-delta/substitution/drop_main.ma | 28 ++--- .../lambda-delta/substitution/psubst_defs.ma | 78 ++++++++++++ .../lambda-delta/substitution/subst_defs.ma | 112 ------------------ .../lambda-delta/substitution/thin_defs.ma | 44 ------- matita/matita/lib/lambda-delta/syntax/item.ma | 1 + matita/matita/lib/lambda-delta/xoa_defs.ma | 17 +-- .../matita/lib/lambda-delta/xoa_notation.ma | 8 +- 14 files changed, 254 insertions(+), 312 deletions(-) rename matita/matita/lib/lambda-delta/{substitution/thin_main.ma => reduction/lpr_defs.ma} (50%) delete mode 100644 matita/matita/lib/lambda-delta/reduction/pr_defs.ma create mode 100644 matita/matita/lib/lambda-delta/reduction/tpr_defs.ma create mode 100644 matita/matita/lib/lambda-delta/substitution/psubst_defs.ma delete mode 100644 matita/matita/lib/lambda-delta/substitution/subst_defs.ma delete mode 100644 matita/matita/lib/lambda-delta/substitution/thin_defs.ma diff --git a/matita/matita/lib/lambda-delta/ground.ma b/matita/matita/lib/lambda-delta/ground.ma index 97c45196a..d39b3faf4 100644 --- a/matita/matita/lib/lambda-delta/ground.ma +++ b/matita/matita/lib/lambda-delta/ground.ma @@ -12,7 +12,6 @@ include "basics/list.ma". include "lambda-delta/xoa_defs.ma". include "lambda-delta/xoa_notation.ma". -include "lambda-delta/notation.ma". (* ARITHMETICAL PROPERTIES **************************************************) diff --git a/matita/matita/lib/lambda-delta/notation.ma b/matita/matita/lib/lambda-delta/notation.ma index 79fcc3a97..6f883cc71 100644 --- a/matita/matita/lib/lambda-delta/notation.ma +++ b/matita/matita/lib/lambda-delta/notation.ma @@ -17,7 +17,7 @@ notation "hvbox( ⋆ )" non associative with precedence 90 for @{ 'Star }. -notation "hvbox( ⋆ k )" +notation "hvbox( ⋆ term 90 k )" non associative with precedence 90 for @{ 'Star $k }. @@ -53,18 +53,18 @@ notation "hvbox( ↑ [ d , break e ] break T1 ≡ break T2 )" notation "hvbox( ↓ [ d , break e ] break L1 ≡ break L2 )" non associative with precedence 45 - for @{ 'RSubst $L1 $d $e $L2 }. + for @{ 'RDrop $L1 $d $e $L2 }. -notation "hvbox( L ⊢ break ↓ [ d , break e ] break T1 ≡ break T2 )" +notation "hvbox( L ⊢ break (term 90 T1) break [ d , break e ] ≫ break T2 )" non associative with precedence 45 - for @{ 'RSubst $L $T1 $d $e $T2 }. + for @{ 'PSubst $L $T1 $d $e $T2 }. (* reduction ****************************************************************) notation "hvbox( T1 ⇒ break T2 )" non associative with precedence 45 - for @{ 'PR $T1 $T2 }. + for @{ 'PRed $T1 $T2 }. notation "hvbox( L ⊢ break (term 90 T1) ⇒ break T2 )" non associative with precedence 45 - for @{ 'PR $L $T1 $T2 }. + for @{ 'PRed $L $T1 $T2 }. diff --git a/matita/matita/lib/lambda-delta/substitution/thin_main.ma b/matita/matita/lib/lambda-delta/reduction/lpr_defs.ma similarity index 50% rename from matita/matita/lib/lambda-delta/substitution/thin_main.ma rename to matita/matita/lib/lambda-delta/reduction/lpr_defs.ma index f16fb3a48..dab96f2dd 100644 --- a/matita/matita/lib/lambda-delta/substitution/thin_main.ma +++ b/matita/matita/lib/lambda-delta/reduction/lpr_defs.ma @@ -12,23 +12,30 @@ (* *) (**************************************************************************) -include "lambda-delta/substitution/thin_defs.ma". +include "lambda-delta/reduction/tpr_defs.ma". -(* THINNING *****************************************************************) +(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************) -(* the main properties ******************************************************) +inductive lpr: lenv → lenv → Prop ≝ +| lpr_sort: lpr (⋆) (⋆) +| lpr_item: ∀K1,K2,I,V1,V2. + lpr K1 K2 → V1 ⇒ V2 → lpr (K1. 𝕓{I} V1) (K2. 𝕓{I} V2) (*𝕓*) +. -axiom thin_conf_ge: ∀d1,e1,L,L1. ↓[d1,e1] L ≡ L1 → - ∀e2,L2. ↓[0,e2] L ≡ L2 → d1 + e1 ≤ e2 → ↓[0,e2-e1] L1 ≡ L2. +interpretation + "context-free parallel reduction (environment)" + 'PR L1 L2 = (lpr L1 L2). -axiom thin_conf_lt: ∀d1,e1,L,L1. ↓[d1,e1] L ≡ L1 → - ∀e2,K2,I,V2. ↓[0,e2] L ≡ K2. 𝕓{I} V2 → - e2 < d1 → let d ≝ d1 - e2 - 1 in - ∃∃K1,V1. ↓[0,e2] L1 ≡ K1. 𝕓{I} V1 & ↓[d,e1] K2 ≡ K1 & ↑[d,e1] V1 ≡ V2. +(* Basic inversion lemmas ***************************************************) -axiom thin_trans_le: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L → - ∀e2,L2. ↓[0, e2] L ≡ L2 → e2 ≤ d1 → - ∃∃L0. ↓[0, e2] L1 ≡ L0 & ↓[d1 - e2, e1] L0 ≡ L2. +lemma lpr_inv_item1_aux: ∀L1,L2. L1 ⇒ L2 → ∀K1,I,V1. L1 = K1. 𝕓{I} V1 → + ∃∃K2,V2. K1 ⇒ K2 & V1 ⇒ V2 & L2 = K2. 𝕓{I} V2. +#L1 #L2 #H elim H -H L1 L2 +[ #K1 #I #V1 #H destruct +| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #_ #L #J #W #H destruct - K1 I V1 /2 width=5/ +] +qed. -axiom thin_trans_ge: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L → - ∀e2,L2. ↓[0, e2] L ≡ L2 → d1 ≤ e2 → ↓[0, e1 + e2] L1 ≡ L2. +lemma lpr_inv_item1: ∀K1,I,V1,L2. K1. 𝕓{I} V1 ⇒ L2 → + ∃∃K2,V2. K1 ⇒ K2 & V1 ⇒ V2 & L2 = K2. 𝕓{I} V2. +/2/ qed. diff --git a/matita/matita/lib/lambda-delta/reduction/pr_defs.ma b/matita/matita/lib/lambda-delta/reduction/pr_defs.ma deleted file mode 100644 index d45cbd0d8..000000000 --- a/matita/matita/lib/lambda-delta/reduction/pr_defs.ma +++ /dev/null @@ -1,81 +0,0 @@ -(* - ||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/substitution/drop_defs.ma". - -(* SINGLE STEP PARALLEL REDUCTION ON TERMS **********************************) - -inductive pr: lenv → term → term → Prop ≝ -| pr_sort : ∀L,k. pr L (⋆k) (⋆k) -| pr_lref : ∀L,i. pr L (#i) (#i) -| pr_bind : ∀L,I,V1,V2,T1,T2. pr L V1 V2 → pr (L. 𝕓{I} V1) T1 T2 → - pr L (𝕓{I} V1. T1) (𝕓{I} V2. T2) -| pr_flat : ∀L,I,V1,V2,T1,T2. pr L V1 V2 → pr L T1 T2 → - pr L (𝕗{I} V1. T1) (𝕗{I} V2. T2) -| pr_beta : ∀L,V1,V2,W,T1,T2. - pr L V1 V2 → pr (L. 𝕓{Abst} W) T1 T2 → (*𝕓*) - pr L (𝕚{Appl} V1. 𝕚{Abst} W. T1) (𝕚{Abbr} V2. T2) -| pr_delta: ∀L,K,V1,V2,V,i. - ↑[0,i] K. 𝕓{Abbr} V1 ≡ L → pr K V1 V2 → ↑[0,i+1] V2 ≡ V → - pr L (#i) V -| pr_theta: ∀L,V,V1,V2,W1,W2,T1,T2. - pr L V1 V2 → ↑[0,1] V2 ≡ V → pr L W1 W2 → pr (L. 𝕓{Abbr} W1) T1 T2 → (*𝕓*) - pr L (𝕚{Appl} V1. 𝕚{Abbr} W1. T1) (𝕚{Abbr} W2. 𝕚{Appl} V. T2) -| pr_zeta : ∀L,V,T,T1,T2. ↑[0,1] T1 ≡ T → pr L T1 T2 → - pr L (𝕚{Abbr} V. T) T2 -| pr_tau : ∀L,V,T1,T2. pr L T1 T2 → pr L (𝕚{Cast} V. T1) T2 -. - -interpretation - "single step parallel reduction (term)" - 'PR L T1 T2 = (pr L T1 T2). - -(* Basic properties *********************************************************) - -lemma pr_refl: ∀T,L. L ⊢ T ⇒ T. -#T elim T -T // -#I elim I -I /2/ -qed. - -(* The basic inversion lemmas ***********************************************) - -lemma pr_inv_lref2_aux: ∀L,T1,T2. L ⊢ T1 ⇒ T2 → ∀i. T2 = #i → - ∨∨ T1 = #i - | ∃∃K,V1,j. j < i & K ⊢ V1 ⇒ #(i-j-1) & - ↑[O,j] K. 𝕓{Abbr} V1 ≡ L & T1 = #j - | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & L ⊢ T0 ⇒ #i & - T1 = 𝕓{Abbr} V. T - | ∃∃V,T. L ⊢ T ⇒ #i & T1 = 𝕗{Cast} V. T. -#L #T1 #T2 #H elim H -H L T1 T2 -[ #L #k #i #H destruct -| #L #j #i /2/ -| #L #I #V1 #V2 #T1 #T2 #_ #_ #_ #_ #i #H destruct -| #L #I #V1 #V2 #T1 #T2 #_ #_ #_ #_ #i #H destruct -| #L #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #i #H destruct -| #L #K #V1 #V2 #V #j #HLK #HV12 #HV2 #_ #i #H destruct -V; - elim (lift_inv_lref2 … HV2) -HV2 * #H1 #H2 - [ elim (lt_zero_false … H1) - | destruct -V2 /3 width=7/ - ] -| #L #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #i #H destruct -| #L #V #T #T1 #T2 #HT1 #HT12 #_ #i #H destruct /3 width=6/ -| #L #V #T1 #T2 #HT12 #_ #i #H destruct /3/ -] -qed. - -lemma pr_inv_lref2: ∀L,T1,i. L ⊢ T1 ⇒ #i → - ∨∨ T1 = #i - | ∃∃K,V1,j. j < i & K ⊢ V1 ⇒ #(i-j-1) & - ↑[O,j] K. 𝕓{Abbr} V1 ≡ L & T1 = #j - | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & L ⊢ T0 ⇒ #i & - T1 = 𝕓{Abbr} V. T - | ∃∃V,T. L ⊢ T ⇒ #i & T1 = 𝕗{Cast} V. T. -/2/ qed. diff --git a/matita/matita/lib/lambda-delta/reduction/pr_pr.ma b/matita/matita/lib/lambda-delta/reduction/pr_pr.ma index fc284e06d..c8942bea2 100644 --- a/matita/matita/lib/lambda-delta/reduction/pr_pr.ma +++ b/matita/matita/lib/lambda-delta/reduction/pr_pr.ma @@ -22,6 +22,20 @@ lemma pr_conf_sort_sort: ∀L,k1. ∃∃T0. L ⊢ (⋆k1) ⇒ T0 & L ⊢ (⋆k1) lemma pr_conf_lref_lref: ∀L,i1. ∃∃T0. L ⊢ (#i1) ⇒ T0 & L ⊢ (#i1) ⇒ T0. /2/ qed. +lemma pr_conf_bind_bind: + ∀L,I1,V11,V12,T11,T12,V22,T22. ( + ∀L1,T1. #L1 + #T1 < #L + (#V11 + #T11 + 1) → + ∀T3,T4. L1 ⊢ T1 ⇒ T3 → L1 ⊢ T1 ⇒ T4 → + ∃∃T0. L1 ⊢ T3 ⇒ T0 & L1 ⊢ T4 ⇒ T0 + ) → + L ⊢ V11 ⇒ V12 → L. 𝕓{I1} V11 ⊢ T11 ⇒ T12 → + L ⊢ V11 ⇒ V22 → L. 𝕓{I1} V11 ⊢ T11 ⇒ T22 → + ∃∃T0. L ⊢ 𝕓{I1} V12. T12 ⇒ T0 & L ⊢ 𝕓{I1} V22. T22 ⇒ T0. +#L #I1 #V11 #V12 #T11 #T12 #V22 #T22 #IH #HV1 #HT1 #HV2 #HT2 +elim (IH … HV1 … HV2) [2: /2/ ] #V #HV1 #HV2 +elim (IH … HT1 … HT2) [2: normalize // ] -HT1 HT2 T11 IH #T #HT1 #HT2 +@ex2_1_intro [2: @pr_bind [3: @HV1 |1: skip |4: + (* Confluence ***************************************************************) lemma pr_conf_aux: @@ -37,7 +51,7 @@ lemma pr_conf_aux: * -K1 U1 T1 [ #K1 #k1 * -K2 U2 T2 (* case 1: sort, sort *) - [ #K2 #k2 #H1 #H2 #H3 #H4 destruct -K1 K2 T k2 IH // + [ #K2 #k2 #H1 #H2 #H3 #H4 destruct -K1 K2 T k2 // (* case 2: sort, lref (excluded) *) | #K2 #i2 #H1 #H2 #H3 #H4 destruct (* case 3: sort, bind (excluded) *) @@ -56,10 +70,10 @@ lemma pr_conf_aux: | #K2 #V2 #T21 #T22 #_ #H1 #H2 #H3 #H4 destruct ] | #K1 #i1 * -K2 U2 T2 -(* case 10: lref, sort (excluded) *) +(* case 10: lref, sort (excluded) broken *) [ #K2 #k2 #H1 #H2 #H3 #H4 destruct (* case 11: lref, sort (excluded) *) - | #K2 #i2 #H1 #H2 #H3 #H4 destruct -K1 K2 T i2 IH // + | #K2 #i2 #H1 #H2 #H3 #H4 destruct -K1 K2 T i2 // (* case 12: lref, bind (excluded) *) | #K2 #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 #H3 #H4 destruct (* case 13: lref, flat (excluded) *) @@ -74,11 +88,28 @@ lemma pr_conf_aux: | #K2 #V2 #T21 #T22 #T20 #_ #_ #H1 #H2 #H3 #H4 destruct (* case 18: lref, tau (excluded) *) | #K2 #V2 #T21 #T22 #_ #H1 #H2 #H3 #H4 destruct - ] + ] +| #K1 #I1 #V11 #V12 #T11 #T12 #HV112 #HT112 * -K2 U2 T2 +(* case 19: bind, sort (excluded) broken *) + [ #K2 #k2 #H1 #H2 #H3 #H4 destruct +(* case 20: bind, lref (excluded) *) + | #K2 #i2 #H1 #H2 #H3 #H4 destruct +(* case 21: bind, bind *) + | #K2 #I2 #V21 #V22 #T21 #T22 #HV212 #HT212 #H1 #H2 #H3 #H4 + destruct -T K1 K2 I2 V21 T21; + theorem pr_conf: ∀L,T,T1,T2. L ⊢ T ⇒ T1 → L ⊢ T ⇒ T2 → ∃∃T0. L ⊢ T1 ⇒ T0 & L ⊢ T2 ⇒ T0. #L #T @(cw_wf_ind … L T) -L T /3 width=12/ qed. - +lemma pr_conf_bind_bind: + ∀L,I1,V11,V12,T11,T12,V22,T22. ( + ∀L1,T1. #L1 + #T1 < #L + (#V11 + #T11 + 1) → + ∀T3,T4. L1 ⊢ T1 ⇒ T3 → L1 ⊢ T1 ⇒ T4 → + ∃∃T0. L1 ⊢ T3 ⇒ T0 & L1 ⊢ T4 ⇒ T0 + ) → + L ⊢ V11 ⇒ V12 → L. 𝕓{I1} V11 ⊢ T11 ⇒ T12 → + L ⊢ V11 ⇒ V22 → L. 𝕓{I1} V11 ⊢ T11 ⇒ T22 → + ∃∃T0. L ⊢ 𝕓{I1} V12. T12 ⇒ T0 & L ⊢ 𝕓{I1} V22. T22 ⇒ T0. diff --git a/matita/matita/lib/lambda-delta/reduction/tpr_defs.ma b/matita/matita/lib/lambda-delta/reduction/tpr_defs.ma new file mode 100644 index 000000000..29f8ae4e7 --- /dev/null +++ b/matita/matita/lib/lambda-delta/reduction/tpr_defs.ma @@ -0,0 +1,74 @@ +(* + ||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/substitution/subst_defs.ma". + +(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) + +inductive tpr: term → term → Prop ≝ +| tpr_sort : ∀k. tpr (⋆k) (⋆k) +| tpr_lref : ∀i. tpr (#i) (#i) +| tpr_bind : ∀I,V1,V2,T1,T2. tpr V1 V2 → tpr T1 T2 → + tpr (𝕓{I} V1. T1) (𝕓{I} V2. T2) +| tpr_flat : ∀I,V1,V2,T1,T2. tpr V1 V2 → tpr T1 T2 → + tpr (𝕗{I} V1. T1) (𝕗{I} V2. T2) +| tpr_beta : ∀V1,V2,W,T1,T2. + tpr V1 V2 → tpr T1 T2 → + tpr (𝕚{Appl} V1. 𝕚{Abst} W. T1) (𝕚{Abbr} V2. T2) +| tpr_delta: ∀V1,V2,T1,T2,T0,T. + tpr V1 V2 → tpr T1 T2 → + ⋆. 𝕓{Abbr} V2 ⊢ ↓[0, 1] T2 ≡ T0 → ↑[0, 1] T0 ≡ T → + tpr (𝕚{Abbr} V1. T1) (𝕚{Abbr} V2. T) +| tpr_theta: ∀V,V1,V2,W1,W2,T1,T2. + tpr V1 V2 → ↑[0,1] V2 ≡ V → tpr W1 W2 → tpr T1 T2 → + tpr (𝕚{Appl} V1. 𝕚{Abbr} W1. T1) (𝕚{Abbr} W2. 𝕚{Appl} V. T2) +| tpr_zeta : ∀V,T,T1,T2. ↑[0,1] T1 ≡ T → tpr T1 T2 → + tpr (𝕚{Abbr} V. T) T2 +| tpr_tau : ∀V,T1,T2. tpr T1 T2 → tpr (𝕚{Cast} V. T1) T2 +. + +interpretation + "context-free parallel reduction (term)" + 'PR T1 T2 = (tpr T1 T2). + +(* Basic properties *********************************************************) + +lemma tpr_refl: ∀T. T ⇒ T. +#T elim T -T // +#I elim I -I /2/ +qed. + +(* The basic inversion lemmas ***********************************************) + +lemma tpr_inv_lref2_aux: ∀T1,T2. T1 ⇒ T2 → ∀i. T2 = #i → + ∨∨ T1 = #i + | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i & + T1 = 𝕓{Abbr} V. T + | ∃∃V,T. T ⇒ #i & T1 = 𝕗{Cast} V. T. +#T1 #T2 #H elim H -H T1 T2 +[ #k #i #H destruct +| #j #i /2/ +| #I #V1 #V2 #T1 #T2 #_ #_ #_ #_ #i #H destruct +| #I #V1 #V2 #T1 #T2 #_ #_ #_ #_ #i #H destruct +| #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #i #H destruct +| #V1 #V2 #T1 #T2 #T0 #T #_ #_ #_ #_ #_ #_ #i #H destruct +| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #i #H destruct +| #V #T #T1 #T2 #HT1 #HT12 #_ #i #H destruct /3 width=6/ +| #V #T1 #T2 #HT12 #_ #i #H destruct /3/ +] +qed. + +lemma tpr_inv_lref2: ∀T1,i. T1 ⇒ #i → + ∨∨ T1 = #i + | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i & + T1 = 𝕓{Abbr} V. T + | ∃∃V,T. T ⇒ #i & T1 = 𝕗{Cast} V. T. +/2/ qed. diff --git a/matita/matita/lib/lambda-delta/substitution/drop_defs.ma b/matita/matita/lib/lambda-delta/substitution/drop_defs.ma index 623467dd5..1bf8e278d 100644 --- a/matita/matita/lib/lambda-delta/substitution/drop_defs.ma +++ b/matita/matita/lib/lambda-delta/substitution/drop_defs.ma @@ -22,19 +22,19 @@ inductive drop: lenv → nat → nat → lenv → Prop ≝ drop (L1. 𝕓{I} V1) (d + 1) e (L2. 𝕓{I} V2) . -interpretation "dropping" 'RLift L2 d e L1 = (drop L1 d e L2). +interpretation "dropping" 'RDrop L1 d e L2 = (drop L1 d e L2). (* Basic properties *********************************************************) lemma drop_drop_lt: ∀L1,L2,I,V,e. - ↑[0, e - 1] L2 ≡ L1 → 0 < e → ↑[0, e] L2 ≡ L1. 𝕓{I} V. + ↓[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/ qed. (* Basic inversion lemmas ***************************************************) -lemma drop_inv_refl_aux: ∀d,e,L2,L1. ↑[d, e] L2 ≡ L1 → d = 0 → e = 0 → L1 = L2. -#d #e #L2 #L1 #H elim H -H d e L2 L1 +lemma drop_inv_refl_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 → e = 0 → L1 = L2. +#d #e #L1 #L2 #H elim H -H d e L1 L2 [ // | #L1 #L2 #I #V #e #_ #_ #_ #H elim (plus_S_eq_O_false … H) @@ -43,35 +43,35 @@ lemma drop_inv_refl_aux: ∀d,e,L2,L1. ↑[d, e] L2 ≡ L1 → d = 0 → e = 0 ] qed. -lemma drop_inv_refl: ∀L2,L1. ↑[0, 0] L2 ≡ L1 → L1 = L2. +lemma drop_inv_refl: ∀L1,L2. ↓[0, 0] L1 ≡ L2 → L1 = L2. /2 width=5/ qed. -lemma drop_inv_O1_aux: ∀d,e,L2,L1. ↑[d, e] L2 ≡ L1 → d = 0 → +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] L2 ≡ K). -#d #e #L2 #L1 #H elim H -H d e L2 L1 + (0 < e ∧ ↓[d, e - 1] K ≡ L2). +#d #e #L1 #L2 #H elim H -H d e L1 L2 [ /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) ] qed. -lemma drop_inv_O1: ∀e,L2,K,I,V. ↑[0, e] L2 ≡ K. 𝕓{I} V → +lemma drop_inv_O1: ∀e,K,I,V,L2. ↓[0, e] K. 𝕓{I} V ≡ L2 → (e = 0 ∧ L2 = K. 𝕓{I} V) ∨ - (0 < e ∧ ↑[0, e - 1] L2 ≡ K). + (0 < e ∧ ↓[0, e - 1] K ≡ L2). /2/ qed. -lemma drop_inv_drop1: ∀e,L2,K,I,V. - ↑[0, e] L2 ≡ K. 𝕓{I} V → 0 < e → ↑[0, e - 1] L2 ≡ K. -#e #L2 #K #I #V #H #He +lemma drop_inv_drop1: ∀e,K,I,V,L2. + ↓[0, e] K. 𝕓{I} V ≡ L2 → 0 < e → ↓[0, e - 1] K ≡ L2. +#e #K #I #V #L2 #H #He elim (drop_inv_O1 … H) -H * // #H destruct -e; elim (lt_refl_false … He) qed. -lemma drop_inv_skip2_aux: ∀d,e,L1,L2. ↑[d, e] L2 ≡ L1 → 0 < d → +lemma drop_inv_skip2_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d → ∀I,K2,V2. L2 = K2. 𝕓{I} V2 → - ∃∃K1,V1. ↑[d - 1, e] K2 ≡ K1 & + ∃∃K1,V1. ↓[d - 1, e] K1 ≡ K2 & ↑[d - 1, e] V2 ≡ V1 & L1 = K1. 𝕓{I} V1. #d #e #L1 #L2 #H elim H -H d e L1 L2 @@ -82,7 +82,7 @@ lemma drop_inv_skip2_aux: ∀d,e,L1,L2. ↑[d, e] L2 ≡ L1 → 0 < d → ] qed. -lemma drop_inv_skip2: ∀d,e,I,L1,K2,V2. ↑[d, e] K2. 𝕓{I} V2 ≡ L1 → 0 < d → - ∃∃K1,V1. ↑[d - 1, e] K2 ≡ K1 & ↑[d - 1, e] V2 ≡ V1 & +lemma drop_inv_skip2: ∀d,e,I,L1,K2,V2. ↓[d, e] L1 ≡ K2. 𝕓{I} V2 → 0 < d → + ∃∃K1,V1. ↓[d - 1, e] K1 ≡ K2 & ↑[d - 1, e] V2 ≡ V1 & L1 = K1. 𝕓{I} V1. /2/ qed. diff --git a/matita/matita/lib/lambda-delta/substitution/drop_main.ma b/matita/matita/lib/lambda-delta/substitution/drop_main.ma index 4665b770c..a305b78c7 100644 --- a/matita/matita/lib/lambda-delta/substitution/drop_main.ma +++ b/matita/matita/lib/lambda-delta/substitution/drop_main.ma @@ -18,9 +18,9 @@ include "lambda-delta/substitution/drop_defs.ma". (* the main properties ******************************************************) -lemma drop_conf_ge: ∀d1,e1,L,L1. ↑[d1, e1] L1 ≡ L → - ∀e2,L2. ↑[0, e2] L2 ≡ L → d1 + e1 ≤ e2 → - ↑[0, e2 - e1] L2 ≡ L1. +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 [ // | #L #K #I #V #e #_ #IHLK #e2 #L2 #H #He2 @@ -34,11 +34,11 @@ lemma drop_conf_ge: ∀d1,e1,L,L1. ↑[d1, e1] L1 ≡ L → ] qed. -lemma drop_conf_lt: ∀d1,e1,L,L1. ↑[d1, e1] L1 ≡ L → - ∀e2,K2,I,V2. ↑[0, e2] K2. 𝕓{I} V2 ≡ L → +lemma drop_conf_lt: ∀d1,e1,L,L1. ↓[d1, e1] L ≡ L1 → + ∀e2,K2,I,V2. ↓[0, e2] L ≡ K2. 𝕓{I} V2 → e2 < d1 → let d ≝ d1 - e2 - 1 in - ∃∃K1,V1. ↑[0, e2] K1. 𝕓{I} V1 ≡ L1 & - ↑[d, e1] K1 ≡ K2 & ↑[d,e1] V1 ≡ V2. + ∃∃K1,V1. ↓[0, e2] L1 ≡ K1. 𝕓{I} V1 & + ↓[d, e1] K2 ≡ K1 & ↑[d, e1] V1 ≡ V2. #d1 #e1 #L #L1 #H elim H -H d1 e1 L L1 [ #L0 #e2 #K2 #I #V2 #_ #H elim (lt_zero_false … H) @@ -53,9 +53,9 @@ lemma drop_conf_lt: ∀d1,e1,L,L1. ↑[d1, e1] L1 ≡ L → ] qed. -lemma drop_trans_le: ∀d1,e1,L1. ∀L:lenv. ↑[d1, e1] L ≡ L1 → - ∀e2,L2. ↑[0, e2] L2 ≡ L → e2 ≤ d1 → - ∃∃L0. ↑[0, e2] L0 ≡ L1 & ↑[d1 - e2, e1] L2 ≡ L0. +lemma drop_trans_le: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L → + ∀e2,L2. ↓[0, e2] L ≡ L2 → e2 ≤ d1 → + ∃∃L0. ↓[0, e2] L1 ≡ L0 & ↓[d1 - e2, e1] L0 ≡ L2. #d1 #e1 #L1 #L #H elim H -H d1 e1 L1 L [ #L #e2 #L2 #HL2 #H lapply (le_O_to_eq_O … H) -H #H destruct -e2 /2/ @@ -73,8 +73,8 @@ lemma drop_trans_le: ∀d1,e1,L1. ∀L:lenv. ↑[d1, e1] L ≡ L1 → ] qed. -lemma drop_trans_ge: ∀d1,e1,L1,L. ↑[d1, e1] L ≡ L1 → - ∀e2,L2. ↑[0, e2] L2 ≡ L → d1 ≤ e2 → ↑[0, e1 + e2] L2 ≡ L1. +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 [ // | /3/ @@ -86,5 +86,5 @@ lemma drop_trans_ge: ∀d1,e1,L1,L. ↑[d1, e1] L ≡ L1 → ] qed. -axiom drop_div: ∀e1,L1. ∀L:lenv. ↑[0, e1] L ≡ L1 → ∀e2,L2. ↑[0, e2] L ≡ L2 → - ∃∃L0. ↑[0, e1] L2 ≡ L0 & ↑[e1, e2] L1 ≡ L0. +axiom drop_div: ∀e1,L1,L. ↓[0, e1] L1 ≡ L → ∀e2,L2. ↓[0, e2] L2 ≡ L → + ∃∃L0. ↓[0, e1] L0 ≡ L2 & ↓[e1, e2] L0 ≡ L1. diff --git a/matita/matita/lib/lambda-delta/substitution/psubst_defs.ma b/matita/matita/lib/lambda-delta/substitution/psubst_defs.ma new file mode 100644 index 000000000..514e0ad2e --- /dev/null +++ b/matita/matita/lib/lambda-delta/substitution/psubst_defs.ma @@ -0,0 +1,78 @@ +(* + ||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/substitution/drop_defs.ma". + +(* PARALLEL SUBSTITUTION ****************************************************) + +inductive ps: lenv → term → nat → nat → term → Prop ≝ +| ps_sort : ∀L,k,d,e. ps L (⋆k) d e (⋆k) +| ps_lref : ∀L,i,d,e. ps L (#i) d e (#i) +| ps_subst: ∀L,K,V,U1,U2,i,d,e. + d ≤ i → i < d + e → + ↓[0, i] L ≡ K. 𝕓{Abbr} V → ps K V 0 (d + e - i - 1) U1 → + ↑[0, i + 1] U1 ≡ U2 → ps L (#i) d e U2 +| ps_bind : ∀L,I,V1,V2,T1,T2,d,e. + ps L V1 d e V2 → ps (L. 𝕓{I} V1) T1 (d + 1) e T2 → + ps L (𝕓{I} V1. T1) d e (𝕓{I} V2. T2) +| ps_flat : ∀L,I,V1,V2,T1,T2,d,e. + ps L V1 d e V2 → ps L T1 d e T2 → + ps L (𝕗{I} V1. T1) d e (𝕗{I} V2. T2) +. + +interpretation "parallel substritution" 'PSubst L T1 d e T2 = (ps L T1 d e T2). + +(* Basic properties *********************************************************) + +lemma subst_refl: ∀T,L,d,e. L ⊢ T [d, e] ≫ T. +#T elim T -T // +#I elim I -I /2/ +qed. + +(* Basic inversion lemmas ***************************************************) + +lemma ps_inv_bind1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ≫ U2 → + ∀I,V1,T1. U1 = 𝕓{I} V1. T1 → + ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 & + L. 𝕓{I} V1 ⊢ T1 [d + 1, e] ≫ T2 & + U2 = 𝕓{I} V2. T2. +#d #e #L #U1 #U2 #H elim H -H d e L U1 U2 +[ #L #k #d #e #I #V1 #T1 #H destruct +| #L #i #d #e #I #V1 #T1 #H destruct +| #L #K #V #U1 #U2 #i #d #e #_ #_ #_ #_ #_ #_ #I #V1 #T1 #H destruct +| #L #J #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #I #V #T #H destruct /2 width=5/ +| #L #J #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #I #V #T #H destruct +] +qed. + +lemma subst_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕓{I} V1. T1 [d, e] ≫ U2 → + ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 & + L. 𝕓{I} V1 ⊢ T1 [d + 1, e] ≫ T2 & + U2 = 𝕓{I} V2. T2. +/2/ qed. + +lemma subst_inv_flat1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ≫ U2 → + ∀I,V1,T1. U1 = 𝕗{I} V1. T1 → + ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 & L ⊢ T1 [d, e] ≫ T2 & + U2 = 𝕗{I} V2. T2. +#d #e #L #U1 #U2 #H elim H -H d e L U1 U2 +[ #L #k #d #e #I #V1 #T1 #H destruct +| #L #i #d #e #I #V1 #T1 #H destruct +| #L #K #V #U1 #U2 #i #d #e #_ #_ #_ #_ #_ #_ #I #V1 #T1 #H destruct +| #L #J #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #I #V #T #H destruct +| #L #J #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #I #V #T #H destruct /2 width=5/ +] +qed. + +lemma subst_inv_flat1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕗{I} V1. T1 [d, e] ≫ U2 → + ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 & L ⊢ T1 [d, e] ≫ T2 & + U2 = 𝕗{I} V2. T2. +/2/ qed. diff --git a/matita/matita/lib/lambda-delta/substitution/subst_defs.ma b/matita/matita/lib/lambda-delta/substitution/subst_defs.ma deleted file mode 100644 index c563157f4..000000000 --- a/matita/matita/lib/lambda-delta/substitution/subst_defs.ma +++ /dev/null @@ -1,112 +0,0 @@ -(* - ||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/substitution/drop_defs.ma". - -(* TELESCOPIC SUBSTITUTION **************************************************) - -inductive subst: lenv → term → nat → nat → term → Prop ≝ -| subst_sort : ∀L,k,d,e. subst L (⋆k) d e (⋆k) -| subst_lref_lt: ∀L,i,d,e. i < d → subst L (#i) d e (#i) -| subst_lref_be: ∀L,K,V,U1,U2,i,d,e. - d ≤ i → i < d + e → - ↑[0, i] K. 𝕓{Abbr} V ≡ L → subst K V 0 (d + e - i - 1) U1 → - ↑[0, d] U1 ≡ U2 → subst L (#i) d e U2 -| subst_lref_ge: ∀L,i,d,e. d + e ≤ i → subst L (#i) d e (#(i - e)) -| subst_bind : ∀L,I,V1,V2,T1,T2,d,e. - subst L V1 d e V2 → subst (L. 𝕓{I} V1) T1 (d + 1) e T2 → - subst L (𝕓{I} V1. T1) d e (𝕓{I} V2. T2) -| subst_flat : ∀L,I,V1,V2,T1,T2,d,e. - subst L V1 d e V2 → subst L T1 d e T2 → - subst L (𝕗{I} V1. T1) d e (𝕗{I} V2. T2) -. - -interpretation "telescopic substritution" 'RSubst L T1 d e T2 = (subst L T1 d e T2). - -(* The basic properties *****************************************************) - -lemma subst_lift_inv: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀L. L ⊢ ↓[d,e] T2 ≡ T1. -#d #e #T1 #T2 #H elim H -H d e T1 T2 /2/ -#i #d #e #Hdi #L >(minus_plus_m_m i e) in ⊢ (? ? ? ? ? %) /3/ -qed. -(* -| subst_lref_O : ∀L,V1,V2,e. subst L V1 0 e V2 → - subst (L. 𝕓{Abbr} V1) #0 0 (e + 1) V2 -| subst_lref_S : ∀L,I,V,i,T1,T2,d,e. - d ≤ i → i < d + e → subst L #i d e T1 → ↑[d,1] T2 ≡ T1 → - subst (L. 𝕓{I} V) #(i + 1) (d + 1) e T2 -*) -(* The basic inversion lemmas ***********************************************) - -lemma subst_inv_bind1_aux: ∀d,e,L,U1,U2. L ⊢ ↓[d, e] U1 ≡ U2 → - ∀I,V1,T1. U1 = 𝕓{I} V1. T1 → - ∃∃V2,T2. subst L V1 d e V2 & - subst (L. 𝕓{I} V1) T1 (d + 1) e T2 & - U2 = 𝕓{I} V2. T2. -#d #e #L #U1 #U2 #H elim H -H d e L U1 U2 -[ #L #k #d #e #I #V1 #T1 #H destruct -| #L #i #d #e #_ #I #V1 #T1 #H destruct -| #L #K #V #U1 #U2 #i #d #e #_ #_ #_ #_ #_ #_ #I #V1 #T1 #H destruct -| #L #i #d #e #_ #I #V1 #T1 #H destruct -| #L #J #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #I #V #T #H destruct /2 width=5/ -| #L #J #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #I #V #T #H destruct -] -qed. - -lemma subst_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ ↓[d, e] 𝕓{I} V1. T1 ≡ U2 → - ∃∃V2,T2. subst L V1 d e V2 & - subst (L. 𝕓{I} V1) T1 (d + 1) e T2 & - U2 = 𝕓{I} V2. T2. -/2/ qed. - -lemma subst_inv_flat1_aux: ∀d,e,L,U1,U2. L ⊢ ↓[d, e] U1 ≡ U2 → - ∀I,V1,T1. U1 = 𝕗{I} V1. T1 → - ∃∃V2,T2. subst L V1 d e V2 & subst L T1 d e T2 & - U2 = 𝕗{I} V2. T2. -#d #e #L #U1 #U2 #H elim H -H d e L U1 U2 -[ #L #k #d #e #I #V1 #T1 #H destruct -| #L #i #d #e #_ #I #V1 #T1 #H destruct -| #L #K #V #U1 #U2 #i #d #e #_ #_ #_ #_ #_ #_ #I #V1 #T1 #H destruct -| #L #i #d #e #_ #I #V1 #T1 #H destruct -| #L #J #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #I #V #T #H destruct -| #L #J #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #I #V #T #H destruct /2 width=5/ -] -qed. - -lemma subst_inv_flat1: ∀d,e,L,I,V1,T1,U2. L ⊢ ↓[d, e] 𝕗{I} V1. T1 ≡ U2 → - ∃∃V2,T2. subst L V1 d e V2 & subst L T1 d e T2 & - U2 = 𝕗{I} V2. T2. -/2/ qed. -(* -lemma subst_inv_lref1_be_aux: ∀d,e,L,T,U. L ⊢ ↓[d, e] T ≡ U → - ∀i. d ≤ i → i < d + e → T = #i → - ∃∃K,V. ↑[0, i] K. 𝕓{Abbr} V ≡ L & - K ⊢ ↓[d, d + e - i - 1] V ≡ U. -#d #e #L #T #U #H elim H -H d e L T U -[ #L #k #d #e #i #_ #_ #H destruct -| #L #j #d #e #Hid #i #Hdi #_ #H destruct -j; - lapply (le_to_lt_to_lt … Hdi … Hid) -Hdi Hid #Hdd - elim (lt_false … Hdd) -| #L #K #V #U #j #d #e #_ #_ #HLK #HVU #_ #i #Hdi #Hide #H destruct -j /2/ -| #L #j #d #e #Hdei #i #_ #Hide #H destruct -j; - lapply (le_to_lt_to_lt … Hdei … Hide) -Hdei Hide #Hdede - elim (lt_false … Hdede) -| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #i #_ #_ #H destruct -| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #i #_ #_ #H destruct -] -qed. - -lemma subst_inv_lref1_be: ∀d,e,i,L,U. L ⊢ ↓[d, e] #i ≡ U → - d ≤ i → i < d + e → - ∃∃K,V. ↑[0, i] K. 𝕓{Abbr} V ≡ L & - K ⊢ ↓[d, d + e - i - 1] V ≡ U. -/2/ qed. -*) diff --git a/matita/matita/lib/lambda-delta/substitution/thin_defs.ma b/matita/matita/lib/lambda-delta/substitution/thin_defs.ma deleted file mode 100644 index c8ef44925..000000000 --- a/matita/matita/lib/lambda-delta/substitution/thin_defs.ma +++ /dev/null @@ -1,44 +0,0 @@ -(* - ||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/substitution/subst_defs.ma". - -(* THINNING *****************************************************************) - -inductive thin: lenv → nat → nat → lenv → Prop ≝ -| thin_refl: ∀L. thin L 0 0 L -| thin_thin: ∀L1,L2,I,V,e. thin L1 0 e L2 → thin (L1. 𝕓{I} V) 0 (e + 1) L2 -| thin_skip: ∀L1,L2,I,V1,V2,d,e. - thin L1 d e L2 → L1 ⊢ ↓[d,e] V1 ≡ V2 → - thin (L1. 𝕓{I} V1) (d + 1) e (L2. 𝕓{I} V2) -. - -interpretation "thinning" 'RSubst L1 d e L2 = (thin L1 d e L2). - -(* the basic inversion lemmas ***********************************************) - -lemma thin_inv_skip2_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d → - ∀I,K2,V2. L2 = K2. 𝕓{I} V2 → - ∃∃K1,V1. ↓[d - 1, e] K1 ≡ K2 & - K1 ⊢ ↓[d - 1, e] V1 ≡ V2 & - L1 = K1. 𝕓{I} V1. -#d #e #L1 #L2 #H elim H -H d e L1 L2 -[ #L #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/ -] -qed. - -lemma thin_inv_skip2: ∀d,e,I,L1,K2,V2. ↓[d, e] L1 ≡ K2. 𝕓{I} V2 → 0 < d → - ∃∃K1,V1. ↓[d - 1, e] K1 ≡ K2 & K1 ⊢ ↓[d - 1, e] V1 ≡ V2 & - L1 = K1. 𝕓{I} V1. -/2/ qed. diff --git a/matita/matita/lib/lambda-delta/syntax/item.ma b/matita/matita/lib/lambda-delta/syntax/item.ma index 742ff2272..ea7a45362 100644 --- a/matita/matita/lib/lambda-delta/syntax/item.ma +++ b/matita/matita/lib/lambda-delta/syntax/item.ma @@ -16,6 +16,7 @@ *) include "lambda-delta/ground.ma". +include "lambda-delta/notation.ma". (* BINARY ITEMS *************************************************************) diff --git a/matita/matita/lib/lambda-delta/xoa_defs.ma b/matita/matita/lib/lambda-delta/xoa_defs.ma index 38c434304..5e66ef789 100644 --- a/matita/matita/lib/lambda-delta/xoa_defs.ma +++ b/matita/matita/lib/lambda-delta/xoa_defs.ma @@ -40,18 +40,11 @@ inductive ex3_3 (A0,A1,A2:Type[0]) (P0,P1,P2:A0→A1→A2→Prop) : Prop ≝ interpretation "multiple existental quantifier (3, 3)" 'Ex P0 P1 P2 = (ex3_3 ? ? ? P0 P1 P2). -inductive ex4_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3:A0→A1→A2→Prop) : Prop ≝ - | ex4_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → P3 x0 x1 x2 → ex4_3 ? ? ? ? ? ? ? +inductive or3 (P0,P1,P2:Prop) : Prop ≝ + | or3_intro0: P0 → or3 ? ? ? + | or3_intro1: P1 → or3 ? ? ? + | or3_intro2: P2 → or3 ? ? ? . -interpretation "multiple existental quantifier (4, 3)" 'Ex P0 P1 P2 P3 = (ex4_3 ? ? ? P0 P1 P2 P3). - -inductive or4 (P0,P1,P2,P3:Prop) : Prop ≝ - | or4_intro0: P0 → or4 ? ? ? ? - | or4_intro1: P1 → or4 ? ? ? ? - | or4_intro2: P2 → or4 ? ? ? ? - | or4_intro3: P3 → or4 ? ? ? ? -. - -interpretation "multiple disjunction connective (4)" 'Or P0 P1 P2 P3 = (or4 P0 P1 P2 P3). +interpretation "multiple disjunction connective (3)" 'Or P0 P1 P2 = (or3 P0 P1 P2). diff --git a/matita/matita/lib/lambda-delta/xoa_notation.ma b/matita/matita/lib/lambda-delta/xoa_notation.ma index 2e441f1cb..f21488be3 100644 --- a/matita/matita/lib/lambda-delta/xoa_notation.ma +++ b/matita/matita/lib/lambda-delta/xoa_notation.ma @@ -30,11 +30,7 @@ notation "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & non associative with precedence 20 for @{ 'Ex (λ${ident x0},${ident x1},${ident x2}.$P0) (λ${ident x0},${ident x1},${ident x2}.$P1) (λ${ident x0},${ident x1},${ident x2}.$P2) }. -notation "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" +notation "hvbox(∨∨ term 19 P0 break | term 19 P1 break | term 19 P2)" non associative with precedence 20 - for @{ 'Ex (λ${ident x0},${ident x1},${ident x2}.$P0) (λ${ident x0},${ident x1},${ident x2}.$P1) (λ${ident x0},${ident x1},${ident x2}.$P2) (λ${ident x0},${ident x1},${ident x2}.$P3) }. - -notation "hvbox(∨∨ term 19 P0 break | term 19 P1 break | term 19 P2 break | term 19 P3)" - non associative with precedence 20 - for @{ 'Or $P0 $P1 $P2 $P3 }. + for @{ 'Or $P0 $P1 $P2 }. -- 2.39.2