--- /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 "ground_2/ynat/ynat_plus.ma".
+include "basic_2/notation/relations/freestar_4.ma".
+include "basic_2/substitution/lift_neg.ma".
+include "basic_2/substitution/drop.ma".
+
+(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
+
+inductive frees: relation4 ynat lenv term ynat ≝
+| frees_eq: ∀L,U,l,i. (∀T. ⬆[i, 1] T ≡ U → ⊥) → frees l L U i
+| frees_be: ∀I,L,K,U,W,l,i,j. l ≤ yinj j → yinj j < i →
+ (∀T. ⬆[j, 1] T ≡ U → ⊥) → ⬇[j]L ≡ K.ⓑ{I}W →
+ frees 0 K W (⫰(i-j)) → frees l L U i.
+
+interpretation
+ "context-sensitive free variables (term)"
+ 'FreeStar L i l U = (frees l L U i).
+
+definition frees_trans: predicate (relation3 lenv term term) ≝
+ λR. ∀L,U1,U2,i. R L U1 U2 → L ⊢ i ϵ 𝐅*[0]⦃U2⦄ → L ⊢ i ϵ 𝐅*[0]⦃U1⦄.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma frees_inv: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ →
+ (∀T. ⬆[i, 1] T ≡ U → ⊥) ∨
+ ∃∃I,K,W,j. l ≤ yinj j & j < i & (∀T. ⬆[j, 1] T ≡ U → ⊥) &
+ ⬇[j]L ≡ K.ⓑ{I}W & K ⊢ ⫰(i-j) ϵ 𝐅*[yinj 0]⦃W⦄.
+#L #U #l #i * -L -U -l -i /4 width=9 by ex5_4_intro, or_intror, or_introl/
+qed-.
+
+lemma frees_inv_sort: ∀L,l,i,k. L ⊢ i ϵ 𝐅*[l]⦃⋆k⦄ → ⊥.
+#L #l #i #k #H elim (frees_inv … H) -H [|*] /2 width=2 by/
+qed-.
+
+lemma frees_inv_gref: ∀L,l,i,p. L ⊢ i ϵ 𝐅*[l]⦃§p⦄ → ⊥.
+#L #l #i #p #H elim (frees_inv … H) -H [|*] /2 width=2 by/
+qed-.
+
+lemma frees_inv_lref: ∀L,l,j,i. L ⊢ i ϵ 𝐅*[l]⦃#j⦄ →
+ yinj j = i ∨
+ ∃∃I,K,W. l ≤ yinj j & yinj j < i & ⬇[j] L ≡ K.ⓑ{I}W & K ⊢ ⫰(i-j) ϵ 𝐅*[yinj 0]⦃W⦄.
+#L #l #x #i #H elim (frees_inv … H) -H
+[ /4 width=2 by nlift_inv_lref_be_SO, or_introl/
+| * #I #K #W #j #Hlj #Hji #Hnx #HLK #HW
+ lapply (nlift_inv_lref_be_SO … Hnx) -Hnx #H
+ lapply (yinj_inj … H) -H #H destruct
+ /3 width=5 by ex4_3_intro, or_intror/
+]
+qed-.
+
+lemma frees_inv_lref_free: ∀L,l,j,i. L ⊢ i ϵ 𝐅*[l]⦃#j⦄ → |L| ≤ j → yinj j = i.
+#L #l #j #i #H #Hj elim (frees_inv_lref … H) -H //
+* #I #K #W #_ #_ #HLK lapply (drop_fwd_length_lt2 … HLK) -I
+#H elim (lt_refl_false j) /2 width=3 by lt_to_le_to_lt/
+qed-.
+
+lemma frees_inv_lref_skip: ∀L,l,j,i. L ⊢ i ϵ 𝐅*[l]⦃#j⦄ → yinj j < l → yinj j = i.
+#L #l #j #i #H #Hjl elim (frees_inv_lref … H) -H //
+* #I #K #W #Hlj elim (ylt_yle_false … Hlj) -Hlj //
+qed-.
+
+lemma frees_inv_lref_ge: ∀L,l,j,i. L ⊢ i ϵ 𝐅*[l]⦃#j⦄ → i ≤ j → yinj j = i.
+#L #l #j #i #H #Hij elim (frees_inv_lref … H) -H //
+* #I #K #W #_ #Hji elim (ylt_yle_false … Hji Hij)
+qed-.
+
+lemma frees_inv_lref_lt: ∀L,l,j,i.L ⊢ i ϵ 𝐅*[l]⦃#j⦄ → j < i →
+ ∃∃I,K,W. l ≤ yinj j & ⬇[j] L ≡ K.ⓑ{I}W & K ⊢ ⫰(i-j) ϵ 𝐅*[yinj 0]⦃W⦄.
+#L #l #j #i #H #Hji elim (frees_inv_lref … H) -H
+[ #H elim (ylt_yle_false … Hji) //
+| * /2 width=5 by ex3_3_intro/
+]
+qed-.
+
+lemma frees_inv_bind: ∀a,I,L,W,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃ⓑ{a,I}W.U⦄ →
+ L ⊢ i ϵ 𝐅*[l]⦃W⦄ ∨ L.ⓑ{I}W ⊢ ⫯i ϵ 𝐅*[⫯l]⦃U⦄ .
+#a #J #L #V #U #l #i #H elim (frees_inv … H) -H
+[ #HnX elim (nlift_inv_bind … HnX) -HnX
+ /4 width=2 by frees_eq, or_intror, or_introl/
+| * #I #K #W #j #Hlj #Hji #HnX #HLK #HW elim (nlift_inv_bind … HnX) -HnX
+ [ /4 width=9 by frees_be, or_introl/
+ | #HnT @or_intror @(frees_be … HnT) -HnT
+ [4: lapply (yle_succ … Hlj) // (**)
+ |5: lapply (ylt_succ … Hji) // (**)
+ |6: /2 width=4 by drop_drop/
+ |7: <yminus_succ in HW; // (**)
+ |*: skip
+ ]
+ ]
+]
+qed-.
+
+lemma frees_inv_flat: ∀I,L,W,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃ⓕ{I}W.U⦄ →
+ L ⊢ i ϵ 𝐅*[l]⦃W⦄ ∨ L ⊢ i ϵ 𝐅*[l]⦃U⦄ .
+#J #L #V #U #l #i #H elim (frees_inv … H) -H
+[ #HnX elim (nlift_inv_flat … HnX) -HnX
+ /4 width=2 by frees_eq, or_intror, or_introl/
+| * #I #K #W #j #Hlj #Hji #HnX #HLK #HW elim (nlift_inv_flat … HnX) -HnX
+ /4 width=9 by frees_be, or_intror, or_introl/
+]
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma frees_lref_eq: ∀L,l,i. L ⊢ i ϵ 𝐅*[l]⦃#i⦄.
+/4 width=7 by frees_eq, lift_inv_lref2_be, ylt_inj/ qed.
+
+lemma frees_lref_be: ∀I,L,K,W,l,i,j. l ≤ yinj j → j < i → ⬇[j]L ≡ K.ⓑ{I}W →
+ K ⊢ ⫰(i-j) ϵ 𝐅*[0]⦃W⦄ → L ⊢ i ϵ 𝐅*[l]⦃#j⦄.
+/4 width=9 by frees_be, lift_inv_lref2_be, ylt_inj/ qed.
+
+lemma frees_bind_sn: ∀a,I,L,W,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃W⦄ →
+ L ⊢ i ϵ 𝐅*[l]⦃ⓑ{a,I}W.U⦄.
+#a #I #L #W #U #l #i #H elim (frees_inv … H) -H [|*]
+/4 width=9 by frees_be, frees_eq, nlift_bind_sn/
+qed.
+
+lemma frees_bind_dx: ∀a,I,L,W,U,l,i. L.ⓑ{I}W ⊢ ⫯i ϵ 𝐅*[⫯l]⦃U⦄ →
+ L ⊢ i ϵ 𝐅*[l]⦃ⓑ{a,I}W.U⦄.
+#a #J #L #V #U #l #i #H elim (frees_inv … H) -H
+[ /4 width=9 by frees_eq, nlift_bind_dx/
+| * #I #K #W #j #Hlj elim (yle_inv_succ1 … Hlj) -Hlj #Hlj
+ #Hj <Hj >yminus_succ
+ lapply (ylt_O … Hj) -Hj #Hj #H
+ lapply (ylt_inv_succ … H) -H #Hji #HnU #HLK #HW
+ @(frees_be … Hlj Hji … HW) -HW -Hlj -Hji (**) (* explicit constructor *)
+ [2: #X #H lapply (nlift_bind_dx … H) /2 width=2 by/ (**)
+ |3: lapply (drop_inv_drop1_lt … HLK ?) -HLK //
+ |*: skip
+]
+qed.
+
+lemma frees_flat_sn: ∀I,L,W,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃W⦄ →
+ L ⊢ i ϵ 𝐅*[l]⦃ⓕ{I}W.U⦄.
+#I #L #W #U #l #i #H elim (frees_inv … H) -H [|*]
+/4 width=9 by frees_be, frees_eq, nlift_flat_sn/
+qed.
+
+lemma frees_flat_dx: ∀I,L,W,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ →
+ L ⊢ i ϵ 𝐅*[l]⦃ⓕ{I}W.U⦄.
+#I #L #W #U #l #i #H elim (frees_inv … H) -H [|*]
+/4 width=9 by frees_be, frees_eq, nlift_flat_dx/
+qed.
+
+lemma frees_weak: ∀L,U,l1,i. L ⊢ i ϵ 𝐅*[l1]⦃U⦄ →
+ ∀l2. l2 ≤ l1 → L ⊢ i ϵ 𝐅*[l2]⦃U⦄.
+#L #U #l1 #i #H elim H -L -U -l1 -i
+/3 width=9 by frees_be, frees_eq, yle_trans/
+qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma frees_inv_bind_O: ∀a,I,L,W,U,i. L ⊢ i ϵ 𝐅*[0]⦃ⓑ{a,I}W.U⦄ →
+ L ⊢ i ϵ 𝐅*[0]⦃W⦄ ∨ L.ⓑ{I}W ⊢ ⫯i ϵ 𝐅*[0]⦃U⦄ .
+#a #I #L #W #U #i #H elim (frees_inv_bind … H) -H
+/3 width=3 by frees_weak, or_intror, or_introl/
+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 "ground_2/ynat/ynat_plus.ma".
-include "basic_2/notation/relations/freestar_4.ma".
-include "basic_2/substitution/lift_neg.ma".
-include "basic_2/substitution/drop.ma".
-
-(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
-
-inductive frees: relation4 ynat lenv term ynat ≝
-| frees_eq: ∀L,U,l,i. (∀T. ⬆[i, 1] T ≡ U → ⊥) → frees l L U i
-| frees_be: ∀I,L,K,U,W,l,i,j. l ≤ yinj j → yinj j < i →
- (∀T. ⬆[j, 1] T ≡ U → ⊥) → ⬇[j]L ≡ K.ⓑ{I}W →
- frees 0 K W (⫰(i-j)) → frees l L U i.
-
-interpretation
- "context-sensitive free variables (term)"
- 'FreeStar L i l U = (frees l L U i).
-
-definition frees_trans: predicate (relation3 lenv term term) ≝
- λR. ∀L,U1,U2,i. R L U1 U2 → L ⊢ i ϵ 𝐅*[0]⦃U2⦄ → L ⊢ i ϵ 𝐅*[0]⦃U1⦄.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma frees_inv: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ →
- (∀T. ⬆[i, 1] T ≡ U → ⊥) ∨
- ∃∃I,K,W,j. l ≤ yinj j & j < i & (∀T. ⬆[j, 1] T ≡ U → ⊥) &
- ⬇[j]L ≡ K.ⓑ{I}W & K ⊢ ⫰(i-j) ϵ 𝐅*[yinj 0]⦃W⦄.
-#L #U #l #i * -L -U -l -i /4 width=9 by ex5_4_intro, or_intror, or_introl/
-qed-.
-
-lemma frees_inv_sort: ∀L,l,i,k. L ⊢ i ϵ 𝐅*[l]⦃⋆k⦄ → ⊥.
-#L #l #i #k #H elim (frees_inv … H) -H [|*] /2 width=2 by/
-qed-.
-
-lemma frees_inv_gref: ∀L,l,i,p. L ⊢ i ϵ 𝐅*[l]⦃§p⦄ → ⊥.
-#L #l #i #p #H elim (frees_inv … H) -H [|*] /2 width=2 by/
-qed-.
-
-lemma frees_inv_lref: ∀L,l,j,i. L ⊢ i ϵ 𝐅*[l]⦃#j⦄ →
- yinj j = i ∨
- ∃∃I,K,W. l ≤ yinj j & yinj j < i & ⬇[j] L ≡ K.ⓑ{I}W & K ⊢ ⫰(i-j) ϵ 𝐅*[yinj 0]⦃W⦄.
-#L #l #x #i #H elim (frees_inv … H) -H
-[ /4 width=2 by nlift_inv_lref_be_SO, or_introl/
-| * #I #K #W #j #Hlj #Hji #Hnx #HLK #HW
- lapply (nlift_inv_lref_be_SO … Hnx) -Hnx #H
- lapply (yinj_inj … H) -H #H destruct
- /3 width=5 by ex4_3_intro, or_intror/
-]
-qed-.
-
-lemma frees_inv_lref_free: ∀L,l,j,i. L ⊢ i ϵ 𝐅*[l]⦃#j⦄ → |L| ≤ j → yinj j = i.
-#L #l #j #i #H #Hj elim (frees_inv_lref … H) -H //
-* #I #K #W #_ #_ #HLK lapply (drop_fwd_length_lt2 … HLK) -I
-#H elim (lt_refl_false j) /2 width=3 by lt_to_le_to_lt/
-qed-.
-
-lemma frees_inv_lref_skip: ∀L,l,j,i. L ⊢ i ϵ 𝐅*[l]⦃#j⦄ → yinj j < l → yinj j = i.
-#L #l #j #i #H #Hjl elim (frees_inv_lref … H) -H //
-* #I #K #W #Hlj elim (ylt_yle_false … Hlj) -Hlj //
-qed-.
-
-lemma frees_inv_lref_ge: ∀L,l,j,i. L ⊢ i ϵ 𝐅*[l]⦃#j⦄ → i ≤ j → yinj j = i.
-#L #l #j #i #H #Hij elim (frees_inv_lref … H) -H //
-* #I #K #W #_ #Hji elim (ylt_yle_false … Hji Hij)
-qed-.
-
-lemma frees_inv_lref_lt: ∀L,l,j,i.L ⊢ i ϵ 𝐅*[l]⦃#j⦄ → j < i →
- ∃∃I,K,W. l ≤ yinj j & ⬇[j] L ≡ K.ⓑ{I}W & K ⊢ ⫰(i-j) ϵ 𝐅*[yinj 0]⦃W⦄.
-#L #l #j #i #H #Hji elim (frees_inv_lref … H) -H
-[ #H elim (ylt_yle_false … Hji) //
-| * /2 width=5 by ex3_3_intro/
-]
-qed-.
-
-lemma frees_inv_bind: ∀a,I,L,W,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃ⓑ{a,I}W.U⦄ →
- L ⊢ i ϵ 𝐅*[l]⦃W⦄ ∨ L.ⓑ{I}W ⊢ ⫯i ϵ 𝐅*[⫯l]⦃U⦄ .
-#a #J #L #V #U #l #i #H elim (frees_inv … H) -H
-[ #HnX elim (nlift_inv_bind … HnX) -HnX
- /4 width=2 by frees_eq, or_intror, or_introl/
-| * #I #K #W #j #Hlj #Hji #HnX #HLK #HW elim (nlift_inv_bind … HnX) -HnX
- [ /4 width=9 by frees_be, or_introl/
- | #HnT @or_intror @(frees_be … HnT) -HnT
- [4: lapply (yle_succ … Hlj) // (**)
- |5: lapply (ylt_succ … Hji) // (**)
- |6: /2 width=4 by drop_drop/
- |7: <yminus_succ in HW; // (**)
- |*: skip
- ]
- ]
-]
-qed-.
-
-lemma frees_inv_flat: ∀I,L,W,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃ⓕ{I}W.U⦄ →
- L ⊢ i ϵ 𝐅*[l]⦃W⦄ ∨ L ⊢ i ϵ 𝐅*[l]⦃U⦄ .
-#J #L #V #U #l #i #H elim (frees_inv … H) -H
-[ #HnX elim (nlift_inv_flat … HnX) -HnX
- /4 width=2 by frees_eq, or_intror, or_introl/
-| * #I #K #W #j #Hlj #Hji #HnX #HLK #HW elim (nlift_inv_flat … HnX) -HnX
- /4 width=9 by frees_be, or_intror, or_introl/
-]
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma frees_lref_eq: ∀L,l,i. L ⊢ i ϵ 𝐅*[l]⦃#i⦄.
-/4 width=7 by frees_eq, lift_inv_lref2_be, ylt_inj/ qed.
-
-lemma frees_lref_be: ∀I,L,K,W,l,i,j. l ≤ yinj j → j < i → ⬇[j]L ≡ K.ⓑ{I}W →
- K ⊢ ⫰(i-j) ϵ 𝐅*[0]⦃W⦄ → L ⊢ i ϵ 𝐅*[l]⦃#j⦄.
-/4 width=9 by frees_be, lift_inv_lref2_be, ylt_inj/ qed.
-
-lemma frees_bind_sn: ∀a,I,L,W,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃W⦄ →
- L ⊢ i ϵ 𝐅*[l]⦃ⓑ{a,I}W.U⦄.
-#a #I #L #W #U #l #i #H elim (frees_inv … H) -H [|*]
-/4 width=9 by frees_be, frees_eq, nlift_bind_sn/
-qed.
-
-lemma frees_bind_dx: ∀a,I,L,W,U,l,i. L.ⓑ{I}W ⊢ ⫯i ϵ 𝐅*[⫯l]⦃U⦄ →
- L ⊢ i ϵ 𝐅*[l]⦃ⓑ{a,I}W.U⦄.
-#a #J #L #V #U #l #i #H elim (frees_inv … H) -H
-[ /4 width=9 by frees_eq, nlift_bind_dx/
-| * #I #K #W #j #Hlj elim (yle_inv_succ1 … Hlj) -Hlj #Hlj
- #Hj <Hj >yminus_succ
- lapply (ylt_O … Hj) -Hj #Hj #H
- lapply (ylt_inv_succ … H) -H #Hji #HnU #HLK #HW
- @(frees_be … Hlj Hji … HW) -HW -Hlj -Hji (**) (* explicit constructor *)
- [2: #X #H lapply (nlift_bind_dx … H) /2 width=2 by/ (**)
- |3: lapply (drop_inv_drop1_lt … HLK ?) -HLK //
- |*: skip
-]
-qed.
-
-lemma frees_flat_sn: ∀I,L,W,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃W⦄ →
- L ⊢ i ϵ 𝐅*[l]⦃ⓕ{I}W.U⦄.
-#I #L #W #U #l #i #H elim (frees_inv … H) -H [|*]
-/4 width=9 by frees_be, frees_eq, nlift_flat_sn/
-qed.
-
-lemma frees_flat_dx: ∀I,L,W,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ →
- L ⊢ i ϵ 𝐅*[l]⦃ⓕ{I}W.U⦄.
-#I #L #W #U #l #i #H elim (frees_inv … H) -H [|*]
-/4 width=9 by frees_be, frees_eq, nlift_flat_dx/
-qed.
-
-lemma frees_weak: ∀L,U,l1,i. L ⊢ i ϵ 𝐅*[l1]⦃U⦄ →
- ∀l2. l2 ≤ l1 → L ⊢ i ϵ 𝐅*[l2]⦃U⦄.
-#L #U #l1 #i #H elim H -L -U -l1 -i
-/3 width=9 by frees_be, frees_eq, yle_trans/
-qed-.
-
-(* Advanced inversion lemmas ************************************************)
-
-lemma frees_inv_bind_O: ∀a,I,L,W,U,i. L ⊢ i ϵ 𝐅*[0]⦃ⓑ{a,I}W.U⦄ →
- L ⊢ i ϵ 𝐅*[0]⦃W⦄ ∨ L.ⓑ{I}W ⊢ ⫯i ϵ 𝐅*[0]⦃U⦄ .
-#a #I #L #W #U #i #H elim (frees_inv_bind … H) -H
-/3 width=3 by frees_weak, or_intror, or_introl/
-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/drop_append.ma".
+include "basic_2/multiple/frees.ma".
+
+(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
+
+(* Properties on append for local environments ******************************)
+
+lemma frees_append: ∀L2,U,l,i. L2 ⊢ i ϵ 𝐅*[l]⦃U⦄ → i ≤ |L2| →
+ ∀L1. L1 @@ L2 ⊢ i ϵ 𝐅*[l]⦃U⦄.
+#L2 #U #l #i #H elim H -L2 -U -l -i /3 width=2 by frees_eq/
+#I #L2 #K2 #U #W #l #i #j #Hlj #Hji #HnU #HLK2 #_ #IHW #Hi #L1
+lapply (drop_fwd_length_minus2 … HLK2) normalize #H0
+lapply (drop_O1_append_sn_le … HLK2 … L1) -HLK2
+[ -I -L1 -K2 -U -W -l /4 width=3 by ylt_yle_trans, ylt_inv_inj, lt_to_le/
+| #HLK2 @(frees_be … HnU HLK2) // -HnU -HLK2 @IHW -IHW
+ >(minus_plus_m_m (|K2|) 1) >H0 -H0 <yminus_inj >yminus_SO2
+ /3 width=1 by monotonic_yle_minus_dx, yle_pred/
+]
+qed.
+
+(* Inversion lemmas on append for local environments ************************)
+
+fact frees_inv_append_aux: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ → ∀L1,L2. L = L1 @@ L2 →
+ i ≤ |L2| → L2 ⊢ i ϵ 𝐅*[l]⦃U⦄.
+#L #U #l #i #H elim H -L -U -l -i /3 width=2 by frees_eq/
+#Z #L #Y #U #X #l #i #j #Hlj #Hji #HnU #HLY #_ #IHW #L1 #L2 #H #Hi destruct
+elim (drop_O1_lt (Ⓕ) L2 j) [2: -Z -Y -L1 -X -U -l /3 width=3 by ylt_yle_trans, ylt_inv_inj/ ]
+#I #K2 #W #HLK2 lapply (drop_fwd_length_minus2 … HLK2) normalize #H0
+lapply (drop_O1_inv_append1_le … HLY … HLK2) -HLY
+[ -Z -I -Y -K2 -L1 -X -U -W -l /4 width=3 by ylt_yle_trans, ylt_inv_inj, lt_to_le/
+| normalize #H destruct
+ @(frees_be … HnU HLK2) -HnU -HLK2 // @IHW -IHW //
+ >(minus_plus_m_m (|K2|) 1) >H0 -H0 <yminus_inj >yminus_SO2
+ /3 width=1 by monotonic_yle_minus_dx, yle_pred/
+]
+qed-.
+
+lemma frees_inv_append: ∀L1,L2,U,l,i. L1 @@ L2 ⊢ i ϵ 𝐅*[l]⦃U⦄ →
+ i ≤ |L2| → L2 ⊢ i ϵ 𝐅*[l]⦃U⦄.
+/2 width=4 by frees_inv_append_aux/ 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/drop_append.ma".
-include "basic_2/multiple/frees.ma".
-
-(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
-
-(* Properties on append for local environments ******************************)
-
-lemma frees_append: ∀L2,U,l,i. L2 ⊢ i ϵ 𝐅*[l]⦃U⦄ → i ≤ |L2| →
- ∀L1. L1 @@ L2 ⊢ i ϵ 𝐅*[l]⦃U⦄.
-#L2 #U #l #i #H elim H -L2 -U -l -i /3 width=2 by frees_eq/
-#I #L2 #K2 #U #W #l #i #j #Hlj #Hji #HnU #HLK2 #_ #IHW #Hi #L1
-lapply (drop_fwd_length_minus2 … HLK2) normalize #H0
-lapply (drop_O1_append_sn_le … HLK2 … L1) -HLK2
-[ -I -L1 -K2 -U -W -l /4 width=3 by ylt_yle_trans, ylt_inv_inj, lt_to_le/
-| #HLK2 @(frees_be … HnU HLK2) // -HnU -HLK2 @IHW -IHW
- >(minus_plus_m_m (|K2|) 1) >H0 -H0 <yminus_inj >yminus_SO2
- /3 width=1 by monotonic_yle_minus_dx, yle_pred/
-]
-qed.
-
-(* Inversion lemmas on append for local environments ************************)
-
-fact frees_inv_append_aux: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ → ∀L1,L2. L = L1 @@ L2 →
- i ≤ |L2| → L2 ⊢ i ϵ 𝐅*[l]⦃U⦄.
-#L #U #l #i #H elim H -L -U -l -i /3 width=2 by frees_eq/
-#Z #L #Y #U #X #l #i #j #Hlj #Hji #HnU #HLY #_ #IHW #L1 #L2 #H #Hi destruct
-elim (drop_O1_lt (Ⓕ) L2 j) [2: -Z -Y -L1 -X -U -l /3 width=3 by ylt_yle_trans, ylt_inv_inj/ ]
-#I #K2 #W #HLK2 lapply (drop_fwd_length_minus2 … HLK2) normalize #H0
-lapply (drop_O1_inv_append1_le … HLY … HLK2) -HLY
-[ -Z -I -Y -K2 -L1 -X -U -W -l /4 width=3 by ylt_yle_trans, ylt_inv_inj, lt_to_le/
-| normalize #H destruct
- @(frees_be … HnU HLK2) -HnU -HLK2 // @IHW -IHW //
- >(minus_plus_m_m (|K2|) 1) >H0 -H0 <yminus_inj >yminus_SO2
- /3 width=1 by monotonic_yle_minus_dx, yle_pred/
-]
-qed-.
-
-lemma frees_inv_append: ∀L1,L2,U,l,i. L1 @@ L2 ⊢ i ϵ 𝐅*[l]⦃U⦄ →
- i ≤ |L2| → L2 ⊢ i ϵ 𝐅*[l]⦃U⦄.
-/2 width=4 by frees_inv_append_aux/ 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 "ground_2/ynat/ynat_max.ma".
+include "basic_2/substitution/drop_drop.ma".
+include "basic_2/multiple/frees.ma".
+
+(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
+
+(* Advanced properties ******************************************************)
+
+lemma frees_dec: ∀L,U,l,i. Decidable (frees l L U i).
+#L #U @(f2_ind … rfw … L U) -L -U
+#x #IH #L * *
+[ -IH /3 width=5 by frees_inv_sort, or_intror/
+| #j #Hx #l #i elim (ylt_split_eq i j) #Hji
+ [ -x @or_intror #H elim (ylt_yle_false … Hji)
+ lapply (frees_inv_lref_ge … H ?) -L -l /2 width=1 by ylt_fwd_le/
+ | -x /2 width=1 by or_introl/
+ | elim (ylt_split j l) #Hli
+ [ -x @or_intror #H elim (ylt_yle_false … Hji)
+ lapply (frees_inv_lref_skip … H ?) -L //
+ | elim (lt_or_ge j (|L|)) #Hj
+ [ elim (drop_O1_lt (Ⓕ) L j) // -Hj #I #K #W #HLK destruct
+ elim (IH K W … 0 (i-j-1)) -IH [1,3: /3 width=5 by frees_lref_be, drop_fwd_rfw, or_introl/ ] #HnW
+ @or_intror #H elim (frees_inv_lref_lt … H) // #Z #Y #X #_ #HLY -l
+ lapply (drop_mono … HLY … HLK) -L #H destruct /2 width=1 by/
+ | -x @or_intror #H elim (ylt_yle_false … Hji)
+ lapply (frees_inv_lref_free … H ?) -l //
+ ]
+ ]
+ ]
+| -IH /3 width=5 by frees_inv_gref, or_intror/
+| #a #I #W #U #Hx #l #i destruct
+ elim (IH L W … l i) [1,3: /3 width=1 by frees_bind_sn, or_introl/ ] #HnW
+ elim (IH (L.ⓑ{I}W) U … (⫯l) (i+1)) -IH [1,3: /3 width=1 by frees_bind_dx, or_introl/ ] #HnU
+ @or_intror #H elim (frees_inv_bind … H) -H /2 width=1 by/
+| #I #W #U #Hx #l #i destruct
+ elim (IH L W … l i) [1,3: /3 width=1 by frees_flat_sn, or_introl/ ] #HnW
+ elim (IH L U … l i) -IH [1,3: /3 width=1 by frees_flat_dx, or_introl/ ] #HnU
+ @or_intror #H elim (frees_inv_flat … H) -H /2 width=1 by/
+]
+qed-.
+
+lemma frees_S: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[yinj l]⦃U⦄ → ∀I,K,W. ⬇[l] L ≡ K.ⓑ{I}W →
+ (K ⊢ ⫰(i-l) ϵ 𝐅*[0]⦃W⦄ → ⊥) → L ⊢ i ϵ 𝐅*[⫯l]⦃U⦄.
+#L #U #l #i #H elim (frees_inv … H) -H /3 width=2 by frees_eq/
+* #I #K #W #j #Hlj #Hji #HnU #HLK #HW #I0 #K0 #W0 #HLK0 #HnW0
+lapply (yle_inv_inj … Hlj) -Hlj #Hlj
+elim (le_to_or_lt_eq … Hlj) -Hlj
+[ -I0 -K0 -W0 /3 width=9 by frees_be, yle_inj/
+| -Hji -HnU #H destruct
+ lapply (drop_mono … HLK0 … HLK) #H destruct -I
+ elim HnW0 -L -U -HnW0 //
+]
+qed.
+
+(* Note: lemma 1250 *)
+lemma frees_bind_dx_O: ∀a,I,L,W,U,i. L.ⓑ{I}W ⊢ ⫯i ϵ 𝐅*[0]⦃U⦄ →
+ L ⊢ i ϵ 𝐅*[0]⦃ⓑ{a,I}W.U⦄.
+#a #I #L #W #U #i #HU elim (frees_dec L W 0 i)
+/4 width=5 by frees_S, frees_bind_dx, frees_bind_sn/
+qed.
+
+(* Properties on relocation *************************************************)
+
+lemma frees_lift_ge: ∀K,T,l,i. K ⊢ i ϵ𝐅*[l]⦃T⦄ →
+ ∀L,s,l0,m0. ⬇[s, l0, m0] L ≡ K →
+ ∀U. ⬆[l0, m0] T ≡ U → l0 ≤ i →
+ L ⊢ i+m0 ϵ 𝐅*[l]⦃U⦄.
+#K #T #l #i #H elim H -K -T -l -i
+[ #K #T #l #i #HnT #L #s #l0 #m0 #_ #U #HTU #Hl0i -K -s
+ @frees_eq #X #HXU elim (lift_div_le … HTU … HXU) -U /2 width=2 by/
+| #I #K #K0 #T #V #l #i #j #Hlj #Hji #HnT #HK0 #HV #IHV #L #s #l0 #m0 #HLK #U #HTU #Hl0i
+ elim (ylt_split j l0) #H0
+ [ elim (drop_trans_lt … HLK … HK0) // -K #L0 #W #HL0 >yminus_SO2 #HLK0 #HVW
+ @(frees_be … HL0) -HL0 -HV /3 width=3 by ylt_plus_dx2_trans/
+ [ lapply (ylt_fwd_lt_O1 … H0) #H1
+ #X #HXU <(ymax_pre_sn l0 1) in HTU; /2 width=1 by ylt_fwd_le_succ1/ #HTU
+ <(ylt_inv_O1 l0) in H0; // -H1 #H0
+ elim (lift_div_le … HXU … HTU ?) -U /2 width=2 by ylt_fwd_succ2/
+ | >yplus_minus_comm_inj /2 width=1 by ylt_fwd_le/
+ <yplus_pred1 /4 width=5 by monotonic_yle_minus_dx, yle_pred, ylt_to_minus/
+ ]
+ | lapply (drop_trans_ge … HLK … HK0 ?) // -K #HLK0
+ lapply (drop_inv_gen … HLK0) >commutative_plus -HLK0 #HLK0
+ @(frees_be … HLK0) -HLK0 -IHV
+ /2 width=1 by monotonic_ylt_plus_dx, yle_plus_dx1_trans/
+ [ #X <yplus_inj #HXU elim (lift_div_le … HTU … HXU) -U /2 width=2 by/
+ | <yplus_minus_assoc_comm_inj //
+ ]
+ ]
+]
+qed.
+
+(* Inversion lemmas on relocation *******************************************)
+
+lemma frees_inv_lift_be: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ →
+ ∀K,s,l0,m0. ⬇[s, l0, m0+1] L ≡ K →
+ ∀T. ⬆[l0, m0+1] T ≡ U → l0 ≤ i → i ≤ l0 + m0 → ⊥.
+#L #U #l #i #H elim H -L -U -l -i
+[ #L #U #l #i #HnU #K #s #l0 #m0 #_ #T #HTU #Hl0i #Hilm0
+ elim (lift_split … HTU i m0) -HTU /2 width=2 by/
+| #I #L #K0 #U #W #l #i #j #Hli #Hij #HnU #HLK0 #_ #IHW #K #s #l0 #m0 #HLK #T #HTU #Hl0i #Hilm0
+ elim (ylt_split j l0) #H1
+ [ elim (drop_conf_lt … HLK … HLK0) -L // #L0 #V #H #HKL0 #HVW
+ @(IHW … HKL0 … HVW)
+ [ /3 width=1 by monotonic_yle_minus_dx, yle_pred/
+ | >yplus_pred1 /2 width=1 by ylt_to_minus/
+ <yplus_minus_comm_inj /3 width=1 by monotonic_yle_minus_dx, yle_pred, ylt_fwd_le/
+ ]
+ | elim (lift_split … HTU j m0) -HTU /3 width=3 by ylt_yle_trans, ylt_fwd_le/
+ ]
+]
+qed-.
+
+lemma frees_inv_lift_ge: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ →
+ ∀K,s,l0,m0. ⬇[s, l0, m0] L ≡ K →
+ ∀T. ⬆[l0, m0] T ≡ U → l0 + m0 ≤ i →
+ K ⊢ i-m0 ϵ𝐅*[l-yinj m0]⦃T⦄.
+#L #U #l #i #H elim H -L -U -l -i
+[ #L #U #l #i #HnU #K #s #l0 #m0 #HLK #T #HTU #Hlm0i -L -s
+ elim (yle_inv_plus_inj2 … Hlm0i) -Hlm0i #Hl0im0 #Hm0i @frees_eq #X #HXT -K
+ elim (lift_trans_le … HXT … HTU) -T // >ymax_pre_sn /2 width=2 by/
+| #I #L #K0 #U #W #l #i #j #Hli #Hij #HnU #HLK0 #_ #IHW #K #s #l0 #m0 #HLK #T #HTU #Hlm0i
+ elim (ylt_split j l0) #H1
+ [ elim (drop_conf_lt … HLK … HLK0) -L // #L0 #V #H #HKL0 #HVW
+ elim (yle_inv_plus_inj2 … Hlm0i) #H0 #Hm0i
+ @(frees_be … H) -H
+ [ /3 width=1 by yle_plus_dx1_trans, monotonic_yle_minus_dx/
+ | /2 width=3 by ylt_yle_trans/
+ | #X #HXT elim (lift_trans_ge … HXT … HTU) -T /2 width=2 by ylt_fwd_le_succ1/
+ | lapply (IHW … HKL0 … HVW ?) // -I -K -K0 -L0 -V -W -T -U -s
+ >yplus_pred1 /2 width=1 by ylt_to_minus/
+ <yplus_minus_comm_inj /3 width=1 by monotonic_yle_minus_dx, yle_pred, ylt_fwd_le/
+ ]
+ | elim (ylt_split j (l0+m0)) #H2
+ [ -L -I -W elim (yle_inv_inj2 … H1) -H1 #x #H1 #H destruct
+ lapply (ylt_plus2_to_minus_inj1 … H2) /2 width=1 by yle_inj/ #H3
+ lapply (ylt_fwd_lt_O1 … H3) -H3 #H3
+ elim (lift_split … HTU j (m0-1)) -HTU /2 width=1 by yle_inj/
+ [ >minus_minus_associative /2 width=1 by ylt_inv_inj/ <minus_n_n
+ -H2 #X #_ #H elim (HnU … H)
+ | <yminus_inj >yminus_SO2 >yplus_pred2 /2 width=1 by ylt_fwd_le_pred2/
+ ]
+ | lapply (drop_conf_ge … HLK … HLK0 ?) // -L #HK0
+ elim ( yle_inv_plus_inj2 … H2) -H2 #H2 #Hm0j
+ @(frees_be … HK0)
+ [ /2 width=1 by monotonic_yle_minus_dx/
+ | /2 width=1 by monotonic_ylt_minus_dx/
+ | #X #HXT elim (lift_trans_le … HXT … HTU) -T //
+ <yminus_inj >ymax_pre_sn /2 width=2 by/
+ | <yminus_inj >yplus_minus_assoc_comm_inj //
+ >ymax_pre_sn /3 width=5 by yle_trans, ylt_fwd_le/
+ ]
+ ]
+ ]
+]
+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 "ground_2/ynat/ynat_max.ma".
-include "basic_2/substitution/drop_drop.ma".
-include "basic_2/multiple/frees.ma".
-
-(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
-
-(* Advanced properties ******************************************************)
-
-lemma frees_dec: ∀L,U,l,i. Decidable (frees l L U i).
-#L #U @(f2_ind … rfw … L U) -L -U
-#x #IH #L * *
-[ -IH /3 width=5 by frees_inv_sort, or_intror/
-| #j #Hx #l #i elim (ylt_split_eq i j) #Hji
- [ -x @or_intror #H elim (ylt_yle_false … Hji)
- lapply (frees_inv_lref_ge … H ?) -L -l /2 width=1 by ylt_fwd_le/
- | -x /2 width=1 by or_introl/
- | elim (ylt_split j l) #Hli
- [ -x @or_intror #H elim (ylt_yle_false … Hji)
- lapply (frees_inv_lref_skip … H ?) -L //
- | elim (lt_or_ge j (|L|)) #Hj
- [ elim (drop_O1_lt (Ⓕ) L j) // -Hj #I #K #W #HLK destruct
- elim (IH K W … 0 (i-j-1)) -IH [1,3: /3 width=5 by frees_lref_be, drop_fwd_rfw, or_introl/ ] #HnW
- @or_intror #H elim (frees_inv_lref_lt … H) // #Z #Y #X #_ #HLY -l
- lapply (drop_mono … HLY … HLK) -L #H destruct /2 width=1 by/
- | -x @or_intror #H elim (ylt_yle_false … Hji)
- lapply (frees_inv_lref_free … H ?) -l //
- ]
- ]
- ]
-| -IH /3 width=5 by frees_inv_gref, or_intror/
-| #a #I #W #U #Hx #l #i destruct
- elim (IH L W … l i) [1,3: /3 width=1 by frees_bind_sn, or_introl/ ] #HnW
- elim (IH (L.ⓑ{I}W) U … (⫯l) (i+1)) -IH [1,3: /3 width=1 by frees_bind_dx, or_introl/ ] #HnU
- @or_intror #H elim (frees_inv_bind … H) -H /2 width=1 by/
-| #I #W #U #Hx #l #i destruct
- elim (IH L W … l i) [1,3: /3 width=1 by frees_flat_sn, or_introl/ ] #HnW
- elim (IH L U … l i) -IH [1,3: /3 width=1 by frees_flat_dx, or_introl/ ] #HnU
- @or_intror #H elim (frees_inv_flat … H) -H /2 width=1 by/
-]
-qed-.
-
-lemma frees_S: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[yinj l]⦃U⦄ → ∀I,K,W. ⬇[l] L ≡ K.ⓑ{I}W →
- (K ⊢ ⫰(i-l) ϵ 𝐅*[0]⦃W⦄ → ⊥) → L ⊢ i ϵ 𝐅*[⫯l]⦃U⦄.
-#L #U #l #i #H elim (frees_inv … H) -H /3 width=2 by frees_eq/
-* #I #K #W #j #Hlj #Hji #HnU #HLK #HW #I0 #K0 #W0 #HLK0 #HnW0
-lapply (yle_inv_inj … Hlj) -Hlj #Hlj
-elim (le_to_or_lt_eq … Hlj) -Hlj
-[ -I0 -K0 -W0 /3 width=9 by frees_be, yle_inj/
-| -Hji -HnU #H destruct
- lapply (drop_mono … HLK0 … HLK) #H destruct -I
- elim HnW0 -L -U -HnW0 //
-]
-qed.
-
-(* Note: lemma 1250 *)
-lemma frees_bind_dx_O: ∀a,I,L,W,U,i. L.ⓑ{I}W ⊢ ⫯i ϵ 𝐅*[0]⦃U⦄ →
- L ⊢ i ϵ 𝐅*[0]⦃ⓑ{a,I}W.U⦄.
-#a #I #L #W #U #i #HU elim (frees_dec L W 0 i)
-/4 width=5 by frees_S, frees_bind_dx, frees_bind_sn/
-qed.
-
-(* Properties on relocation *************************************************)
-
-lemma frees_lift_ge: ∀K,T,l,i. K ⊢ i ϵ𝐅*[l]⦃T⦄ →
- ∀L,s,l0,m0. ⬇[s, l0, m0] L ≡ K →
- ∀U. ⬆[l0, m0] T ≡ U → l0 ≤ i →
- L ⊢ i+m0 ϵ 𝐅*[l]⦃U⦄.
-#K #T #l #i #H elim H -K -T -l -i
-[ #K #T #l #i #HnT #L #s #l0 #m0 #_ #U #HTU #Hl0i -K -s
- @frees_eq #X #HXU elim (lift_div_le … HTU … HXU) -U /2 width=2 by/
-| #I #K #K0 #T #V #l #i #j #Hlj #Hji #HnT #HK0 #HV #IHV #L #s #l0 #m0 #HLK #U #HTU #Hl0i
- elim (ylt_split j l0) #H0
- [ elim (drop_trans_lt … HLK … HK0) // -K #L0 #W #HL0 >yminus_SO2 #HLK0 #HVW
- @(frees_be … HL0) -HL0 -HV /3 width=3 by ylt_plus_dx2_trans/
- [ lapply (ylt_fwd_lt_O1 … H0) #H1
- #X #HXU <(ymax_pre_sn l0 1) in HTU; /2 width=1 by ylt_fwd_le_succ1/ #HTU
- <(ylt_inv_O1 l0) in H0; // -H1 #H0
- elim (lift_div_le … HXU … HTU ?) -U /2 width=2 by ylt_fwd_succ2/
- | >yplus_minus_comm_inj /2 width=1 by ylt_fwd_le/
- <yplus_pred1 /4 width=5 by monotonic_yle_minus_dx, yle_pred, ylt_to_minus/
- ]
- | lapply (drop_trans_ge … HLK … HK0 ?) // -K #HLK0
- lapply (drop_inv_gen … HLK0) >commutative_plus -HLK0 #HLK0
- @(frees_be … HLK0) -HLK0 -IHV
- /2 width=1 by monotonic_ylt_plus_dx, yle_plus_dx1_trans/
- [ #X <yplus_inj #HXU elim (lift_div_le … HTU … HXU) -U /2 width=2 by/
- | <yplus_minus_assoc_comm_inj //
- ]
- ]
-]
-qed.
-
-(* Inversion lemmas on relocation *******************************************)
-
-lemma frees_inv_lift_be: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ →
- ∀K,s,l0,m0. ⬇[s, l0, m0+1] L ≡ K →
- ∀T. ⬆[l0, m0+1] T ≡ U → l0 ≤ i → i ≤ l0 + m0 → ⊥.
-#L #U #l #i #H elim H -L -U -l -i
-[ #L #U #l #i #HnU #K #s #l0 #m0 #_ #T #HTU #Hl0i #Hilm0
- elim (lift_split … HTU i m0) -HTU /2 width=2 by/
-| #I #L #K0 #U #W #l #i #j #Hli #Hij #HnU #HLK0 #_ #IHW #K #s #l0 #m0 #HLK #T #HTU #Hl0i #Hilm0
- elim (ylt_split j l0) #H1
- [ elim (drop_conf_lt … HLK … HLK0) -L // #L0 #V #H #HKL0 #HVW
- @(IHW … HKL0 … HVW)
- [ /3 width=1 by monotonic_yle_minus_dx, yle_pred/
- | >yplus_pred1 /2 width=1 by ylt_to_minus/
- <yplus_minus_comm_inj /3 width=1 by monotonic_yle_minus_dx, yle_pred, ylt_fwd_le/
- ]
- | elim (lift_split … HTU j m0) -HTU /3 width=3 by ylt_yle_trans, ylt_fwd_le/
- ]
-]
-qed-.
-
-lemma frees_inv_lift_ge: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ →
- ∀K,s,l0,m0. ⬇[s, l0, m0] L ≡ K →
- ∀T. ⬆[l0, m0] T ≡ U → l0 + m0 ≤ i →
- K ⊢ i-m0 ϵ𝐅*[l-yinj m0]⦃T⦄.
-#L #U #l #i #H elim H -L -U -l -i
-[ #L #U #l #i #HnU #K #s #l0 #m0 #HLK #T #HTU #Hlm0i -L -s
- elim (yle_inv_plus_inj2 … Hlm0i) -Hlm0i #Hl0im0 #Hm0i @frees_eq #X #HXT -K
- elim (lift_trans_le … HXT … HTU) -T // >ymax_pre_sn /2 width=2 by/
-| #I #L #K0 #U #W #l #i #j #Hli #Hij #HnU #HLK0 #_ #IHW #K #s #l0 #m0 #HLK #T #HTU #Hlm0i
- elim (ylt_split j l0) #H1
- [ elim (drop_conf_lt … HLK … HLK0) -L // #L0 #V #H #HKL0 #HVW
- elim (yle_inv_plus_inj2 … Hlm0i) #H0 #Hm0i
- @(frees_be … H) -H
- [ /3 width=1 by yle_plus_dx1_trans, monotonic_yle_minus_dx/
- | /2 width=3 by ylt_yle_trans/
- | #X #HXT elim (lift_trans_ge … HXT … HTU) -T /2 width=2 by ylt_fwd_le_succ1/
- | lapply (IHW … HKL0 … HVW ?) // -I -K -K0 -L0 -V -W -T -U -s
- >yplus_pred1 /2 width=1 by ylt_to_minus/
- <yplus_minus_comm_inj /3 width=1 by monotonic_yle_minus_dx, yle_pred, ylt_fwd_le/
- ]
- | elim (ylt_split j (l0+m0)) #H2
- [ -L -I -W elim (yle_inv_inj2 … H1) -H1 #x #H1 #H destruct
- lapply (ylt_plus2_to_minus_inj1 … H2) /2 width=1 by yle_inj/ #H3
- lapply (ylt_fwd_lt_O1 … H3) -H3 #H3
- elim (lift_split … HTU j (m0-1)) -HTU /2 width=1 by yle_inj/
- [ >minus_minus_associative /2 width=1 by ylt_inv_inj/ <minus_n_n
- -H2 #X #_ #H elim (HnU … H)
- | <yminus_inj >yminus_SO2 >yplus_pred2 /2 width=1 by ylt_fwd_le_pred2/
- ]
- | lapply (drop_conf_ge … HLK … HLK0 ?) // -L #HK0
- elim ( yle_inv_plus_inj2 … H2) -H2 #H2 #Hm0j
- @(frees_be … HK0)
- [ /2 width=1 by monotonic_yle_minus_dx/
- | /2 width=1 by monotonic_ylt_minus_dx/
- | #X #HXT elim (lift_trans_le … HXT … HTU) -T //
- <yminus_inj >ymax_pre_sn /2 width=2 by/
- | <yminus_inj >yplus_minus_assoc_comm_inj //
- >ymax_pre_sn /3 width=5 by yle_trans, ylt_fwd_le/
- ]
- ]
- ]
-]
-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/drop_lreq.ma".
+include "basic_2/multiple/frees.ma".
+
+(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
+
+(* Properties on equivalence for local environments *************************)
+
+lemma lreq_frees_trans: ∀L2,U,l,i. L2 ⊢ i ϵ 𝐅*[l]⦃U⦄ →
+ ∀L1. L1 ⩬[l, ∞] L2 → L1 ⊢ i ϵ 𝐅*[l]⦃U⦄.
+#L2 #U #l #i #H elim H -L2 -U -l -i /3 width=2 by frees_eq/
+#I2 #L2 #K2 #U #W2 #l #i #j #Hlj #Hji #HnU #HLK2 #_ #IHW2 #L1 #HL12
+elim (lreq_drop_trans_be … HL12 … HLK2) -L2 // >yminus_Y_inj #K1 #HK12 #HLK1
+lapply (lreq_inv_O_Y … HK12) -HK12 #H destruct /3 width=9 by frees_be/
+qed-.
+
+lemma frees_lreq_conf: ∀L1,U,l,i. L1 ⊢ i ϵ 𝐅*[l]⦃U⦄ →
+ ∀L2. L1 ⩬[l, ∞] L2 → L2 ⊢ i ϵ 𝐅*[l]⦃U⦄.
+/3 width=3 by lreq_sym, lreq_frees_trans/ 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/drop_lreq.ma".
-include "basic_2/multiple/frees.ma".
-
-(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
-
-(* Properties on equivalence for local environments *************************)
-
-lemma lreq_frees_trans: ∀L2,U,l,i. L2 ⊢ i ϵ 𝐅*[l]⦃U⦄ →
- ∀L1. L1 ⩬[l, ∞] L2 → L1 ⊢ i ϵ 𝐅*[l]⦃U⦄.
-#L2 #U #l #i #H elim H -L2 -U -l -i /3 width=2 by frees_eq/
-#I2 #L2 #K2 #U #W2 #l #i #j #Hlj #Hji #HnU #HLK2 #_ #IHW2 #L1 #HL12
-elim (lreq_drop_trans_be … HL12 … HLK2) -L2 // >yminus_Y_inj #K1 #HK12 #HLK1
-lapply (lreq_inv_O_Y … HK12) -HK12 #H destruct /3 width=9 by frees_be/
-qed-.
-
-lemma frees_lreq_conf: ∀L1,U,l,i. L1 ⊢ i ϵ 𝐅*[l]⦃U⦄ →
- ∀L2. L1 ⩬[l, ∞] L2 → L2 ⊢ i ϵ 𝐅*[l]⦃U⦄.
-/3 width=3 by lreq_sym, lreq_frees_trans/ 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 "ground_2/ynat/ynat_lt.ma".
+include "basic_2/notation/relations/midiso_4.ma".
+include "basic_2/grammar/lenv_length.ma".
+
+(* EQUIVALENCE FOR LOCAL ENVIRONMENTS ***************************************)
+
+inductive lreq: relation4 ynat ynat lenv lenv ≝
+| lreq_atom: ∀l,m. lreq l m (⋆) (⋆)
+| lreq_zero: ∀I1,I2,L1,L2,V1,V2.
+ lreq 0 0 L1 L2 → lreq 0 0 (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2)
+| lreq_pair: ∀I,L1,L2,V,m. lreq 0 m L1 L2 →
+ lreq 0 (⫯m) (L1.ⓑ{I}V) (L2.ⓑ{I}V)
+| lreq_succ: ∀I1,I2,L1,L2,V1,V2,l,m.
+ lreq l m L1 L2 → lreq (⫯l) m (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2)
+.
+
+interpretation
+ "equivalence (local environment)"
+ 'MidIso l m L1 L2 = (lreq l m L1 L2).
+
+(* Basic properties *********************************************************)
+
+lemma lreq_pair_lt: ∀I,L1,L2,V,m. L1 ⩬[0, ⫰m] L2 → 0 < m →
+ L1.ⓑ{I}V ⩬[0, m] L2.ⓑ{I}V.
+#I #L1 #L2 #V #m #HL12 #Hm <(ylt_inv_O1 … Hm) /2 width=1 by lreq_pair/
+qed.
+
+lemma lreq_succ_lt: ∀I1,I2,L1,L2,V1,V2,l,m. L1 ⩬[⫰l, m] L2 → 0 < l →
+ L1.ⓑ{I1}V1 ⩬[l, m] L2. ⓑ{I2}V2.
+#I1 #I2 #L1 #L2 #V1 #V2 #l #m #HL12 #Hl <(ylt_inv_O1 … Hl) /2 width=1 by lreq_succ/
+qed.
+
+lemma lreq_pair_O_Y: ∀L1,L2. L1 ⩬[0, ∞] L2 →
+ ∀I,V. L1.ⓑ{I}V ⩬[0, ∞] L2.ⓑ{I}V.
+#L1 #L2 #HL12 #I #V lapply (lreq_pair I … V … HL12) -HL12 //
+qed.
+
+lemma lreq_refl: ∀L,l,m. L ⩬[l, m] L.
+#L elim L -L //
+#L #I #V #IHL #l elim (ynat_cases … l) [| * #x ]
+#Hl destruct /2 width=1 by lreq_succ/
+#m elim (ynat_cases … m) [| * #x ]
+#Hm destruct /2 width=1 by lreq_zero, lreq_pair/
+qed.
+
+lemma lreq_O2: ∀L1,L2,l. |L1| = |L2| → L1 ⩬[l, 0] L2.
+#L1 elim L1 -L1 [| #L1 #I1 #V1 #IHL1 ]
+* // [1,3: #L2 #I2 #V2 ] #l
+[ #H elim (ysucc_inv_O_sn … H)
+| >length_pair >length_pair #H
+ lapply (ysucc_inv_inj … H) -H #HL12
+ elim (ynat_cases l) /3 width=1 by lreq_zero/
+ * /3 width=1 by lreq_succ/
+| #H elim (ysucc_inv_O_dx … H)
+]
+qed.
+
+lemma lreq_sym: ∀l,m. symmetric … (lreq l m).
+#l #m #L1 #L2 #H elim H -L1 -L2 -l -m
+/2 width=1 by lreq_zero, lreq_pair, lreq_succ/
+qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lreq_inv_atom1_aux: ∀L1,L2,l,m. L1 ⩬[l, m] L2 → L1 = ⋆ → L2 = ⋆.
+#L1 #L2 #l #m * -L1 -L2 -l -m //
+[ #I1 #I2 #L1 #L2 #V1 #V2 #_ #H destruct
+| #I #L1 #L2 #V #m #_ #H destruct
+| #I1 #I2 #L1 #L2 #V1 #V2 #l #m #_ #H destruct
+]
+qed-.
+
+lemma lreq_inv_atom1: ∀L2,l,m. ⋆ ⩬[l, m] L2 → L2 = ⋆.
+/2 width=5 by lreq_inv_atom1_aux/ qed-.
+
+fact lreq_inv_zero1_aux: ∀L1,L2,l,m. L1 ⩬[l, m] L2 →
+ ∀J1,K1,W1. L1 = K1.ⓑ{J1}W1 → l = 0 → m = 0 →
+ ∃∃J2,K2,W2. K1 ⩬[0, 0] K2 & L2 = K2.ⓑ{J2}W2.
+#L1 #L2 #l #m * -L1 -L2 -l -m
+[ #l #m #J1 #K1 #W1 #H destruct
+| #I1 #I2 #L1 #L2 #V1 #V2 #HL12 #J1 #K1 #W1 #H #_ #_ destruct
+ /2 width=5 by ex2_3_intro/
+| #I #L1 #L2 #V #m #_ #J1 #K1 #W1 #_ #_ #H
+ elim (ysucc_inv_O_dx … H)
+| #I1 #I2 #L1 #L2 #V1 #V2 #l #m #_ #J1 #K1 #W1 #_ #H
+ elim (ysucc_inv_O_dx … H)
+]
+qed-.
+
+lemma lreq_inv_zero1: ∀I1,K1,L2,V1. K1.ⓑ{I1}V1 ⩬[0, 0] L2 →
+ ∃∃I2,K2,V2. K1 ⩬[0, 0] K2 & L2 = K2.ⓑ{I2}V2.
+/2 width=9 by lreq_inv_zero1_aux/ qed-.
+
+fact lreq_inv_pair1_aux: ∀L1,L2,l,m. L1 ⩬[l, m] L2 →
+ ∀J,K1,W. L1 = K1.ⓑ{J}W → l = 0 → 0 < m →
+ ∃∃K2. K1 ⩬[0, ⫰m] K2 & L2 = K2.ⓑ{J}W.
+#L1 #L2 #l #m * -L1 -L2 -l -m
+[ #l #m #J #K1 #W #H destruct
+| #I1 #I2 #L1 #L2 #V1 #V2 #_ #J #K1 #W #_ #_ #H
+ elim (ylt_yle_false … H) //
+| #I #L1 #L2 #V #m #HL12 #J #K1 #W #H #_ #_ destruct
+ /2 width=3 by ex2_intro/
+| #I1 #I2 #L1 #L2 #V1 #V2 #l #m #_ #J #K1 #W #_ #H
+ elim (ysucc_inv_O_dx … H)
+]
+qed-.
+
+lemma lreq_inv_pair1: ∀I,K1,L2,V,m. K1.ⓑ{I}V ⩬[0, m] L2 → 0 < m →
+ ∃∃K2. K1 ⩬[0, ⫰m] K2 & L2 = K2.ⓑ{I}V.
+/2 width=6 by lreq_inv_pair1_aux/ qed-.
+
+lemma lreq_inv_pair: ∀I1,I2,L1,L2,V1,V2,m. L1.ⓑ{I1}V1 ⩬[0, m] L2.ⓑ{I2}V2 → 0 < m →
+ ∧∧ L1 ⩬[0, ⫰m] L2 & I1 = I2 & V1 = V2.
+#I1 #I2 #L1 #L2 #V1 #V2 #m #H #Hm elim (lreq_inv_pair1 … H) -H //
+#Y #HL12 #H destruct /2 width=1 by and3_intro/
+qed-.
+
+fact lreq_inv_succ1_aux: ∀L1,L2,l,m. L1 ⩬[l, m] L2 →
+ ∀J1,K1,W1. L1 = K1.ⓑ{J1}W1 → 0 < l →
+ ∃∃J2,K2,W2. K1 ⩬[⫰l, m] K2 & L2 = K2.ⓑ{J2}W2.
+#L1 #L2 #l #m * -L1 -L2 -l -m
+[ #l #m #J1 #K1 #W1 #H destruct
+| #I1 #I2 #L1 #L2 #V1 #V2 #_ #J1 #K1 #W1 #_ #H
+ elim (ylt_yle_false … H) //
+| #I #L1 #L2 #V #m #_ #J1 #K1 #W1 #_ #H
+ elim (ylt_yle_false … H) //
+| #I1 #I2 #L1 #L2 #V1 #V2 #l #m #HL12 #J1 #K1 #W1 #H #_ destruct
+ /2 width=5 by ex2_3_intro/
+]
+qed-.
+
+lemma lreq_inv_succ1: ∀I1,K1,L2,V1,l,m. K1.ⓑ{I1}V1 ⩬[l, m] L2 → 0 < l →
+ ∃∃I2,K2,V2. K1 ⩬[⫰l, m] K2 & L2 = K2.ⓑ{I2}V2.
+/2 width=5 by lreq_inv_succ1_aux/ qed-.
+
+lemma lreq_inv_atom2: ∀L1,l,m. L1 ⩬[l, m] ⋆ → L1 = ⋆.
+/3 width=3 by lreq_inv_atom1, lreq_sym/
+qed-.
+
+lemma lreq_inv_succ: ∀I1,I2,L1,L2,V1,V2,l,m. L1.ⓑ{I1}V1 ⩬[l, m] L2.ⓑ{I2}V2 → 0 < l →
+ L1 ⩬[⫰l, m] L2.
+#I1 #I2 #L1 #L2 #V1 #V2 #l #m #H #Hl elim (lreq_inv_succ1 … H) -H //
+#Z #Y #X #HL12 #H destruct //
+qed-.
+
+lemma lreq_inv_zero2: ∀I2,K2,L1,V2. L1 ⩬[0, 0] K2.ⓑ{I2}V2 →
+ ∃∃I1,K1,V1. K1 ⩬[0, 0] K2 & L1 = K1.ⓑ{I1}V1.
+#I2 #K2 #L1 #V2 #H elim (lreq_inv_zero1 … (lreq_sym … H)) -H
+/3 width=5 by lreq_sym, ex2_3_intro/
+qed-.
+
+lemma lreq_inv_pair2: ∀I,K2,L1,V,m. L1 ⩬[0, m] K2.ⓑ{I}V → 0 < m →
+ ∃∃K1. K1 ⩬[0, ⫰m] K2 & L1 = K1.ⓑ{I}V.
+#I #K2 #L1 #V #m #H #Hm elim (lreq_inv_pair1 … (lreq_sym … H)) -H
+/3 width=3 by lreq_sym, ex2_intro/
+qed-.
+
+lemma lreq_inv_succ2: ∀I2,K2,L1,V2,l,m. L1 ⩬[l, m] K2.ⓑ{I2}V2 → 0 < l →
+ ∃∃I1,K1,V1. K1 ⩬[⫰l, m] K2 & L1 = K1.ⓑ{I1}V1.
+#I2 #K2 #L1 #V2 #l #m #H #Hl elim (lreq_inv_succ1 … (lreq_sym … H)) -H
+/3 width=5 by lreq_sym, ex2_3_intro/
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lreq_fwd_length: ∀L1,L2,l,m. L1 ⩬[l, m] L2 → |L1| = |L2|.
+#L1 #L2 #l #m #H elim H -L1 -L2 -l -m //
+qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+fact lreq_inv_O_Y_aux: ∀L1,L2,l,m. L1 ⩬[l, m] L2 → l = 0 → m = ∞ → L1 = L2.
+#L1 #L2 #l #m #H elim H -L1 -L2 -l -m //
+[ #I1 #I2 #L1 #L2 #V1 #V2 #_ #_ #_ #H destruct
+| /4 width=1 by eq_f3, ysucc_inv_Y_dx/
+| #I1 #I2 #L1 #L2 #V1 #V2 #l #m #_ #_ #H elim (ysucc_inv_O_dx … H)
+]
+qed-.
+
+lemma lreq_inv_O_Y: ∀L1,L2. L1 ⩬[0, ∞] L2 → L1 = L2.
+/2 width=5 by lreq_inv_O_Y_aux/ 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 "ground_2/ynat/ynat_plus.ma".
+include "basic_2/grammar/lreq.ma".
+
+(* EQUIVALENCE FOR LOCAL ENVIRONMENTS ***************************************)
+
+(* Main properties **********************************************************)
+
+theorem lreq_trans: ∀l,m. Transitive … (lreq l m).
+#l #m #L1 #L2 #H elim H -L1 -L2 -l -m
+[ #l #m #X #H lapply (lreq_inv_atom1 … H) -H
+ #H destruct //
+| #I1 #I #L1 #L #V1 #V #_ #IHL1 #X #H elim (lreq_inv_zero1 … H) -H
+ #I2 #L2 #V2 #HL2 #H destruct /3 width=1 by lreq_zero/
+| #I #L1 #L #V #m #_ #IHL1 #X #H elim (lreq_inv_pair1 … H) -H //
+ #L2 #HL2 #H destruct /3 width=1 by lreq_pair/
+| #I1 #I #L1 #L #V1 #V #l #m #_ #IHL1 #X #H elim (lreq_inv_succ1 … H) -H //
+ #I2 #L2 #V2 #HL2 #H destruct /3 width=1 by lreq_succ/
+]
+qed-.
+
+theorem lreq_canc_sn: ∀l,m,L,L1,L2. L ⩬[l, m] L1 → L ⩬[l, m] L2 → L1 ⩬[l, m] L2.
+/3 width=3 by lreq_trans, lreq_sym/ qed-.
+
+theorem lreq_canc_dx: ∀l,m,L,L1,L2. L1 ⩬[l, m] L → L2 ⩬[l, m] L → L1 ⩬[l, m] L2.
+/3 width=3 by lreq_trans, lreq_sym/ qed-.
+
+theorem lreq_join: ∀L1,L2,l,i. L1 ⩬[l, i] L2 →
+ ∀m. L1 ⩬[i+l, m] L2 → L1 ⩬[l, i+m] L2.
+#L1 #L2 #l #i #H elim H -L1 -L2 -l -i //
+[ #I #L1 #L2 #V #m #_ #IHL12 #m #H
+ lapply (lreq_inv_succ … H ?) -H // >ypred_succ /3 width=1 by lreq_pair/
+| #I1 #I2 #L1 #L2 #V1 #V2 #l #m #_ #IHL12 #m #H
+ lapply (lreq_inv_succ … H ?) -H // >yplus_succ2 >ypred_succ /3 width=1 by lreq_succ/
+]
+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 "ground_2/ynat/ynat_lt.ma".
-include "basic_2/notation/relations/midiso_4.ma".
-include "basic_2/grammar/lenv_length.ma".
-
-(* EQUIVALENCE FOR LOCAL ENVIRONMENTS ***************************************)
-
-inductive lreq: relation4 ynat ynat lenv lenv ≝
-| lreq_atom: ∀l,m. lreq l m (⋆) (⋆)
-| lreq_zero: ∀I1,I2,L1,L2,V1,V2.
- lreq 0 0 L1 L2 → lreq 0 0 (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2)
-| lreq_pair: ∀I,L1,L2,V,m. lreq 0 m L1 L2 →
- lreq 0 (⫯m) (L1.ⓑ{I}V) (L2.ⓑ{I}V)
-| lreq_succ: ∀I1,I2,L1,L2,V1,V2,l,m.
- lreq l m L1 L2 → lreq (⫯l) m (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2)
-.
-
-interpretation
- "equivalence (local environment)"
- 'MidIso l m L1 L2 = (lreq l m L1 L2).
-
-(* Basic properties *********************************************************)
-
-lemma lreq_pair_lt: ∀I,L1,L2,V,m. L1 ⩬[0, ⫰m] L2 → 0 < m →
- L1.ⓑ{I}V ⩬[0, m] L2.ⓑ{I}V.
-#I #L1 #L2 #V #m #HL12 #Hm <(ylt_inv_O1 … Hm) /2 width=1 by lreq_pair/
-qed.
-
-lemma lreq_succ_lt: ∀I1,I2,L1,L2,V1,V2,l,m. L1 ⩬[⫰l, m] L2 → 0 < l →
- L1.ⓑ{I1}V1 ⩬[l, m] L2. ⓑ{I2}V2.
-#I1 #I2 #L1 #L2 #V1 #V2 #l #m #HL12 #Hl <(ylt_inv_O1 … Hl) /2 width=1 by lreq_succ/
-qed.
-
-lemma lreq_pair_O_Y: ∀L1,L2. L1 ⩬[0, ∞] L2 →
- ∀I,V. L1.ⓑ{I}V ⩬[0, ∞] L2.ⓑ{I}V.
-#L1 #L2 #HL12 #I #V lapply (lreq_pair I … V … HL12) -HL12 //
-qed.
-
-lemma lreq_refl: ∀L,l,m. L ⩬[l, m] L.
-#L elim L -L //
-#L #I #V #IHL #l elim (ynat_cases … l) [| * #x ]
-#Hl destruct /2 width=1 by lreq_succ/
-#m elim (ynat_cases … m) [| * #x ]
-#Hm destruct /2 width=1 by lreq_zero, lreq_pair/
-qed.
-
-lemma lreq_O2: ∀L1,L2,l. |L1| = |L2| → L1 ⩬[l, 0] L2.
-#L1 elim L1 -L1 [| #L1 #I1 #V1 #IHL1 ]
-* // [1,3: #L2 #I2 #V2 ] #l
-[ #H elim (ysucc_inv_O_sn … H)
-| >length_pair >length_pair #H
- lapply (ysucc_inv_inj … H) -H #HL12
- elim (ynat_cases l) /3 width=1 by lreq_zero/
- * /3 width=1 by lreq_succ/
-| #H elim (ysucc_inv_O_dx … H)
-]
-qed.
-
-lemma lreq_sym: ∀l,m. symmetric … (lreq l m).
-#l #m #L1 #L2 #H elim H -L1 -L2 -l -m
-/2 width=1 by lreq_zero, lreq_pair, lreq_succ/
-qed-.
-
-(* Basic inversion lemmas ***************************************************)
-
-fact lreq_inv_atom1_aux: ∀L1,L2,l,m. L1 ⩬[l, m] L2 → L1 = ⋆ → L2 = ⋆.
-#L1 #L2 #l #m * -L1 -L2 -l -m //
-[ #I1 #I2 #L1 #L2 #V1 #V2 #_ #H destruct
-| #I #L1 #L2 #V #m #_ #H destruct
-| #I1 #I2 #L1 #L2 #V1 #V2 #l #m #_ #H destruct
-]
-qed-.
-
-lemma lreq_inv_atom1: ∀L2,l,m. ⋆ ⩬[l, m] L2 → L2 = ⋆.
-/2 width=5 by lreq_inv_atom1_aux/ qed-.
-
-fact lreq_inv_zero1_aux: ∀L1,L2,l,m. L1 ⩬[l, m] L2 →
- ∀J1,K1,W1. L1 = K1.ⓑ{J1}W1 → l = 0 → m = 0 →
- ∃∃J2,K2,W2. K1 ⩬[0, 0] K2 & L2 = K2.ⓑ{J2}W2.
-#L1 #L2 #l #m * -L1 -L2 -l -m
-[ #l #m #J1 #K1 #W1 #H destruct
-| #I1 #I2 #L1 #L2 #V1 #V2 #HL12 #J1 #K1 #W1 #H #_ #_ destruct
- /2 width=5 by ex2_3_intro/
-| #I #L1 #L2 #V #m #_ #J1 #K1 #W1 #_ #_ #H
- elim (ysucc_inv_O_dx … H)
-| #I1 #I2 #L1 #L2 #V1 #V2 #l #m #_ #J1 #K1 #W1 #_ #H
- elim (ysucc_inv_O_dx … H)
-]
-qed-.
-
-lemma lreq_inv_zero1: ∀I1,K1,L2,V1. K1.ⓑ{I1}V1 ⩬[0, 0] L2 →
- ∃∃I2,K2,V2. K1 ⩬[0, 0] K2 & L2 = K2.ⓑ{I2}V2.
-/2 width=9 by lreq_inv_zero1_aux/ qed-.
-
-fact lreq_inv_pair1_aux: ∀L1,L2,l,m. L1 ⩬[l, m] L2 →
- ∀J,K1,W. L1 = K1.ⓑ{J}W → l = 0 → 0 < m →
- ∃∃K2. K1 ⩬[0, ⫰m] K2 & L2 = K2.ⓑ{J}W.
-#L1 #L2 #l #m * -L1 -L2 -l -m
-[ #l #m #J #K1 #W #H destruct
-| #I1 #I2 #L1 #L2 #V1 #V2 #_ #J #K1 #W #_ #_ #H
- elim (ylt_yle_false … H) //
-| #I #L1 #L2 #V #m #HL12 #J #K1 #W #H #_ #_ destruct
- /2 width=3 by ex2_intro/
-| #I1 #I2 #L1 #L2 #V1 #V2 #l #m #_ #J #K1 #W #_ #H
- elim (ysucc_inv_O_dx … H)
-]
-qed-.
-
-lemma lreq_inv_pair1: ∀I,K1,L2,V,m. K1.ⓑ{I}V ⩬[0, m] L2 → 0 < m →
- ∃∃K2. K1 ⩬[0, ⫰m] K2 & L2 = K2.ⓑ{I}V.
-/2 width=6 by lreq_inv_pair1_aux/ qed-.
-
-lemma lreq_inv_pair: ∀I1,I2,L1,L2,V1,V2,m. L1.ⓑ{I1}V1 ⩬[0, m] L2.ⓑ{I2}V2 → 0 < m →
- ∧∧ L1 ⩬[0, ⫰m] L2 & I1 = I2 & V1 = V2.
-#I1 #I2 #L1 #L2 #V1 #V2 #m #H #Hm elim (lreq_inv_pair1 … H) -H //
-#Y #HL12 #H destruct /2 width=1 by and3_intro/
-qed-.
-
-fact lreq_inv_succ1_aux: ∀L1,L2,l,m. L1 ⩬[l, m] L2 →
- ∀J1,K1,W1. L1 = K1.ⓑ{J1}W1 → 0 < l →
- ∃∃J2,K2,W2. K1 ⩬[⫰l, m] K2 & L2 = K2.ⓑ{J2}W2.
-#L1 #L2 #l #m * -L1 -L2 -l -m
-[ #l #m #J1 #K1 #W1 #H destruct
-| #I1 #I2 #L1 #L2 #V1 #V2 #_ #J1 #K1 #W1 #_ #H
- elim (ylt_yle_false … H) //
-| #I #L1 #L2 #V #m #_ #J1 #K1 #W1 #_ #H
- elim (ylt_yle_false … H) //
-| #I1 #I2 #L1 #L2 #V1 #V2 #l #m #HL12 #J1 #K1 #W1 #H #_ destruct
- /2 width=5 by ex2_3_intro/
-]
-qed-.
-
-lemma lreq_inv_succ1: ∀I1,K1,L2,V1,l,m. K1.ⓑ{I1}V1 ⩬[l, m] L2 → 0 < l →
- ∃∃I2,K2,V2. K1 ⩬[⫰l, m] K2 & L2 = K2.ⓑ{I2}V2.
-/2 width=5 by lreq_inv_succ1_aux/ qed-.
-
-lemma lreq_inv_atom2: ∀L1,l,m. L1 ⩬[l, m] ⋆ → L1 = ⋆.
-/3 width=3 by lreq_inv_atom1, lreq_sym/
-qed-.
-
-lemma lreq_inv_succ: ∀I1,I2,L1,L2,V1,V2,l,m. L1.ⓑ{I1}V1 ⩬[l, m] L2.ⓑ{I2}V2 → 0 < l →
- L1 ⩬[⫰l, m] L2.
-#I1 #I2 #L1 #L2 #V1 #V2 #l #m #H #Hl elim (lreq_inv_succ1 … H) -H //
-#Z #Y #X #HL12 #H destruct //
-qed-.
-
-lemma lreq_inv_zero2: ∀I2,K2,L1,V2. L1 ⩬[0, 0] K2.ⓑ{I2}V2 →
- ∃∃I1,K1,V1. K1 ⩬[0, 0] K2 & L1 = K1.ⓑ{I1}V1.
-#I2 #K2 #L1 #V2 #H elim (lreq_inv_zero1 … (lreq_sym … H)) -H
-/3 width=5 by lreq_sym, ex2_3_intro/
-qed-.
-
-lemma lreq_inv_pair2: ∀I,K2,L1,V,m. L1 ⩬[0, m] K2.ⓑ{I}V → 0 < m →
- ∃∃K1. K1 ⩬[0, ⫰m] K2 & L1 = K1.ⓑ{I}V.
-#I #K2 #L1 #V #m #H #Hm elim (lreq_inv_pair1 … (lreq_sym … H)) -H
-/3 width=3 by lreq_sym, ex2_intro/
-qed-.
-
-lemma lreq_inv_succ2: ∀I2,K2,L1,V2,l,m. L1 ⩬[l, m] K2.ⓑ{I2}V2 → 0 < l →
- ∃∃I1,K1,V1. K1 ⩬[⫰l, m] K2 & L1 = K1.ⓑ{I1}V1.
-#I2 #K2 #L1 #V2 #l #m #H #Hl elim (lreq_inv_succ1 … (lreq_sym … H)) -H
-/3 width=5 by lreq_sym, ex2_3_intro/
-qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma lreq_fwd_length: ∀L1,L2,l,m. L1 ⩬[l, m] L2 → |L1| = |L2|.
-#L1 #L2 #l #m #H elim H -L1 -L2 -l -m //
-qed-.
-
-(* Advanced inversion lemmas ************************************************)
-
-fact lreq_inv_O_Y_aux: ∀L1,L2,l,m. L1 ⩬[l, m] L2 → l = 0 → m = ∞ → L1 = L2.
-#L1 #L2 #l #m #H elim H -L1 -L2 -l -m //
-[ #I1 #I2 #L1 #L2 #V1 #V2 #_ #_ #_ #H destruct
-| /4 width=1 by eq_f3, ysucc_inv_Y_dx/
-| #I1 #I2 #L1 #L2 #V1 #V2 #l #m #_ #_ #H elim (ysucc_inv_O_dx … H)
-]
-qed-.
-
-lemma lreq_inv_O_Y: ∀L1,L2. L1 ⩬[0, ∞] L2 → L1 = L2.
-/2 width=5 by lreq_inv_O_Y_aux/ 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 "ground_2/ynat/ynat_plus.ma".
-include "basic_2/grammar/lreq.ma".
-
-(* EQUIVALENCE FOR LOCAL ENVIRONMENTS ***************************************)
-
-(* Main properties **********************************************************)
-
-theorem lreq_trans: ∀l,m. Transitive … (lreq l m).
-#l #m #L1 #L2 #H elim H -L1 -L2 -l -m
-[ #l #m #X #H lapply (lreq_inv_atom1 … H) -H
- #H destruct //
-| #I1 #I #L1 #L #V1 #V #_ #IHL1 #X #H elim (lreq_inv_zero1 … H) -H
- #I2 #L2 #V2 #HL2 #H destruct /3 width=1 by lreq_zero/
-| #I #L1 #L #V #m #_ #IHL1 #X #H elim (lreq_inv_pair1 … H) -H //
- #L2 #HL2 #H destruct /3 width=1 by lreq_pair/
-| #I1 #I #L1 #L #V1 #V #l #m #_ #IHL1 #X #H elim (lreq_inv_succ1 … H) -H //
- #I2 #L2 #V2 #HL2 #H destruct /3 width=1 by lreq_succ/
-]
-qed-.
-
-theorem lreq_canc_sn: ∀l,m,L,L1,L2. L ⩬[l, m] L1 → L ⩬[l, m] L2 → L1 ⩬[l, m] L2.
-/3 width=3 by lreq_trans, lreq_sym/ qed-.
-
-theorem lreq_canc_dx: ∀l,m,L,L1,L2. L1 ⩬[l, m] L → L2 ⩬[l, m] L → L1 ⩬[l, m] L2.
-/3 width=3 by lreq_trans, lreq_sym/ qed-.
-
-theorem lreq_join: ∀L1,L2,l,i. L1 ⩬[l, i] L2 →
- ∀m. L1 ⩬[i+l, m] L2 → L1 ⩬[l, i+m] L2.
-#L1 #L2 #l #i #H elim H -L1 -L2 -l -i //
-[ #I #L1 #L2 #V #m #_ #IHL12 #m #H
- lapply (lreq_inv_succ … H ?) -H // >ypred_succ /3 width=1 by lreq_pair/
-| #I1 #I2 #L1 #L2 #V1 #V2 #l #m #_ #IHL12 #m #H
- lapply (lreq_inv_succ … H ?) -H // >yplus_succ2 >ypred_succ /3 width=1 by lreq_succ/
-]
-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 "ground_2/lib/list.ma".
+
+(* MULTIPLE RELOCATION WITH PAIRS *******************************************)
+
+definition mr2: Type[0] ≝ list2 nat nat.
projects / helm.git / commitdiff