X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Flsubsv.ma;h=29d6151fe877e584e1ccb65efa0c1caa6fc5cd8c;hb=29973426e0227ee48368d1c24dc0c17bf2baef77;hp=8d4e9b67a0ea6e9ab0e8ee9bcafb2cc813071b9b;hpb=f95f6cb21b86f3dad114b21f687aa5df36088064;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma index 8d4e9b67a..29d6151fe 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma @@ -22,8 +22,8 @@ inductive lsubsv (h:sh) (g:sd h): relation lenv ≝ | lsubsv_atom: lsubsv h g (⋆) (⋆) | lsubsv_pair: ∀I,L1,L2,V. lsubsv h g L1 L2 → lsubsv h g (L1.ⓑ{I}V) (L2.ⓑ{I}V) -| lsubsv_abbr: ∀L1,L2,W,V,W1,V2,l. ⦃h, L1⦄ ⊢ ⓝW.V ¡[g] → ⦃h, L2⦄ ⊢ W ¡[g] → - ⦃h, L1⦄ ⊢ V •[g] ⦃l+1, W1⦄ → ⦃h, L2⦄ ⊢ W •[g] ⦃l, V2⦄ → +| lsubsv_abbr: ∀L1,L2,W,V,W1,V2,l. ⦃h, L1⦄ ⊢ ⓝW.V ¡[h, g] → ⦃h, L2⦄ ⊢ W ¡[h, g] → + ⦃h, L1⦄ ⊢ V •[h, g] ⦃l+1, W1⦄ → ⦃h, L2⦄ ⊢ W •[h, g] ⦃l, V2⦄ → lsubsv h g L1 L2 → lsubsv h g (L1.ⓓⓝW.V) (L2.ⓛW) . @@ -33,7 +33,7 @@ interpretation (* Basic inversion lemmas ***************************************************) -fact lsubsv_inv_atom1_aux: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → L1 = ⋆ → L2 = ⋆. +fact lsubsv_inv_atom1_aux: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[h, g] L2 → L1 = ⋆ → L2 = ⋆. #h #g #L1 #L2 * -L1 -L2 [ // | #I #L1 #L2 #V #_ #H destruct @@ -41,15 +41,15 @@ fact lsubsv_inv_atom1_aux: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → L1 = ⋆ → L ] qed-. -lemma lsubsv_inv_atom1: ∀h,g,L2. h ⊢ ⋆ ¡⊑[g] L2 → L2 = ⋆. +lemma lsubsv_inv_atom1: ∀h,g,L2. h ⊢ ⋆ ¡⊑[h, g] L2 → L2 = ⋆. /2 width=5 by lsubsv_inv_atom1_aux/ qed-. -fact lsubsv_inv_pair1_aux: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → +fact lsubsv_inv_pair1_aux: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[h, g] L2 → ∀I,K1,X. L1 = K1.ⓑ{I}X → - (∃∃K2. h ⊢ K1 ¡⊑[g] K2 & L2 = K2.ⓑ{I}X) ∨ - ∃∃K2,W,V,W1,V2,l. ⦃h, K1⦄ ⊢ X ¡[g] & ⦃h, K2⦄ ⊢ W ¡[g] & - ⦃h, K1⦄ ⊢ V •[g] ⦃l+1, W1⦄ & ⦃h, K2⦄ ⊢ W •[g] ⦃l, V2⦄ & - h ⊢ K1 ¡⊑[g] K2 & + (∃∃K2. h ⊢ K1 ¡⊑[h, g] K2 & L2 = K2.ⓑ{I}X) ∨ + ∃∃K2,W,V,W1,V2,l. ⦃h, K1⦄ ⊢ X ¡[h, g] & ⦃h, K2⦄ ⊢ W ¡[h, g] & + ⦃h, K1⦄ ⊢ V •[h, g] ⦃l+1, W1⦄ & ⦃h, K2⦄ ⊢ W •[h, g] ⦃l, V2⦄ & + h ⊢ K1 ¡⊑[h, g] K2 & I = Abbr & L2 = K2.ⓛW & X = ⓝW.V. #h #g #L1 #L2 * -L1 -L2 [ #J #K1 #X #H destruct @@ -58,15 +58,15 @@ fact lsubsv_inv_pair1_aux: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → ] qed-. -lemma lsubsv_inv_pair1: ∀h,g,I,K1,L2,X. h ⊢ K1.ⓑ{I}X ¡⊑[g] L2 → - (∃∃K2. h ⊢ K1 ¡⊑[g] K2 & L2 = K2.ⓑ{I}X) ∨ - ∃∃K2,W,V,W1,V2,l. ⦃h, K1⦄ ⊢ X ¡[g] & ⦃h, K2⦄ ⊢ W ¡[g] & - ⦃h, K1⦄ ⊢ V •[g] ⦃l+1, W1⦄ & ⦃h, K2⦄ ⊢ W •[g] ⦃l, V2⦄ & - h ⊢ K1 ¡⊑[g] K2 & +lemma lsubsv_inv_pair1: ∀h,g,I,K1,L2,X. h ⊢ K1.ⓑ{I}X ¡⊑[h, g] L2 → + (∃∃K2. h ⊢ K1 ¡⊑[h, g] K2 & L2 = K2.ⓑ{I}X) ∨ + ∃∃K2,W,V,W1,V2,l. ⦃h, K1⦄ ⊢ X ¡[h, g] & ⦃h, K2⦄ ⊢ W ¡[h, g] & + ⦃h, K1⦄ ⊢ V •[h, g] ⦃l+1, W1⦄ & ⦃h, K2⦄ ⊢ W •[h, g] ⦃l, V2⦄ & + h ⊢ K1 ¡⊑[h, g] K2 & I = Abbr & L2 = K2.ⓛW & X = ⓝW.V. /2 width=3 by lsubsv_inv_pair1_aux/ qed-. -fact lsubsv_inv_atom2_aux: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → L2 = ⋆ → L1 = ⋆. +fact lsubsv_inv_atom2_aux: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[h, g] L2 → L2 = ⋆ → L1 = ⋆. #h #g #L1 #L2 * -L1 -L2 [ // | #I #L1 #L2 #V #_ #H destruct @@ -74,15 +74,15 @@ fact lsubsv_inv_atom2_aux: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → L2 = ⋆ → L ] qed-. -lemma lsubsv_inv_atom2: ∀h,g,L1. h ⊢ L1 ¡⊑[g] ⋆ → L1 = ⋆. +lemma lsubsv_inv_atom2: ∀h,g,L1. h ⊢ L1 ¡⊑[h, g] ⋆ → L1 = ⋆. /2 width=5 by lsubsv_inv_atom2_aux/ qed-. -fact lsubsv_inv_pair2_aux: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → +fact lsubsv_inv_pair2_aux: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[h, g] L2 → ∀I,K2,W. L2 = K2.ⓑ{I}W → - (∃∃K1. h ⊢ K1 ¡⊑[g] K2 & L1 = K1.ⓑ{I}W) ∨ - ∃∃K1,V,W1,V2,l. ⦃h, K1⦄ ⊢ ⓝW.V ¡[g] & ⦃h, K2⦄ ⊢ W ¡[g] & - ⦃h, K1⦄ ⊢ V •[g] ⦃l+1, W1⦄ & ⦃h, K2⦄ ⊢ W •[g] ⦃l, V2⦄ & - h ⊢ K1 ¡⊑[g] K2 & I = Abst & L1 = K1. ⓓⓝW.V. + (∃∃K1. h ⊢ K1 ¡⊑[h, g] K2 & L1 = K1.ⓑ{I}W) ∨ + ∃∃K1,V,W1,V2,l. ⦃h, K1⦄ ⊢ ⓝW.V ¡[h, g] & ⦃h, K2⦄ ⊢ W ¡[h, g] & + ⦃h, K1⦄ ⊢ V •[h, g] ⦃l+1, W1⦄ & ⦃h, K2⦄ ⊢ W •[h, g] ⦃l, V2⦄ & + h ⊢ K1 ¡⊑[h, g] K2 & I = Abst & L1 = K1. ⓓⓝW.V. #h #g #L1 #L2 * -L1 -L2 [ #J #K2 #U #H destruct | #I #L1 #L2 #V #HL12 #J #K2 #U #H destruct /3 width=3/ @@ -90,26 +90,26 @@ fact lsubsv_inv_pair2_aux: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → ] qed-. -lemma lsubsv_inv_pair2: ∀h,g,I,L1,K2,W. h ⊢ L1 ¡⊑[g] K2.ⓑ{I}W → - (∃∃K1. h ⊢ K1 ¡⊑[g] K2 & L1 = K1.ⓑ{I}W) ∨ - ∃∃K1,V,W1,V2,l. ⦃h, K1⦄ ⊢ ⓝW.V ¡[g] & ⦃h, K2⦄ ⊢ W ¡[g] & - ⦃h, K1⦄ ⊢ V •[g] ⦃l+1, W1⦄ & ⦃h, K2⦄ ⊢ W •[g] ⦃l, V2⦄ & - h ⊢ K1 ¡⊑[g] K2 & I = Abst & L1 = K1. ⓓⓝW.V. +lemma lsubsv_inv_pair2: ∀h,g,I,L1,K2,W. h ⊢ L1 ¡⊑[h, g] K2.ⓑ{I}W → + (∃∃K1. h ⊢ K1 ¡⊑[h, g] K2 & L1 = K1.ⓑ{I}W) ∨ + ∃∃K1,V,W1,V2,l. ⦃h, K1⦄ ⊢ ⓝW.V ¡[h, g] & ⦃h, K2⦄ ⊢ W ¡[h, g] & + ⦃h, K1⦄ ⊢ V •[h, g] ⦃l+1, W1⦄ & ⦃h, K2⦄ ⊢ W •[h, g] ⦃l, V2⦄ & + h ⊢ K1 ¡⊑[h, g] K2 & I = Abst & L1 = K1. ⓓⓝW.V. /2 width=3 by lsubsv_inv_pair2_aux/ qed-. (* Basic_forward lemmas *****************************************************) -lemma lsubsv_fwd_lsubr: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → L1 ⊑ L2. +lemma lsubsv_fwd_lsubr: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[h, g] L2 → L1 ⊑ L2. #h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ qed-. (* Basic properties *********************************************************) -lemma lsubsv_refl: ∀h,g,L. h ⊢ L ¡⊑[g] L. +lemma lsubsv_refl: ∀h,g,L. h ⊢ L ¡⊑[h, g] L. #h #g #L elim L -L // /2 width=1/ qed. -lemma lsubsv_cprs_trans: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → +lemma lsubsv_cprs_trans: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[h, g] L2 → ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2. /3 width=5 by lsubsv_fwd_lsubr, lsubr_cprs_trans/ qed-.