X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fgrammar%2Fleq.ma;h=a898abdb566f65941eb7d63cb572bdf85838a536;hb=52e675f555f559c047d5449db7fc89a51b977d35;hp=f7f23760d8594c36af97c4b1c5986cd343798b0d;hpb=75fac6d60f67a4dfa38ea6c2cc45a18eda5d8996;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/leq.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/leq.ma index f7f23760d..a898abdb5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/leq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/leq.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "ground_2/ynat/ynat_lt.ma". -include "basic_2/notation/relations/iso_4.ma". +include "basic_2/notation/relations/midiso_4.ma". include "basic_2/grammar/lenv_length.ma". (* EQUIVALENCE FOR LOCAL ENVIRONMENTS ***************************************) @@ -25,31 +25,31 @@ inductive leq: relation4 ynat ynat lenv lenv ≝ | leq_pair: ∀I,L1,L2,V,e. leq 0 e L1 L2 → leq 0 (⫯e) (L1.ⓑ{I}V) (L2.ⓑ{I}V) | leq_succ: ∀I1,I2,L1,L2,V1,V2,d,e. - leq d e L1 L2 → leq (⫯d) e (L1. ⓑ{I1}V1) (L2. ⓑ{I2} V2) + leq d e L1 L2 → leq (⫯d) e (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2) . interpretation "equivalence (local environment)" - 'Iso d e L1 L2 = (leq d e L1 L2). + 'MidIso d e L1 L2 = (leq d e L1 L2). (* Basic properties *********************************************************) -lemma leq_pair_lt: ∀I,L1,L2,V,e. L1 ≃[0, ⫰e] L2 → 0 < e → - L1.ⓑ{I}V ≃[0, e] L2.ⓑ{I}V. +lemma leq_pair_lt: ∀I,L1,L2,V,e. L1 ⩬[0, ⫰e] L2 → 0 < e → + L1.ⓑ{I}V ⩬[0, e] L2.ⓑ{I}V. #I #L1 #L2 #V #e #HL12 #He <(ylt_inv_O1 … He) /2 width=1 by leq_pair/ qed. -lemma leq_succ_lt: ∀I1,I2,L1,L2,V1,V2,d,e. L1 ≃[⫰d, e] L2 → 0 < d → - L1.ⓑ{I1}V1 ≃[d, e] L2. ⓑ{I2}V2. +lemma leq_succ_lt: ∀I1,I2,L1,L2,V1,V2,d,e. L1 ⩬[⫰d, e] L2 → 0 < d → + L1.ⓑ{I1}V1 ⩬[d, e] L2. ⓑ{I2}V2. #I1 #I2 #L1 #L2 #V1 #V2 #d #e #HL12 #Hd <(ylt_inv_O1 … Hd) /2 width=1 by leq_succ/ qed. -lemma leq_pair_O_Y: ∀L1,L2. L1 ≃[0, ∞] L2 → - ∀I,V. L1.ⓑ{I}V ≃[0, ∞] L2.ⓑ{I}V. +lemma leq_pair_O_Y: ∀L1,L2. L1 ⩬[0, ∞] L2 → + ∀I,V. L1.ⓑ{I}V ⩬[0, ∞] L2.ⓑ{I}V. #L1 #L2 #HL12 #I #V lapply (leq_pair I … V … HL12) -HL12 // qed. -lemma leq_refl: ∀L,d,e. L ≃[d, e] L. +lemma leq_refl: ∀L,d,e. L ⩬[d, e] L. #L elim L -L // #L #I #V #IHL #d elim (ynat_cases … d) [| * #x ] #Hd destruct /2 width=1 by leq_succ/ @@ -57,7 +57,7 @@ lemma leq_refl: ∀L,d,e. L ≃[d, e] L. #He destruct /2 width=1 by leq_zero, leq_pair/ qed. -lemma leq_O2: ∀L1,L2,d. |L1| = |L2| → L1 ≃[d, yinj 0] L2. +lemma leq_O2: ∀L1,L2,d. |L1| = |L2| → L1 ⩬[d, yinj 0] L2. #L1 elim L1 -L1 [| #L1 #I1 #V1 #IHL1 ] * // [1,3: #L2 #I2 #V2 ] #d normalize [1,3: