basic_2: simplified formalization starts: partial commit of the grammar component
--- /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 "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 "ground_2/notation/functions/append_2.ma".
+include "ground_2/ynat/ynat_plus.ma".
+include "basic_2/notation/functions/snbind2_3.ma".
+include "basic_2/notation/functions/snabbr_2.ma".
+include "basic_2/notation/functions/snabst_2.ma".
+include "basic_2/grammar/lenv_length.ma".
+
+(* LOCAL ENVIRONMENTS *******************************************************)
+
+let rec append L K on K ≝ match K with
+[ LAtom ⇒ L
+| LPair K I V ⇒ (append L K). ⓑ{I} V
+].
+
+interpretation "append (local environment)" 'Append L1 L2 = (append L1 L2).
+
+interpretation "local environment tail binding construction (binary)"
+ 'SnBind2 I T L = (append (LPair LAtom I T) L).
+
+interpretation "tail abbreviation (local environment)"
+ 'SnAbbr T L = (append (LPair LAtom Abbr T) L).
+
+interpretation "tail abstraction (local environment)"
+ 'SnAbst L T = (append (LPair LAtom Abst T) L).
+
+definition d_appendable_sn: predicate (lenv→relation term) ≝ λR.
+ ∀K,T1,T2. R K T1 T2 → ∀L. R (L @@ K) T1 T2.
+
+(* Basic properties *********************************************************)
+
+lemma append_atom: ∀L. L @@ ⋆ = L.
+// qed.
+
+lemma append_pair: ∀I,L,K,V. L @@ (K.ⓑ{I}V) = (L @@ K).ⓑ{I}V.
+// qed.
+
+lemma append_atom_sn: ∀L. ⋆ @@ L = L.
+#L elim L -L //
+#L #I #V >append_pair //
+qed.
+
+lemma append_assoc: associative … append.
+#L1 #L2 #L3 elim L3 -L3 //
+qed.
+
+lemma append_length: ∀L1,L2. |L1 @@ L2| = |L1| + |L2|.
+#L1 #L2 elim L2 -L2 //
+#L2 #I #V2 >append_pair >length_pair >length_pair //
+qed.
+
+lemma ltail_length: ∀I,L,V. |ⓑ{I}V.L| = ⫯|L|.
+#I #L #V >append_length //
+qed.
+
+(* Basic_1: was just: chead_ctail *)
+lemma lpair_ltail: ∀L,I,V. ∃∃J,K,W. L.ⓑ{I}V = ⓑ{J}W.K & |L| = |K|.
+#L elim L -L /2 width=5 by ex2_3_intro/
+#L #Z #X #IHL #I #V elim (IHL Z X) -IHL
+#J #K #W #H #_ >H -H >ltail_length
+@(ex2_3_intro … J (K.ⓑ{I}V) W) //
+qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma append_inj_sn: ∀K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 → |K1| = |K2| →
+ L1 = L2 ∧ K1 = K2.
+#K1 elim K1 -K1
+[ * /2 width=1 by conj/
+ #K2 #I2 #V2 #L1 #L2 #_ >length_atom >length_pair
+ #H elim (ysucc_inv_O_sn … H)
+| #K1 #I1 #V1 #IH *
+ [ #L1 #L2 #_ >length_atom >length_pair
+ #H elim (ysucc_inv_O_dx … H)
+ | #K2 #I2 #V2 #L1 #L2 #H1 #H2
+ elim (destruct_lpair_lpair_aux … H1) -H1 #H1 #H3 #H4 destruct (**) (* destruct lemma needed *)
+ elim (IH … H1) -IH -H1 /3 width=1 by ysucc_inv_inj, conj/
+ ]
+]
+qed-.
+
+(* Note: lemma 750 *)
+lemma append_inj_dx: ∀K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 → |L1| = |L2| →
+ L1 = L2 ∧ K1 = K2.
+#K1 elim K1 -K1
+[ * /2 width=1 by conj/
+ #K2 #I2 #V2 #L1 #L2 >append_atom >append_pair #H destruct
+ >length_pair >append_length <yplus_succ2 #H
+ elim (discr_yplus_xy_x … H) -H #H
+ [ elim (ylt_yle_false (|L2|) (∞)) // | elim (ysucc_inv_O_dx … H) ]
+| #K1 #I1 #V1 #IH *
+ [ #L1 #L2 >append_pair >append_atom #H destruct
+ >length_pair >append_length <yplus_succ2 #H
+ elim (discr_yplus_x_xy … H) -H #H
+ [ elim (ylt_yle_false (|L1|) (∞)) // | elim (ysucc_inv_O_dx … H) ]
+ | #K2 #I2 #V2 #L1 #L2 >append_pair >append_pair #H1 #H2
+ elim (destruct_lpair_lpair_aux … H1) -H1 #H1 #H3 #H4 destruct (**) (* destruct lemma needed *)
+ elim (IH … H1) -IH -H1 /2 width=1 by conj/
+ ]
+]
+qed-.
+
+lemma append_inv_refl_dx: ∀L,K. L @@ K = L → K = ⋆.
+#L #K #H elim (append_inj_dx … (⋆) … H) //
+qed-.
+
+lemma append_inv_pair_dx: ∀I,L,K,V. L @@ K = L.ⓑ{I}V → K = ⋆.ⓑ{I}V.
+#I #L #K #V #H elim (append_inj_dx … (⋆.ⓑ{I}V) … H) //
+qed-.
+
+lemma length_inv_pos_dx_ltail: ∀L,l. |L| = ⫯l →
+ ∃∃I,K,V. |K| = l & L = ⓑ{I}V.K.
+#Y #l #H elim (length_inv_pos_dx … H) -H #I #L #V #Hl #HLK destruct
+elim (lpair_ltail L I V) /2 width=5 by ex2_3_intro/
+qed-.
+
+lemma length_inv_pos_sn_ltail: ∀L,l. ⫯l = |L| →
+ ∃∃I,K,V. l = |K| & L = ⓑ{I}V.K.
+#Y #l #H elim (length_inv_pos_sn … H) -H #I #L #V #Hl #HLK destruct
+elim (lpair_ltail L I V) /2 width=5 by ex2_3_intro/
+qed-.
+
+(* Basic eliminators ********************************************************)
+
+(* Basic_1: was: c_tail_ind *)
+lemma lenv_ind_alt: ∀R:predicate lenv.
+ R (⋆) → (∀I,L,T. R L → R (ⓑ{I}T.L)) →
+ ∀L. R L.
+#R #IH1 #IH2 #L @(ynat_f_ind … length … L) -L #x #IHx * // -IH1
+#L #I #V #H destruct elim (lpair_ltail L I V)
+/4 width=1 by monotonic_ylt_plus_sn/
+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/grammar/lenv.ma".
+
+(* LENGTH OF A LOCAL ENVIRONMENT ********************************************)
+
+let rec length L ≝ match L with
+[ LAtom ⇒ 0
+| LPair L _ _ ⇒ ⫯(length L)
+].
+
+interpretation "length (local environment)" 'card L = (length L).
+
+(* Basic properties *********************************************************)
+
+lemma length_atom: |⋆| = 0.
+// qed.
+
+lemma length_pair: ∀I,L,V. |L.ⓑ{I}V| = ⫯|L|.
+// qed.
+
+lemma length_inj: ∀L. |L| < ∞.
+#L elim L -L /2 width=1 by ylt_succ_Y/
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma length_inv_zero_dx: ∀L. |L| = 0 → L = ⋆.
+* // #L #I #V >length_pair
+#H elim (ysucc_inv_O_dx … H)
+qed-.
+
+lemma length_inv_zero_sn: ∀L. yinj 0 = |L| → L = ⋆.
+/2 width=1 by length_inv_zero_dx/ qed-.
+
+lemma length_inv_pos_dx: ∀l,L. |L| = ⫯l →
+ ∃∃I,K,V. |K| = l & L = K. ⓑ{I}V.
+#l * /3 width=5 by ysucc_inj, ex2_3_intro/
+>length_atom #H elim (ysucc_inv_O_sn … H)
+qed-.
+
+lemma length_inv_pos_sn: ∀l,L. ⫯l = |L| →
+ ∃∃I,K,V. l = |K| & L = K. ⓑ{I}V.
+#l #L #H lapply (sym_eq ??? H) -H
+#H elim (length_inv_pos_dx … H) -H /2 width=5 by ex2_3_intro/
+qed-.
lemma eq_item0_dec: ∀I1,I2:item0. Decidable (I1 = I2).
* #i1 * #i2 [2,3,4,6,7,8: @or_intror #H destruct ]
-elim (eq_nat_dec i1 i2) /2 width=1 by or_introl/
-#Hni12 @or_intror #H destruct /2 width=1 by/
+[2: elim (eq_nat_dec i1 i2) |1,3: elim (eq_nat_dec i1 i2) ] /2 width=1 by or_introl/
+#Hni12 @or_intror #H destruct /2 width=1 by/
qed-.
(* Basic_1: was: bind_dec *)
+++ /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/notation/functions/append_2.ma".
-include "basic_2/notation/functions/snbind2_3.ma".
-include "basic_2/notation/functions/snabbr_2.ma".
-include "basic_2/notation/functions/snabst_2.ma".
-include "basic_2/grammar/lenv_length.ma".
-
-(* LOCAL ENVIRONMENTS *******************************************************)
-
-let rec append L K on K ≝ match K with
-[ LAtom ⇒ L
-| LPair K I V ⇒ (append L K). ⓑ{I} V
-].
-
-interpretation "append (local environment)" 'Append L1 L2 = (append L1 L2).
-
-interpretation "local environment tail binding construction (binary)"
- 'SnBind2 I T L = (append (LPair LAtom I T) L).
-
-interpretation "tail abbreviation (local environment)"
- 'SnAbbr T L = (append (LPair LAtom Abbr T) L).
-
-interpretation "tail abstraction (local environment)"
- 'SnAbst L T = (append (LPair LAtom Abst T) L).
-
-definition d_appendable_sn: predicate (lenv→relation term) ≝ λR.
- ∀K,T1,T2. R K T1 T2 → ∀L. R (L @@ K) T1 T2.
-
-(* Basic properties *********************************************************)
-
-lemma append_atom_sn: ∀L. ⋆ @@ L = L.
-#L elim L -L normalize //
-qed.
-
-lemma append_assoc: associative … append.
-#L1 #L2 #L3 elim L3 -L3 normalize //
-qed.
-
-lemma append_length: ∀L1,L2. |L1 @@ L2| = |L1| + |L2|.
-#L1 #L2 elim L2 -L2 normalize //
-qed.
-
-lemma ltail_length: ∀I,L,V. |ⓑ{I}V.L| = |L| + 1.
-#I #L #V >append_length //
-qed.
-
-(* Basic_1: was just: chead_ctail *)
-lemma lpair_ltail: ∀L,I,V. ∃∃J,K,W. L.ⓑ{I}V = ⓑ{J}W.K & |L| = |K|.
-#L elim L -L /2 width=5 by ex2_3_intro/
-#L #Z #X #IHL #I #V elim (IHL Z X) -IHL
-#J #K #W #H #_ >H -H >ltail_length
-@(ex2_3_intro … J (K.ⓑ{I}V) W) //
-qed-.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma append_inj_sn: ∀K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 → |K1| = |K2| →
- L1 = L2 ∧ K1 = K2.
-#K1 elim K1 -K1
-[ * normalize /2 width=1 by conj/
- #K2 #I2 #V2 #L1 #L2 #_ <plus_n_Sm #H destruct
-| #K1 #I1 #V1 #IH * normalize
- [ #L1 #L2 #_ <plus_n_Sm #H destruct
- | #K2 #I2 #V2 #L1 #L2 #H1 #H2
- elim (destruct_lpair_lpair_aux … H1) -H1 #H1 #H3 #H4 destruct (**) (* destruct lemma needed *)
- elim (IH … H1) -IH -H1 /2 width=1 by conj/
- ]
-]
-qed-.
-
-(* Note: lemma 750 *)
-lemma append_inj_dx: ∀K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 → |L1| = |L2| →
- L1 = L2 ∧ K1 = K2.
-#K1 elim K1 -K1
-[ * normalize /2 width=1 by conj/
- #K2 #I2 #V2 #L1 #L2 #H1 #H2 destruct
- normalize in H2; >append_length in H2; #H
- elim (plus_xySz_x_false … H)
-| #K1 #I1 #V1 #IH * normalize
- [ #L1 #L2 #H1 #H2 destruct
- normalize in H2; >append_length in H2; #H
- elim (plus_xySz_x_false … (sym_eq … H))
- | #K2 #I2 #V2 #L1 #L2 #H1 #H2
- elim (destruct_lpair_lpair_aux … H1) -H1 #H1 #H3 #H4 destruct (**) (* destruct lemma needed *)
- elim (IH … H1) -IH -H1 /2 width=1 by conj/
- ]
-]
-qed-.
-
-lemma append_inv_refl_dx: ∀L,K. L @@ K = L → K = ⋆.
-#L #K #H elim (append_inj_dx … (⋆) … H) //
-qed-.
-
-lemma append_inv_pair_dx: ∀I,L,K,V. L @@ K = L.ⓑ{I}V → K = ⋆.ⓑ{I}V.
-#I #L #K #V #H elim (append_inj_dx … (⋆.ⓑ{I}V) … H) //
-qed-.
-
-lemma length_inv_pos_dx_ltail: ∀L,l. |L| = l + 1 →
- ∃∃I,K,V. |K| = l & L = ⓑ{I}V.K.
-#Y #l #H elim (length_inv_pos_dx … H) -H #I #L #V #Hl #HLK destruct
-elim (lpair_ltail L I V) /2 width=5 by ex2_3_intro/
-qed-.
-
-lemma length_inv_pos_sn_ltail: ∀L,l. l + 1 = |L| →
- ∃∃I,K,V. l = |K| & L = ⓑ{I}V.K.
-#Y #l #H elim (length_inv_pos_sn … H) -H #I #L #V #Hl #HLK destruct
-elim (lpair_ltail L I V) /2 width=5 by ex2_3_intro/
-qed-.
-
-(* Basic eliminators ********************************************************)
-
-(* Basic_1: was: c_tail_ind *)
-lemma lenv_ind_alt: ∀R:predicate lenv.
- R (⋆) → (∀I,L,T. R L → R (ⓑ{I}T.L)) →
- ∀L. R L.
-#R #IH1 #IH2 #L @(f_ind … length … L) -L #x #IHx * // -IH1
-#L #I #V normalize #H destruct elim (lpair_ltail L I V) /3 width=1 by/
-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/grammar/lenv.ma".
-
-(* LENGTH OF A LOCAL ENVIRONMENT ********************************************)
-
-let rec length L ≝ match L with
-[ LAtom ⇒ 0
-| LPair L _ _ ⇒ length L + 1
-].
-
-interpretation "length (local environment)" 'card L = (length L).
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma length_inv_zero_dx: ∀L. |L| = 0 → L = ⋆.
-* // #L #I #V normalize <plus_n_Sm #H destruct
-qed-.
-
-lemma length_inv_zero_sn: ∀L. 0 = |L| → L = ⋆.
-* // #L #I #V normalize <plus_n_Sm #H destruct
-qed-.
-
-lemma length_inv_pos_dx: ∀l,L. |L| = l + 1 →
- ∃∃I,K,V. |K| = l & L = K. ⓑ{I}V.
-#l *
-[ normalize <plus_n_Sm #H destruct
-| #K #I #V #H
- lapply (injective_plus_l … H) -H /2 width=5 by ex2_3_intro/
-]
-qed-.
-
-lemma length_inv_pos_sn: ∀l,L. l + 1 = |L| →
- ∃∃I,K,V. l = |K| & L = K. ⓑ{I}V.
-#l *
-[ normalize <plus_n_Sm #H destruct
-| #K #I #V #H
- lapply (injective_plus_l … H) -H /2 width=5 by ex2_3_intro/
-]
-qed-.
#Hm destruct /2 width=1 by lreq_zero, lreq_pair/
qed.
-lemma lreq_O2: ∀L1,L2,l. |L1| = |L2| → L1 ⩬[l, yinj 0] L2.
+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 normalize
-[1,3: <plus_n_Sm #H destruct ]
-#H lapply (injective_plus_l … H) -H #HL12
-elim (ynat_cases l) /3 width=1 by lreq_zero/
-* /3 width=1 by lreq_succ/
+* // [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).
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
+#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 normalize //
+#L1 #L2 #l #m #H elim H -L1 -L2 -l -m //
qed-.
(* Advanced inversion lemmas ************************************************)
+++ /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 "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 "ground_2/ynat/ynat_lt.ma".
-include "basic_2/notation/relations/rat_3.ma".
-include "basic_2/grammar/term_vector.ma".
-
-(* MULTIPLE RELOCATION WITH PAIRS *******************************************)
-
-inductive at: list2 ynat nat → relation nat ≝
-| at_nil: ∀i. at (◊) i i
-| at_lt : ∀cs,l,m,i1,i2. yinj i1 < l →
- at cs i1 i2 → at ({l, m} @ cs) i1 i2
-| at_ge : ∀cs,l,m,i1,i2. l ≤ yinj i1 →
- at cs (i1 + m) i2 → at ({l, m} @ cs) i1 i2
-.
-
-interpretation "application (multiple relocation with pairs)"
- 'RAt i1 cs i2 = (at cs i1 i2).
-
-(* Basic inversion lemmas ***************************************************)
-
-fact at_inv_nil_aux: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → cs = ◊ → i1 = i2.
-#cs #i1 #i2 * -cs -i1 -i2
-[ //
-| #cs #l #m #i1 #i2 #_ #_ #H destruct
-| #cs #l #m #i1 #i2 #_ #_ #H destruct
-]
-qed-.
-
-lemma at_inv_nil: ∀i1,i2. @⦃i1, ◊⦄ ≡ i2 → i1 = i2.
-/2 width=3 by at_inv_nil_aux/ qed-.
-
-fact at_inv_cons_aux: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 →
- ∀l,m,cs0. cs = {l, m} @ cs0 →
- i1 < l ∧ @⦃i1, cs0⦄ ≡ i2 ∨
- l ≤ i1 ∧ @⦃i1 + m, cs0⦄ ≡ i2.
-#cs #i1 #i2 * -cs -i1 -i2
-[ #i #l #m #cs #H destruct
-| #cs1 #l1 #m1 #i1 #i2 #Hil1 #Hi12 #l2 #m2 #cs2 #H destruct /3 width=1 by or_introl, conj/
-| #cs1 #l1 #m1 #i1 #i2 #Hli1 #Hi12 #l2 #m2 #cs2 #H destruct /3 width=1 by or_intror, conj/
-]
-qed-.
-
-lemma at_inv_cons: ∀cs,l,m,i1,i2. @⦃i1, {l, m} @ cs⦄ ≡ i2 →
- i1 < l ∧ @⦃i1, cs⦄ ≡ i2 ∨
- l ≤ i1 ∧ @⦃i1 + m, cs⦄ ≡ i2.
-/2 width=3 by at_inv_cons_aux/ qed-.
-
-lemma at_inv_cons_lt: ∀cs,l,m,i1,i2. @⦃i1, {l, m} @ cs⦄ ≡ i2 →
- i1 < l → @⦃i1, cs⦄ ≡ i2.
-#cs #l #m #i1 #m2 #H
-elim (at_inv_cons … H) -H * // #Hli1 #_ #Hi1l
-elim (ylt_yle_false … Hi1l Hli1)
-qed-.
-
-lemma at_inv_cons_ge: ∀cs,l,m,i1,i2. @⦃i1, {l, m} @ cs⦄ ≡ i2 →
- l ≤ i1 → @⦃i1 + m, cs⦄ ≡ i2.
-#cs #l #m #i1 #m2 #H
-elim (at_inv_cons … H) -H * // #Hi1l #_ #Hli1
-elim (ylt_yle_false … Hi1l Hli1)
-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_minus.ma".
-include "basic_2/notation/relations/rminus_3.ma".
-include "basic_2/multiple/mr2.ma".
-
-(* MULTIPLE RELOCATION WITH PAIRS *******************************************)
-
-inductive minuss: nat → relation (list2 ynat nat) ≝
-| minuss_nil: ∀i. minuss i (◊) (◊)
-| minuss_lt : ∀cs1,cs2,l,m,i. yinj i < l → minuss i cs1 cs2 →
- minuss i ({l, m} @ cs1) ({l - i, m} @ cs2)
-| minuss_ge : ∀cs1,cs2,l,m,i. l ≤ yinj i → minuss (m + i) cs1 cs2 →
- minuss i ({l, m} @ cs1) cs2
-.
-
-interpretation "minus (multiple relocation with pairs)"
- 'RMinus cs1 i cs2 = (minuss i cs1 cs2).
-
-(* Basic inversion lemmas ***************************************************)
-
-fact minuss_inv_nil1_aux: ∀cs1,cs2,i. cs1 ▭ i ≡ cs2 → cs1 = ◊ → cs2 = ◊.
-#cs1 #cs2 #i * -cs1 -cs2 -i
-[ //
-| #cs1 #cs2 #l #m #i #_ #_ #H destruct
-| #cs1 #cs2 #l #m #i #_ #_ #H destruct
-]
-qed-.
-
-lemma minuss_inv_nil1: ∀cs2,i. ◊ ▭ i ≡ cs2 → cs2 = ◊.
-/2 width=4 by minuss_inv_nil1_aux/ qed-.
-
-fact minuss_inv_cons1_aux: ∀cs1,cs2,i. cs1 ▭ i ≡ cs2 →
- ∀l,m,cs. cs1 = {l, m} @ cs →
- l ≤ i ∧ cs ▭ m + i ≡ cs2 ∨
- ∃∃cs0. i < l & cs ▭ i ≡ cs0 &
- cs2 = {l - i, m} @ cs0.
-#cs1 #cs2 #i * -cs1 -cs2 -i
-[ #i #l #m #cs #H destruct
-| #cs1 #cs #l1 #m1 #i1 #Hil1 #Hcs #l2 #m2 #cs2 #H destruct /3 width=3 by ex3_intro, or_intror/
-| #cs1 #cs #l1 #m1 #i1 #Hli1 #Hcs #l2 #m2 #cs2 #H destruct /3 width=1 by or_introl, conj/
-]
-qed-.
-
-lemma minuss_inv_cons1: ∀cs1,cs2,l,m,i. {l, m} @ cs1 ▭ i ≡ cs2 →
- l ≤ i ∧ cs1 ▭ m + i ≡ cs2 ∨
- ∃∃cs. i < l & cs1 ▭ i ≡ cs &
- cs2 = {l - i, m} @ cs.
-/2 width=3 by minuss_inv_cons1_aux/ qed-.
-
-lemma minuss_inv_cons1_ge: ∀cs1,cs2,l,m,i. {l, m} @ cs1 ▭ i ≡ cs2 →
- l ≤ i → cs1 ▭ m + i ≡ cs2.
-#cs1 #cs2 #l #m #i #H
-elim (minuss_inv_cons1 … H) -H * // #cs #Hil #_ #_ #Hli
-elim (ylt_yle_false … Hil Hli)
-qed-.
-
-lemma minuss_inv_cons1_lt: ∀cs1,cs2,l,m,i. {l, m} @ cs1 ▭ i ≡ cs2 →
- i < l →
- ∃∃cs. cs1 ▭ i ≡ cs & cs2 = {l - i, m} @ cs.
-#cs1 #cs2 #l #m #i #H elim (minuss_inv_cons1 … H) -H * /2 width=3 by ex2_intro/
-#Hli #_ #Hil elim (ylt_yle_false … Hil Hli)
-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/multiple/mr2.ma".
-
-(* MULTIPLE RELOCATION WITH PAIRS *******************************************)
-
-(* Main properties **********************************************************)
-
-theorem at_mono: ∀cs,i,i1. @⦃i, cs⦄ ≡ i1 → ∀i2. @⦃i, cs⦄ ≡ i2 → i1 = i2.
-#cs #i #i1 #H elim H -cs -i -i1
-[ #i #x #H <(at_inv_nil … H) -x //
-| #cs #l #m #i #i1 #Hil #_ #IHi1 #x #H
- lapply (at_inv_cons_lt … H Hil) -H -Hil /2 width=1 by/
-| #cs #l #m #i #i1 #Hli #_ #IHi1 #x #H
- lapply (at_inv_cons_ge … H Hli) -H -Hli /2 width=1 by/
-]
-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/multiple/mr2.ma".
-
-(* MULTIPLE RELOCATION WITH PAIRS *******************************************)
-
-let rec pluss (cs:list2 ynat nat) (i:nat) on cs ≝ match cs with
-[ nil2 ⇒ ◊
-| cons2 l m cs ⇒ {l + i, m} @ pluss cs i
-].
-
-interpretation "plus (multiple relocation with pairs)"
- 'plus x y = (pluss x y).
-
-(* Basic properties *********************************************************)
-
-lemma pluss_SO2: ∀l,m,cs. ({l, m} @ cs) + 1 = {⫯l, m} @ cs + 1.
-// qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma pluss_inv_nil2: ∀i,cs. cs + i = ◊ → cs = ◊.
-#i * // normalize
-#l #m #cs #H destruct
-qed.
-
-lemma pluss_inv_cons2: ∀i,l,m,cs2,cs. cs + i = {l, m} @ cs2 →
- ∃∃cs1. cs1 + i = cs2 & cs = {l - i, m} @ cs1.
-#i #l #m #cs2 *
-[ normalize #H destruct
-| #l1 #m1 #cs1 whd in ⊢ (??%?→?); #H destruct
- >yplus_minus_inj /2 width=3 by ex2_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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( L ⊢ break 𝐅 * ⦃ term 46 T ⦄ ≡ break term 46 f )"
+ non associative with precedence 45
+ for @{ 'FreeStar $L $T $f }.
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( @ ⦃ term 46 T1 , break term 46 f ⦄ ≡ break term 46 T2 )"
- non associative with precedence 45
- for @{ 'RAt $T1 $f $T2 }.
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( T1 ▭ break term 46 T2 ≡ break term 46 T )"
- non associative with precedence 45
- for @{ 'RMinus $T1 $T2 $T }.
(* *)
(**************************************************************************)
+include "ground_2/notation/functions/successor_1.ma".
+include "ground_2/notation/functions/predecessor_1.ma".
include "arithmetics/nat.ma".
include "ground_2/lib/star.ma".
(* ARITHMETICAL PROPERTIES **************************************************)
+interpretation "nat successor" 'Successor m = (S m).
+
+interpretation "nat predecessor" 'Predecessor m = (pred m).
+
(* Iota equations ***********************************************************)
lemma pred_O: pred 0 = 0.
#n #H elim (lt_to_not_le … H) -H /2 width=1 by/
qed-.
+lemma lt_le_false: ∀x,y. x < y → y ≤ x → ⊥.
+/3 width=4 by lt_refl_false, lt_to_le_to_lt/ qed-.
+
lemma pred_inv_refl: ∀m. pred m = m → m = 0.
* // normalize #m #H elim (lt_refl_false m) //
qed-.
interpretation "cons (list)" 'Cons hd tl = (cons ? hd tl).
+let rec length (A:Type[0]) (l:list A) on l ≝ match l with
+[ nil ⇒ 0
+| cons _ l ⇒ length A l + 1
+].
+
+interpretation "length (list)"
+ 'card l = (length ? l).
+
let rec all A (R:predicate A) (l:list A) on l ≝
match l with
[ nil ⇒ ⊤
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "hvbox( f1 ⊚ break term 46 f2 ≡ break term 46 f )"
+ non associative with precedence 45
+ for @{ 'RAfter $f1 $f2 $f }.
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "hvbox( @ ⦃ term 46 T1 , break term 46 f ⦄ ≡ break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'RAt $T1 $f $T2 }.
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "hvbox( T1 ▭ break term 46 T2 ≡ break term 46 T )"
+ non associative with precedence 45
+ for @{ 'RMinus $T1 $T2 $T }.
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "hvbox( L1 ⋓ break term 46 L2 ≡ break term 46 L )"
+ non associative with precedence 45
+ for @{ 'RUnion $L1 $L2 $L }.
--- /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/notation/relations/rat_3.ma".
+include "ground_2/relocation/mr2.ma".
+
+(* MULTIPLE RELOCATION WITH PAIRS *******************************************)
+
+inductive at: mr2 → relation nat ≝
+| at_nil: ∀i. at (◊) i i
+| at_lt : ∀cs,l,m,i1,i2. i1 < l →
+ at cs i1 i2 → at ({l, m} @ cs) i1 i2
+| at_ge : ∀cs,l,m,i1,i2. l ≤ i1 →
+ at cs (i1 + m) i2 → at ({l, m} @ cs) i1 i2
+.
+
+interpretation "application (multiple relocation with pairs)"
+ 'RAt i1 cs i2 = (at cs i1 i2).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact at_inv_nil_aux: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → cs = ◊ → i1 = i2.
+#cs #i1 #i2 * -cs -i1 -i2
+[ //
+| #cs #l #m #i1 #i2 #_ #_ #H destruct
+| #cs #l #m #i1 #i2 #_ #_ #H destruct
+]
+qed-.
+
+lemma at_inv_nil: ∀i1,i2. @⦃i1, ◊⦄ ≡ i2 → i1 = i2.
+/2 width=3 by at_inv_nil_aux/ qed-.
+
+fact at_inv_cons_aux: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 →
+ ∀l,m,cs0. cs = {l, m} @ cs0 →
+ i1 < l ∧ @⦃i1, cs0⦄ ≡ i2 ∨
+ l ≤ i1 ∧ @⦃i1 + m, cs0⦄ ≡ i2.
+#cs #i1 #i2 * -cs -i1 -i2
+[ #i #l #m #cs #H destruct
+| #cs1 #l1 #m1 #i1 #i2 #Hil1 #Hi12 #l2 #m2 #cs2 #H destruct /3 width=1 by or_introl, conj/
+| #cs1 #l1 #m1 #i1 #i2 #Hli1 #Hi12 #l2 #m2 #cs2 #H destruct /3 width=1 by or_intror, conj/
+]
+qed-.
+
+lemma at_inv_cons: ∀cs,l,m,i1,i2. @⦃i1, {l, m} @ cs⦄ ≡ i2 →
+ i1 < l ∧ @⦃i1, cs⦄ ≡ i2 ∨
+ l ≤ i1 ∧ @⦃i1 + m, cs⦄ ≡ i2.
+/2 width=3 by at_inv_cons_aux/ qed-.
+
+lemma at_inv_cons_lt: ∀cs,l,m,i1,i2. @⦃i1, {l, m} @ cs⦄ ≡ i2 →
+ i1 < l → @⦃i1, cs⦄ ≡ i2.
+#cs #l #m #i1 #m2 #H
+elim (at_inv_cons … H) -H * // #Hli1 #_ #Hi1l
+elim (lt_le_false … Hi1l Hli1)
+qed-.
+
+lemma at_inv_cons_ge: ∀cs,l,m,i1,i2. @⦃i1, {l, m} @ cs⦄ ≡ i2 →
+ l ≤ i1 → @⦃i1 + m, cs⦄ ≡ i2.
+#cs #l #m #i1 #m2 #H
+elim (at_inv_cons … H) -H * // #Hi1l #_ #Hli1
+elim (lt_le_false … Hi1l Hli1)
+qed-.
+
+(* Main properties **********************************************************)
+
+theorem at_mono: ∀cs,i,i1. @⦃i, cs⦄ ≡ i1 → ∀i2. @⦃i, cs⦄ ≡ i2 → i1 = i2.
+#cs #i #i1 #H elim H -cs -i -i1
+[ #i #x #H <(at_inv_nil … H) -x //
+| #cs #l #m #i #i1 #Hil #_ #IHi1 #x #H
+ lapply (at_inv_cons_lt … H Hil) -H -Hil /2 width=1 by/
+| #cs #l #m #i #i1 #Hli #_ #IHi1 #x #H
+ lapply (at_inv_cons_ge … H Hli) -H -Hli /2 width=1 by/
+]
+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/notation/relations/rminus_3.ma".
+include "ground_2/relocation/mr2.ma".
+
+(* MULTIPLE RELOCATION WITH PAIRS *******************************************)
+
+inductive minuss: nat → relation mr2 ≝
+| minuss_nil: ∀i. minuss i (◊) (◊)
+| minuss_lt : ∀cs1,cs2,l,m,i. i < l → minuss i cs1 cs2 →
+ minuss i ({l, m} @ cs1) ({l - i, m} @ cs2)
+| minuss_ge : ∀cs1,cs2,l,m,i. l ≤ i → minuss (m + i) cs1 cs2 →
+ minuss i ({l, m} @ cs1) cs2
+.
+
+interpretation "minus (multiple relocation with pairs)"
+ 'RMinus cs1 i cs2 = (minuss i cs1 cs2).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact minuss_inv_nil1_aux: ∀cs1,cs2,i. cs1 ▭ i ≡ cs2 → cs1 = ◊ → cs2 = ◊.
+#cs1 #cs2 #i * -cs1 -cs2 -i
+[ //
+| #cs1 #cs2 #l #m #i #_ #_ #H destruct
+| #cs1 #cs2 #l #m #i #_ #_ #H destruct
+]
+qed-.
+
+lemma minuss_inv_nil1: ∀cs2,i. ◊ ▭ i ≡ cs2 → cs2 = ◊.
+/2 width=4 by minuss_inv_nil1_aux/ qed-.
+
+fact minuss_inv_cons1_aux: ∀cs1,cs2,i. cs1 ▭ i ≡ cs2 →
+ ∀l,m,cs. cs1 = {l, m} @ cs →
+ l ≤ i ∧ cs ▭ m + i ≡ cs2 ∨
+ ∃∃cs0. i < l & cs ▭ i ≡ cs0 &
+ cs2 = {l - i, m} @ cs0.
+#cs1 #cs2 #i * -cs1 -cs2 -i
+[ #i #l #m #cs #H destruct
+| #cs1 #cs #l1 #m1 #i1 #Hil1 #Hcs #l2 #m2 #cs2 #H destruct /3 width=3 by ex3_intro, or_intror/
+| #cs1 #cs #l1 #m1 #i1 #Hli1 #Hcs #l2 #m2 #cs2 #H destruct /3 width=1 by or_introl, conj/
+]
+qed-.
+
+lemma minuss_inv_cons1: ∀cs1,cs2,l,m,i. {l, m} @ cs1 ▭ i ≡ cs2 →
+ l ≤ i ∧ cs1 ▭ m + i ≡ cs2 ∨
+ ∃∃cs. i < l & cs1 ▭ i ≡ cs &
+ cs2 = {l - i, m} @ cs.
+/2 width=3 by minuss_inv_cons1_aux/ qed-.
+
+lemma minuss_inv_cons1_ge: ∀cs1,cs2,l,m,i. {l, m} @ cs1 ▭ i ≡ cs2 →
+ l ≤ i → cs1 ▭ m + i ≡ cs2.
+#cs1 #cs2 #l #m #i #H
+elim (minuss_inv_cons1 … H) -H * // #cs #Hil #_ #_ #Hli
+elim (lt_le_false … Hil Hli)
+qed-.
+
+lemma minuss_inv_cons1_lt: ∀cs1,cs2,l,m,i. {l, m} @ cs1 ▭ i ≡ cs2 →
+ i < l →
+ ∃∃cs. cs1 ▭ i ≡ cs & cs2 = {l - i, m} @ cs.
+#cs1 #cs2 #l #m #i #H elim (minuss_inv_cons1 … H) -H * /2 width=3 by ex2_intro/
+#Hli #_ #Hil elim (lt_le_false … Hil Hli)
+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/relocation/mr2.ma".
+
+(* MULTIPLE RELOCATION WITH PAIRS *******************************************)
+
+let rec pluss (cs:mr2) (i:nat) on cs ≝ match cs with
+[ nil2 ⇒ ◊
+| cons2 l m cs ⇒ {l + i, m} @ pluss cs i
+].
+
+interpretation "plus (multiple relocation with pairs)"
+ 'plus x y = (pluss x y).
+
+(* Basic properties *********************************************************)
+
+lemma pluss_SO2: ∀l,m,cs. ({l, m} @ cs) + 1 = {⫯l, m} @ cs + 1.
+normalize // qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma pluss_inv_nil2: ∀i,cs. cs + i = ◊ → cs = ◊.
+#i * // normalize
+#l #m #cs #H destruct
+qed.
+
+lemma pluss_inv_cons2: ∀i,l,m,cs2,cs. cs + i = {l, m} @ cs2 →
+ ∃∃cs1. cs1 + i = cs2 & cs = {l - i, m} @ cs1.
+#i #l #m #cs2 *
+[ normalize #H destruct
+| #l1 #m1 #cs1 whd in ⊢ (??%?→?); #H destruct
+ <minus_plus_m_m /2 width=3 by ex2_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 "ground_2/lib/bool.ma".
+include "ground_2/lib/list.ma".
+
+(* RELOCATION TRACE *********************************************************)
+
+definition trace: Type[0] ≝ list bool.
--- /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/notation/relations/rafter_3.ma".
+include "ground_2/relocation/trace_at.ma".
+
+(* RELOCATION TRACE *********************************************************)
+
+inductive after: relation3 trace trace trace ≝
+ | after_empty: after (◊) (◊) (◊)
+ | after_true : ∀cs1,cs2,cs. after cs1 cs2 cs →
+ ∀b. after (Ⓣ @ cs1) (b @ cs2) (b @ cs)
+ | after_false: ∀cs1,cs2,cs. after cs1 cs2 cs →
+ after (Ⓕ @ cs1) cs2 (Ⓕ @ cs).
+
+interpretation "composition (trace)"
+ 'RAfter cs1 cs2 cs = (after cs1 cs2 cs).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact after_inv_empty1_aux: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs → cs1 = ◊ →
+ cs2 = ◊ ∧ cs = ◊.
+#cs1 #cs2 #cs * -cs1 -cs2 -cs
+[ /2 width=1 by conj/
+| #cs1 #cs2 #cs #_ #b #H destruct
+| #cs1 #cs2 #cs #_ #H destruct
+]
+qed-.
+
+lemma after_inv_empty1: ∀cs2,cs. ◊ ⊚ cs2 ≡ cs → cs2 = ◊ ∧ cs = ◊.
+/2 width=3 by after_inv_empty1_aux/ qed-.
+
+fact after_inv_true1_aux: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs → ∀tl1. cs1 = Ⓣ @ tl1 →
+ ∃∃tl2,tl,b. cs2 = b @ tl2 & cs = b @ tl & tl1 ⊚ tl2 ≡ tl.
+#cs1 #cs2 #cs * -cs1 -cs2 -cs
+[ #tl1 #H destruct
+| #cs1 #cs2 #cs #H12 #b #tl1 #H destruct
+ /2 width=6 by ex3_3_intro/
+| #cs1 #cs2 #cs #_ #tl1 #H destruct
+]
+qed-.
+
+lemma after_inv_true1: ∀tl1,cs2,cs. (Ⓣ @ tl1) ⊚ cs2 ≡ cs →
+ ∃∃tl2,tl,b. cs2 = b @ tl2 & cs = b @ tl & tl1 ⊚ tl2 ≡ tl.
+/2 width=3 by after_inv_true1_aux/ qed-.
+
+fact after_inv_false1_aux: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs → ∀tl1. cs1 = Ⓕ @ tl1 →
+ ∃∃tl. cs = Ⓕ @ tl & tl1 ⊚ cs2 ≡ tl.
+#cs1 #cs2 #cs * -cs1 -cs2 -cs
+[ #tl1 #H destruct
+| #cs1 #cs2 #cs #_ #b #tl1 #H destruct
+| #cs1 #cs2 #cs #H12 #tl1 #H destruct
+ /2 width=3 by ex2_intro/
+]
+qed-.
+
+lemma after_inv_false1: ∀tl1,cs2,cs. (Ⓕ @ tl1) ⊚ cs2 ≡ cs →
+ ∃∃tl. cs = Ⓕ @ tl & tl1 ⊚ cs2 ≡ tl.
+/2 width=3 by after_inv_false1_aux/ qed-.
+
+fact after_inv_empty3_aux: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs → cs = ◊ →
+ cs1 = ◊ ∧ cs2 = ◊.
+#cs1 #cs2 #cs * -cs1 -cs2 -cs
+[ /2 width=1 by conj/
+| #cs1 #cs2 #cs #_ #b #H destruct
+| #cs1 #cs2 #cs #_ #H destruct
+]
+qed-.
+
+lemma after_inv_empty3: ∀cs1,cs2. cs1 ⊚ cs2 ≡ ◊ → cs1 = ◊ ∧ cs2 = ◊.
+/2 width=3 by after_inv_empty3_aux/ qed-.
+
+fact after_inv_inh3_aux: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs → ∀tl,b. cs = b @ tl →
+ (∃∃tl1,tl2. cs1 = Ⓣ @ tl1 & cs2 = b @ tl2 & tl1 ⊚ tl2 ≡ tl) ∨
+ ∃∃tl1. cs1 = Ⓕ @ tl1 & b = Ⓕ & tl1 ⊚ cs2 ≡ tl.
+#cs1 #cs2 #cs * -cs1 -cs2 -cs
+[ #tl #b #H destruct
+| #cs1 #cs2 #cs #H12 #b0 #tl #b #H destruct
+ /3 width=5 by ex3_2_intro, or_introl/
+| #cs1 #cs2 #cs #H12 #tl #b #H destruct
+ /3 width=3 by ex3_intro, or_intror/
+]
+qed-.
+
+lemma after_inv_inh3: ∀cs1,cs2,tl,b. cs1 ⊚ cs2 ≡ b @ tl →
+ (∃∃tl1,tl2. cs1 = Ⓣ @ tl1 & cs2 = b @ tl2 & tl1 ⊚ tl2 ≡ tl) ∨
+ ∃∃tl1. cs1 = Ⓕ @ tl1 & b = Ⓕ & tl1 ⊚ cs2 ≡ tl.
+/2 width=3 by after_inv_inh3_aux/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma after_at_fwd: ∀cs1,cs2,cs. cs2 ⊚ cs1 ≡ cs → ∀i1,i. @⦃i1, cs⦄ ≡ i →
+ ∃∃i2. @⦃i1, cs1⦄ ≡ i2 & @⦃i2, cs2⦄ ≡ i.
+#cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs
+[ #i1 #i #H elim (at_inv_empty … H)
+| #cs1 #cs2 #cs #_ * #IH #i1 #i #H
+ [ elim (at_inv_true … H) -H *
+ [ -IH #H1 #H2 destruct /2 width=3 by at_zero, ex2_intro/
+ | #j1 #j #H1 #H2 #Hj1 destruct
+ elim (IH … Hj1) -IH -Hj1 /3 width=3 by at_succ, ex2_intro/
+ ]
+ | elim (at_inv_false … H) -H
+ #j #H #Hj destruct
+ elim (IH … Hj) -IH -Hj /3 width=3 by at_succ, at_false, ex2_intro/
+ ]
+| #cs1 #cs2 #cs #_ #IH #i1 #i #H elim (at_inv_false … H) -H
+ #j #H #Hj destruct
+ elim (IH … Hj) -IH -Hj /3 width=3 by at_false, ex2_intro/
+]
+qed-.
+
+lemma after_fwd_at: ∀cs1,cs2,cs. cs2 ⊚ cs1 ≡ cs → ∀i1,i2. @⦃i1, cs1⦄ ≡ i2 →
+ ∃∃i. @⦃i2, cs2⦄ ≡ i & @⦃i1, cs⦄ ≡ i.
+#cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs
+[ #i1 #i2 #H elim (at_inv_empty … H)
+| #cs1 #cs2 #cs #_ * #IH #i1 #i2 #H
+ [ elim (at_inv_true … H) -H *
+ [ -IH #H1 #H2 destruct /2 width=3 by at_zero, ex2_intro/
+ | #j1 #j2 #H1 #H2 #Hj12 destruct
+ elim (IH … Hj12) -IH -Hj12 /3 width=3 by at_succ, ex2_intro/
+ ]
+ | elim (at_inv_false … H) -H
+ #j2 #H #Hj2 destruct
+ elim (IH … Hj2) -IH -Hj2 /3 width=3 by at_succ, at_false, ex2_intro/
+ ]
+| #cs1 #cs2 #cs #_ #IH #i1 #i2 #H elim (IH … H) -IH -H
+ /3 width=3 by at_false, ex2_intro/
+]
+qed-.
+
+(* Main properties **********************************************************)
+
+theorem after_trans1: ∀cs1,cs2,cs0. cs1 ⊚ cs2 ≡ cs0 →
+ ∀cs3, cs4. cs0 ⊚ cs3 ≡ cs4 →
+ ∃∃cs. cs2 ⊚ cs3 ≡ cs & cs1 ⊚ cs ≡ cs4.
+#cs1 #cs2 #cs0 #H elim H -cs1 -cs2 -cs0
+[ #cs3 #cs4 #H elim (after_inv_empty1 … H) -H
+ #H1 #H2 destruct /2 width=3 by ex2_intro, after_empty/
+| #cs1 #cs2 #cs0 #_ * #IH #cs3 #cs4 #H
+ [ elim (after_inv_true1 … H) -H
+ #tl3 #tl4 #b #H1 #H2 #Htl destruct
+ elim (IH … Htl) -cs0
+ /3 width=3 by ex2_intro, after_true/
+ | elim (after_inv_false1 … H) -H
+ #tl4 #H #Htl destruct
+ elim (IH … Htl) -cs0
+ /3 width=3 by ex2_intro, after_true, after_false/
+ ]
+| #cs1 #cs2 #cs0 #_ #IH #cs3 #cs4 #H
+ elim (after_inv_false1 … H) -H
+ #tl4 #H #Htl destruct
+ elim (IH … Htl) -cs0
+ /3 width=3 by ex2_intro, after_false/
+]
+qed-.
+
+theorem after_trans2: ∀cs1,cs0,cs4. cs1 ⊚ cs0 ≡ cs4 →
+ ∀cs2, cs3. cs2 ⊚ cs3 ≡ cs0 →
+ ∃∃cs. cs1 ⊚ cs2 ≡ cs & cs ⊚ cs3 ≡ cs4.
+#cs1 #cs0 #cs4 #H elim H -cs1 -cs0 -cs4
+[ #cs2 #cs3 #H elim (after_inv_empty3 … H) -H
+ #H1 #H2 destruct /2 width=3 by ex2_intro, after_empty/
+| #cs1 #cs0 #cs4 #_ #b #IH #cs2 #cs3 #H elim (after_inv_inh3 … H) -H *
+ [ #tl2 #tl3 #H1 #H2 #Htl destruct
+ elim (IH … Htl) -cs0
+ /3 width=3 by ex2_intro, after_true/
+ | #tl2 #H1 #H2 #Htl destruct
+ elim (IH … Htl) -cs0
+ /3 width=3 by ex2_intro, after_true, after_false/
+ ]
+| #cs1 #cs0 #cs4 #_ #IH #cs2 #cs3 #H elim (IH … H) -cs0
+ /3 width=3 by ex2_intro, after_false/
+]
+qed-.
+
+theorem after_mono: ∀cs1,cs2,x. cs1 ⊚ cs2 ≡ x → ∀y. cs1 ⊚ cs2 ≡ y → x = y.
+#cs1 #cs2 #x #H elim H -cs1 -cs2 -x
+[ #y #H elim (after_inv_empty1 … H) -H //
+| #cs1 #cs #x #_ #b #IH #y #H elim (after_inv_true1 … H) -H
+ #tl #tly #b0 #H1 #H2 #Htl destruct >(IH … Htl) -tl -cs1 -x //
+| #cs1 #cs2 #x #_ #IH #y #H elim (after_inv_false1 … H) -H
+ #tly #H #Htl destruct >(IH … Htl) -cs1 -cs2 -x //
+]
+qed-.
+
+theorem after_inj: ∀cs1,x,cs. cs1 ⊚ x ≡ cs → ∀y. cs1 ⊚ y ≡ cs → x = y.
+#cs1 #x #cs #H elim H -cs1 -x -cs
+[ #y #H elim (after_inv_empty1 … H) -H //
+| #cs1 #x #cs #_ #b #IH #y #H elim (after_inv_true1 … H) -H
+ #tly #tl #b0 #H1 #H2 #Htl destruct >(IH … Htl) -tl -cs1 -x //
+| #cs1 #x #cs #_ #IH #y #H elim (after_inv_false1 … H) -H
+ #tl #H #Htl destruct >(IH … Htl) -tl -cs1 -x //
+]
+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/notation/relations/rat_3.ma".
+include "ground_2/relocation/trace.ma".
+
+(* RELOCATION TRACE *********************************************************)
+
+inductive at: trace → relation nat ≝
+ | at_zero : ∀cs. at (Ⓣ @ cs) 0 0
+ | at_succ : ∀cs,i,j. at cs i j → at (Ⓣ @ cs) (⫯i) (⫯j)
+ | at_false: ∀cs,i,j. at cs i j → at (Ⓕ @ cs) i (⫯j).
+
+interpretation "relocation (trace)"
+ 'RAt i1 cs i2 = (at cs i1 i2).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact at_inv_empty_aux: ∀cs,i,j. @⦃i, cs⦄ ≡ j → cs = ◊ → ⊥.
+#cs #i #j * -cs -i -j
+#cs [2,3: #i #j #_ ] #H destruct
+qed-.
+
+lemma at_inv_empty: ∀i,j. @⦃i, ◊⦄ ≡ j → ⊥.
+/2 width=5 by at_inv_empty_aux/ qed-.
+
+fact at_inv_true_aux: ∀cs,i,j. @⦃i, cs⦄ ≡ j → ∀tl. cs = Ⓣ @ tl →
+ (i = 0 ∧ j = 0) ∨
+ ∃∃i0,j0. i = ⫯i0 & j = ⫯j0 & @⦃i0, tl⦄ ≡ j0.
+#cs #i #j * -cs -i -j
+#cs [2,3: #i #j #Hij ] #tl #H destruct
+/3 width=5 by ex3_2_intro, or_introl, or_intror, conj/
+qed-.
+
+lemma at_inv_true: ∀cs,i,j. @⦃i, Ⓣ @ cs⦄ ≡ j →
+ (i = 0 ∧ j = 0) ∨
+ ∃∃i0,j0. i = ⫯i0 & j = ⫯j0 & @⦃i0, cs⦄ ≡ j0.
+/2 width=3 by at_inv_true_aux/ qed-.
+
+lemma at_inv_true_zero_sn: ∀cs,j. @⦃0, Ⓣ @ cs⦄ ≡ j → j = 0.
+#cs #j #H elim (at_inv_true … H) -H * //
+#i0 #j0 #H destruct
+qed-.
+
+lemma at_inv_true_zero_dx: ∀cs,i. @⦃i, Ⓣ @ cs⦄ ≡ 0 → i = 0.
+#cs #i #H elim (at_inv_true … H) -H * //
+#i0 #j0 #_ #H destruct
+qed-.
+
+lemma at_inv_true_succ_sn: ∀cs,i,j. @⦃⫯i, Ⓣ @ cs⦄ ≡ j →
+ ∃∃j0. j = ⫯j0 & @⦃i, cs⦄ ≡ j0.
+#cs #i #j #H elim (at_inv_true … H) -H *
+[ #H destruct
+| #i0 #j0 #H1 #H2 destruct /2 width=3 by ex2_intro/
+]
+qed-.
+
+lemma at_inv_true_succ_dx: ∀cs,i,j. @⦃i, Ⓣ @ cs⦄ ≡ ⫯j →
+ ∃∃i0. i = ⫯i0 & @⦃i0, cs⦄ ≡ j.
+#cs #i #j #H elim (at_inv_true … H) -H *
+[ #_ #H destruct
+| #i0 #j0 #H1 #H2 destruct /2 width=3 by ex2_intro/
+]
+qed-.
+
+lemma at_inv_true_succ: ∀cs,i,j. @⦃⫯i, Ⓣ @ cs⦄ ≡ ⫯j →
+ @⦃i, cs⦄ ≡ j.
+#cs #i #j #H elim (at_inv_true … H) -H *
+[ #H destruct
+| #i0 #j0 #H1 #H2 destruct //
+]
+qed-.
+
+lemma at_inv_true_O_S: ∀cs,j. @⦃0, Ⓣ @ cs⦄ ≡ ⫯j → ⊥.
+#cs #j #H elim (at_inv_true … H) -H *
+[ #_ #H destruct
+| #i0 #j0 #H1 destruct
+]
+qed-.
+
+lemma at_inv_true_S_O: ∀cs,i. @⦃⫯i, Ⓣ @ cs⦄ ≡ 0 → ⊥.
+#cs #i #H elim (at_inv_true … H) -H *
+[ #H destruct
+| #i0 #j0 #_ #H1 destruct
+]
+qed-.
+
+fact at_inv_false_aux: ∀cs,i,j. @⦃i, cs⦄ ≡ j → ∀tl. cs = Ⓕ @ tl →
+ ∃∃j0. j = ⫯j0 & @⦃i, tl⦄ ≡ j0.
+#cs #i #j * -cs -i -j
+#cs [2,3: #i #j #Hij ] #tl #H destruct
+/2 width=3 by ex2_intro/
+qed-.
+
+lemma at_inv_false: ∀cs,i,j. @⦃i, Ⓕ @ cs⦄ ≡ j →
+ ∃∃j0. j = ⫯j0 & @⦃i, cs⦄ ≡ j0.
+/2 width=3 by at_inv_false_aux/ qed-.
+
+lemma at_inv_false_S: ∀cs,i,j. @⦃i, Ⓕ @ cs⦄ ≡ ⫯j → @⦃i, cs⦄ ≡ j.
+#cs #i #j #H elim (at_inv_false … H) -H
+#j0 #H destruct //
+qed-.
+
+lemma at_inv_false_O: ∀cs,i. @⦃i, Ⓕ @ cs⦄ ≡ 0 → ⊥.
+#cs #i #H elim (at_inv_false … H) -H
+#j0 #H destruct
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma at_monotonic: ∀cs,i2,j2. @⦃i2, cs⦄ ≡ j2 → ∀i1. i1 < i2 →
+ ∃∃j1. @⦃i1, cs⦄ ≡ j1 & j1 < j2.
+#cs #i2 #j2 #H elim H -cs -i2 -j2
+[ #cs #i1 #H elim (lt_zero_false … H)
+| #cs #i #j #Hij #IH * /2 width=3 by ex2_intro, at_zero/
+ #i1 #H lapply (lt_S_S_to_lt … H) -H
+ #H elim (IH … H) -i
+ #j1 #Hij1 #H /3 width=3 by le_S_S, ex2_intro, at_succ/
+| #cs #i #j #_ #IH #i1 #H elim (IH … H) -i
+ /3 width=3 by le_S_S, ex2_intro, at_false/
+]
+qed-.
+
+lemma at_at_dec: ∀cs,i,j. Decidable (@⦃i, cs⦄ ≡ j).
+#cs elim cs -cs [ | * #cs #IH ]
+[ /3 width=3 by at_inv_empty, or_intror/
+| * [2: #i ] * [2,4: #j ]
+ [ elim (IH i j) -IH
+ /4 width=1 by at_inv_true_succ, at_succ, or_introl, or_intror/
+ | -IH /3 width=3 by at_inv_true_O_S, or_intror/
+ | -IH /3 width=3 by at_inv_true_S_O, or_intror/
+ | -IH /2 width=1 by or_introl, at_zero/
+ ]
+| #i * [2: #j ]
+ [ elim (IH i j) -IH
+ /4 width=1 by at_inv_false_S, at_false, or_introl, or_intror/
+ | -IH /3 width=3 by at_inv_false_O, or_intror/
+ ]
+]
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma at_increasing: ∀cs,i,j. @⦃i, cs⦄ ≡ j → i ≤ j.
+#cs #i elim i -i //
+#i0 #IHi #j #H elim (at_monotonic … H i0) -H
+/3 width=3 by le_to_lt_to_lt/
+qed-.
+
+lemma at_length_lt: ∀cs,i,j. @⦃i, cs⦄ ≡ j → j < |cs|.
+#cs elim cs -cs [ | * #cs #IH ] #i #j #H normalize
+[ elim (at_inv_empty … H)
+| elim (at_inv_true … H) * -H //
+ #i0 #j0 #H1 #H2 #Hij0 destruct /3 width=2 by le_S_S/
+| elim (at_inv_false … H) -H
+ #j0 #H #H0 destruct /3 width=2 by le_S_S/
+]
+qed-.
+
+(* Main properties **********************************************************)
+
+theorem at_mono: ∀cs,i,j1. @⦃i, cs⦄ ≡ j1 → ∀j2. @⦃i, cs⦄ ≡ j2 → j1 = j2.
+#cs #i #j1 #H elim H -cs -i -j1
+#cs [ |2,3: #i #j1 #_ #IH ] #j2 #H
+[ lapply (at_inv_true_zero_sn … H) -H //
+| elim (at_inv_true_succ_sn … H) -H
+ #j0 #H destruct #H >(IH … H) -cs -i -j1 //
+| elim (at_inv_false … H) -H
+ #j0 #H destruct #H >(IH … H) -cs -i -j1 //
+]
+qed-.
+
+theorem at_inj: ∀cs,i1,j. @⦃i1, cs⦄ ≡ j → ∀i2. @⦃i2, cs⦄ ≡ j → i1 = i2.
+#cs #i1 #j #H elim H -cs -i1 -j
+#cs [ |2,3: #i1 #j #_ #IH ] #i2 #H
+[ lapply (at_inv_true_zero_dx … H) -H //
+| elim (at_inv_true_succ_dx … H) -H
+ #i0 #H destruct #H >(IH … H) -cs -i1 -j //
+| elim (at_inv_false … H) -H
+ #j0 #H destruct #H >(IH … H) -cs -i1 -j0 //
+]
+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/notation/relations/runion_3.ma".
+include "ground_2/relocation/trace.ma".
+
+(* RELOCATION TRACE *********************************************************)
+
+inductive sor: relation3 trace trace trace ≝
+ | sor_empty: sor (◊) (◊) (◊)
+ | sor_inh : ∀cs1,cs2,cs. sor cs1 cs2 cs →
+ ∀b1,b2. sor (b1 @ cs1) (b2 @ cs2) ((b1 ∨ b2) @ cs).
+
+interpretation
+ "union (trace)"
+ 'RUnion L1 L2 L = (sor L2 L1 L).
+
+(* Basic properties *********************************************************)
+
+lemma sor_sym: ∀cs1,cs2,cs. cs1 ⋓ cs2 ≡ cs → cs2 ⋓ cs1 ≡ cs.
+#cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs /2 width=1 by sor_inh/
+qed-.
and its timeline.
</body>
<table name="ground_2_sum"/>
+ <news class="alpha" date="2015 October 11.">
+ Multiple relocation with lists of booleans.
+ </news>
<news class="alpha" date="2013 November 27.">
Natural numbers with infinity.
</news>
]
}
]
+ class "green"
+ [ { "multiple relocation" * } {
+ [ { "" * } {
+ [ "trace" "trace_at ( @⦃?,?⦄ ≡ ? )" "trace_after ( ? ⊚ ? ≡ ? )" "trace_sor ( ? ⋓ ? ≡ ? )" * ]
+ [ "mr2" "mr2_at ( @⦃?,?⦄ ≡ ? )" "mr2_plus ( ? + ? )" "mr2_minus ( ? ▭ ? ≡ ? )" * ]
+ }
+ ]
+ }
+ ]
class "grass"
[ { "natural numbers with infinity" * } {
[ { "" * } {
class "yellow"
[ { "extensions to the library" * } {
[ { "" * } {
- [ "star" "lstar" "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? )"
+ [ "star" "lstar" "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? ) ( ⫯? ) ( ⫰? )"
"list ( ◊ ) ( ? @ ? ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )" *
]
}
(* Inversion lemmas on successor ********************************************)
-fact yle_inv_succ1_aux: ∀x,y. x ≤ y → ∀m. x = ⫯m → m ≤ ⫰y ∧ ⫯⫰y = y.
+fact yle_inv_succ1_aux: ∀x,y:ynat. x ≤ y → ∀m. x = ⫯m → m ≤ ⫰y ∧ ⫯⫰y = y.
#x #y * -x -y
[ #x #y #Hxy #m #H elim (ysucc_inv_inj_sn … H) -H
#n #H1 #H2 destruct elim (le_inv_S1 … Hxy) -Hxy
]
qed-.
-lemma yle_inv_succ1: ∀m,y. ⫯m ≤ y → m ≤ ⫰y ∧ ⫯⫰y = y.
+lemma yle_inv_succ1: ∀m,y:ynat. ⫯m ≤ y → m ≤ ⫰y ∧ ⫯⫰y = y.
/2 width=3 by yle_inv_succ1_aux/ qed-.
lemma yle_inv_succ: ∀m,n. ⫯m ≤ ⫯n → m ≤ n.
#H elim (ylt_inv_Y1 … H)
qed-.
-lemma ylt_inv_O1: ∀n. 0 < n → ⫯⫰n = n.
+lemma ylt_inv_O1: ∀n:ynat. 0 < n → ⫯⫰n = n.
* // #n #H lapply (ylt_inv_inj … H) -H normalize
/3 width=1 by S_pred, eq_f/
qed-.
(* Inversion lemmas on successor ********************************************)
-fact ylt_inv_succ1_aux: ∀x,y. x < y → ∀m. x = ⫯m → m < ⫰y ∧ ⫯⫰y = y.
+fact ylt_inv_succ1_aux: ∀x,y:ynat. x < y → ∀m. x = ⫯m → m < ⫰y ∧ ⫯⫰y = y.
#x #y * -x -y
[ #x #y #Hxy #m #H elim (ysucc_inv_inj_sn … H) -H
#n #H1 #H2 destruct elim (le_inv_S1 … Hxy) -Hxy
]
qed-.
-lemma ylt_inv_succ1: ∀m,y. ⫯m < y → m < ⫰y ∧ ⫯⫰y = y.
+lemma ylt_inv_succ1: ∀m,y:ynat. ⫯m < y → m < ⫰y ∧ ⫯⫰y = y.
/2 width=3 by ylt_inv_succ1_aux/ qed-.
lemma ylt_inv_succ: ∀m,n. ⫯m < ⫯n → m < n.
(* Basic properties *********************************************************)
-lemma ylt_O1: ∀x. ⫯⫰x = x → 0 < x.
+lemma ylt_O1: ∀x:ynat. ⫯⫰x = x → 0 < x.
* // * /2 width=1 by ylt_inj/ normalize
#H destruct
qed.
(* Properties on predecessor ************************************************)
-lemma ylt_pred: ∀m,n. m < n → 0 < m → ⫰m < ⫰n.
+lemma ylt_pred: ∀m,n:ynat. m < n → 0 < m → ⫰m < ⫰n.
#m #n * -m -n
/4 width=1 by ylt_inv_inj, ylt_inj, monotonic_lt_pred/
qed.
lemma ylt_succ_Y: ∀x. x < ∞ → ⫯x < ∞.
* /2 width=1 by/ qed.
-lemma yle_succ1_inj: ∀x,y. ⫯yinj x ≤ y → x < y.
+lemma yle_succ1_inj: ∀x. ∀y:ynat. ⫯yinj x ≤ y → x < y.
#x * /3 width=1 by yle_inv_inj, ylt_inj/
qed.
+lemma ylt_succ2_refl: ∀x,y:ynat. x < y → x < ⫯x.
+#x #y #H elim (ylt_fwd_gen … H) -y /2 width=1 by ylt_inj/
+qed.
+
(* Properties on order ******************************************************)
lemma yle_split_eq: ∀m,n:ynat. m ≤ n → m < n ∨ m = n.
]
qed-.
-lemma yle_inv_succ1_lt: ∀x,y. ⫯x ≤ y → 0 < y ∧ x ≤ ⫰y.
+lemma yle_inv_succ1_lt: ∀x,y:ynat. ⫯x ≤ y → 0 < y ∧ x ≤ ⫰y.
#x #y #H elim (yle_inv_succ1 … H) -H /3 width=1 by ylt_O1, conj/
qed-.
(* Inversion lemmas on successor *********************************************)
-lemma yplus_inv_succ_lt_dx: ∀x,y,z. 0 < y → x + y = ⫯z → x + ⫰y = z.
+lemma yplus_inv_succ_lt_dx: ∀x,y,z:ynat. 0 < y → x + y = ⫯z → x + ⫰y = z.
#x #y #z #H <(ylt_inv_O1 y) // >yplus_succ2
/2 width=1 by ysucc_inv_inj/
qed-.
-lemma yplus_inv_succ_lt_sn: ∀x,y,z. 0 < x → x + y = ⫯z → ⫰x + y = z.
+lemma yplus_inv_succ_lt_sn: ∀x,y,z:ynat. 0 < x → x + y = ⫯z → ⫰x + y = z.
#x #y #z #H <(ylt_inv_O1 x) // >yplus_succ1
/2 width=1 by ysucc_inv_inj/
(* the predecessor function *)
definition ypred: ynat → ynat ≝ λm. match m with
-[ yinj m ⇒ pred m
+[ yinj m ⇒ ⫰m
| Y ⇒ Y
].
interpretation "ynat predecessor" 'Predecessor m = (ypred m).
-lemma ypred_O: ⫰0 = 0.
+lemma ypred_O: ⫰(yinj 0) = yinj 0.
// qed.
-lemma ypred_S: ∀m:nat. ⫰(S m) = m.
+lemma ypred_S: ∀m:nat. ⫰(⫯m) = yinj m.
// qed.
lemma ypred_Y: (⫰∞) = ∞.
(* Inversion lemmas *********************************************************)
-lemma ypred_inv_refl: ∀m. ⫰m = m → m = 0 ∨ m = ∞.
+lemma ypred_inv_refl: ∀m:ynat. ⫰m = m → m = 0 ∨ m = ∞.
* // #m #H lapply (yinj_inj … H) -H (**) (* destruct lemma needed *)
/4 width=1 by pred_inv_refl, or_introl, eq_f/
qed-.
(* the successor function *)
definition ysucc: ynat → ynat ≝ λm. match m with
-[ yinj m ⇒ S m
+[ yinj m ⇒ ⫯m
| Y ⇒ Y
].
interpretation "ynat successor" 'Successor m = (ysucc m).
-lemma ysucc_inj: ∀m:nat. ⫯m = S m.
+lemma ysucc_inj: ∀m:nat. ⫯(yinj m) = yinj (⫯m).
// qed.
lemma ysucc_Y: ⫯(∞) = ∞.
lemma ypred_succ: ∀m. ⫰⫯m = m.
* // qed.
-lemma ynat_cases: ∀n:ynat. n = 0 ∨ ∃m. n = ⫯m.
+lemma ynat_cases: ∀n:ynat. n = 0 ∨ ∃m:ynat. n = ⫯m.
*
[ * /2 width=1 by or_introl/
#n @or_intror @(ex_intro … n) // (**) (* explicit constructor *)
#n #_ #H destruct
qed-.
-lemma ysucc_inv_O_dx: ∀m. ⫯m = 0 → ⊥.
+lemma ysucc_inv_O_dx: ∀m:ynat. ⫯m = 0 → ⊥.
/2 width=2 by ysucc_inv_O_sn/ qed-.
(* Eliminators **************************************************************)
["M"; "ℳ"; "𝕄"; "𝐌"; "Ⓜ"; ] ;
["n"; "𝕟"; "𝐧"; "𝛈"; "ⓝ"; ] ;
["N"; "ℕ"; "№"; "𝐍"; "Ⓝ"; ] ;
- ["o"; "θ"; "ϑ"; "𝕠"; "∘"; "ø"; "○"; "𝐨"; "𝛉"; "ⓞ"; ] ;
+ ["o"; "θ"; "ϑ"; "𝕠"; "∘"; "⊚"; "ø"; "○"; "𝐨"; "𝛉"; "ⓞ"; ] ;
["O"; "Θ"; "𝕆"; "𝐎"; "𝚯"; "𝚹"; "Ⓞ"; ] ;
["p"; "π"; "𝕡"; "𝐩"; "𝛑"; "ⓟ"; ] ;
["P"; "Π"; "℘"; "ℙ"; "𝐏"; "𝚷"; "Ⓟ"; ] ;
projects / helm.git / commitdiff