From 4c4b73b9ccf2e93901d0352599623c851781b74b Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 26 Jul 2011 19:47:31 +0000 Subject: [PATCH] tpr: more inversion lemmas and a main property stated --- .../lib/lambda-delta/reduction/tpr_defs.ma | 30 +++ .../lib/lambda-delta/reduction/tpr_ps.ma | 26 +++ .../lib/lambda-delta/reduction/tpr_tpr.ma | 198 +++++++++++------- matita/matita/lib/lambda-delta/xoa_defs.ma | 33 +++ .../matita/lib/lambda-delta/xoa_notation.ma | 22 +- 5 files changed, 236 insertions(+), 73 deletions(-) create mode 100644 matita/matita/lib/lambda-delta/reduction/tpr_ps.ma diff --git a/matita/matita/lib/lambda-delta/reduction/tpr_defs.ma b/matita/matita/lib/lambda-delta/reduction/tpr_defs.ma index 498fbb744..a8aac61df 100644 --- a/matita/matita/lib/lambda-delta/reduction/tpr_defs.ma +++ b/matita/matita/lib/lambda-delta/reduction/tpr_defs.ma @@ -127,6 +127,18 @@ lemma tpr_inv_abst1: ∀V1,T1,U2. 𝕚{Abst} V1. T1 ⇒ U2 → ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Abst} V2. T2. /2/ qed. +lemma tpr_inv_bind1: ∀V1,T1,U2,I. 𝕓{I} V1. T1 ⇒ U2 → + ∨∨ ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕓{I} V2. T2 + | ∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 & + ⋆. 𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T & + U2 = 𝕚{Abbr} V2. T & I = Abbr + | ∃∃T. ↑[0,1] T ≡ T1 & tpr T U2 & I = Abbr. +#V1 #T1 #U2 * #H +[ elim (tpr_inv_abbr1 … H) -H * /3 width=7/ +| /3/ +] +qed. + lemma tpr_inv_appl1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,U0. U1 = 𝕚{Appl} V1. U0 → ∨∨ ∃∃V2,T2. V1 ⇒ V2 & U0 ⇒ T2 & U2 = 𝕚{Appl} V2. T2 @@ -184,6 +196,24 @@ lemma tpr_inv_cast1: ∀V1,T1,U2. 𝕚{Cast} V1. T1 ⇒ U2 → ∨ T1 ⇒ U2. /2/ qed. +lemma tpr_inv_flat1: ∀V1,U0,U2,I. 𝕗{I} V1. U0 ⇒ U2 → + ∨∨ ∃∃V2,T2. V1 ⇒ V2 & U0 ⇒ T2 & + U2 = 𝕗{I} V2. T2 + | ∃∃V2,W,T1,T2. V1 ⇒ V2 & T1 ⇒ T2 & + U0 = 𝕚{Abst} W. T1 & + U2 = 𝕓{Abbr} V2. T2 & I = Appl + | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 & + ↑[0,1] V2 ≡ V & + U0 = 𝕚{Abbr} W1. T1 & + U2 = 𝕚{Abbr} W2. 𝕚{Appl} V. T2 & + I = Appl + | (U0 ⇒ U2 ∧ I = Cast). +#V1 #U0 #U2 * #H +[ elim (tpr_inv_appl1 … H) -H * /3 width=12/ +| elim (tpr_inv_cast1 … H) -H [1: *] /3 width=5/ +] +qed. + lemma tpr_inv_lref2_aux: ∀T1,T2. T1 ⇒ T2 → ∀i. T2 = #i → ∨∨ T1 = #i | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i & diff --git a/matita/matita/lib/lambda-delta/reduction/tpr_ps.ma b/matita/matita/lib/lambda-delta/reduction/tpr_ps.ma new file mode 100644 index 000000000..dc4a1098c --- /dev/null +++ b/matita/matita/lib/lambda-delta/reduction/tpr_ps.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reduction/lpr_defs.ma". + +(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) + +axiom tpr_ps_lpr: ∀L1,L2. L1 ⇒ L2 → ∀T1,T2. T1 ⇒ T2 → + ∀d,e,U1. L1 ⊢ T1 [d, e] ≫ U1 → + ∃∃U2. U1 ⇒ U2 & L2 ⊢ T2 [d, e] ≫ U2. + +lemma tpr_ps_bind: ∀I,V1,V2,T1,T2,U1. V1 ⇒ V2 → T1 ⇒ T2 → + ⋆. 𝕓{I} V1 ⊢ T1 [0, 1] ≫ U1 → + ∃∃U2. U1 ⇒ U2 & ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ U2. +/3 width=5/ qed. diff --git a/matita/matita/lib/lambda-delta/reduction/tpr_tpr.ma b/matita/matita/lib/lambda-delta/reduction/tpr_tpr.ma index da8a55071..6e632f72d 100644 --- a/matita/matita/lib/lambda-delta/reduction/tpr_tpr.ma +++ b/matita/matita/lib/lambda-delta/reduction/tpr_tpr.ma @@ -9,111 +9,156 @@ \ / V_______________________________________________________________ *) +include "lambda-delta/substitution/lift_fun.ma". include "lambda-delta/substitution/lift_weight.ma". include "lambda-delta/reduction/tpr_main.ma". +include "lambda-delta/reduction/tpr_ps.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) (* Confluence lemmas ********************************************************) -lemma tpr_conf_sort_sort: ∀k1. ∃∃T0. ⋆k1 ⇒ T0 & ⋆k1 ⇒ T0. +lemma tpr_conf_sort_sort: ∀k. ∃∃X. ⋆k ⇒ X & ⋆k ⇒ X. /2/ qed. -lemma tpr_conf_lref_lref: ∀i1. ∃∃T0. #i1 ⇒ T0 & #i1 ⇒ T0. +lemma tpr_conf_lref_lref: ∀i. ∃∃X. #i ⇒ X & #i ⇒ X. /2/ qed. lemma tpr_conf_bind_bind: - ∀I1,V11,V12,T11,T12,V22,T22. ( - ∀T1. #T1 < #V11 + #T11 + 1 → - ∀T3,T4. T1 ⇒ T3 → T1 ⇒ T4 → - ∃∃T0. T3 ⇒ T0 & T4 ⇒ T0 + ∀I,V0,V1,T0,T1,V2,T2. ( + ∀X0:term. #X0 < #V0 + #T0 + 1 → + ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → + ∃∃X. X1 ⇒ X & X2 ⇒ X + ) → + V0 ⇒ V1 → V0 ⇒ V2 → T0 ⇒ T1 → T0 ⇒ T2 → + ∃∃X. 𝕓{I} V1. T1 ⇒ X & 𝕓{I} V2. T2 ⇒ X. +#I #V0 #V1 #T0 #T1 #V2 #T2 #IH #HV01 #HV02 #HT01 #HT02 +elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2 +elim (IH … HT01 … HT02) -HT01 HT02 IH /3 width=5/ +qed. + +lemma tpr_conf_bind_delta: + ∀V0,V1,T0,T1,V2,T2,T. ( + ∀X0:term. #X0 < #V0 + #T0 + 1 → + ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → + ∃∃X. X1 ⇒ X & X2 ⇒ X ) → - V11 ⇒ V12 → T11 ⇒ T12 → - V11 ⇒ V22 → T11 ⇒ T22 → - ∃∃T0. 𝕓{I1} V12. T12 ⇒ T0 & 𝕓{I1} V22. T22 ⇒ T0. -#I1 #V11 #V12 #T11 #T12 #V22 #T22 #IH #HV1 #HT1 #HV2 #HT2 -elim (IH … HV1 … HV2) -HV1 HV2 // #V #HV1 #HV2 -elim (IH … HT1 … HT2) -HT1 HT2 IH /3 width=5/ + V0 ⇒ V1 → V0 ⇒ V2 → + T0 ⇒ T1 → T0 ⇒ T2 → ⋆. 𝕓{Abbr} V2 ⊢ T2 [O,1] ≫ T → + ∃∃X. 𝕓{Abbr} V1. T1 ⇒ X & 𝕓{Abbr} V2. T ⇒ X. +#V0 #V1 #T0 #T1 #V2 #T2 #T #IH #HV01 #HV02 #HT01 #HT02 #HT2 +elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2 +elim (IH … HT01 … HT02) -HT01 HT02 IH // -V0 T0 #T0 #HT10 #HT20 +elim (tpr_ps_bind … HV2 HT20 … HT2) -HT20 HT2 /3 width=5/ qed. lemma tpr_conf_bind_zeta: - ∀V11,V12,T11,T12,T22,T20. ( - ∀T1. #T1 < #V11 + #T11 +1 → - ∀T3,T4. T1 ⇒ T3 → T1 ⇒ T4 → - ∃∃T0. T3 ⇒ T0 & T4 ⇒ T0 + ∀X2,V0,V1,T0,T1,T. ( + ∀X0:term. #X0 < #V0 + #T0 +1 → + ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → + ∃∃X. X1 ⇒ X & X2 ⇒ X ) → - V11 ⇒ V12 → T22 ⇒ T20 → T11 ⇒ T12 → ↑[O, 1] T22 ≡ T11 → - ∃∃T0. 𝕓{Abbr} V12. T12 ⇒ T0 & T20 ⇒ T0. -#V11 #V12 #T11 #T12 #T22 #T20 #IH #HV112 #HT202 #HT112 #HT -elim (tpr_inv_lift … HT112 … HT) -HT112 #T #HT12 #HT22 -lapply (tw_lift … HT) -HT #HT -elim (IH … HT202 … HT22) -HT202 HT22 IH /3/ + V0 ⇒ V1 → T0 ⇒ T1 → T ⇒ X2 → ↑[O, 1] T ≡ T0 → + ∃∃X. 𝕓{Abbr} V1. T1 ⇒ X & X2 ⇒ X. +#X2 #V0 #V1 #T0 #T1 #T #IH #HV01 #HT01 #HTX2 #HT0 +elim (tpr_inv_lift … HT01 … HT0) -HT01 #U #HUT1 #HTU +lapply (tw_lift … HT0) -HT0 #HT0 +elim (IH … HTX2 … HTU) -HTX2 HTU IH /3/ qed. lemma tpr_conf_flat_flat: - ∀I1,V11,V12,T11,T12,V22,T22. ( - ∀T1. #T1 < #V11 + #T11 + 1 → - ∀T3,T4. T1 ⇒ T3 → T1 ⇒ T4 → - ∃∃T0. T3 ⇒ T0 & T4 ⇒ T0 + ∀I,V0,V1,T0,T1,V2,T2. ( + ∀X0:term. #X0 < #V0 + #T0 + 1 → + ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → + ∃∃X. X1 ⇒ X & X2 ⇒ X ) → - V11 ⇒ V12 → T11 ⇒ T12 → - V11 ⇒ V22 → T11 ⇒ T22 → - ∃∃T0. 𝕗{I1} V12. T12 ⇒ T0 & 𝕗{I1} V22. T22 ⇒ T0. -#I1 #V11 #V12 #T11 #T12 #V22 #T22 #IH #HV1 #HT1 #HV2 #HT2 -elim (IH … HV1 … HV2) -HV1 HV2 // #V #HV1 #HV2 -elim (IH … HT1 … HT2) -HT1 HT2 /3 width=5/ + V0 ⇒ V1 → V0 ⇒ V2 → T0 ⇒ T1 → T0 ⇒ T2 → + ∃∃T0. 𝕗{I} V1. T1 ⇒ T0 & 𝕗{I} V2. T2 ⇒ T0. +#I #V0 #V1 #T0 #T1 #V2 #T2 #IH #HV01 #HV02 #HT01 #HT02 +elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2 +elim (IH … HT01 … HT02) -HT01 HT02 /3 width=5/ qed. lemma tpr_conf_flat_beta: - ∀V11,V12,T12,V22,W2,T21,T22. ( - ∀T1. #T1 < #V11 + (#W2 + #T21 + 1) + 1 → - ∀T3,T4. T1 ⇒ T3 → T1 ⇒ T4 → - ∃∃T0. T3 ⇒ T0 & T4 ⇒ T0 + ∀V0,V1,T1,V2,W0,U0,T2. ( + ∀X0:term. #X0 < #V0 + (#W0 + #U0 + 1) + 1 → + ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → + ∃∃X. X1 ⇒ X & X2 ⇒ X ) → - V11 ⇒ V12 → V11 ⇒ V22 → - T21 ⇒ T22 → 𝕓{Abst} W2. T21 ⇒ T12 → - ∃∃T0. 𝕗{Appl} V12. T12 ⇒ T0 & 𝕓{Abbr} V22. T22 ⇒ T0. -#V11 #V12 #T12 #V22 #W2 #T21 #T22 #IH #HV1 #HV2 #HT1 #HT2 -elim (tpr_inv_abst1 … HT2) -HT2 #W1 #T1 #HW21 #HT21 #H destruct -T12; -elim (IH … HV1 … HV2) -HV1 HV2 // #V #HV12 #HV22 -elim (IH … HT21 … HT1) -HT21 HT1 IH /3 width=5/ + V0 ⇒ V1 → V0 ⇒ V2 → + U0 ⇒ T2 → 𝕓{Abst} W0. U0 ⇒ T1 → + ∃∃X. 𝕗{Appl} V1. T1 ⇒ X & 𝕓{Abbr} V2. T2 ⇒ X. +#V0 #V1 #T1 #V2 #W0 #U0 #T2 #IH #HV01 #HV02 #HT02 #H +elim (tpr_inv_abst1 … H) -H #W1 #U1 #HW01 #HU01 #H destruct -T1; +elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2 +elim (IH … HT02 … HU01) -HT02 HU01 IH /3 width=5/ qed. -(* + lemma tpr_conf_flat_theta: - ∀V11,V12,T12,V2,V22,W21,W22,T21,T22. ( - ∀T1. #T1 < #V11 + (#W21 + #T21 + 1) + 1 → - ∀T3,T4. T1 ⇒ T3 → T1 ⇒ T4 → - ∃∃T0. T3 ⇒ T0 & T4 ⇒T0 + ∀V0,V1,T1,V2,V,W0,W2,U0,U2. ( + ∀X0:term. #X0 < #V0 + (#W0 + #U0 + 1) + 1 → + ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → + ∃∃X. X1 ⇒ X & X2 ⇒ X ) → - V11 ⇒ V12 → V11 ⇒ V22 → ↑[O,1] V22 ≡ V2 → - W21 ⇒ W22 → T21 ⇒ T22 → 𝕓{Abbr} W21. T21 ⇒ T12 → - ∃∃T0. 𝕗{Appl} V12. T12 ⇒ T0 & 𝕓{Abbr} W22. 𝕗{Appl} V2. T22 ⇒T0. -*) - + V0 ⇒ V1 → V0 ⇒ V2 → ↑[O,1] V2 ≡ V → + W0 ⇒ W2 → U0 ⇒ U2 → 𝕓{Abbr} W0. U0 ⇒ T1 → + ∃∃X. 𝕗{Appl} V1. T1 ⇒ X & 𝕓{Abbr} W2. 𝕗{Appl} V. U2 ⇒ X. +#V0 #V1 #T1 #V2 #V #W0 #W2 #U0 #U2 #IH #HV01 #HV02 #HV2 #HW02 #HU02 #H +elim (IH … HV01 … HV02) -HV01 HV02 // #VV #HVV1 #HVV2 +elim (lift_total VV 0 1) #VVV #HVV +lapply (tpr_lift … HVV2 … HV2 … HVV) #HVVV +elim (tpr_inv_abbr1 … H) -H * +(* case 1: bind *) +[ -HV2 HVV2 #WW #UU #HWW0 #HUU0 #H destruct -T1; + elim (IH … HW02 … HWW0) -HW02 HWW0 // #W #HW2 #HWW + elim (IH … HU02 … HUU0) -HU02 HUU0 IH // #U #HU2 #HUU + @ex2_1_intro + [2: @tpr_theta [5: @HVV1 |6: @HVV |7:// by {}; (*@HWW*) |8: @HUU |1,2,3,4:skip ] + |3: @tpr_bind [ @HW2 | @tpr_flat [ @HVVV | @HU2 ] ] + | skip (* Confluence ***************************************************************) -(* + lemma tpr_conf_aux: - ∀T. ( - ∀T1. #T1 < #T → ∀T3,T4. T1 ⇒ T3 → T1 ⇒ T4 → - ∃∃T0. T3 ⇒ T0 & T4 ⇒ T0 + ∀Y0:term. ( + ∀X0:term. #X0 < #Y0 → ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → + ∃∃X. X1 ⇒ X & X2 ⇒ X ) → - ∀U1,T1,T2. U1 ⇒ T1 → U1 ⇒ T2 → U1 = T → - ∃∃T0. T1 ⇒ T0 & T2 ⇒ T0. -#T #IH #U1 #T1 #T2 * -U1 T1 -[ #k1 #H1 #H2 destruct -T; + ∀X0,X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → X0 = Y0 → + ∃∃X. X1 ⇒ X & X2 ⇒ X. +#Y0 #IH #X0 #X1 #X2 * -X0 X1 +[ #k1 #H1 #H2 destruct -Y0; lapply (tpr_inv_sort1 … H1) -H1 -(* case 1: sort, sort *) - #H1 destruct -T2 // -| #i1 #H1 #H2 destruct -T; +(* case 1: sort, sort *) + #H1 destruct -X2 // +| #i1 #H1 #H2 destruct -Y0; lapply (tpr_inv_lref1 … H1) -H1 -(* case 2: lref, lref *) - #H1 destruct -T2 // -| #I1 #V11 #V12 #T11 #T12 #HV112 #HT112 #H1 #H2 destruct -T; - lapply (tpr_inv_bind1 … H1) -H1 - [ - -theorem tpr_conf: ∀T,T1,T2. T ⇒ T1 → T ⇒ T2 → - ∃∃T0. T1 ⇒ T0 & T2 ⇒ T0. +(* case 2: lref, lref *) + #H1 destruct -X2 // +| #I #V0 #V1 #T0 #T1 #HV01 #HT01 #H1 #H2 destruct -Y0; + elim (tpr_inv_bind1 … H1) -H1 * +(* case 3: bind, bind *) + [ #V2 #T2 #HV02 #HT02 #H destruct -X2 + @tpr_conf_bind_bind /2 width=7/ (**) (* /3 width=7/ is too slow *) +(* case 4: bind, delta *) + | #V2 #T2 #T #HV02 #HT02 #HT2 #H1 #H2 destruct -X2 I + @tpr_conf_bind_delta /2 width=9/ (**) (* /3 width=9/ is too slow *) +(* case 5: bind, zeta *) + | #T #HT0 #HTX2 #H destruct -I + @tpr_conf_bind_zeta /2 width=8/ (**) (* /3 width=8/ is too slow *) + ] +| #I #V0 #V1 #T0 #T1 #HV01 #HT01 #H1 #H2 destruct -Y0; + elim (tpr_inv_flat1 … H1) -H1 * +(* case 6: flat, flat *) + [ #V2 #T2 #HV02 #HT02 #H destruct -X2 + @tpr_conf_flat_flat /2 width=7/ (**) (* /3 width=7/ is too slow *) +(* case 7: flat, beta *) + | #V2 #W #U0 #T2 #HV02 #HT02 #H1 #H2 #H3 destruct -T0 X2 I + @tpr_conf_flat_beta /2 width=8/ (**) (* /3 width=8/ is too slow *) +(* case 8: flat, theta *) + | #V2 #V #W0 #W2 #U0 #U2 #HV02 #HW02 #HT02 #HV2 #H1 #H2 #H3 destruct -T0 X2 I + // +theorem tpr_conf: ∀T0,T1,T2. T0 ⇒ T1 → T0 ⇒ T2 → + ∃∃T. T1 ⇒ T & T2 ⇒ T. #T @(tw_wf_ind … T) -T /3 width=6/ qed. *) @@ -218,3 +263,12 @@ lemma tpr_conf_flat_theta: W21 ⇒ W22 → T21 ⇒ T22 → 𝕓{Abbr} W21. T21 ⇒ T12 → ∃∃T0. 𝕗{Appl} V12. T12 ⇒ T0 & 𝕓{Abbr} W22. 𝕗{Appl} V2. T22 ⇒T0. +lemma tpr_conf_bind_delta: + ∀V0,V1,T0,T1,V2,T2,T. ( + ∀X. #X < #V0 + #T0 + 1 → + ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → + ∃∃X. X1 ⇒ X & X2⇒X + ) → + V0 ⇒ V1 → V0 ⇒ V2 → + T0 ⇒ T1 → T0 ⇒ T2 → ⋆. 𝕓{Abbr} V2 ⊢ T2 [O,1] ≫ T → + ∃∃X. 𝕓{Abbr} V1. T1 ⇒ X & 𝕓{Abbr} V2. T ⇒ X. \ No newline at end of file diff --git a/matita/matita/lib/lambda-delta/xoa_defs.ma b/matita/matita/lib/lambda-delta/xoa_defs.ma index af9ba3708..9dbf226f4 100644 --- a/matita/matita/lib/lambda-delta/xoa_defs.ma +++ b/matita/matita/lib/lambda-delta/xoa_defs.ma @@ -28,6 +28,12 @@ inductive ex2_2 (A0,A1:Type[0]) (P0,P1:A0→A1→Prop) : Prop ≝ interpretation "multiple existental quantifier (2, 2)" 'Ex P0 P1 = (ex2_2 ? ? P0 P1). +inductive ex3_1 (A0:Type[0]) (P0,P1,P2:A0→Prop) : Prop ≝ + | ex3_1_intro: ∀x0. P0 x0 → P1 x0 → P2 x0 → ex3_1 ? ? ? ? +. + +interpretation "multiple existental quantifier (3, 1)" 'Ex P0 P1 P2 = (ex3_1 ? P0 P1 P2). + inductive ex3_2 (A0,A1:Type[0]) (P0,P1,P2:A0→A1→Prop) : Prop ≝ | ex3_2_intro: ∀x0,x1. P0 x0 x1 → P1 x0 x1 → P2 x0 x1 → ex3_2 ? ? ? ? ? . @@ -52,12 +58,30 @@ inductive ex4_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3:A0→A1→A2→A3→Prop) : P interpretation "multiple existental quantifier (4, 4)" 'Ex P0 P1 P2 P3 = (ex4_4 ? ? ? ? P0 P1 P2 P3). +inductive ex5_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3,P4:A0→A1→A2→Prop) : Prop ≝ + | ex5_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → P3 x0 x1 x2 → P4 x0 x1 x2 → ex5_3 ? ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (5, 3)" 'Ex P0 P1 P2 P3 P4 = (ex5_3 ? ? ? P0 P1 P2 P3 P4). + +inductive ex5_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4:A0→A1→A2→A3→Prop) : Prop ≝ + | ex5_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → P3 x0 x1 x2 x3 → P4 x0 x1 x2 x3 → ex5_4 ? ? ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (5, 4)" 'Ex P0 P1 P2 P3 P4 = (ex5_4 ? ? ? ? P0 P1 P2 P3 P4). + inductive ex6_6 (A0,A1,A2,A3,A4,A5:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→A3→A4→A5→Prop) : Prop ≝ | ex6_6_intro: ∀x0,x1,x2,x3,x4,x5. P0 x0 x1 x2 x3 x4 x5 → P1 x0 x1 x2 x3 x4 x5 → P2 x0 x1 x2 x3 x4 x5 → P3 x0 x1 x2 x3 x4 x5 → P4 x0 x1 x2 x3 x4 x5 → P5 x0 x1 x2 x3 x4 x5 → ex6_6 ? ? ? ? ? ? ? ? ? ? ? ? . interpretation "multiple existental quantifier (6, 6)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_6 ? ? ? ? ? ? P0 P1 P2 P3 P4 P5). +inductive ex7_6 (A0,A1,A2,A3,A4,A5:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→A4→A5→Prop) : Prop ≝ + | ex7_6_intro: ∀x0,x1,x2,x3,x4,x5. P0 x0 x1 x2 x3 x4 x5 → P1 x0 x1 x2 x3 x4 x5 → P2 x0 x1 x2 x3 x4 x5 → P3 x0 x1 x2 x3 x4 x5 → P4 x0 x1 x2 x3 x4 x5 → P5 x0 x1 x2 x3 x4 x5 → P6 x0 x1 x2 x3 x4 x5 → ex7_6 ? ? ? ? ? ? ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (7, 6)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_6 ? ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6). + inductive or3 (P0,P1,P2:Prop) : Prop ≝ | or3_intro0: P0 → or3 ? ? ? | or3_intro1: P1 → or3 ? ? ? @@ -66,3 +90,12 @@ inductive or3 (P0,P1,P2:Prop) : Prop ≝ interpretation "multiple disjunction connective (3)" 'Or P0 P1 P2 = (or3 P0 P1 P2). +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). + diff --git a/matita/matita/lib/lambda-delta/xoa_notation.ma b/matita/matita/lib/lambda-delta/xoa_notation.ma index 18b3c0293..e37c37eb1 100644 --- a/matita/matita/lib/lambda-delta/xoa_notation.ma +++ b/matita/matita/lib/lambda-delta/xoa_notation.ma @@ -22,6 +22,10 @@ notation "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 non associative with precedence 20 for @{ 'Ex (λ${ident x0},${ident x1}.$P0) (λ${ident x0},${ident x1}.$P1) }. +notation "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.$P0) (λ${ident x0}.$P1) (λ${ident x0}.$P2) }. + notation "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2)" non associative with precedence 20 for @{ 'Ex (λ${ident x0},${ident x1}.$P0) (λ${ident x0},${ident x1}.$P1) (λ${ident x0},${ident x1}.$P2) }. @@ -38,11 +42,27 @@ notation "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 non associative with precedence 20 for @{ 'Ex (λ${ident x0},${ident x1},${ident x2},${ident x3}.$P0) (λ${ident x0},${ident x1},${ident x2},${ident x3}.$P1) (λ${ident x0},${ident x1},${ident x2},${ident x3}.$P2) (λ${ident x0},${ident x1},${ident x2},${ident x3}.$P3) }. +notation "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)" + 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) (λ${ident x0},${ident x1},${ident x2}.$P4) }. + +notation "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0},${ident x1},${ident x2},${ident x3}.$P0) (λ${ident x0},${ident x1},${ident x2},${ident x3}.$P1) (λ${ident x0},${ident x1},${ident x2},${ident x3}.$P2) (λ${ident x0},${ident x1},${ident x2},${ident x3}.$P3) (λ${ident x0},${ident x1},${ident x2},${ident x3}.$P4) }. + notation "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)" non associative with precedence 20 for @{ 'Ex (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P0) (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P1) (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P2) (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P3) (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P4) (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P5) }. -notation "hvbox(∨∨ term 19 P0 break | term 19 P1 break | term 19 P2)" +notation "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)" non associative with precedence 20 + for @{ 'Ex (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P0) (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P1) (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P2) (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P3) (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P4) (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P5) (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P6) }. + +notation "hvbox(∨∨ term 29 P0 break | term 29 P1 break | term 29 P2)" + non associative with precedence 30 for @{ 'Or $P0 $P1 $P2 }. +notation "hvbox(∨∨ term 29 P0 break | term 29 P1 break | term 29 P2 break | term 29 P3)" + non associative with precedence 30 + for @{ 'Or $P0 $P1 $P2 $P3 }. + -- 2.39.2