From: Ferruccio Guidi Date: Mon, 25 Jul 2016 18:40:47 +0000 (+0000) Subject: we count rt parallel steps in a different way: X-Git-Tag: make_still_working~546 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=89ea663d91904f483f8248cfaeaed5eda8715da2;p=helm.git we count rt parallel steps in a different way: we use the maximum, that is idempotent, rather than the sum --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma index fd44b81fd..e322f490f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "ground_2/steps/rtc_max.ma". include "ground_2/steps/rtc_plus.ma". include "basic_2/notation/relations/predty_6.ma". include "basic_2/grammar/lenv.ma". @@ -33,21 +34,21 @@ inductive cpg (h): rtc → relation4 genv lenv term term ≝ ⬆*[1] T ≡ U → cpg h c G (L.ⓑ{I}V) (#⫯i) U | cpg_bind : ∀cV,cT,p,I,G,L,V1,V2,T1,T2. cpg h cV G L V1 V2 → cpg h cT G (L.ⓑ{I}V1) T1 T2 → - cpg h ((↓cV)+cT) G L (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2) + cpg h ((↓cV)∨cT) G L (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2) | cpg_flat : ∀cV,cT,I,G,L,V1,V2,T1,T2. cpg h cV G L V1 V2 → cpg h cT G L T1 T2 → - cpg h ((↓cV)+cT) G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2) + cpg h ((↓cV)∨cT) G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2) | cpg_zeta : ∀c,G,L,V,T1,T,T2. cpg h c G (L.ⓓV) T1 T → ⬆*[1] T2 ≡ T → cpg h (c+𝟙𝟘) G L (+ⓓV.T1) T2 | cpg_eps : ∀c,G,L,V,T1,T2. cpg h c G L T1 T2 → cpg h (c+𝟙𝟘) G L (ⓝV.T1) T2 | cpg_ee : ∀c,G,L,V1,V2,T. cpg h c G L V1 V2 → cpg h (c+𝟘𝟙) G L (ⓝV1.T) V2 | cpg_beta : ∀cV,cW,cT,p,G,L,V1,V2,W1,W2,T1,T2. cpg h cV G L V1 V2 → cpg h cW G L W1 W2 → cpg h cT G (L.ⓛW1) T1 T2 → - cpg h ((↓cV)+(↓cW)+cT+𝟙𝟘) G L (ⓐV1.ⓛ{p}W1.T1) (ⓓ{p}ⓝW2.V2.T2) + cpg h (((↓cV)∨(↓cW)∨cT)+𝟙𝟘) G L (ⓐV1.ⓛ{p}W1.T1) (ⓓ{p}ⓝW2.V2.T2) | cpg_theta: ∀cV,cW,cT,p,G,L,V1,V,V2,W1,W2,T1,T2. cpg h cV G L V1 V → ⬆*[1] V ≡ V2 → cpg h cW G L W1 W2 → cpg h cT G (L.ⓓW1) T1 T2 → - cpg h ((↓cV)+(↓cW)+cT+𝟙𝟘) G L (ⓐV1.ⓓ{p}W1.T1) (ⓓ{p}W2.ⓐV2.T2) + cpg h (((↓cV)∨(↓cW)∨cT)+𝟙𝟘) G L (ⓐV1.ⓓ{p}W1.T1) (ⓓ{p}W2.ⓐV2.T2) . interpretation @@ -151,7 +152,7 @@ qed-. fact cpg_inv_bind1_aux: ∀c,h,G,L,U,U2. ⦃G, L⦄ ⊢ U ⬈[c, h] U2 → ∀p,J,V1,U1. U = ⓑ{p,J}V1.U1 → ( ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L.ⓑ{J}V1⦄ ⊢ U1 ⬈[cT, h] T2 & - U2 = ⓑ{p,J}V2.T2 & c = (↓cV)+cT + U2 = ⓑ{p,J}V2.T2 & c = ((↓cV)∨cT) ) ∨ ∃∃cT,T. ⦃G, L.ⓓV1⦄ ⊢ U1 ⬈[cT, h] T & ⬆*[1] U2 ≡ T & p = true & J = Abbr & c = cT+𝟙𝟘. @@ -173,7 +174,7 @@ qed-. lemma cpg_inv_bind1: ∀c,h,p,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈[c, h] U2 → ( ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬈[cT, h] T2 & - U2 = ⓑ{p,I}V2.T2 & c = (↓cV)+cT + U2 = ⓑ{p,I}V2.T2 & c = ((↓cV)∨cT) ) ∨ ∃∃cT,T. ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈[cT, h] T & ⬆*[1] U2 ≡ T & p = true & I = Abbr & c = cT+𝟙𝟘. @@ -181,7 +182,7 @@ lemma cpg_inv_bind1: ∀c,h,p,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈[c lemma cpg_inv_abbr1: ∀c,h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{p}V1.T1 ⬈[c, h] U2 → ( ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈[cT, h] T2 & - U2 = ⓓ{p}V2.T2 & c = (↓cV)+cT + U2 = ⓓ{p}V2.T2 & c = ((↓cV)∨cT) ) ∨ ∃∃cT,T. ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈[cT, h] T & ⬆*[1] U2 ≡ T & p = true & c = cT+𝟙𝟘. @@ -191,7 +192,7 @@ qed-. lemma cpg_inv_abst1: ∀c,h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{p}V1.T1 ⬈[c, h] U2 → ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 ⬈[cT, h] T2 & - U2 = ⓛ{p}V2.T2 & c = (↓cV)+cT. + U2 = ⓛ{p}V2.T2 & c = ((↓cV)∨cT). #c #h #p #G #L #V1 #T1 #U2 #H elim (cpg_inv_bind1 … H) -H * [ /3 width=8 by ex4_4_intro/ | #c #T #_ #_ #_ #H destruct @@ -201,13 +202,13 @@ qed-. fact cpg_inv_flat1_aux: ∀c,h,G,L,U,U2. ⦃G, L⦄ ⊢ U ⬈[c, h] U2 → ∀J,V1,U1. U = ⓕ{J}V1.U1 → ∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ U1 ⬈[cT, h] T2 & - U2 = ⓕ{J}V2.T2 & c = (↓cV)+cT + U2 = ⓕ{J}V2.T2 & c = ((↓cV)∨cT) | ∃∃cT. ⦃G, L⦄ ⊢ U1 ⬈[cT, h] U2 & J = Cast & c = cT+𝟙𝟘 | ∃∃cV. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] U2 & J = Cast & c = cV+𝟘𝟙 | ∃∃cV,cW,cT,p,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ W1 ⬈[cW, h] W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ⬈[cT, h] T2 & - J = Appl & U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2 & c = (↓cV)+(↓cW)+cT+𝟙𝟘 + J = Appl & U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2 & c = ((↓cV)∨(↓cW)∨cT)+𝟙𝟘 | ∃∃cV,cW,cT,p,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V & ⬆*[1] V ≡ V2 & ⦃G, L⦄ ⊢ W1 ⬈[cW, h] W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ⬈[cT, h] T2 & - J = Appl & U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2 & c = (↓cV)+(↓cW)+cT+𝟙𝟘. + J = Appl & U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2 & c = ((↓cV)∨(↓cW)∨cT)+𝟙𝟘. #c #h #G #L #U #U2 * -c -G -L -U -U2 [ #I #G #L #J #W #U1 #H destruct | #G #L #s #J #W #U1 #H destruct @@ -226,22 +227,22 @@ qed-. lemma cpg_inv_flat1: ∀c,h,I,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓕ{I}V1.U1 ⬈[c, h] U2 → ∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ U1 ⬈[cT, h] T2 & - U2 = ⓕ{I}V2.T2 & c = (↓cV)+cT + U2 = ⓕ{I}V2.T2 & c = ((↓cV)∨cT) | ∃∃cT. ⦃G, L⦄ ⊢ U1 ⬈[cT, h] U2 & I = Cast & c = cT+𝟙𝟘 | ∃∃cV. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] U2 & I = Cast & c = cV+𝟘𝟙 | ∃∃cV,cW,cT,p,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ W1 ⬈[cW, h] W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ⬈[cT, h] T2 & - I = Appl & U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2 & c = (↓cV)+(↓cW)+cT+𝟙𝟘 + I = Appl & U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2 & c = ((↓cV)∨(↓cW)∨cT)+𝟙𝟘 | ∃∃cV,cW,cT,p,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V & ⬆*[1] V ≡ V2 & ⦃G, L⦄ ⊢ W1 ⬈[cW, h] W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ⬈[cT, h] T2 & - I = Appl & U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2 & c = (↓cV)+(↓cW)+cT+𝟙𝟘. + I = Appl & U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2 & c = ((↓cV)∨(↓cW)∨cT)+𝟙𝟘. /2 width=3 by cpg_inv_flat1_aux/ qed-. lemma cpg_inv_appl1: ∀c,h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓐV1.U1 ⬈[c, h] U2 → ∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ U1 ⬈[cT, h] T2 & - U2 = ⓐV2.T2 & c = (↓cV)+cT + U2 = ⓐV2.T2 & c = ((↓cV)∨cT) | ∃∃cV,cW,cT,p,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ W1 ⬈[cW, h] W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ⬈[cT, h] T2 & - U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2 & c = (↓cV)+(↓cW)+cT+𝟙𝟘 + U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2 & c = ((↓cV)∨(↓cW)∨cT)+𝟙𝟘 | ∃∃cV,cW,cT,p,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V & ⬆*[1] V ≡ V2 & ⦃G, L⦄ ⊢ W1 ⬈[cW, h] W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ⬈[cT, h] T2 & - U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2 & c = (↓cV)+(↓cW)+cT+𝟙𝟘. + U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2 & c = ((↓cV)∨(↓cW)∨cT)+𝟙𝟘. #c #h #G #L #V1 #U1 #U2 #H elim (cpg_inv_flat1 … H) -H * [ /3 width=8 by or3_intro0, ex4_4_intro/ |2,3: #c #_ #H destruct @@ -252,7 +253,7 @@ qed-. lemma cpg_inv_cast1: ∀c,h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓝV1.U1 ⬈[c, h] U2 → ∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ U1 ⬈[cT, h] T2 & - U2 = ⓝV2.T2 & c = (↓cV)+cT + U2 = ⓝV2.T2 & c = ((↓cV)∨cT) | ∃∃cT. ⦃G, L⦄ ⊢ U1 ⬈[cT, h] U2 & c = cT+𝟙𝟘 | ∃∃cV. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] U2 & c = cV+𝟘𝟙. #c #h #G #L #V1 #U1 #U2 #H elim (cpg_inv_flat1 … H) -H * diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_simple.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_simple.ma index a53be69b0..b03705a2e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_simple.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_simple.ma @@ -22,7 +22,7 @@ include "basic_2/rt_transition/cpg.ma". (* Note: the main property of simple terms *) lemma cpg_inv_appl1_simple: ∀c,h,G,L,V1,T1,U. ⦃G, L⦄ ⊢ ⓐV1.T1 ⬈[c, h] U → 𝐒⦃T1⦄ → ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ T1 ⬈[cT, h] T2 & - U = ⓐV2.T2 & c = (↓cV)+cT. + U = ⓐV2.T2 & c = ((↓cV)∨cT). #c #h #G #L #V1 #T1 #U #H #HT1 elim (cpg_inv_appl1 … H) -H * [ /2 width=8 by ex4_4_intro/ | #cV #cW #cT #p #V2 #W1 #W2 #U1 #U2 #_ #_ #_ #H destruct diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma index 7138b3210..870f93598 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma @@ -58,7 +58,7 @@ lemma cpm_bind: ∀n,h,p,I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡[n, h] T2 → ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ➡[n, h] ⓑ{p,I}V2.T2. #n #h #p #I #G #L #V1 #V2 #T1 #T2 * #riV #rhV #HV12 * -/5 width=5 by cpg_bind, isrt_plus_O1, isr_shift, ex2_intro/ +/5 width=5 by cpg_bind, isrt_max_O1, isr_shift, ex2_intro/ qed. (* Note: cpr_flat: does not hold in basic_1 *) @@ -68,7 +68,7 @@ lemma cpm_flat: ∀n,h,I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 → ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ➡[n, h] ⓕ{I}V2.T2. #n #h #I #G #L #V1 #V2 #T1 #T2 * #riV #rhV #HV12 * -/5 width=5 by isrt_plus_O1, isr_shift, cpg_flat, ex2_intro/ +/5 width=5 by isrt_max_O1, isr_shift, cpg_flat, ex2_intro/ qed. (* Basic_2A1: includes: cpr_zeta *) @@ -94,7 +94,7 @@ lemma cpm_beta: ∀n,h,p,G,L,V1,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L⦄ ⊢ W1 ➡[h] W2 → ⦃G, L.ⓛW1⦄ ⊢ T1 ➡[n, h] T2 → ⦃G, L⦄ ⊢ ⓐV1.ⓛ{p}W1.T1 ➡[n, h] ⓓ{p}ⓝW2.V2.T2. #n #h #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 * #riV #rhV #HV12 * #riW #rhW #HW12 * -/6 width=7 by cpg_beta, isrt_plus_O2, isrt_plus, isr_shift, ex2_intro/ +/6 width=7 by cpg_beta, isrt_plus_O2, isrt_max, isr_shift, ex2_intro/ qed. (* Basic_2A1: includes: cpr_theta *) @@ -103,7 +103,7 @@ lemma cpm_theta: ∀n,h,p,G,L,V1,V,V2,W1,W2,T1,T2. ⦃G, L.ⓓW1⦄ ⊢ T1 ➡[n, h] T2 → ⦃G, L⦄ ⊢ ⓐV1.ⓓ{p}W1.T1 ➡[n, h] ⓓ{p}W2.ⓐV2.T2. #n #h #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 * #riV #rhV #HV1 #HV2 * #riW #rhW #HW12 * -/6 width=9 by cpg_theta, isrt_plus_O2, isrt_plus, isr_shift, ex2_intro/ +/6 width=9 by cpg_theta, isrt_plus_O2, isrt_max, isr_shift, ex2_intro/ qed. (* Basic properties on r-transition *****************************************) @@ -192,7 +192,7 @@ lemma cpm_inv_bind1: ∀n,h,p,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ➡[n p = true & I = Abbr. #n #h #p #I #G #L #V1 #T1 #U2 * #c #Hc #H elim (cpg_inv_bind1 … H) -H * [ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct - elim (isrt_inv_plus … Hc) -Hc #nV #nT #HcV #HcT #H destruct + elim (isrt_inv_max … Hc) -Hc #nV #nT #HcV #HcT #H destruct elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct /4 width=5 by ex3_2_intro, ex2_intro, or_introl/ | #cT #T2 #HT12 #HUT2 #H1 #H2 #H3 destruct @@ -209,7 +209,7 @@ lemma cpm_inv_abbr1: ∀n,h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{p}V1.T1 ➡[n, h] ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡[n, h] T & ⬆*[1] U2 ≡ T & p = true. #n #h #p #G #L #V1 #T1 #U2 * #c #Hc #H elim (cpg_inv_abbr1 … H) -H * [ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct - elim (isrt_inv_plus … Hc) -Hc #nV #nT #HcV #HcT #H destruct + elim (isrt_inv_max … Hc) -Hc #nV #nT #HcV #HcT #H destruct elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct /4 width=5 by ex3_2_intro, ex2_intro, or_introl/ | #cT #T2 #HT12 #HUT2 #H1 #H2 destruct @@ -224,7 +224,7 @@ lemma cpm_inv_abst1: ∀n,h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{p}V1.T1 ➡[n, h] U2 = ⓛ{p}V2.T2. #n #h #p #G #L #V1 #T1 #U2 * #c #Hc #H elim (cpg_inv_abst1 … H) -H #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct -elim (isrt_inv_plus … Hc) -Hc #nV #nT #HcV #HcT #H destruct +elim (isrt_inv_max … Hc) -Hc #nV #nT #HcV #HcT #H destruct elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct /3 width=5 by ex3_2_intro, ex2_intro/ qed-. @@ -244,7 +244,7 @@ lemma cpm_inv_flat1: ∀n,h,I,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓕ{I}V1.U1 ➡[n, h] U2 = ⓓ{p}W2.ⓐV2.T2 & I = Appl. #n #h #I #G #L #V1 #U1 #U2 * #c #Hc #H elim (cpg_inv_flat1 … H) -H * [ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct - elim (isrt_inv_plus … Hc) -Hc #nV #nT #HcV #HcT #H destruct + elim (isrt_inv_max … Hc) -Hc #nV #nT #HcV #HcT #H destruct elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct /4 width=5 by or5_intro0, ex3_2_intro, ex2_intro/ | #cU #U12 #H1 #H2 destruct @@ -254,15 +254,15 @@ lemma cpm_inv_flat1: ∀n,h,I,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓕ{I}V1.U1 ➡[n, h] /4 width=3 by or5_intro2, ex3_intro, ex2_intro/ | #cV #cW #cT #p #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12 #H1 #H2 #H3 #H4 destruct lapply (isrt_inv_plus_O_dx … Hc ?) -Hc // #Hc - elim (isrt_inv_plus … Hc) -Hc #n0 #nT #Hc #HcT #H destruct - elim (isrt_inv_plus … Hc) -Hc #nV #nW #HcV #HcW #H destruct + elim (isrt_inv_max … Hc) -Hc #n0 #nT #Hc #HcT #H destruct + elim (isrt_inv_max … Hc) -Hc #nV #nW #HcV #HcW #H destruct elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct elim (isrt_inv_shift … HcW) -HcW #HcW #H destruct /4 width=11 by or5_intro3, ex6_6_intro, ex2_intro/ | #cV #cW #cT #p #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HW12 #HT12 #H1 #H2 #H3 #H4 destruct lapply (isrt_inv_plus_O_dx … Hc ?) -Hc // #Hc - elim (isrt_inv_plus … Hc) -Hc #n0 #nT #Hc #HcT #H destruct - elim (isrt_inv_plus … Hc) -Hc #nV #nW #HcV #HcW #H destruct + elim (isrt_inv_max … Hc) -Hc #n0 #nT #Hc #HcT #H destruct + elim (isrt_inv_max … Hc) -Hc #nV #nW #HcV #HcW #H destruct elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct elim (isrt_inv_shift … HcW) -HcW #HcW #H destruct /4 width=13 by or5_intro4, ex7_7_intro, ex2_intro/ @@ -282,20 +282,20 @@ lemma cpm_inv_appl1: ∀n,h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓐ V1.U1 ➡[n, h] U2 U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2. #n #h #G #L #V1 #U1 #U2 * #c #Hc #H elim (cpg_inv_appl1 … H) -H * [ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct - elim (isrt_inv_plus … Hc) -Hc #nV #nT #HcV #HcT #H destruct + elim (isrt_inv_max … Hc) -Hc #nV #nT #HcV #HcT #H destruct elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct /4 width=5 by or3_intro0, ex3_2_intro, ex2_intro/ | #cV #cW #cT #p #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12 #H1 #H2 #H3 destruct lapply (isrt_inv_plus_O_dx … Hc ?) -Hc // #Hc - elim (isrt_inv_plus … Hc) -Hc #n0 #nT #Hc #HcT #H destruct - elim (isrt_inv_plus … Hc) -Hc #nV #nW #HcV #HcW #H destruct + elim (isrt_inv_max … Hc) -Hc #n0 #nT #Hc #HcT #H destruct + elim (isrt_inv_max … Hc) -Hc #nV #nW #HcV #HcW #H destruct elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct elim (isrt_inv_shift … HcW) -HcW #HcW #H destruct /4 width=11 by or3_intro1, ex5_6_intro, ex2_intro/ | #cV #cW #cT #p #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HW12 #HT12 #H1 #H2 #H3 destruct lapply (isrt_inv_plus_O_dx … Hc ?) -Hc // #Hc - elim (isrt_inv_plus … Hc) -Hc #n0 #nT #Hc #HcT #H destruct - elim (isrt_inv_plus … Hc) -Hc #nV #nW #HcV #HcW #H destruct + elim (isrt_inv_max … Hc) -Hc #n0 #nT #Hc #HcT #H destruct + elim (isrt_inv_max … Hc) -Hc #nV #nW #HcV #HcW #H destruct elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct elim (isrt_inv_shift … HcW) -HcW #HcW #H destruct /4 width=13 by or3_intro2, ex6_7_intro, ex2_intro/ @@ -309,7 +309,7 @@ lemma cpm_inv_cast1: ∀n,h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓝV1.U1 ➡[n, h] U2 | ∃∃m. ⦃G, L⦄ ⊢ V1 ➡[m, h] U2 & n = ⫯m. #n #h #G #L #V1 #U1 #U2 * #c #Hc #H elim (cpg_inv_cast1 … H) -H * [ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct - elim (isrt_inv_plus … Hc) -Hc #nV #nT #HcV #HcT #H destruct + elim (isrt_inv_max … Hc) -Hc #nV #nT #HcV #HcT #H destruct elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct /4 width=5 by or3_intro0, ex3_2_intro, ex2_intro/ | #cU #U12 #H destruct diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma index 83322f4d8..dad1f9382 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma @@ -96,6 +96,20 @@ qed. lemma arith_i: ∀x,y,z. y < x → x+z-y-1 = x-y-1+z. /2 width=1 by plus_minus/ qed-. +lemma idempotent_max: ∀n:nat. n = (n ∨ n). +#n normalize >le_to_leb_true // +qed. + +lemma associative_max: associative … max. +#x #y #z normalize +@(leb_elim x y) normalize #Hxy +@(leb_elim y z) normalize #Hyz // +[1,2: >le_to_leb_true /2 width=3 by transitive_le/ +| >not_le_to_leb_false /4 width=3 by lt_to_not_le, not_le_to_lt, transitive_lt/ + >not_le_to_leb_false // +] +qed. + (* Properties ***************************************************************) lemma eq_nat_dec: ∀n1,n2:nat. Decidable (n1 = n2). diff --git a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_max.ma b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_max.ma index 1c8861fa8..46f457536 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_max.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_max.ma @@ -36,6 +36,10 @@ lemma max_O_dx: ∀c. c = (c ∨ 𝟘𝟘). * #ri #rs #ti #ts