+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 "basic_2/relocation/llor.ma".
-include "basic_2/substitution/lleq_alt.ma".
-
-(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)
-
-(* Properties on poinwise union for local environments **********************)
-
-lemma llor_lleq_O: ∀T,L1,L2,L. L1 ⩖[T] L2 ≡ L → |L1| ≤ |L2| → |L2| = |L| → L2 ⋕[T, yinj 0] L.
-#T #L1 @(f2_ind … rfw … L1 T) -L1 -T
-#n #IH #L1 #T #Hn #L2 #L #H #HL12 #HL2 elim (llor_inv_alt … H) // destruct
-#HL1 #IHT @lleq_intro_alt //
-#I2 #I #K2 #K #V2 #V #i #_ #HnT #HLK2 #HLK lapply (ldrop_fwd_length_lt2 … HLK)
-#Hi elim (ldrop_O1_lt L1 i) //
-#I1 #K1 #V1 #HLK1 elim (IHT … HLK1 HLK) >HL1 >HL2 <minus_n_n -IHT -HLK1 -HLK
-[
-| * #I0 #K0 #V0 #_ #HLK0 lapply (ldrop_mono … HLK0 … HLK2) -HLK0 -HLK2
- #H1 #H2 #H3 #_ destruct
-
-
-
-
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 "basic_2/notation/relations/lazyor_4.ma".
+include "basic_2/relocation/lpx_sn.ma".
+include "basic_2/substitution/cofrees.ma".
+
+(* POINTWISE UNION FOR LOCAL ENVIRONMENTS ***********************************)
+
+inductive clor (T) (L2) (K1) (V1): predicate term ≝
+| clor_sn: |K1| < |L2| → K1 ⊢ |L2|-|K1|-1 ~ϵ 𝐅*[yinj 0]⦃T⦄ → clor T L2 K1 V1 V1
+| clor_dx: ∀I,K2,V2. |K1| < |L2| → (K1 ⊢ |L2|-|K1|-1 ~ϵ 𝐅*[yinj 0]⦃T⦄ → ⊥) →
+ ⇩[|L2|-|K1|-1] L2 ≡ K2.ⓑ{I}V2 → clor T L2 K1 V1 V2
+.
+
+definition llor: relation4 term lenv lenv lenv ≝
+ λT,L2. lpx_sn (clor T L2).
+
+interpretation
+ "lazy union (local environment)"
+ 'LazyOr L1 T L2 L = (llor T L2 L1 L).
+
+(* Basic properties *********************************************************)
+
+lemma llor_pair_sn: ∀I,L1,L2,L,V,T. L1 ⩖[T] L2 ≡ L →
+ |L1| < |L2| → L1 ⊢ |L2|-|L1|-1 ~ϵ 𝐅*[yinj 0]⦃T⦄ →
+ L1.ⓑ{I}V ⩖[T] L2 ≡ L.ⓑ{I}V.
+/3 width=2 by clor_sn, lpx_sn_pair/ qed.
+
+lemma llor_pair_dx: ∀I,J,L1,L2,L,K2,V1,V2,T. L1 ⩖[T] L2 ≡ L →
+ |L1| < |L2| → (L1 ⊢ |L2|-|L1|-1 ~ϵ 𝐅*[yinj 0]⦃T⦄ → ⊥) →
+ ⇩[|L2|-|L1|-1] L2 ≡ K2.ⓑ{J}V2 →
+ L1.ⓑ{I}V1 ⩖[T] L2 ≡ L.ⓑ{I}V2.
+/4 width=3 by clor_dx, lpx_sn_pair/ qed.
+
+lemma llor_total: ∀T,L2,L1. |L1| ≤ |L2| → ∃L. L1 ⩖[T] L2 ≡ L.
+#T #L2 #L1 elim L1 -L1 /2 width=2 by ex_intro/
+#L1 #I1 #V1 #IHL1 normalize
+#H elim IHL1 -IHL1 /2 width=3 by transitive_le/
+#L #HT elim (cofrees_dec L1 T 0 (|L2|-|L1|-1))
+[ /3 width=2 by llor_pair_sn, ex_intro/
+| elim (ldrop_O1_lt (Ⓕ) L2 (|L2|-|L1|-1))
+ /5 width=4 by llor_pair_dx, monotonic_lt_minus_l, ex_intro/
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 "basic_2/relocation/lpx_sn_alt.ma".
+include "basic_2/substitution/llor.ma".
+
+(* POINTWISE UNION FOR LOCAL ENVIRONMENTS ***********************************)
+
+(* Alternative definition ***************************************************)
+
+theorem llor_intro_alt: ∀T,L2,L1,L. |L1| ≤ |L2| → |L1| = |L| →
+ (∀I1,I,K1,K,V1,V,i. ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L ≡ K.ⓑ{I}V →
+ (K1 ⊢ |L2|-|L1|+i ~ϵ 𝐅*[yinj 0]⦃T⦄ → I1 = I ∧ V1 = V) ∧
+ (∀I2,K2,V2. (K1 ⊢ |L2|-|L1|+i ~ϵ 𝐅*[yinj 0]⦃T⦄ → ⊥) →
+ ⇩[|L2|-|L1|+i] L2 ≡ K2.ⓑ{I2}V2 → I1 = I ∧ V2 = V
+ )
+ ) → L1 ⩖[T] L2 ≡ L.
+#T #L2 #L1 #L #HL12 #HL1 #IH @lpx_sn_intro_alt // -HL1
+#I1 #I #K1 #K #V1 #V #i #HLK1 #HLK
+lapply (ldrop_fwd_length_minus4 … HLK1)
+lapply (ldrop_fwd_length_le4 … HLK1)
+normalize in ⊢ (%→%→?); #HKL1 #Hi
+lapply (plus_minus_minus_be_aux … HL12 Hi) // -Hi <minus_plus #Hi
+lapply (transitive_le … HKL1 HL12) -HKL1 -HL12 #HKL1
+elim (IH … HLK1 HLK) -IH -HLK1 -HLK #IH1 #IH2
+elim (cofrees_dec K1 T 0 (|L2|-|L1|+i))
+[ -IH2 #HT elim (IH1 … HT) -IH1
+ #HI1 #HV1 @conj // <HV1 -V @clor_sn // <Hi -Hi //
+| -IH1 #HnT elim (ldrop_O1_lt (Ⓕ) L2 (|L2|-|L1|+i)) /2 width=1 by monotonic_lt_minus_l/
+ #I2 #K2 #V2 #HLK2 elim (IH2 … HLK2) -IH2 /2 width=1 by/
+ #HI1 #HV2 @conj // <HV2 -V @(clor_dx … I2 K2) // <Hi -Hi /2 width=1 by/
+]
+qed.
+
+theorem llor_inv_alt: ∀T,L2,L1,L. L1 ⩖[T] L2 ≡ L → |L1| ≤ |L2| →
+ |L1| = |L| ∧
+ (∀I1,I,K1,K,V1,V,i.
+ ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L ≡ K.ⓑ{I}V →
+ (∧∧ K1 ⊢ |L2|-|L1|+i ~ϵ 𝐅*[yinj 0]⦃T⦄ & I1 = I & V1 = V) ∨
+ (∃∃I2,K2,V2. (K1 ⊢ |L2|-|L1|+i ~ϵ 𝐅*[yinj 0]⦃T⦄ → ⊥) &
+ ⇩[|L2|-|L1|+i] L2 ≡ K2.ⓑ{I2}V2 &
+ I1 = I & V2 = V
+ )
+ ).
+#T #L2 #L1 #L #H #HL12 elim (lpx_sn_inv_alt … H) -H
+#HL1 #IH @conj // -HL1
+#I1 #I #K1 #K #V1 #V #i #HLK1 #HLK
+lapply (ldrop_fwd_length_minus4 … HLK1)
+lapply (ldrop_fwd_length_le4 … HLK1)
+normalize in ⊢ (%→%→?); #HKL1 #Hi
+lapply (plus_minus_minus_be_aux … HL12 Hi) // -HL12 -Hi -HKL1
+<minus_plus #Hi >Hi -Hi
+elim (IH … HLK1 HLK) -IH #HI1 *
+/4 width=5 by or_introl, or_intror, and3_intro, ex4_3_intro/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 "basic_2/substitution/llor.ma".
+include "basic_2/substitution/lleq_alt.ma".
+
+(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)
+
+(* Properties on poinwise union for local environments **********************)
+(*
+lemma llor_lleq_O: ∀R,L1,L2,T. llpx_sn R 0 T L1 L2 →
+ ∀L. L1 ⩖[T] L2 ≡ L → L2 ≡[T, 0] L.
+#R #L1 #L2 #T #H1 #L #H2
+elim (llpx_sn_llpx_sn_alt … H1) -H1 #HL12 #IH1
+elim H2 -H2 #_ #HL1 #IH2
+@lleq_intro_alt // #I2 #I #K2 #K #V2 #V #i #Hi #HnT #HLK2 #HLK
+lapply (ldrop_fwd_length_lt2 … HLK) #HiL
+elim (ldrop_O1_lt (Ⓕ) L1 i) // -HiL #I1 #K1 #V1 #HLK1
+elim (IH1 … HLK1 HLK2) // -IH1
+[ #H #_ destruct
+ elim (IH2 … HLK1 HLK2 HLK) * /2 width=1 by conj/
+ #H elim HnT -HnT
+| #H @HnT -HnT
+]
+*)
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 "basic_2/notation/relations/lazyor_4.ma".
-include "basic_2/relocation/lpx_sn.ma".
-include "basic_2/substitution/cofrees.ma".
-
-(* POINTWISE UNION FOR LOCAL ENVIRONMENTS ***********************************)
-
-inductive clor (T) (L2) (K1) (V1): predicate term ≝
-| clor_sn: |K1| < |L2| → K1 ⊢ |L2|-|K1|-1 ~ϵ 𝐅*[yinj 0]⦃T⦄ → clor T L2 K1 V1 V1
-| clor_dx: ∀I,K2,V2. |K1| < |L2| → (K1 ⊢ |L2|-|K1|-1 ~ϵ 𝐅*[yinj 0]⦃T⦄ → ⊥) →
- ⇩[|L2|-|K1|-1] L2 ≡ K2.ⓑ{I}V2 → clor T L2 K1 V1 V2
-.
-
-definition llor: relation4 term lenv lenv lenv ≝
- λT,L2. lpx_sn (clor T L2).
-
-interpretation
- "lazy union (local environment)"
- 'LazyOr L1 T L2 L = (llor T L2 L1 L).
-
-(* Basic properties *********************************************************)
-
-lemma llor_pair_sn: ∀I,L1,L2,L,V,T. L1 ⩖[T] L2 ≡ L →
- |L1| < |L2| → L1 ⊢ |L2|-|L1|-1 ~ϵ 𝐅*[yinj 0]⦃T⦄ →
- L1.ⓑ{I}V ⩖[T] L2 ≡ L.ⓑ{I}V.
-/3 width=2 by clor_sn, lpx_sn_pair/ qed.
-
-lemma llor_pair_dx: ∀I,J,L1,L2,L,K2,V1,V2,T. L1 ⩖[T] L2 ≡ L →
- |L1| < |L2| → (L1 ⊢ |L2|-|L1|-1 ~ϵ 𝐅*[yinj 0]⦃T⦄ → ⊥) →
- ⇩[|L2|-|L1|-1] L2 ≡ K2.ⓑ{J}V2 →
- L1.ⓑ{I}V1 ⩖[T] L2 ≡ L.ⓑ{I}V2.
-/4 width=3 by clor_dx, lpx_sn_pair/ qed.
-
-lemma llor_total: ∀T,L2,L1. |L1| ≤ |L2| → ∃L. L1 ⩖[T] L2 ≡ L.
-#T #L2 #L1 elim L1 -L1 /2 width=2 by ex_intro/
-#L1 #I1 #V1 #IHL1 normalize
-#H elim IHL1 -IHL1 /2 width=3 by transitive_le/
-#L #HT elim (cofrees_dec L1 T 0 (|L2|-|L1|-1))
-[ /3 width=2 by llor_pair_sn, ex_intro/
-| elim (ldrop_O1_lt (Ⓕ) L2 (|L2|-|L1|-1))
- /5 width=4 by llor_pair_dx, monotonic_lt_minus_l, ex_intro/
-]
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 "basic_2/relocation/lpx_sn_alt.ma".
-include "basic_2/substitution/llor.ma".
-
-(* POINTWISE UNION FOR LOCAL ENVIRONMENTS ***********************************)
-
-(* Alternative definition ***************************************************)
-
-theorem llor_intro_alt: ∀T,L2,L1,L. |L1| ≤ |L2| → |L1| = |L| →
- (∀I1,I,K1,K,V1,V,i. ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L ≡ K.ⓑ{I}V →
- (K1 ⊢ |L2|-|L1|+i ~ϵ 𝐅*[yinj 0]⦃T⦄ → I1 = I ∧ V1 = V) ∧
- (∀I2,K2,V2. (K1 ⊢ |L2|-|L1|+i ~ϵ 𝐅*[yinj 0]⦃T⦄ → ⊥) →
- ⇩[|L2|-|L1|+i] L2 ≡ K2.ⓑ{I2}V2 → I1 = I ∧ V2 = V
- )
- ) → L1 ⩖[T] L2 ≡ L.
-#T #L2 #L1 #L #HL12 #HL1 #IH @lpx_sn_intro_alt // -HL1
-#I1 #I #K1 #K #V1 #V #i #HLK1 #HLK
-lapply (ldrop_fwd_length_minus4 … HLK1)
-lapply (ldrop_fwd_length_le4 … HLK1)
-normalize in ⊢ (%→%→?); #HKL1 #Hi
-lapply (plus_minus_minus_be_aux … HL12 Hi) // -Hi <minus_plus #Hi
-lapply (transitive_le … HKL1 HL12) -HKL1 -HL12 #HKL1
-elim (IH … HLK1 HLK) -IH -HLK1 -HLK #IH1 #IH2
-elim (cofrees_dec K1 T 0 (|L2|-|L1|+i))
-[ -IH2 #HT elim (IH1 … HT) -IH1
- #HI1 #HV1 @conj // <HV1 -V @clor_sn // <Hi -Hi //
-| -IH1 #HnT elim (ldrop_O1_lt (Ⓕ) L2 (|L2|-|L1|+i)) /2 width=1 by monotonic_lt_minus_l/
- #I2 #K2 #V2 #HLK2 elim (IH2 … HLK2) -IH2 /2 width=1 by/
- #HI1 #HV2 @conj // <HV2 -V @(clor_dx … I2 K2) // <Hi -Hi /2 width=1 by/
-]
-qed.
-
-theorem llor_inv_alt: ∀T,L2,L1,L. L1 ⩖[T] L2 ≡ L → |L1| ≤ |L2| →
- |L1| = |L| ∧
- (∀I1,I,K1,K,V1,V,i.
- ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L ≡ K.ⓑ{I}V →
- (∧∧ K1 ⊢ |L2|-|L1|+i ~ϵ 𝐅*[yinj 0]⦃T⦄ & I1 = I & V1 = V) ∨
- (∃∃I2,K2,V2. (K1 ⊢ |L2|-|L1|+i ~ϵ 𝐅*[yinj 0]⦃T⦄ → ⊥) &
- ⇩[|L2|-|L1|+i] L2 ≡ K2.ⓑ{I2}V2 &
- I1 = I & V2 = V
- )
- ).
-#T #L2 #L1 #L #H #HL12 elim (lpx_sn_inv_alt … H) -H
-#HL1 #IH @conj // -HL1
-#I1 #I #K1 #K #V1 #V #i #HLK1 #HLK
-lapply (ldrop_fwd_length_minus4 … HLK1)
-lapply (ldrop_fwd_length_le4 … HLK1)
-normalize in ⊢ (%→%→?); #HKL1 #Hi
-lapply (plus_minus_minus_be_aux … HL12 Hi) // -HL12 -Hi -HKL1
-<minus_plus #Hi >Hi -Hi
-elim (IH … HLK1 HLK) -IH #HI1 *
-/4 width=5 by or_introl, or_intror, and3_intro, ex4_3_intro/
-qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 "basic_2/relocation/lpx_sn_alt.ma".
+include "basic_2/substitution/llor.ma".
+include "basic_2/substitution/lleq_alt.ma".
+
+(* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****)
+
+(* Inversion lemmas on poinwise union for local environments ****************)
+
+lemma llpx_sn_llor_fwd_sn: ∀R. (∀L. reflexive … (R L)) →
+ ∀L1,L2,T. llpx_sn R 0 T L1 L2 →
+ ∀L. L1 ⩖[T] L2 ≡ L → lpx_sn R L1 L.
+#R #HR #L1 #L2 #T #H1 #L #H2
+elim (llpx_sn_llpx_sn_alt … H1) -H1 #HL12 #IH1
+elim H2 -H2 #_ #HL1 #IH2
+@lpx_sn_intro_alt // #I1 #I #K1 #K #V1 #V #i #HLK1 #HLK
+lapply (ldrop_fwd_length_lt2 … HLK) #HiL
+elim (ldrop_O1_lt (Ⓕ) L2 i) // -HiL -HL1 -HL12 #I2 #K2 #V2 #HLK2
+elim (IH2 … HLK1 HLK2 HLK) -IH2 -HLK * [ /2 width=1 by conj/ ]
+#HnT #H1 #H2 elim (IH1 … HnT … HLK1 HLK2) -IH1 -HnT -HLK1 -HLK2 /2 width=1 by conj/
+qed-.
[ { "substitution" * } {
[ { "lazy equivalence" * } {
[ "fleq ( ⦃?,?,?⦄ ⋕[?] ⦃?,?,?⦄ )" "fleq_fleq" * ]
- [ "lleq ( ? ⋕[?,?] ? )" "lleq_alt" + "lleq_alt_rec" + "lleq_leq" + "lleq_ldrop" + "lleq_fqus" + "lleq_lleq" * ]
+ [ "lleq ( ? ⋕[?,?] ? )" "lleq_alt" + "lleq_alt_rec" + "lleq_leq" + "lleq_ldrop" + "lleq_fqus" + "lleq_llor" + "lleq_lleq" * ]
}
]
[ { "lazy pointwise extension of a relation" * } {
- [ "llpx_sn" "llpx_sn_alt" + "llpx_sn_alt_rec" + "llpx_sn_tc" + "llpx_sn_leq" + "llpx_sn_ldrop" + "llpx_sn_lpx_sn" * ]
+ [ "llpx_sn" "llpx_sn_alt" + "llpx_sn_alt_rec" + "llpx_sn_tc" + "llpx_sn_leq" + "llpx_sn_ldrop" + "llpx_sn_lpx_sn" + "llpx_sn_llor" * ]
}
]
[ { "pointwise union for local environments" * } {
- [ "llor ( ? ⩖[?] ? ≡ ? )" "llor_alt" * ]
+ [ "llor ( ? ⩖[?] ? ≡ ? )" * ]
}
]
[ { "context-sensitive exclusion from free variables" * } {
projects / helm.git / commitdiff