+++ /dev/null
-lemma length_inv_pos_dx_append: ∀d,L. |L| = d + 1 →
- ∃∃I,K,V. |K| = d & L = ⋆.ⓑ{I}V @@ K.
-#d @(nat_ind_plus … d) -d
-[ #L #H
- elim (length_inv_pos_dx … H) -H #I #K #V #H
- >(length_inv_zero_dx … H) -H #H destruct
- @ex2_3_intro [4: /2 width=2/ |5: // |1,2,3: skip ] (**) (* /3/ does not work *)
-| #d #IHd #L #H
- elim (length_inv_pos_dx … H) -H #I #K #V #H
- elim (IHd … H) -IHd -H #I0 #K0 #V0 #H1 #H2 #H3 destruct
- @(ex2_3_intro … (K0.ⓑ{I}V)) //
-]
-qed-.
-
-lemma length_inv_pos_sn_append: ∀d,L. 1 + d = |L| →
- ∃∃I,K,V. d = |K| & L = ⋆. ⓑ{I}V @@ K.
-#d >commutative_plus @(nat_ind_plus … d) -d
-[ #L #H elim (length_inv_pos_sn … H) -H #I #K #V #H1 #H2 destruct
- >(length_inv_zero_sn … H1) -K
- @(ex2_3_intro … (⋆)) // (**) (* explicit constructor *)
-| #d #IHd #L #H elim (length_inv_pos_sn … H) -H #I #K #V #H1 #H2 destruct
- >H1 in IHd; -H1 #IHd
- elim (IHd K) -IHd // #J #L #W #H1 #H2 destruct
- @(ex2_3_intro … (L.ⓑ{I}V)) // (**) (* explicit constructor *)
- >append_length /2 width=1/
-]
-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 "hvbox( T1 𝟙 break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'RTop $T1 $T2 }.
+
+include "basic_2/grammar/lenv_px.ma".
+
+(* POINTWISE EXTENSION OF TOP RELATION FOR TERMS ****************************)
+
+definition ttop: relation term ≝ λT1,T2. True.
+
+definition ltop: relation lenv ≝ lpx ttop.
+
+interpretation
+ "top reduction (environment)"
+ 'RTop L1 L2 = (ltop L1 L2).
+
+(* Basic properties *********************************************************)
+
+lemma ltop_refl: reflexive … ltop.
+/2 width=1/ qed.
+
+lemma ltop_sym: symmetric … ltop.
+/2 width=1/ qed.
+
+lemma ltop_trans: transitive … ltop.
+/2 width=3/ qed.
+
+lemma ltop_append: ∀K1,K2. K1 𝟙 K2 → ∀L1,L2. L1 𝟙 L2 → L1 @@ K1 𝟙 L2 @@ K2.
+/2 width=1/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma ltop_inv_atom1: ∀L2. ⋆ 𝟙 L2 → L2 = ⋆.
+/2 width=2 by lpx_inv_atom1/ qed-.
+
+lemma ltop_inv_pair1: ∀K1,I,V1,L2. K1. ⓑ{I} V1 𝟙 L2 →
+ ∃∃K2,V2. K1 𝟙 K2 & L2 = K2. ⓑ{I} V2.
+#K1 #I #V1 #L2 #H
+elim (lpx_inv_pair1 … H) -H /2 width=4/
+qed-.
+
+lemma ltop_inv_atom2: ∀L1. L1 𝟙 ⋆ → L1 = ⋆.
+/2 width=2 by lpx_inv_atom2/ qed-.
+
+lemma ltop_inv_pair2: ∀L1,K2,I,V2. L1 𝟙 K2. ⓑ{I} V2 →
+ ∃∃K1,V1. K1 𝟙 K2 & L1 = K1. ⓑ{I} V1.
+#L1 #K2 #I #V2 #H
+elim (lpx_inv_pair2 … H) -H /2 width=4/
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma ltop_fwd_length: ∀L1,L2. L1 𝟙 L2 → |L1| = |L2|.
+/2 width=2 by lpx_fwd_length/ 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/notation/relations/lazyor_4.ma".
-include "basic_2/relocation/lpx_sn.ma".
-include "basic_2/substitution/cofrees.ma".
-
-(* POINTWISE UNION FOR LOCAL ENVIRONMENTS ***********************************)
-
-inductive clor (T) (L2) (K1) (V1): predicate term ≝
-| clor_sn: |K1| < |L2| → K1 ⊢ |L2|-|K1|-1 ~ϵ 𝐅*[yinj 0]⦃T⦄ → clor T L2 K1 V1 V1
-| clor_dx: ∀I,K2,V2. |K1| < |L2| → (K1 ⊢ |L2|-|K1|-1 ~ϵ 𝐅*[yinj 0]⦃T⦄ → ⊥) →
- ⇩[|L2|-|K1|-1] L2 ≡ K2.ⓑ{I}V2 → clor T L2 K1 V1 V2
-.
-
-definition llor: relation4 term lenv lenv lenv ≝
- λT,L2. lpx_sn (clor T L2).
-
-interpretation
- "lazy union (local environment)"
- 'LazyOr L1 T L2 L = (llor T L2 L1 L).
-
-(* Basic properties *********************************************************)
-
-lemma llor_pair_sn: ∀I,L1,L2,L,V,T. L1 ⩖[T] L2 ≡ L →
- |L1| < |L2| → L1 ⊢ |L2|-|L1|-1 ~ϵ 𝐅*[yinj 0]⦃T⦄ →
- L1.ⓑ{I}V ⩖[T] L2 ≡ L.ⓑ{I}V.
-/3 width=2 by clor_sn, lpx_sn_pair/ qed.
-
-lemma llor_pair_dx: ∀I,J,L1,L2,L,K2,V1,V2,T. L1 ⩖[T] L2 ≡ L →
- |L1| < |L2| → (L1 ⊢ |L2|-|L1|-1 ~ϵ 𝐅*[yinj 0]⦃T⦄ → ⊥) →
- ⇩[|L2|-|L1|-1] L2 ≡ K2.ⓑ{J}V2 →
- L1.ⓑ{I}V1 ⩖[T] L2 ≡ L.ⓑ{I}V2.
-/4 width=3 by clor_dx, lpx_sn_pair/ qed.
-
-lemma llor_total: ∀T,L2,L1. |L1| ≤ |L2| → ∃L. L1 ⩖[T] L2 ≡ L.
-#T #L2 #L1 elim L1 -L1 /2 width=2 by ex_intro/
-#L1 #I1 #V1 #IHL1 normalize
-#H elim IHL1 -IHL1 /2 width=3 by transitive_le/
-#L #HT elim (cofrees_dec L1 T 0 (|L2|-|L1|-1))
-[ /3 width=2 by llor_pair_sn, ex_intro/
-| elim (ldrop_O1_lt (Ⓕ) L2 (|L2|-|L1|-1))
- /5 width=4 by llor_pair_dx, monotonic_lt_minus_l, ex_intro/
-]
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/relocation/lpx_sn_alt.ma".
-include "basic_2/substitution/llor.ma".
-
-(* POINTWISE UNION FOR LOCAL ENVIRONMENTS ***********************************)
-
-(* Alternative definition ***************************************************)
-
-theorem llor_intro_alt: ∀T,L2,L1,L. |L1| ≤ |L2| → |L1| = |L| →
- (∀I1,I,K1,K,V1,V,i. ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L ≡ K.ⓑ{I}V →
- (K1 ⊢ |L2|-|L1|+i ~ϵ 𝐅*[yinj 0]⦃T⦄ → I1 = I ∧ V1 = V) ∧
- (∀I2,K2,V2. (K1 ⊢ |L2|-|L1|+i ~ϵ 𝐅*[yinj 0]⦃T⦄ → ⊥) →
- ⇩[|L2|-|L1|+i] L2 ≡ K2.ⓑ{I2}V2 → I1 = I ∧ V2 = V
- )
- ) → L1 ⩖[T] L2 ≡ L.
-#T #L2 #L1 #L #HL12 #HL1 #IH @lpx_sn_intro_alt // -HL1
-#I1 #I #K1 #K #V1 #V #i #HLK1 #HLK
-lapply (ldrop_fwd_length_minus4 … HLK1)
-lapply (ldrop_fwd_length_le4 … HLK1)
-normalize in ⊢ (%→%→?); #HKL1 #Hi
-lapply (plus_minus_minus_be_aux … HL12 Hi) // -Hi <minus_plus #Hi
-lapply (transitive_le … HKL1 HL12) -HKL1 -HL12 #HKL1
-elim (IH … HLK1 HLK) -IH -HLK1 -HLK #IH1 #IH2
-elim (cofrees_dec K1 T 0 (|L2|-|L1|+i))
-[ -IH2 #HT elim (IH1 … HT) -IH1
- #HI1 #HV1 @conj // <HV1 -V @clor_sn // <Hi -Hi //
-| -IH1 #HnT elim (ldrop_O1_lt (Ⓕ) L2 (|L2|-|L1|+i)) /2 width=1 by monotonic_lt_minus_l/
- #I2 #K2 #V2 #HLK2 elim (IH2 … HLK2) -IH2 /2 width=1 by/
- #HI1 #HV2 @conj // <HV2 -V @(clor_dx … I2 K2) // <Hi -Hi /2 width=1 by/
-]
-qed.
-
-theorem llor_inv_alt: ∀T,L2,L1,L. L1 ⩖[T] L2 ≡ L → |L1| ≤ |L2| →
- |L1| = |L| ∧
- (∀I1,I,K1,K,V1,V,i.
- ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L ≡ K.ⓑ{I}V →
- (∧∧ K1 ⊢ |L2|-|L1|+i ~ϵ 𝐅*[yinj 0]⦃T⦄ & I1 = I & V1 = V) ∨
- (∃∃I2,K2,V2. (K1 ⊢ |L2|-|L1|+i ~ϵ 𝐅*[yinj 0]⦃T⦄ → ⊥) &
- ⇩[|L2|-|L1|+i] L2 ≡ K2.ⓑ{I2}V2 &
- I1 = I & V2 = V
- )
- ).
-#T #L2 #L1 #L #H #HL12 elim (lpx_sn_inv_alt … H) -H
-#HL1 #IH @conj // -HL1
-#I1 #I #K1 #K #V1 #V #i #HLK1 #HLK
-lapply (ldrop_fwd_length_minus4 … HLK1)
-lapply (ldrop_fwd_length_le4 … HLK1)
-normalize in ⊢ (%→%→?); #HKL1 #Hi
-lapply (plus_minus_minus_be_aux … HL12 Hi) // -HL12 -Hi -HKL1
-<minus_plus #Hi >Hi -Hi
-elim (IH … HLK1 HLK) -IH #HI1 *
-/4 width=5 by or_introl, or_intror, and3_intro, ex4_3_intro/
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/relocation/llor.ma".
-include "basic_2/computation/cpxs_lleq.ma".
-include "basic_2/computation/lpxs_ldrop.ma".
-include "basic_2/computation/lpxs_cpxs.ma".
-include "basic_2/computation/lpxs_lpxs.ma".
-
-(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
-
-axiom llor_fwd_sort: ∀L1,L2,L,d,k. L1 ⩖ [⋆k, d] L2 ≡ L → L = L2.
-
-axiom llor_fwd_lref: ∀L1,L2,L,d,i. L1 ⩖ [#i, d] L2 ≡ L →
- ∨∨ (|L| ≤ i ∧ L = L2)
- | (yinj i < d ∧ L = L2)
- | ∃∃I1,I2,K1,K2,K,V1,V2. ⇩[i] L1 ≡ K1.ⓑ{I1}V1 &
- ⇩[i] L2 ≡ K2.ⓑ{I2}V2 &
- ⇩[i] L ≡ K.ⓑ{I2}V1 &
- L2 ≃[yinj 0, yinj i] L &
- K1 ⩖[V1, yinj 0] K2 ≡ K &
- d ≤ yinj i.
-
-
-axiom llor_fwd_lref_lt: ∀L1,L2,L,d,i. L1 ⩖ [#i, d] L2 ≡ L → i < d → L = L2.
-
-axiom llor_inv_lref_be: ∀L1,L2,L,d,i. L1 ⩖ [#i, d] L2 ≡ L → d ≤ i →
- ∀I1,I2,K1,K2,V1,V2. ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
- ∃∃K. ⇩[i] L ≡ K.ⓑ{I2}V1 & L2 ≃[0, i] L &
- K1 ⩖[V1, 0] K2 ≡ K.
-
-axiom llor_fwd_gref: ∀L1,L2,L,d,p. L1 ⩖ [§p, d] L2 ≡ L → L = L2.
-
-axiom llor_inv_bind: ∀a,I,L1,L2,L,V,T,d. L1 ⩖ [ⓑ{a,I}V.T, d] L2 ≡ L →
- ∃∃L0. L1 ⩖ [V, d] L2 ≡ L0 & L1.ⓑ{I}V ⩖ [T, ⫯d] L0.ⓑ{I}V ≡ L.ⓑ{I}V.
-
-axiom llor_inv_flat: ∀I,L1,L2,L,V,T,d. L1 ⩖ [ⓕ{I}V.T, d] L2 ≡ L →
- ∃∃L0. L1 ⩖ [V, d] L2 ≡ L0 & L1 ⩖ [T, d] L0 ≡ L.
-
-axiom llor_fwd_length_13: ∀L1,L2,L,T,d. L1 ⩖ [T, d] L2 ≡ L → |L1| = |L|.
-
-(* Properties obn lazy union for local environments *************************)
-
-lemma lpxs_llor_sn: ∀h,g,G,L1s,L0,L1d,T,d. L1s ⩖[T, d] L0 ≡ L1d →
- ∀L2s,L2d. L2s ⩖[T, d] L0 ≡ L2d →
- ⦃G, L1s⦄ ⊢ ➡*[h, g] L2s → ⦃G, L1d⦄ ⊢ ➡*[h, g] L2d.
-#h #g #G #L1s #L0 #L1d #T #d #H elim H -L1s -L0 -L1d -T -d
-[ #L1s #L0 #d #k #_ #L2s #L2d #H #_ >(llor_fwd_sort … H) //
-| #L1s #L0 #d #i #_ #Hid #L2s #L2d #H #_ >(llor_fwd_lref_lt … H) //
-| #I1s #I0 #L1s #L0 #L1d #K1s #K0 #K1d #V1s #V0 #d #i #Hdi #HLK1s #HLK0 #HLK1d #HL01d #HV1s #IHV1s #L2s #L2d #H #HL12s
- elim (lpxs_ldrop_conf … HLK1s … HL12s) -L1s #Y #H #HLK2s
- elim (lpxs_inv_pair1 … H) -H #K2s #V2s #HK12s #HV12s #H destruct
- elim (llor_inv_lref_be … H … HLK2s HLK0) // -L2s -HLK0 -Hdi #K2d #HLK2d #HL02d #HV2s
- lapply (leq_canc_sn … HL01d … HL02d) -L0 #HL12d
- lapply (IHV1s … K2d … HK12s) -IHV1s -HK12s [2: #HK12d
-
-
-
-
-[ #I2d #I1s #L2d #L1s #L2s #K2d #K1s #K2s #V2d #V1s #d #i #Hdi #HLK2d #HLK1s #HLK2s #HL12s #_ #IHV2s #L1d #HL1sd #HL12d
- elim (lpxs_ldrop_trans_O1 … HL12d … HLK2d) -L2d #Y #HLK1d #H
- elim (lpxs_inv_pair2 … H) -H #K1d #V1d #HK12d #HV12d #H destruct
- elim (lleq_inv_lref_ge … HL1sd … HLK1s HLK1d) // -d -I2d #H #HV1d destruct
- lapply (lleq_cpxs_conf_dx … HV12d … HV1d) #HV2d
- lapply (lleq_cpxs_trans … HV12d … HV1d) -HV12d -HV1d #HV12d
- lapply (IHV2s … HV2d HK12d) -L1d -K1d -K2d #HK12s
- elim (ldrop_lpxs_trans h g G … HLK1s (K2s.ⓑ{I1s}V2d)) /2 width=1 by lpxs_pair/ -V1d -K1s #Y #HL1sY #HYK2s #H
- lapply (leq_canc_sn … HL12s … H) -HL12s -H #HL2sY
- lapply (ldrop_O_inj … HLK2s HYK2s) -I1s -K2s -V2d #H
- lapply (leq_join … HL2sY … H) -HL2sY -H #HL2sY
- >(leq_inv_O_Y … HL2sY) -HL2sY //
-
-
-
-
-
-lemma lleq_lpxs_trans_llor: ∀h,g,G,L1s,L2s,L2d,T,d. L2d ⩖[T, d] L1s ≡ L2s →
- ∀L1d. L1s ⋕[T, d] L1d → ⦃G, L1d⦄ ⊢ ➡*[h, g] L2d → ⦃G, L1s⦄ ⊢ ➡*[h, g] L2s.
-#h #g #G #L1s #L2s #L2d #T #d #H elim H -L1s -L2s -L2d -T -d //
-[ #I2d #I1s #L2d #L1s #L2s #K2d #K1s #K2s #V2d #V1s #d #i #Hdi #HLK2d #HLK1s #HLK2s #HL12s #_ #IHV2s #L1d #HL1sd #HL12d
- elim (lpxs_ldrop_trans_O1 … HL12d … HLK2d) -L2d #Y #HLK1d #H
- elim (lpxs_inv_pair2 … H) -H #K1d #V1d #HK12d #HV12d #H destruct
- elim (lleq_inv_lref_ge … HL1sd … HLK1s HLK1d) // -d -I2d #H #HV1d destruct
- lapply (lleq_cpxs_conf_dx … HV12d … HV1d) #HV2d
- lapply (lleq_cpxs_trans … HV12d … HV1d) -HV12d -HV1d #HV12d
- lapply (IHV2s … HV2d HK12d) -L1d -K1d -K2d #HK12s
- elim (ldrop_lpxs_trans h g G … HLK1s (K2s.ⓑ{I1s}V2d)) /2 width=1 by lpxs_pair/ -V1d -K1s #Y #HL1sY #HYK2s #H
- lapply (leq_canc_sn … HL12s … H) -HL12s -H #HL2sY
- lapply (ldrop_O_inj … HLK2s HYK2s) -I1s -K2s -V2d #H
- lapply (leq_join … HL2sY … H) -HL2sY -H #HL2sY
- >(leq_inv_O_Y … HL2sY) -HL2sY //
-(*
-| #a #I #L2d #L1s #L0 #L2s #V #T #d #H0 #_ #IHV #IHT #L1d #H #HL12d
- elim (lleq_inv_bind … H) -H #HV #HT
-*)
-| #I #L2d #L1s #LV #LT #L2s #V #T #d #H0 #_ #_ #IHV #IHT #IH #L1d #H #HL12d
- elim (lleq_inv_flat … H) -H #HV #HT
- lapply (IHV … HV HL12d) -HV #H1
- lapply (IHT … HT HL12d) #H2
-
-
-
- @(lpxs_trans … LV) /2 width=3 by/ -IHV
- lapply (IHT … HL12d) // -IHT #H @(IH … H) -IH -H
-
- @(IH … HL12d) -IHT -IHV
-
- /4 width=5 by lpxs_trans/
-
-
-lemma lleq_lpx_conf_llor: ∀h,g,G,L1,L2,T,d. L1 ⋕[T, d] L2 → ∀K1. ⦃G, L1⦄ ⊢ ➡[h, g] K1 →
- ∀K2. K1 ⩖[T, d] L2 ≡ K2 → ⦃G, L2⦄ ⊢ ➡[h, g] K2.
-#h #g #G #L1 #L2 #T #d #H @(lleq_ind_alt … H) -L1 -L2 -T -d
-[ #L1 #L2 #d #k #HL12 #K1 #HLK1 #K2 #H
+++ /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 "hvbox( T1 𝟙 break term 46 T2 )"
- non associative with precedence 45
- for @{ 'RTop $T1 $T2 }.
-
-include "basic_2/grammar/lenv_px.ma".
-
-(* POINTWISE EXTENSION OF TOP RELATION FOR TERMS ****************************)
-
-definition ttop: relation term ≝ λT1,T2. True.
-
-definition ltop: relation lenv ≝ lpx ttop.
-
-interpretation
- "top reduction (environment)"
- 'RTop L1 L2 = (ltop L1 L2).
-
-(* Basic properties *********************************************************)
-
-lemma ltop_refl: reflexive … ltop.
-/2 width=1/ qed.
-
-lemma ltop_sym: symmetric … ltop.
-/2 width=1/ qed.
-
-lemma ltop_trans: transitive … ltop.
-/2 width=3/ qed.
-
-lemma ltop_append: ∀K1,K2. K1 𝟙 K2 → ∀L1,L2. L1 𝟙 L2 → L1 @@ K1 𝟙 L2 @@ K2.
-/2 width=1/ qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma ltop_inv_atom1: ∀L2. ⋆ 𝟙 L2 → L2 = ⋆.
-/2 width=2 by lpx_inv_atom1/ qed-.
-
-lemma ltop_inv_pair1: ∀K1,I,V1,L2. K1. ⓑ{I} V1 𝟙 L2 →
- ∃∃K2,V2. K1 𝟙 K2 & L2 = K2. ⓑ{I} V2.
-#K1 #I #V1 #L2 #H
-elim (lpx_inv_pair1 … H) -H /2 width=4/
-qed-.
-
-lemma ltop_inv_atom2: ∀L1. L1 𝟙 ⋆ → L1 = ⋆.
-/2 width=2 by lpx_inv_atom2/ qed-.
-
-lemma ltop_inv_pair2: ∀L1,K2,I,V2. L1 𝟙 K2. ⓑ{I} V2 →
- ∃∃K1,V1. K1 𝟙 K2 & L1 = K1. ⓑ{I} V1.
-#L1 #K2 #I #V2 #H
-elim (lpx_inv_pair2 … H) -H /2 width=4/
-qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma ltop_fwd_length: ∀L1,L2. L1 𝟙 L2 → |L1| = |L2|.
-/2 width=2 by lpx_fwd_length/ qed-.
#I #L #K #V #H elim (append_inj_dx … (⋆.ⓑ{I}V) … H) //
qed-.
+lemma length_inv_pos_dx_ltail: ∀L,d. |L| = d + 1 →
+ ∃∃I,K,V. |K| = d & L = ⓑ{I}V.K.
+#Y #d #H elim (length_inv_pos_dx … H) -H #I #L #V #Hd #HLK destruct
+elim (lpair_ltail L I V) /2 width=5 by ex2_3_intro/
+qed-.
+
+lemma length_inv_pos_sn_ltail: ∀L,d. d + 1 = |L| →
+ ∃∃I,K,V. d = |K| & L = ⓑ{I}V.K.
+#Y #d #H elim (length_inv_pos_sn … H) -H #I #L #V #Hd #HLK destruct
+elim (lpair_ltail L I V) /2 width=5 by ex2_3_intro/
+qed-.
+
(* Basic_eliminators ********************************************************)
(* Basic_1: was: c_tail_ind *)
--- /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/ldrop_append.ma".
+include "basic_2/multiple/frees.ma".
+
+(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
+
+(* Properties on append for local environments ******************************)
+
+lemma frees_append: ∀L2,U,d,i. L2 ⊢ i ϵ 𝐅*[d]⦃U⦄ → i ≤ |L2| →
+ ∀L1. L1 @@ L2 ⊢ i ϵ 𝐅*[d]⦃U⦄.
+#L2 #U #d #i #H elim H -L2 -U -d -i /3 width=2 by frees_eq/
+#I #L2 #K2 #U #W #d #i #j #Hdj #Hji #HnU #HLK2 #_ #IHW #Hi #L1
+lapply (ldrop_fwd_length_minus2 … HLK2) normalize #H0
+lapply (ldrop_O1_append_sn_le … HLK2 … L1) -HLK2
+[ -I -L1 -K2 -U -W -d /3 width=3 by lt_to_le, lt_to_le_to_lt/
+| #HLK2 @(frees_be … HnU HLK2) // -HnU -HLK2 @IHW -IHW
+ >(minus_plus_m_m (|K2|) 1) >H0 -H0 /2 width=1 by monotonic_le_minus_l2/
+]
+qed.
+
+(* Inversion lemmas on append for local environments ************************)
+
+fact frees_inv_append_aux: ∀L,U,d,i. L ⊢ i ϵ 𝐅*[d]⦃U⦄ → ∀L1,L2. L = L1 @@ L2 →
+ i ≤ |L2| → L2 ⊢ i ϵ 𝐅*[d]⦃U⦄.
+#L #U #d #i #H elim H -L -U -d -i /3 width=2 by frees_eq/
+#Z #L #Y #U #X #d #i #j #Hdj #Hji #HnU #HLY #_ #IHW #L1 #L2 #H #Hi destruct
+elim (ldrop_O1_lt (Ⓕ) L2 j) [2: -Z -Y -L1 -X -U -d /2 width=3 by lt_to_le_to_lt/ ]
+#I #K2 #W #HLK2 lapply (ldrop_fwd_length_minus2 … HLK2) normalize #H0
+lapply (ldrop_O1_inv_append1_le … HLY … HLK2) -HLY
+[ -Z -I -Y -K2 -L1 -X -U -W -d /3 width=3 by lt_to_le, lt_to_le_to_lt/
+| normalize #H destruct
+ @(frees_be … HnU HLK2) -HnU -HLK2 // @IHW -IHW //
+ >(minus_plus_m_m (|K2|) 1) >H0 -H0 /2 width=1 by monotonic_le_minus_l2/
+]
+qed-.
+
+lemma frees_inv_append: ∀L1,L2,U,d,i. L1 @@ L2 ⊢ i ϵ 𝐅*[d]⦃U⦄ →
+ i ≤ |L2| → L2 ⊢ i ϵ 𝐅*[d]⦃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/multiple/frees_append.ma".
+include "basic_2/multiple/llor.ma".
+
+(* POINTWISE UNION FOR LOCAL ENVIRONMENTS ***********************************)
+
+(* Alternative definition ***************************************************)
+
+lemma llor_tail_frees: ∀L1,L2,L,U,d. L1 ⩖[U, d] L2 ≡ L → d ≤ yinj (|L1|) →
+ ∀I1,W1. ⓑ{I1}W1.L1 ⊢ |L1| ϵ 𝐅*[d]⦃U⦄ →
+ ∀I2,W2. ⓑ{I1}W1.L1 ⩖[U, d] ⓑ{I2}W2.L2 ≡ ⓑ{I2}W2.L.
+#L1 #L2 #L #U #d * #HL12 #HL1 #IH #Hd #I1 #W1 #HU #I2 #W2
+@and3_intro [1,2: >ltail_length /2 width=1 by le_S_S/ ]
+#J1 #J2 #J #K1 #K2 #K #V1 #V2 #V #i #HLK1 #HLK2 #HLK
+lapply (ldrop_fwd_length_lt2 … HLK1) >ltail_length #H
+lapply (lt_plus_SO_to_le … H) -H #H
+elim (le_to_or_lt_eq … H) -H #H
+[ elim (ldrop_O1_lt (Ⓕ) … H) #Z1 #Y1 #X1 #HLY1
+ elim (ldrop_O1_lt (Ⓕ) L2 i) // #Z2 #Y2 #X2 #HLY2
+ elim (ldrop_O1_lt (Ⓕ) L i) // #Z #Y #X #HLY
+ lapply (ldrop_O1_inv_append1_le … HLK1 … HLY1) /2 width=1 by lt_to_le/ -HLK1 normalize #H destruct
+ lapply (ldrop_O1_inv_append1_le … HLK2 … HLY2) /2 width=1 by lt_to_le/ -HLK2 normalize #H destruct
+ lapply (ldrop_O1_inv_append1_le … HLK … HLY) /2 width=1 by lt_to_le/ -HLK normalize #H destruct
+ elim (IH … HLY1 HLY2 HLY) -IH -HLY1 -HLY2 -HLY *
+ [ /3 width=1 by and3_intro, or3_intro0/
+ | /6 width=2 by frees_inv_append, lt_to_le, or3_intro1, and3_intro/
+ | /5 width=1 by frees_append, lt_to_le, or3_intro2, and4_intro/
+ ]
+| -IH -HLK1 destruct
+ lapply (ldrop_O1_inv_append1_le … HLK2 … (⋆) ?) // -HLK2 normalize #H destruct
+ lapply (ldrop_O1_inv_append1_le … HLK … (⋆) ?) // -HLK normalize #H destruct
+ /3 width=1 by or3_intro2, and4_intro/
+]
+qed.
+
+lemma llor_tail_cofrees: ∀L1,L2,L,U,d. L1 ⩖[U, d] L2 ≡ L →
+ ∀I1,W1. (ⓑ{I1}W1.L1 ⊢ |L1| ϵ 𝐅*[d]⦃U⦄ → ⊥) →
+ ∀I2,W2. ⓑ{I1}W1.L1 ⩖[U, d] ⓑ{I2}W2.L2 ≡ ⓑ{I1}W1.L.
+#L1 #L2 #L #U #d * #HL12 #HL1 #IH #I1 #W1 #HU #I2 #W2
+@and3_intro [1,2: >ltail_length /2 width=1 by le_S_S/ ]
+#J1 #J2 #J #K1 #K2 #K #V1 #V2 #V #i #HLK1 #HLK2 #HLK
+lapply (ldrop_fwd_length_lt2 … HLK1) >ltail_length #H
+lapply (lt_plus_SO_to_le … H) -H #H
+elim (le_to_or_lt_eq … H) -H #H
+[ elim (ldrop_O1_lt (Ⓕ) … H) #Z1 #Y1 #X1 #HLY1
+ elim (ldrop_O1_lt (Ⓕ) L2 i) // #Z2 #Y2 #X2 #HLY2
+ elim (ldrop_O1_lt (Ⓕ) L i) // #Z #Y #X #HLY
+ lapply (ldrop_O1_inv_append1_le … HLK1 … HLY1) /2 width=1 by lt_to_le/ -HLK1 normalize #H destruct
+ lapply (ldrop_O1_inv_append1_le … HLK2 … HLY2) /2 width=1 by lt_to_le/ -HLK2 normalize #H destruct
+ lapply (ldrop_O1_inv_append1_le … HLK … HLY) /2 width=1 by lt_to_le/ -HLK normalize #H destruct
+ elim (IH … HLY1 HLY2 HLY) -IH -HLY1 -HLY2 -HLY *
+ [ /3 width=1 by and3_intro, or3_intro0/
+ | /6 width=2 by frees_inv_append, lt_to_le, or3_intro1, and3_intro/
+ | /5 width=1 by frees_append, lt_to_le, or3_intro2, and4_intro/
+ ]
+| -IH -HLK2 destruct
+ lapply (ldrop_O1_inv_append1_le … HLK1 … (⋆) ?) // -HLK1 normalize #H destruct
+ lapply (ldrop_O1_inv_append1_le … HLK … (⋆) ?) // -HLK normalize #H destruct
+ /4 width=1 by or3_intro1, and3_intro/
+]
+qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/substitution/ldrop_append.ma".
-include "basic_2/multiple/llor_ldrop.ma".
-
-(* POINTWISE UNION FOR LOCAL ENVIRONMENTS ***********************************)
-
-lemma lt_plus_SO_to_le: ∀x,y. x < y + 1 → x ≤ y.
-/2 width=1 by monotonic_pred/ qed-.
-
-
-lemma llor_tail_frees: ∀L1,L2,L,U,d. L1 ⩖[U, d] L2 ≡ L → d < yinj (|L1|) →
- ∀I1,W1. ⓑ{I1}W1.L1 ⊢ |L1| ϵ 𝐅*[d]⦃U⦄ →
- ∀I2,W2. ⓑ{I1}W1.L1 ⩖[U, d] ⓑ{I2}W2.L2 ≡ ⓑ{I2}W2.L.
-#L1 #L2 #L #U #d * #HL12 #HL1 #IH #Hd #I1 #W1 #HU #I2 #W2
-@and3_intro [1,2: >ltail_length /2 width=1 by le_S_S/ ]
-#J1 #J2 #J #K1 #K2 #K #V1 #V2 #V #i #HLK1 #HLK2 #HLK
-lapply (ldrop_fwd_length_lt2 … HLK1) >ltail_length #H
-lapply (lt_plus_SO_to_le … H) -H #H
-elim (le_to_or_lt_eq … H) -H #H
-[ elim (ldrop_O1_lt (Ⓕ) … H) #Z1 #Y1 #X1 #HLY1
- elim (ldrop_O1_lt (Ⓕ) L2 i) [2: /2 width=3 by lt_to_le_to_lt/ ] #Z2 #Y2 #X2 #HLY2
- elim (ldrop_O1_lt (Ⓕ) L i) // #Z #Y #X #HLY
- lapply (ldrop_O1_inv_append1_le … HLK1 … HLY1) /2 width=1 by lt_to_le/ -HLK1 normalize #H destruct
- lapply (ldrop_O1_inv_append1_le … HLK2 … HLY2) /3 width=3 by lt_to_le_to_lt, lt_to_le/ -HLK2 normalize #H destruct
- lapply (ldrop_O1_inv_append1_le … HLK … HLY) /2 width=1 by lt_to_le/ -HLK normalize #H destruct
- elim (IH … HLY1 HLY2 HLY) -IH -HLY1 -HLY2 -HLY *
- [ /3 width=1 by and3_intro, or3_intro0/
- | #HnU #HZ #HX
- | #Hdi #H2U #HZ #HX
- ]
-| -IH -HLK1 destruct
- lapply (ldrop_O1_inv_append1_le … HLK2 … (⋆) ?) // -HLK2 normalize #H destruct
- lapply (ldrop_O1_inv_append1_le … HLK … (⋆) ?) // -HLK normalize #H destruct
- /4 width=1 by ylt_fwd_le, or3_intro2, and4_intro/
-]
(**************************************************************************)
include "basic_2/multiple/frees_lift.ma".
-include "basic_2/multiple/llor.ma".
+include "basic_2/multiple/llor_alt.ma".
(* POINTWISE UNION FOR LOCAL ENVIRONMENTS ***********************************)
/5 width=3 by ylt_yle_trans, ylt_inj, or3_intro0, and3_intro/
qed.
-axiom llor_total: ∀L1,L2,T,d. |L1| = |L2| → ∃L. L1 ⩖[T, d] L2 ≡ L.
+lemma llor_total: ∀L1,L2,T,d. |L1| = |L2| → ∃L. L1 ⩖[T, d] L2 ≡ L.
+#L1 @(lenv_ind_alt … L1) -L1
+[ #L2 #T #d #H >(length_inv_zero_sn … H) -L2 /2 width=2 by ex_intro/
+| #I1 #L1 #V1 #IHL1 #Y #T #d >ltail_length #H
+ elim (length_inv_pos_sn_ltail … H) -H #I2 #L2 #V2 #HL12 #H destruct
+ elim (ylt_split d (|ⓑ{I1}V1.L1|))
+ [ elim (frees_dec (ⓑ{I1}V1.L1) T d (|L1|)) #HnU
+ elim (IHL1 L2 T d) // -IHL1 -HL12
+ [ #L #HL12 >ltail_length /4 width=2 by llor_tail_frees, ylt_fwd_succ2, ex_intro/
+ | /4 width=2 by llor_tail_cofrees, ex_intro/
+ ]
+ | -IHL1 /4 width=3 by llor_skip, plus_to_minus, ex_intro/
+ ]
+]
+qed-.
for native type assignment.
</news>
<news date="In progress.">
- Closure of native validity
- for context-sensitive extended computation.
+ Preservation of stratified native validity
+ for "big tree" computation on closures.
+ </news>
+ <news date="2014 June 9.">
+ "Big tree" strong normalization
+ for simply typed terms.
</news>
<news date="2014 April 16.">
lazy equivalence on local environments
- serves as irrelevant step in "big tree" computation
+ serves as irrelevant step in "big tree" computation on closures
(anniversary milestone).
</news>
<news date="2014 January 20.">
}
]
[ { "\"big tree\" parallel computation" * } {
- [ "fpbg ( â¦\83?,?,?â¦\84 >â\8b\95[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fleq" + "fpbg_fpbg" * ]
- [ "fpbc ( â¦\83?,?,?â¦\84 â\89»â\8b\95[?,?] ⦃?,?,?⦄ )" "fpbc_fleq" + "fpbc_fpbs" * ]
+ [ "fpbg ( â¦\83?,?,?â¦\84 >â\89¡[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fleq" + "fpbg_fpbg" * ]
+ [ "fpbc ( â¦\83?,?,?â¦\84 â\89»â\89¡[?,?] ⦃?,?,?⦄ )" "fpbc_fleq" + "fpbc_fpbs" * ]
[ "fpbu ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpbu_lift" + "fpbu_lleq" "fpbu_fleq" * ]
[ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_fleq" + "fpbs_aaa" + "fpbs_fpbs" + "fpbs_ext" * ]
}
class "yellow"
[ { "multiple substitution" * } {
[ { "lazy equivalence" * } {
- [ "fleq ( â¦\83?,?,?â¦\84 â\8b\95[?] ⦃?,?,?⦄ )" "fleq_fleq" * ]
- [ "lleq ( ? â\8b\95[?,?] ? )" "lleq_alt" + "lleq_alt_rec" + "lleq_leq" + "lleq_ldrop" + "lleq_fqus" + "lleq_llor" + "lleq_lleq" * ]
+ [ "fleq ( â¦\83?,?,?â¦\84 â\89¡[?] ⦃?,?,?⦄ )" "fleq_fleq" * ]
+ [ "lleq ( ? â\89¡[?,?] ? )" "lleq_alt" + "lleq_alt_rec" + "lleq_leq" + "lleq_ldrop" + "lleq_fqus" + "lleq_llor" + "lleq_lleq" * ]
}
]
[ { "lazy pointwise extension of a relation" * } {
}
]
[ { "pointwise union for local environments" * } {
- [ "llor ( ? ⩖[?,?] ? ≡ ? )" "llor_ldrop" * ]
+ [ "llor ( ? ⩖[?,?] ? ≡ ? )" "llor_alt" + "llor_ldrop" * ]
}
]
[ { "context-sensitive exclusion from free variables" * } {
- [ "frees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ )" "frees_leq" + "frees_lift" * ]
+ [ "frees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ )" "frees_append" + "frees_leq" + "frees_lift" * ]
}
]
[ { "contxt-sensitive extended multiple substitution" * } {
(* Properties ***************************************************************)
+axiom eq_nat_dec: ∀n1,n2:nat. Decidable (n1 = n2).
+
+axiom lt_dec: ∀n1,n2. Decidable (n1 < n2).
+
+lemma lt_or_eq_or_gt: ∀m,n. ∨∨ m < n | n = m | n < m.
+#m #n elim (lt_or_ge m n) /2 width=1 by or3_intro0/
+#H elim H -m /2 width=1 by or3_intro1/
+#m #Hm * /3 width=1 by not_le_to_lt, le_S_S, or3_intro2/
+qed-.
+
fact le_repl_sn_conf_aux: ∀x,y,z:nat. x ≤ z → x = y → y ≤ z.
// qed-.
(* Inversion & forward lemmas ***********************************************)
-axiom eq_nat_dec: ∀n1,n2:nat. Decidable (n1 = n2).
-
-axiom lt_dec: ∀n1,n2. Decidable (n1 < n2).
-
-lemma lt_or_eq_or_gt: ∀m,n. ∨∨ m < n | n = m | n < m.
-#m #n elim (lt_or_ge m n) /2 width=1 by or3_intro0/
-#H elim H -m /2 width=1 by or3_intro1/
-#m #Hm * /3 width=1 by not_le_to_lt, le_S_S, or3_intro2/
-qed-.
+lemma lt_plus_SO_to_le: ∀x,y. x < y + 1 → x ≤ y.
+/2 width=1 by monotonic_pred/ qed-.
lemma lt_refl_false: ∀n. n < n → ⊥.
#n #H elim (lt_to_not_eq … H) -H /2 width=1 by/
projects / helm.git / commitdiff