+++ /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( L1 ⋕ break [ term 46 T ] break term 46 L2 )"
- non associative with precedence 45
- for @{ 'LazyEq $T $L1 $L2 }.
--- /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( L1 ⋕ break [ term 46 d , break term 46 T ] break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'LazyEq $d $T $L1 $L2 }.
+++ /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/lleq_lleq.ma".
-include "basic_2/relocation/fqu.ma".
-
-(* SUPCLOSURE ***************************************************************)
-
-(* Advanced properties ******************************************************)
-
-lemma lleq_fqu_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃ ⦃G2, K2, U⦄ →
- ∀L1. L1 ⋕[T] L2 →
- ∃∃K1. ⦃G1, L1, T⦄ ⊃ ⦃G2, K1, U⦄ & K1 ⋕[U] K2.
-#G1 #G2 #L2 #K2 #T #U #H elim H -G1 -G2 -L2 -K2 -T -U
-[ #I #G #L2 #V #L1 #H elim (lleq_inv_lref_dx … H I L2 V) -H //
- #K1 #H1 #H2 lapply (ldrop_inv_O2 … H1) -H1
- #H destruct /2 width=3 by fqu_lref_O, ex2_intro/
-| * [ #a ] #I #G #L2 #V #T #L1 #H
- [ elim (lleq_inv_bind … H)
- | elim (lleq_inv_flat … H)
- ] -H
- /2 width=3 by fqu_pair_sn, ex2_intro/
-| #a #I #G #L2 #V #T #L1 #H elim (lleq_inv_bind … H) -H
- /2 width=3 by fqu_bind_dx, ex2_intro/
-| #I #G #L2 #V #T #L1 #H elim (lleq_inv_flat … H) -H
- /2 width=3 by fqu_flat_dx, ex2_intro/
-| #G #L2 #K2 #T #U #e #HLK2 #HTU #L1 #HL12
- elim (ldrop_O1_le (e+1) L1)
- [ /3 width=11 by fqu_drop, lleq_inv_lift, ex2_intro/
- | lapply (ldrop_fwd_length_le2 … HLK2) -K2
- lapply (lleq_fwd_length … HL12) -T -U //
- ]
-]
-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/lleq_lleq.ma".
+include "basic_2/relocation/fqu.ma".
+
+(* SUPCLOSURE ***************************************************************)
+
+(* Properties on lazy equivalence for local environments ********************)
+
+lemma lleq_fqu_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃ ⦃G2, K2, U⦄ →
+ ∀L1. L1 ⋕[0, T] L2 →
+ ∃∃K1. ⦃G1, L1, T⦄ ⊃ ⦃G2, K1, U⦄ & K1 ⋕[0, U] K2.
+#G1 #G2 #L2 #K2 #T #U #H elim H -G1 -G2 -L2 -K2 -T -U
+[ #I #G #L2 #V #L1 #H elim (lleq_inv_lref_ge_dx … H … I L2 V) -H //
+ #K1 #H1 #H2 lapply (ldrop_inv_O2 … H1) -H1
+ #H destruct /2 width=3 by fqu_lref_O, ex2_intro/
+| * [ #a ] #I #G #L2 #V #T #L1 #H
+ [ elim (lleq_inv_bind … H)
+ | elim (lleq_inv_flat … H)
+ ] -H
+ /2 width=3 by fqu_pair_sn, ex2_intro/
+| #a #I #G #L2 #V #T #L1 #H elim (lleq_inv_bind_O … H) -H
+ #H3 #H4 /2 width=3 by fqu_bind_dx, ex2_intro/
+| #I #G #L2 #V #T #L1 #H elim (lleq_inv_flat … H) -H
+ /2 width=3 by fqu_flat_dx, ex2_intro/
+| #G #L2 #K2 #T #U #e #HLK2 #HTU #L1 #HL12
+ elim (ldrop_O1_le (e+1) L1)
+ [ /3 width=12 by fqu_drop, lleq_inv_lift_le, ex2_intro/
+ | lapply (ldrop_fwd_length_le2 … HLK2) -K2
+ lapply (lleq_fwd_length … HL12) -T -U //
+ ]
+]
+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/fqu_fqu.ma".
-include "basic_2/relocation/fquq_alt.ma".
-
-(* OPTIONAL SUPCLOSURE ******************************************************)
-
-(* Advanced properties ******************************************************)
-
-lemma lleq_fquq_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃⸮ ⦃G2, K2, U⦄ →
- ∀L1. L1 ⋕[T] L2 →
- ∃∃K1. ⦃G1, L1, T⦄ ⊃⸮ ⦃G2, K1, U⦄ & K1 ⋕[U] K2.
-#G1 #G2 #L2 #K2 #T #U #H #L1 #HL12 elim(fquq_inv_gen … H) -H
-[ #H elim (lleq_fqu_trans … H … HL12) -L2 /3 width=3 by fqu_fquq, ex2_intro/
-| * #HG #HL #HT destruct /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 "basic_2/relocation/fqu_lleq.ma".
+include "basic_2/relocation/fquq_alt.ma".
+
+(* OPTIONAL SUPCLOSURE ******************************************************)
+
+(* Properties on lazy equivalence for local environments ********************)
+
+lemma lleq_fquq_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃⸮ ⦃G2, K2, U⦄ →
+ ∀L1. L1 ⋕[0, T] L2 →
+ ∃∃K1. ⦃G1, L1, T⦄ ⊃⸮ ⦃G2, K1, U⦄ & K1 ⋕[0, U] K2.
+#G1 #G2 #L2 #K2 #T #U #H #L1 #HL12 elim(fquq_inv_gen … H) -H
+[ #H elim (lleq_fqu_trans … H … HL12) -L2 /3 width=3 by fqu_fquq, ex2_intro/
+| * #HG #HL #HT destruct /2 width=3 by ex2_intro/
+]
+qed-.
include "basic_2/grammar/cl_restricted_weight.ma".
include "basic_2/relocation/lift.ma".
-(* LOCAL ENVIRONMENT SLICING ************************************************)
+(* BASIC SLICING FOR LOCAL ENVIRONMENTS *************************************)
(* Basic_1: includes: drop_skip_bind *)
inductive ldrop: relation4 nat nat lenv lenv ≝
ldrop (d + 1) e (L1. ⓑ{I} V1) (L2. ⓑ{I} V2)
.
-interpretation "local slicing" 'RDrop d e L1 L2 = (ldrop d e L1 L2).
+interpretation
+ "basic slicing (local environment)"
+ 'RDrop d e L1 L2 = (ldrop d e L1 L2).
definition l_liftable: predicate (lenv → relation term) ≝
λR. ∀K,T1,T2. R K T1 T2 → ∀L,d,e. ⇩[d, e] L ≡ K →
fact ldrop_inv_atom1_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → L1 = ⋆ →
L2 = ⋆ ∧ e = 0.
#d #e #L1 #L2 * -d -e -L1 -L2
-[ /2 width=1/
+[ /2 width=1 by conj/
| #L #I #V #H destruct
| #L1 #L2 #I #V #e #_ #H destruct
| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H destruct
(0 < e ∧ ⇩[d, e - 1] K ≡ L2).
#d #e #L1 #L2 * -d -e -L1 -L2
[ #d #_ #K #I #V #H destruct
-| #L #I #V #_ #K #J #W #HX destruct /3 width=1/
-| #L1 #L2 #I #V #e #HL12 #_ #K #J #W #H destruct /3 width=1/
+| #L #I #V #_ #K #J #W #HX destruct /3 width=1 by or_introl, conj/
+| #L1 #L2 #I #V #e #HL12 #_ #K #J #W #H destruct /3 width=1 by or_intror, conj/
| #L1 #L2 #I #V1 #V2 #d #e #_ #_ >commutative_plus normalize #H destruct
]
qed-.
qed-.
(* Basic_1: was: drop_gen_drop *)
-lemma ldrop_inv_ldrop1: ∀e,K,I,V,L2.
- ⇩[0, e] K. ⓑ{I} V ≡ L2 → 0 < e → ⇩[0, e - 1] K ≡ L2.
+lemma ldrop_inv_ldrop1_lt: ∀e,K,I,V,L2.
+ ⇩[0, e] K. ⓑ{I} V ≡ L2 → 0 < e → ⇩[0, e - 1] K ≡ L2.
#e #K #I #V #L2 #H #He
elim (ldrop_inv_O1_pair1 … H) -H * // #H destruct
elim (lt_refl_false … He)
qed-.
+lemma ldrop_inv_ldrop1: ∀e,K,I,V,L2.
+ ⇩[0, e+1] K. ⓑ{I} V ≡ L2 → ⇩[0, e] K ≡ L2.
+#e #K #I #V #L2 #H lapply (ldrop_inv_ldrop1_lt … H ?) -H //
+qed-.
+
fact ldrop_inv_skip1_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → 0 < d →
∀I,K1,V1. L1 = K1. ⓑ{I} V1 →
∃∃K2,V2. ⇩[d - 1, e] K1 ≡ K2 &
[ #d #_ #I #K #V #H destruct
| #L #I #V #H elim (lt_refl_false … H)
| #L1 #L2 #I #V #e #_ #H elim (lt_refl_false … H)
-| #X #L2 #Y #Z #V2 #d #e #HL12 #HV12 #_ #I #L1 #V1 #H destruct /2 width=5/
+| #X #L2 #Y #Z #V2 #d #e #HL12 #HV12 #_ #I #L1 #V1 #H destruct /2 width=5 by ex3_2_intro/
]
qed-.
[ #H elim (ldrop_inv_atom1 … H) -H #H destruct
| #L1 #I1 #V1 #H
elim (ldrop_inv_O1_pair1 … H) -H *
- [ #H1 #H2 destruct /3 width=1/
+ [ #H1 #H2 destruct /3 width=1 by or_introl, conj/
| /3 width=5/
]
]
[ #d #_ #I #K #V #H destruct
| #L #I #V #H elim (lt_refl_false … H)
| #L1 #L2 #I #V #e #_ #H elim (lt_refl_false … H)
-| #L1 #X #Y #V1 #Z #d #e #HL12 #HV12 #_ #I #L2 #V2 #H destruct /2 width=5/
+| #L1 #X #Y #V1 #Z #d #e #HL12 #HV12 #_ #I #L2 #V2 #H destruct /2 width=5 by ex3_2_intro/
]
qed-.
(* Basic_1: was by definition: drop_refl *)
lemma ldrop_refl: ∀L,d. ⇩[d, 0] L ≡ L.
#L elim L -L //
-#L #I #V #IHL #d @(nat_ind_plus … d) -d // /2 width=1/
+#L #I #V #IHL #d @(nat_ind_plus … d) -d /2 width=1 by ldrop_pair, ldrop_skip/
qed.
lemma ldrop_ldrop_lt: ∀L1,L2,I,V,e.
⇩[0, e - 1] L1 ≡ L2 → 0 < e → ⇩[0, e] L1. ⓑ{I} V ≡ L2.
-#L1 #L2 #I #V #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/
+#L1 #L2 #I #V #e #HL12 #He >(plus_minus_m_m e 1) /2 width=1 by ldrop_ldrop/
qed.
lemma ldrop_skip_lt: ∀L1,L2,I,V1,V2,d,e.
⇩[d - 1, e] L1 ≡ L2 → ⇧[d - 1, e] V2 ≡ V1 → 0 < d →
⇩[d, e] L1. ⓑ{I} V1 ≡ L2. ⓑ{I} V2.
-#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV21 #Hd >(plus_minus_m_m d 1) // /2 width=1/
+#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV21 #Hd >(plus_minus_m_m d 1) /2 width=1 by ldrop_skip/
qed.
lemma ldrop_O1_le: ∀e,L. e ≤ |L| → ∃K. ⇩[0, e] L ≡ K.
#e #IHe *
[ #H lapply (le_n_O_to_eq … H) -H >commutative_plus normalize #H destruct
| #L #I #V normalize #H
- elim (IHe L) -IHe /2 width=1/ -H /3 width=2/
+ elim (IHe L) -IHe /2 width=1/ -H /3 width=2 by ldrop_ldrop, ex_intro/
]
qed.
lemma ldrop_O1_lt: ∀L,e. e < |L| → ∃∃I,K,V. ⇩[0, e] L ≡ K.ⓑ{I}V.
#L elim L -L
[ #e #H elim (lt_zero_false … H)
-| #L #I #V #IHL #e @(nat_ind_plus … e) -e /2 width=4/
+| #L #I #V #IHL #e @(nat_ind_plus … e) -e /2 width=4 by ldrop_pair, ex1_3_intro/
#e #_ normalize #H
- elim (IHL e) -IHL /2 width=1/ -H /3 width=4/
+ elim (IHL e) -IHL /3 width=4 by ldrop_ldrop, lt_plus_to_minus_r, lt_plus_to_lt_l, ex1_3_intro/
]
qed.
#R #HR #K #T1 #T2 #H elim H -T2
[ /3 width=9/
| #T #T2 #_ #HT2 #IHT1 #L #d #e #HLK #U1 #HTU1 #U2 #HTU2
- elim (lift_total T d e) /4 width=11 by step/ (**) (* auto too slow without trace *)
+ elim (lift_total T d e) /4 width=11 by step/
]
qed.
lemma l_deliftable_sn_LTC: ∀R. l_deliftable_sn R → l_deliftable_sn (LTC … R).
#R #HR #L #U1 #U2 #H elim H -U2
[ #U2 #HU12 #K #d #e #HLK #T1 #HTU1
- elim (HR … HU12 … HLK … HTU1) -HR -L -U1 /3 width=3/
+ elim (HR … HU12 … HLK … HTU1) -HR -L -U1 /3 width=3 by inj, ex2_intro/
| #U #U2 #_ #HU2 #IHU1 #K #d #e #HLK #T1 #HTU1
elim (IHU1 … HLK … HTU1) -IHU1 -U1 #T #HTU #HT1
- elim (HR … HU2 … HLK … HTU) -HR -L -U /3 width=5/
+ elim (HR … HU2 … HLK … HTU) -HR -L -U /3 width=5 by step, ex2_intro/
]
qed.
lemma dropable_sn_TC: ∀R. dropable_sn R → dropable_sn (TC … R).
#R #HR #L1 #K1 #d #e #HLK1 #L2 #H elim H -L2
[ #L2 #HL12
- elim (HR … HLK1 … HL12) -HR -L1 /3 width=3/
+ elim (HR … HLK1 … HL12) -HR -L1 /3 width=3 by inj, ex2_intro/
| #L #L2 #_ #HL2 * #K #HK1 #HLK
- elim (HR … HLK … HL2) -HR -L /3 width=3/
+ elim (HR … HLK … HL2) -HR -L /3 width=3 by step, ex2_intro/
]
qed.
lemma dedropable_sn_TC: ∀R. dedropable_sn R → dedropable_sn (TC … R).
#R #HR #L1 #K1 #d #e #HLK1 #K2 #H elim H -K2
[ #K2 #HK12
- elim (HR … HLK1 … HK12) -HR -K1 /3 width=3/
+ elim (HR … HLK1 … HK12) -HR -K1 /3 width=3 by inj, ex2_intro/
| #K #K2 #_ #HK2 * #L #HL1 #HLK
- elim (HR … HLK … HK2) -HR -K /3 width=3/
+ elim (HR … HLK … HK2) -HR -K /3 width=3 by step, ex2_intro/
]
qed.
lemma dropable_dx_TC: ∀R. dropable_dx R → dropable_dx (TC … R).
#R #HR #L1 #L2 #H elim H -L2
[ #L2 #HL12 #K2 #e #HLK2
- elim (HR … HL12 … HLK2) -HR -L2 /3 width=3/
+ elim (HR … HL12 … HLK2) -HR -L2 /3 width=3 by inj, ex2_intro/
| #L #L2 #_ #HL2 #IHL1 #K2 #e #HLK2
elim (HR … HL2 … HLK2) -HR -L2 #K #HLK #HK2
- elim (IHL1 … HLK) -L /3 width=5/
+ elim (IHL1 … HLK) -L /3 width=5 by step, ex2_intro/
]
qed.
lemma l_deliftable_sn_llstar: ∀R. l_deliftable_sn R →
∀l. l_deliftable_sn (llstar … R l).
#R #HR #l #L #U1 #U2 #H @(lstar_ind_r … l U2 H) -l -U2
-[ /2 width=3/
+[ /2 width=3 by lstar_O, ex2_intro/
| #l #U #U2 #_ #HU2 #IHU1 #K #d #e #HLK #T1 #HTU1
elim (IHU1 … HLK … HTU1) -IHU1 -U1 #T #HTU #HT1
- elim (HR … HU2 … HLK … HTU) -HR -L -U /3 width=5/
+ elim (HR … HU2 … HLK … HTU) -HR -L -U /3 width=5 by lstar_dx, ex2_intro/
]
qed.
| #K1 #I1 #V1 #IHL1 #I2 #K2 #V2 #e #H
elim (ldrop_inv_O1_pair1 … H) -H * #He #H
[ -IHL1 destruct /2 width=1/
- | @ldrop_ldrop >(plus_minus_m_m e 1) // /2 width=3/
+ | @ldrop_ldrop >(plus_minus_m_m e 1) /2 width=3 by /
]
]
qed-.
lemma ldrop_fwd_length: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → |L1| = |L2| + e.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize /2 width=1/
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize /2 width=1 by /
qed-.
lemma ldrop_fwd_length_minus2: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → |L2| = |L1| - e.
-#L1 #L2 #d #e #H lapply (ldrop_fwd_length … H) -H /2 width=1/
+#L1 #L2 #d #e #H lapply (ldrop_fwd_length … H) -H /2 width=1 by plus_minus, le_n/
qed-.
lemma ldrop_fwd_length_minus4: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → e = |L1| - |L2|.
qed-.
lemma ldrop_fwd_length_lt4: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → 0 < e → |L2| < |L1|.
-#L1 #L2 #d #e #H lapply (ldrop_fwd_length … H) -H /2 width=1/
+#L1 #L2 #d #e #H lapply (ldrop_fwd_length … H) -H /2 width=1 by lt_minus_to_plus_r/
qed-.
-lemma ldrop_fwd_length_eq: ∀L1,L2,K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 →
- |L1| = |L2| → |K1| = |K2|.
+lemma ldrop_fwd_length_eq1: ∀L1,L2,K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 →
+ |L1| = |L2| → |K1| = |K2|.
#L1 #L2 #K1 #K2 #d #e #HLK1 #HLK2 #HL12
lapply (ldrop_fwd_length … HLK1) -HLK1
lapply (ldrop_fwd_length … HLK2) -HLK2
-/2 width=2 by injective_plus_r/ (**) (* full auto fails *)
+/2 width=2 by injective_plus_r/
+qed-.
+
+lemma ldrop_fwd_length_eq2: ∀L1,L2,K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 →
+ |K1| = |K2| → |L1| = |L2|.
+#L1 #L2 #K1 #K2 #d #e #HLK1 #HLK2 #HL12
+lapply (ldrop_fwd_length … HLK1) -HLK1
+lapply (ldrop_fwd_length … HLK2) -HLK2 //
qed-.
lemma ldrop_fwd_lw: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ♯{L2} ≤ ♯{L1}.
#L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize
-[ /2 width=3/
+[ /2 width=3 by transitive_le/
| #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12
- >(lift_fwd_tw … HV21) -HV21 /2 width=1/
+ >(lift_fwd_tw … HV21) -HV21 /2 width=1 by monotonic_le_plus_l/
]
qed-.
lapply (ldrop_fwd_lw … HL12) -HL12 #HL12
@(le_to_lt_to_lt … HL12) -HL12 //
| #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12 #H normalize in ⊢ (?%%); -I
- >(lift_fwd_tw … HV21) -V2 /3 by lt_minus_to_plus/ (**) (* auto too slow without trace *)
+ >(lift_fwd_tw … HV21) -V2 /3 by lt_minus_to_plus/
]
qed-.
fact ldrop_O1_append_sn_le_aux: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 →
d = 0 → e ≤ |L1| →
∀L. ⇩[0, e] L @@ L1 ≡ L @@ L2.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize // /4 width=1/
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize
+/4 width=1 by ldrop_skip_lt, ldrop_ldrop, arith_b1, lt_minus_to_plus_r, monotonic_pred/
qed-.
lemma ldrop_O1_append_sn_le: ∀L1,L2,e. ⇩[0, e] L1 ≡ L2 → e ≤ |L1| →
elim (ldrop_inv_O1_pair1 … H) -H * #H2e #HL12 destruct
[ lapply (le_n_O_to_eq … H1e) -H1e -IHL2
>commutative_plus normalize #H destruct
-| <minus_plus >minus_minus_comm /3 width=1/
+| <minus_plus >minus_minus_comm /3 width=1 by monotonic_pred/
]
qed-.
[ #H1 #_ #K2 #H2
lapply (ldrop_inv_O2 … H1) -H1 #H1
lapply (ldrop_inv_O2 … H2) -H2 #H2 destruct //
- | #e #_ #H1 #H #K2 #H2
- lapply (le_plus_to_le_r … H) -H
- lapply (ldrop_inv_ldrop1 … H1 ?) -H1 //
- lapply (ldrop_inv_ldrop1 … H2 ?) -H2 //
- <minus_plus_m_m /2 width=4/
+ | /4 width=6 by ldrop_inv_ldrop1, le_plus_to_le_r/
]
]
qed-.
include "basic_2/relocation/lift_lift.ma".
include "basic_2/relocation/ldrop.ma".
-(* DROPPING *****************************************************************)
+(* BASIC SLICING FOR LOCAL ENVIRONMENTS *************************************)
(* Main properties **********************************************************)
[ #d #L2 #H elim (ldrop_inv_atom1 … H) -H //
| #K #I #V #L2 #HL12 <(ldrop_inv_O2 … HL12) -L2 //
| #L #K #I #V #e #_ #IHLK #L2 #H
- lapply (ldrop_inv_ldrop1 … H ?) -H // /2 width=1/
+ lapply (ldrop_inv_ldrop1 … H) -H /2 width=1 by/
| #L #K1 #I #T #V1 #d #e #_ #HVT1 #IHLK1 #X #H
elim (ldrop_inv_skip1 … H) -H // <minus_plus_m_m #K2 #V2 #HLK2 #HVT2 #H destruct
>(lift_inj … HVT1 … HVT2) -HVT1 -HVT2
⇩[0, e2 - e1] L1 ≡ L2.
#d1 #e1 #L #L1 #H elim H -d1 -e1 -L -L1 //
[ #L #K #I #V #e #_ #IHLK #e2 #L2 #H #He2
- lapply (ldrop_inv_ldrop1 … H ?) -H /2 width=2/ #HL2
- <minus_plus >minus_minus_comm /3 width=1/
+ lapply (ldrop_inv_ldrop1_lt … H ?) -H /2 width=2 by ltn_to_ltO/ #HL2
+ <minus_plus >minus_minus_comm /3 width=1 by monotonic_pred/
| #L #K #I #V1 #V2 #d #e #_ #_ #IHLK #e2 #L2 #H #Hdee2
lapply (transitive_le 1 … Hdee2) // #He2
- lapply (ldrop_inv_ldrop1 … H ?) -H // -He2 #HL2
+ lapply (ldrop_inv_ldrop1_lt … H ?) -H // -He2 #HL2
lapply (transitive_le (1 + e) … Hdee2) // #Hee2
- @ldrop_ldrop_lt >minus_minus_comm /3 width=1/ (**) (* explicit constructor *)
+ @ldrop_ldrop_lt >minus_minus_comm /3 width=1 by O, lt_minus_to_plus_r, monotonic_le_minus_r, monotonic_pred/ (**) (* explicit constructor *)
]
qed.
∃∃L. ⇩[0, d1 + e1 - e2] L2 ≡ L & ⇩[0, d1] L1 ≡ L.
#L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
[ #d1 #L2 #e2 #H #Hd1 #_ elim (ldrop_inv_atom1 … H) -H #H1 #H2 destruct
- <(le_n_O_to_eq … Hd1) -d1 /2 width=3/
+ <(le_n_O_to_eq … Hd1) -d1 /2 width=3 by ldrop_atom, ex2_intro/
| normalize #L #I #V #L2 #e2 #HL2 #_ #He2
lapply (le_n_O_to_eq … He2) -He2 #H destruct
- lapply (ldrop_inv_O2 … HL2) -HL2 #H destruct /2 width=3/
+ lapply (ldrop_inv_O2 … HL2) -HL2 #H destruct /2 width=3 by ldrop_pair, ex2_intro/
| normalize #L0 #K0 #I #V1 #e1 #HLK0 #IHLK0 #L2 #e2 #H #_ #He21
lapply (ldrop_inv_O1_pair1 … H) -H * * #He2 #HL20
- [ -IHLK0 -He21 destruct <minus_n_O /3 width=3/
+ [ -IHLK0 -He21 destruct <minus_n_O /3 width=3 by ldrop_ldrop, ex2_intro/
| -HLK0 <minus_le_minus_minus_comm //
- elim (IHLK0 … HL20) -L0 // /2 width=1/ /2 width=3/
+ elim (IHLK0 … HL20) -L0 /2 width=3 by monotonic_pred, ex2_intro/
]
| #L0 #K0 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHLK0 #L2 #e2 #H #Hd1e2 #He2de1
elim (le_inv_plus_l … Hd1e2) #_ #He2
<minus_le_minus_minus_comm //
- lapply (ldrop_inv_ldrop1 … H ?) -H // #HL02
- elim (IHLK0 … HL02) -L0 /2 width=1/ /3 width=3/
+ lapply (ldrop_inv_ldrop1_lt … H ?) -H // #HL02
+ elim (IHLK0 … HL02) -L0 /3 width=3 by ldrop_ldrop, monotonic_pred, ex2_intro/
]
qed.
∃∃L. ⇩[0, e2] L1 ≡ L & ⇩[d1 - e2, e1] L2 ≡ L.
#L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
[ #d1 #L2 #e2 #H
- elim (ldrop_inv_atom1 … H) -H #H destruct /2 width=3/
+ elim (ldrop_inv_atom1 … H) -H #H destruct /2 width=3 by ldrop_atom, ex2_intro/
| #K0 #I #V0 #L2 #e2 #H1 #H2
lapply (le_n_O_to_eq … H2) -H2 #H destruct
- lapply (ldrop_inv_pair1 … H1) -H1 #H destruct /2 width=3/
+ lapply (ldrop_inv_pair1 … H1) -H1 #H destruct /2 width=3 by ldrop_pair, ex2_intro/
| #K0 #K1 #I #V0 #e1 #HK01 #_ #L2 #e2 #H1 #H2
lapply (le_n_O_to_eq … H2) -H2 #H destruct
- lapply (ldrop_inv_pair1 … H1) -H1 #H destruct /3 width=3/
+ lapply (ldrop_inv_pair1 … H1) -H1 #H destruct /3 width=3 by ldrop_ldrop, ex2_intro/
| #K0 #K1 #I #V0 #V1 #d1 #e1 #HK01 #HV10 #IHK01 #L2 #e2 #H #He2d1
elim (ldrop_inv_O1_pair1 … H) -H *
- [ -IHK01 -He2d1 #H1 #H2 destruct /3 width=5/
+ [ -IHK01 -He2d1 #H1 #H2 destruct /3 width=5 by ldrop_pair, ldrop_skip, ex2_intro/
| -HK01 -HV10 #He2 #HK0L2
- elim (IHK01 … HK0L2) -IHK01 -HK0L2 /2 width=1/ >minus_le_minus_minus_comm // /3 width=3/
+ elim (IHK01 … HK0L2) -IHK01 -HK0L2 /2 width=1 by monotonic_pred/
+ >minus_le_minus_minus_comm /3 width=3 by ldrop_ldrop_lt, ex2_intro/
]
]
qed.
| #L1 #L2 #I #V1 #V2 #d #e #H_ #_ #IHL12 #e2 #L #H #Hde2
lapply (lt_to_le_to_lt 0 … Hde2) // #He2
lapply (lt_to_le_to_lt … (e + e2) He2 ?) // #Hee2
- lapply (ldrop_inv_ldrop1 … H ?) -H // #HL2
- @ldrop_ldrop_lt // >le_plus_minus // @IHL12 /2 width=1/ (**) (* explicit constructor *)
+ lapply (ldrop_inv_ldrop1_lt … H ?) -H // #HL2
+ @ldrop_ldrop_lt // >le_plus_minus /3 width=1 by monotonic_pred/
]
qed.
∃∃L0. ⇩[0, e2] L1 ≡ L0 & ⇩[d1 - e2, e1] L0 ≡ L2.
#d1 #e1 #L1 #L #H elim H -d1 -e1 -L1 -L
[ #d #e2 #L2 #H
- elim (ldrop_inv_atom1 … H) -H /2 width=3/
+ elim (ldrop_inv_atom1 … H) -H /2 width=3 by ldrop_atom, ex2_intro/
| #K #I #V #e2 #L2 #HL2 #H
- lapply (le_n_O_to_eq … H) -H #H destruct /2 width=3/
+ lapply (le_n_O_to_eq … H) -H #H destruct /2 width=3 by ldrop_pair, ex2_intro/
| #L1 #L2 #I #V #e #_ #IHL12 #e2 #L #HL2 #H
lapply (le_n_O_to_eq … H) -H #H destruct
elim (IHL12 … HL2) -IHL12 -HL2 // #L0 #H #HL0
- lapply (ldrop_inv_O2 … H) -H #H destruct /3 width=5/
+ lapply (ldrop_inv_O2 … H) -H #H destruct /3 width=5 by ldrop_pair, ldrop_ldrop, ex2_intro/
| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #IHL12 #e2 #L #H #He2d
elim (ldrop_inv_O1_pair1 … H) -H *
- [ -He2d -IHL12 #H1 #H2 destruct /3 width=5/
+ [ -He2d -IHL12 #H1 #H2 destruct /3 width=5 by ldrop_pair, ldrop_skip, ex2_intro/
| -HL12 -HV12 #He2 #HL2
- elim (IHL12 … HL2) -L2 [ >minus_le_minus_minus_comm // /3 width=3/ | /2 width=1/ ]
+ elim (IHL12 … HL2) -L2 [ >minus_le_minus_minus_comm // /3 width=3 by ldrop_ldrop_lt, ex2_intro/ | /2 width=1 by monotonic_pred/ ]
]
]
qed.
[ #L #d #e #_ #U1 #HTU1 #U2 #HTU2 -HR -K
>(lift_mono … HTU2 … HTU1) -T1 -U2 -d -e //
| #l #T #T2 #_ #HT2 #IHT1 #L #d #e #HLK #U1 #HTU1 #U2 #HTU2
- elim (lift_total T d e) /3 width=11 by lstar_dx/ (**) (* auto too slow without trace *)
+ elim (lift_total T d e) /3 width=11 by lstar_dx/
]
qed.
∃∃K1,V1. ⇩[0, e2] L1 ≡ K1. ⓑ{I} V1 &
⇩[d, e1] K2 ≡ K1 & ⇧[d, e1] V1 ≡ V2.
#d1 #e1 #L #L1 #H1 #e2 #K2 #I #V2 #H2 #He2d1
-elim (ldrop_conf_le … H1 … H2) -L [2: /2 width=2/] #K #HL1K #HK2
-elim (ldrop_inv_skip1 … HK2) -HK2 [2: /2 width=1/] #K1 #V1 #HK21 #HV12 #H destruct /2 width=5/
+elim (ldrop_conf_le … H1 … H2) -L /2 width=2 by lt_to_le/ #K #HL1K #HK2
+elim (ldrop_inv_skip1 … HK2) -HK2 /2 width=1 by lt_plus_to_minus_r/ #K1 #V1 #HK21 #HV12 #H destruct /2 width=5 by ex3_2_intro/
qed.
(* Note: apparently this was missing in basic_1 *)
∃∃L0,V0. ⇩[0, e2] L1 ≡ L0.ⓑ{I}V0 &
⇩[d, e1] L0 ≡ L2 & ⇧[d, e1] V2 ≡ V0.
#d1 #e1 #L1 #L #HL1 #e2 #L2 #I #V2 #HL2 #Hd21
-elim (ldrop_trans_le … HL1 … HL2) -L [2: /2 width=1/ ] #L0 #HL10 #HL02
-elim (ldrop_inv_skip2 … HL02) -HL02 [2: /2 width=1/ ] #L #V1 #HL2 #HV21 #H destruct /2 width=5/
+elim (ldrop_trans_le … HL1 … HL2) -L /2 width=1 by lt_to_le/ #L0 #HL10 #HL02
+elim (ldrop_inv_skip2 … HL02) -HL02 /2 width=1 by lt_plus_to_minus_r/ #L #V1 #HL2 #HV21 #H destruct /2 width=5 by ex3_2_intro/
qed-.
lemma ldrop_trans_ge_comm: ∀d1,e1,e2,L1,L2,L.
⇩[d1, e1] L1 ≡ L → ⇩[0, e2] L ≡ L2 → d1 ≤ e2 →
⇩[0, e2 + e1] L1 ≡ L2.
-#e1 #e1 #e2 >commutative_plus /2 width=5/
+#e1 #e1 #e2 >commutative_plus /2 width=5 by ldrop_trans_ge/
qed.
lemma ldrop_conf_div: ∀I1,L,K,V1,e1. ⇩[0, e1] L ≡ K. ⓑ{I1} V1 →
[1,3: normalize <plus_n_Sm #H destruct ]
#H >H in HK; #HK
lapply (ldrop_inv_O2 … HK) -HK #H destruct
-lapply (inv_eq_minus_O … H) -H /3 width=1/
+lapply (inv_eq_minus_O … H) -H /3 width=1 by le_to_le_to_eq, and3_intro/
+qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma ldrop_fwd_be: ∀L,K,d,e,i. ⇩[d, e] L ≡ K → |K| ≤ i → i < d → |L| ≤ i.
+#L #K #d #e #i #HLK #HK #Hd elim (lt_or_ge i (|L|)) //
+#HL elim (ldrop_O1_lt … HL) #I #K0 #V #HLK0 -HL
+elim (ldrop_conf_lt … HLK … HLK0) // -HLK -HLK0 -Hd
+#K1 #V1 #HK1 #_ #_ lapply (ldrop_fwd_length_lt2 … HK1) -I -K1 -V1
+#H elim (lt_refl_false i) /2 width=3 by lt_to_le_to_lt/
qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/ynat/ynat_plus.ma".
+include "basic_2/grammar/leq.ma".
+include "basic_2/relocation/ldrop.ma".
+
+(* BASIC SLICING FOR LOCAL ENVIRONMENTS *************************************)
+
+lemma ldrop_leq_conf_ge: ∀L1,L2,d,e. L1 ≃[d, e] L2 →
+ ∀I,K,V,i. ⇩[O, i]L1 ≡ K.ⓑ{I}V → d + e ≤ i →
+ ⇩[O, i]L2 ≡ K.ⓑ{I}V.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
+[ #d #e #J #K #W #i #H elim (ldrop_inv_atom1 … H) -H
+ #H destruct
+| #I #L1 #L2 #V #HL12 #IHL12 #J #K #W #i #H #_ elim (ldrop_inv_O1_pair1 … H) -H
+ * #H1 #H2
+ [ -IHL12 lapply (leq_inv_O2 … HL12) -HL12
+ #H3 destruct //
+ | -HL12 /4 width=1 by ldrop_ldrop_lt, yle_inj/
+ ]
+| #I1 #I2 #L1 #L2 #V1 #V2 #e #_ #IHL12 #J #K #W #i #H1 >yplus_succ_swap
+ #Hei elim (yle_inv_inj2 … Hei) -Hei
+ #x #Hei #H elim (yplus_inv_inj … H) -H normalize
+ #y #z >commutative_plus
+ #H1 #H2 #H3 destruct elim (le_inv_plus_l … Hei) -Hei
+ #Hzi #Hi lapply (ldrop_inv_ldrop1_lt … H1 ?) -H1
+ /4 width=1 by ldrop_ldrop_lt, yle_inj/
+| #I #L1 #L2 #V #d #e #_ #IHL12 #J #K #W #i #H0 #Hdei elim (yle_inv_inj2 … Hdei) -Hdei
+ #x #Hdei #H elim (yplus_inv_inj … H) -H
+ #y #z >commutative_plus
+ #H1 #H2 #H3 destruct elim (ysucc_inv_inj_dx … H2) -H2
+ #x #H1 #H2 destruct elim (le_inv_plus_l … Hdei)
+ #_ #Hi lapply (ldrop_inv_ldrop1_lt … H0 ?) -H0
+ [2: #H0 @ldrop_ldrop_lt ] [2,3: /2 width=3 by lt_to_le_to_lt/ ]
+ /4 width=3 by yle_inj, monotonic_pred/
+]
+qed-.
+
+lemma ldrop_leq_conf_be: ∀L1,L2,d,e. L1 ≃[d, e] L2 →
+ ∀I1,K1,V1,i. ⇩[O, i]L1 ≡ K1.ⓑ{I1}V1 → d ≤ i → i < d + e →
+ ∃∃I2,K2,V2. K1 ≃[0, ⫰(d+e-i)] K2 & ⇩[O, i]L2 ≡ K2.ⓑ{I2}V2.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
+[ #d #e #J1 #K1 #W1 #i #H elim (ldrop_inv_atom1 … H) -H
+ #H destruct
+| #I #L1 #L2 #V #HL12 #IHL12 #J1 #K1 #W1 #i #_ #_ #H elim (ylt_yle_false … H) //
+| #I1 #I2 #L1 #L2 #V1 #V2 #e #HL12 >yplus_O_sn >yplus_O_sn
+ #IHL12 #J1 #K1 #W1 #i #H #_ elim (eq_or_gt i) #Hi destruct [ -IHL12 | -HL12 ]
+ [ #_ lapply (ldrop_inv_O2 … H) -H
+ #H destruct >ypred_succ /2 width=5 by ldrop_pair, ex2_3_intro/
+ | lapply (ldrop_inv_ldrop1_lt … H ?) -H //
+ #H <(ylt_inv_O1 i) /2 width=1 by ylt_inj/
+ #Hie lapply (ylt_inv_succ … Hie) -Hie
+ #Hie elim (IHL12 … H) -IHL12 -H //
+ >yminus_succ /3 width=5 by ldrop_ldrop_lt, ex2_3_intro/
+ ]
+| #I #L1 #L2 #V #d #e #_ #IHL12 #J1 #K1 #W1 #i #H #Hdi lapply (ylt_yle_trans 0 … Hdi ?) //
+ #Hi <(ylt_inv_O1 … Hi) >yplus_succ1 >yminus_succ lapply (yle_fwd_succ1 … Hdi) -Hdi
+ #Hdi #Hide lapply (ylt_inv_succ … Hide)
+ #Hide lapply (ylt_inv_inj … Hi) -Hi
+ #Hi lapply (ldrop_inv_ldrop1_lt … H ?) -H //
+ #H elim (IHL12 … H) -IHL12 -H
+ /3 width=5 by ldrop_ldrop_lt, ex2_3_intro/
+]
+qed-.
+
+lemma ldrop_leq_conf_lt: ∀L1,L2,d,e. L1 ≃[d, e] L2 →
+ ∀I,K1,V,i. ⇩[O, i]L1 ≡ K1.ⓑ{I}V → i < d →
+ ∃∃K2. K1 ≃[⫰(d-i), e] K2 & ⇩[O, i]L2 ≡ K2.ⓑ{I}V.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
+[ #d #e #J #K1 #W #i #H elim (ldrop_inv_atom1 … H) -H
+ #H destruct
+| #I #L1 #L2 #V #_ #_ #J #K1 #W #i #_ #H elim (ylt_yle_false … H) //
+| #I1 #I2 #L1 #L2 #V1 #V2 #e #_ #_ #J #K1 #W #i #_ #H elim (ylt_yle_false … H) //
+| #I #L1 #L2 #V #d #e #HL12 #IHL12 #J #K1 #W #i #H elim (eq_or_gt i) #Hi destruct [ -IHL12 | -HL12 ]
+ [ #_ lapply (ldrop_inv_O2 … H) -H
+ #H destruct >ypred_succ /2 width=5 by ldrop_pair, ex2_intro/
+ | lapply (ldrop_inv_ldrop1_lt … H ?) -H //
+ #H <(ylt_inv_O1 i) /2 width=1 by ylt_inj/
+ #Hie lapply (ylt_inv_succ … Hie) -Hie
+ #Hie elim (IHL12 … H) -IHL12 -H
+ >yminus_succ /3 width=5 by ldrop_ldrop_lt, ex2_intro/
+ ]
+]
+qed-.
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/lazyeq_3.ma".
+include "basic_2/notation/relations/lazyeq_4.ma".
include "basic_2/relocation/ldrop.ma".
(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)
-inductive lleq: term → relation lenv ≝
-| lleq_sort: ∀L1,L2,k. |L1| = |L2| → lleq (⋆k) L1 L2
-| lleq_lref: ∀I,L1,L2,K1,K2,V,i.
+inductive lleq: nat → term → relation lenv ≝
+| lleq_sort: ∀L1,L2,d,k. |L1| = |L2| → lleq d (⋆k) L1 L2
+| lleq_skip: ∀I1,I2,L1,L2,K1,K2,V1,V2,d,i. i < d →
+ ⇩[0, i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[0, i] L2 ≡ K2.ⓑ{I2}V2 →
+ lleq (d-i-1) V1 K1 K2 → lleq (d-i-1) V2 K1 K2 → lleq d (#i) L1 L2
+| lleq_lref: ∀I,L1,L2,K1,K2,V,d,i. d ≤ i →
⇩[0, i] L1 ≡ K1.ⓑ{I}V → ⇩[0, i] L2 ≡ K2.ⓑ{I}V →
- lleq V K1 K2 → lleq (#i) L1 L2
-| lleq_free: ∀L1,L2,i. |L1| ≤ i → |L2| ≤ i → |L1| = |L2| → lleq (#i) L1 L2
-| lleq_gref: ∀L1,L2,p. |L1| = |L2| → lleq (§p) L1 L2
-| lleq_bind: ∀a,I,L1,L2,V,T.
- lleq V L1 L2 → lleq T (L1.ⓑ{I}V) (L2.ⓑ{I}V) →
- lleq (ⓑ{a,I}V.T) L1 L2
-| lleq_flat: ∀I,L1,L2,V,T.
- lleq V L1 L2 → lleq T L1 L2 → lleq (ⓕ{I}V.T) L1 L2
+ lleq 0 V K1 K2 → lleq d (#i) L1 L2
+| lleq_free: ∀L1,L2,d,i. |L1| ≤ i → |L2| ≤ i → |L1| = |L2| → lleq d (#i) L1 L2
+| lleq_gref: ∀L1,L2,d,p. |L1| = |L2| → lleq d (§p) L1 L2
+| lleq_bind: ∀a,I,L1,L2,V,T,d.
+ lleq d V L1 L2 → lleq (d+1) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) →
+ lleq d (ⓑ{a,I}V.T) L1 L2
+| lleq_flat: ∀I,L1,L2,V,T,d.
+ lleq d V L1 L2 → lleq d T L1 L2 → lleq d (ⓕ{I}V.T) L1 L2
.
interpretation
"lazy equivalence (local environment)"
- 'LazyEq T L1 L2 = (lleq T L1 L2).
+ 'LazyEq d T L1 L2 = (lleq d T L1 L2).
(* Basic_properties *********************************************************)
-lemma lleq_sym: ∀T. symmetric … (lleq T).
-#T #L1 #L2 #H elim H -T -L1 -L2
-/2 width=7 by lleq_sort, lleq_lref, lleq_free, lleq_gref, lleq_bind, lleq_flat/
+lemma lleq_sym: ∀d,T. symmetric … (lleq d T).
+#d #T #L1 #L2 #H elim H -d -T -L1 -L2
+/2 width=10 by lleq_sort, lleq_skip, lleq_lref, lleq_free, lleq_gref, lleq_bind, lleq_flat/
qed-.
-lemma lleq_refl: ∀T. reflexive … (lleq T).
-#T #L @(f2_ind … rfw … L T)
+(* Note this is: "∀d,T. reflexive … (lleq d T)" *)
+axiom lleq_refl: ∀T,L,d. L ⋕[d, T] L.
+(*
+#T #L @(f2_ind … rfw … L T) -L -T
#n #IH #L * * /3 width=1 by lleq_sort, lleq_gref, lleq_bind, lleq_flat/
#i #H elim (lt_or_ge i (|L|)) /2 width=1 by lleq_free/
-#HiL elim (ldrop_O1_lt … HiL) -HiL destruct /4 width=7 by lleq_lref, ldrop_fwd_rfw/
+#HiL #d elim (lt_or_ge i d) /2 width=1 by lleq_skip/
+elim (ldrop_O1_lt … HiL) -HiL destruct /4 width=7 by lleq_lref, ldrop_fwd_rfw/
qed.
+*)
+
+lemma lleq_ge: ∀L1,L2,T,d1. L1 ⋕[d1, T] L2 → ∀d2. d1 ≤ d2 → L1 ⋕[d2, T] L2.
+#L1 #L2 #T #d1 #H elim H -L1 -L2 -T -d1
+/4 width=1 by lleq_sort, lleq_free, lleq_gref, lleq_bind, lleq_flat, le_S_S/
+[ /5 width=10 by lleq_skip, lt_to_le_to_lt, monotonic_le_minus_l, monotonic_pred/ (**) (* a bit slow *)
+| #I #L1 #L2 #K1 #K2 #V #d1 #i #Hi #HLK1 #HLK2 #HV #IHV #d2 #Hd12 elim (lt_or_ge i d2)
+ [ -d1 /3 width=10 by lleq_skip/
+ | /3 width=7 by lleq_lref, transitive_le/
+ ]
+]
+qed-.
(* Basic inversion lemmas ***************************************************)
-fact lleq_inv_lref_aux: ∀X,L1,L2. L1 ⋕[X] L2 → ∀i. X = #i →
- (|L1| ≤ i ∧ |L2| ≤ i) ∨
- ∃∃I,K1,K2,V. ⇩[0, i] L1 ≡ K1.ⓑ{I}V &
- ⇩[0, i] L2 ≡ K2.ⓑ{I}V &
- K1 ⋕[V] K2.
-#X #L1 #L2 * -X -L1 -L2
-[ #L1 #L2 #k #_ #j #H destruct
-| #I #L1 #L2 #K1 #K2 #V #i #HLK1 #HLK2 #HK12 #j #H destruct /3 width=7 by ex3_4_intro, or_intror/
-| #L1 #L2 #i #HL1 #HL2 #_ #j #H destruct /3 width=1 by or_introl, conj/
-| #L1 #L2 #p #_ #j #H destruct
-| #a #I #L1 #L2 #V #T #_ #_ #j #H destruct
-| #I #L1 #L2 #V #T #_ #_ #j #H destruct
+fact lleq_inv_lref_aux: ∀d,X,L1,L2. L1 ⋕[d, X] L2 → ∀i. X = #i →
+ ∨∨ |L1| ≤ i ∧ |L2| ≤ i
+ | ∃∃I1,I2,K1,K2,V1,V2. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V1 &
+ ⇩[0, i] L2 ≡ K2.ⓑ{I2}V2 &
+ K1 ⋕[d-i-1, V1] K2 &
+ K1 ⋕[d-i-1, V2] K2 &
+ i < d
+ | ∃∃I,K1,K2,V. ⇩[0, i] L1 ≡ K1.ⓑ{I}V &
+ ⇩[0, i] L2 ≡ K2.ⓑ{I}V &
+ K1 ⋕[0, V] K2 & d ≤ i.
+#d #X #L1 #L2 * -d -X -L1 -L2
+[ #L1 #L2 #d #k #_ #j #H destruct
+| #I1 #I2 #L1 #L2 #K1 #K2 #V1 #V2 #d #i #Hid #HLK1 #HLK2 #HV1 #HV2 #j #H destruct /3 width=10 by or3_intro1, ex5_6_intro/
+| #I #L1 #L2 #K1 #K2 #V #d #i #Hdi #HLK1 #HLK2 #HK12 #j #H destruct /3 width=7 by or3_intro2, ex4_4_intro/
+| #L1 #L2 #d #i #HL1 #HL2 #_ #j #H destruct /3 width=1 by or3_intro0, conj/
+| #L1 #L2 #d #p #_ #j #H destruct
+| #a #I #L1 #L2 #V #T #d #_ #_ #j #H destruct
+| #I #L1 #L2 #V #T #d #_ #_ #j #H destruct
]
qed-.
-lemma lleq_inv_lref: ∀L1,L2,i. L1 ⋕[#i] L2 →
- (|L1| ≤ i ∧ |L2| ≤ i) ∨
- ∃∃I,K1,K2,V. ⇩[0, i] L1 ≡ K1.ⓑ{I}V &
- ⇩[0, i] L2 ≡ K2.ⓑ{I}V &
- K1 ⋕[V] K2.
+lemma lleq_inv_lref: ∀L1,L2,d,i. L1 ⋕[d, #i] L2 →
+ ∨∨ |L1| ≤ i ∧ |L2| ≤ i
+ | ∃∃I1,I2,K1,K2,V1,V2. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V1 &
+ ⇩[0, i] L2 ≡ K2.ⓑ{I2}V2 &
+ K1 ⋕[d-i-1, V1] K2 &
+ K1 ⋕[d-i-1, V2] K2 &
+ i < d
+ | ∃∃I,K1,K2,V. ⇩[0, i] L1 ≡ K1.ⓑ{I}V &
+ ⇩[0, i] L2 ≡ K2.ⓑ{I}V &
+ K1 ⋕[0, V] K2 & d ≤ i.
/2 width=3 by lleq_inv_lref_aux/ qed-.
-fact lleq_inv_bind_aux: ∀X,L1,L2. L1 ⋕[X] L2 → ∀a,I,V,T. X = ⓑ{a,I}V.T →
- L1 ⋕[V] L2 ∧ L1.ⓑ{I}V ⋕[T] L2.ⓑ{I}V.
-#X #L1 #L2 * -X -L1 -L2
-[ #L1 #L2 #k #_ #b #J #W #U #H destruct
-| #I #L1 #L2 #K1 #K2 #V #i #_ #_ #_ #b #J #W #U #H destruct
-| #L1 #L2 #i #_ #_ #_ #b #J #W #U #H destruct
-| #L1 #L2 #p #_ #b #J #W #U #H destruct
-| #a #I #L1 #L2 #V #T #HV #HT #b #J #W #U #H destruct /2 width=1 by conj/
-| #I #L1 #L2 #V #T #_ #_ #b #J #W #U #H destruct
+fact lleq_inv_bind_aux: ∀d,X,L1,L2. L1 ⋕[d,X] L2 → ∀a,I,V,T. X = ⓑ{a,I}V.T →
+ L1 ⋕[d, V] L2 ∧ L1.ⓑ{I}V ⋕[d+1, T] L2.ⓑ{I}V.
+#d #X #L1 #L2 * -d -X -L1 -L2
+[ #L1 #L2 #d #k #_ #b #J #W #U #H destruct
+| #I1 #I2 #L1 #L2 #K1 #K2 #V1 #V2 #d #i #_ #_ #_ #_ #_ #b #J #W #U #H destruct
+| #I #L1 #L2 #K1 #K2 #V #d #i #_ #_ #_ #_ #b #J #W #U #H destruct
+| #L1 #L2 #d #i #_ #_ #_ #b #J #W #U #H destruct
+| #L1 #L2 #d #p #_ #b #J #W #U #H destruct
+| #a #I #L1 #L2 #V #T #d #HV #HT #b #J #W #U #H destruct /2 width=1 by conj/
+| #I #L1 #L2 #V #T #d #_ #_ #b #J #W #U #H destruct
]
qed-.
-lemma lleq_inv_bind: ∀a,I,L1,L2,V,T. L1 ⋕[ ⓑ{a,I}V.T] L2 →
- L1 ⋕[V] L2 ∧ L1.ⓑ{I}V ⋕[T] L2.ⓑ{I}V.
+lemma lleq_inv_bind: ∀a,I,L1,L2,V,T,d. L1 ⋕[d, ⓑ{a,I}V.T] L2 →
+ L1 ⋕[d, V] L2 ∧ L1.ⓑ{I}V ⋕[d+1, T] L2.ⓑ{I}V.
/2 width=4 by lleq_inv_bind_aux/ qed-.
-fact lleq_inv_flat_aux: ∀X,L1,L2. L1 ⋕[X] L2 → ∀I,V,T. X = ⓕ{I}V.T →
- L1 ⋕[V] L2 ∧ L1 ⋕[T] L2.
-#X #L1 #L2 * -X -L1 -L2
-[ #L1 #L2 #k #_ #J #W #U #H destruct
-| #I #L1 #L2 #K1 #K2 #V #i #_ #_ #_ #J #W #U #H destruct
-| #L1 #L2 #i #_ #_ #_ #J #W #U #H destruct
-| #L1 #L2 #p #_ #J #W #U #H destruct
-| #a #I #L1 #L2 #V #T #_ #_ #J #W #U #H destruct
-| #I #L1 #L2 #V #T #HV #HT #J #W #U #H destruct /2 width=1 by conj/
+fact lleq_inv_flat_aux: ∀d,X,L1,L2. L1 ⋕[d, X] L2 → ∀I,V,T. X = ⓕ{I}V.T →
+ L1 ⋕[d, V] L2 ∧ L1 ⋕[d, T] L2.
+#d #X #L1 #L2 * -d -X -L1 -L2
+[ #L1 #L2 #d #k #_ #J #W #U #H destruct
+| #I1 #I2 #L1 #L2 #K1 #K2 #V1 #V2 #d #i #_ #_ #_ #_ #_ #J #W #U #H destruct
+| #I #L1 #L2 #K1 #K2 #V #d #i #_ #_ #_ #_ #J #W #U #H destruct
+| #L1 #L2 #d #i #_ #_ #_ #J #W #U #H destruct
+| #L1 #L2 #d #p #_ #J #W #U #H destruct
+| #a #I #L1 #L2 #V #T #d #_ #_ #J #W #U #H destruct
+| #I #L1 #L2 #V #T #d #HV #HT #J #W #U #H destruct /2 width=1 by conj/
]
qed-.
-lemma lleq_inv_flat: ∀I,L1,L2,V,T. L1 ⋕[ ⓕ{I}V.T] L2 →
- L1 ⋕[V] L2 ∧ L1 ⋕[T] L2.
+lemma lleq_inv_flat: ∀I,L1,L2,V,T,d. L1 ⋕[d, ⓕ{I}V.T] L2 →
+ L1 ⋕[d, V] L2 ∧ L1 ⋕[d, T] L2.
/2 width=4 by lleq_inv_flat_aux/ qed-.
(* Basic forward lemmas *****************************************************)
-lemma lleq_fwd_length: ∀L1,L2,T. L1 ⋕[T] L2 → |L1| = |L2|.
-#L1 #L2 #T #H elim H -L1 -L2 -T //
-#I #L1 #L2 #K1 #K2 #V #i #HLK1 #HLK2 #_ #IHK12
+lemma lleq_fwd_length: ∀L1,L2,T,d. L1 ⋕[d, T] L2 → |L1| = |L2|.
+#L1 #L2 #T #d #H elim H -L1 -L2 -T -d //
+[ #I1 #I2 #L1 #L2 #K1 #K2 #V1 #V2 #d #i #_ #HLK1 #HLK2 #_ #_ #HK12 #_
+| #I #L1 #L2 #K1 #K2 #V #d #i #_ #HLK1 #HLK2 #_ #IHK12
+]
lapply (ldrop_fwd_length … HLK1) -HLK1
lapply (ldrop_fwd_length … HLK2) -HLK2
normalize //
qed-.
-lemma lleq_fwd_ldrop_sn: ∀L1,L2,T. L1 ⋕[T] L2 → ∀K1,i. ⇩[0, i] L1 ≡ K1 →
+lemma lleq_fwd_ldrop_sn: ∀L1,L2,T,d. L1 ⋕[d, T] L2 → ∀K1,i. ⇩[0, i] L1 ≡ K1 →
∃K2. ⇩[0, i] L2 ≡ K2.
-#L1 #L2 #T #H #K1 #i #HLK1 lapply (lleq_fwd_length … H) -H
-#HL12 lapply (ldrop_fwd_length_le2 … HLK1) -HLK1 /2 width=1 by ldrop_O1_le/ (**) (* full auto fails *)
+#L1 #L2 #T #d #H #K1 #i #HLK1 lapply (lleq_fwd_length … H) -H
+#HL12 lapply (ldrop_fwd_length_le2 … HLK1) -HLK1 /2 width=1 by ldrop_O1_le/
qed-.
+
+lemma lleq_fwd_ldrop_dx: ∀L1,L2,T,d. L1 ⋕[d, T] L2 → ∀K2,i. ⇩[0, i] L2 ≡ K2 →
+ ∃K1. ⇩[0, i] L1 ≡ K1.
+/3 width=6 by lleq_fwd_ldrop_sn, lleq_sym/ qed-.
(* Advanced inversion lemmas ************************************************)
-lemma lleq_inv_lref_dx: ∀L1,L2,i. L1 ⋕[#i] L2 →
+lemma lleq_inv_lref_dx: ∀L1,L2,d,i. L1 ⋕[d, #i] L2 →
∀I,K2,V. ⇩[0, i] L2 ≡ K2.ⓑ{I}V →
- ∃∃K1. ⇩[0, i] L1 ≡ K1.ⓑ{I}V & K1 ⋕[V] K2.
-#L1 #L2 #i #H #I #K2 #V #HLK2 elim (lleq_inv_lref … H) -H *
+ (∃∃K1. ⇩[0, i] L1 ≡ K1.ⓑ{I}V & K1 ⋕[0, V] K2 & d ≤ i) ∨
+ ∃∃I1,K1,V1. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V1 &
+ K1 ⋕[d-i-1, V1] K2 & K1 ⋕[d-i-1, V] K2 &
+ i < d.
+#L1 #L2 #d #i #H #I #K2 #V #HLK2 elim (lleq_inv_lref … H) -H *
[ #_ #H elim (lt_refl_false i)
- /3 width=5 by ldrop_fwd_length_lt2, lt_to_le_to_lt/
-| #I0 #K1 #K0 #V0 #HLK1 #HLK0 #HK10 lapply (ldrop_mono … HLK0 … HLK2) -L2
+ lapply (ldrop_fwd_length_lt2 … HLK2) -HLK2
+ /2 width=3 by lt_to_le_to_lt/ (**) (* full auto too slow *)
+| #I1 #I2 #K11 #K22 #V1 #V2 #HLK11 #HLK22 #HV1 #HV2 #Hdi lapply (ldrop_mono … HLK22 … HLK2) -L2
+ #H destruct /3 width=6 by ex4_3_intro, or_intror/
+| #I0 #K1 #K0 #V0 #HLK1 #HLK0 #HK10 #Hdi lapply (ldrop_mono … HLK0 … HLK2) -L2
+ #H destruct /3 width=3 by ex3_intro, or_introl/
+]
+qed-.
+
+lemma lleq_inv_lref_sn: ∀L1,L2,d,i. L1 ⋕[d, #i] L2 →
+ ∀I,K1,V. ⇩[0, i] L1 ≡ K1.ⓑ{I}V →
+ (∃∃K2. ⇩[0, i] L2 ≡ K2.ⓑ{I}V & K1 ⋕[0, V] K2 & d ≤ i) ∨
+ ∃∃I2,K2,V2. ⇩[0, i] L2 ≡ K2.ⓑ{I2}V2 &
+ K1 ⋕[d-i-1, V] K2 & K1 ⋕[d-i-1, V2] K2 &
+ i < d.
+#L1 #L2 #d #i #HL12 #I #K1 #V #HLK1 elim (lleq_inv_lref_dx L2 … d … HLK1) -HLK1
+[1,2: * ] /4 width=6 by lleq_sym, ex4_3_intro, ex3_intro, or_introl, or_intror/
+qed-.
+
+lemma lleq_inv_lref_ge_dx: ∀L1,L2,d,i. L1 ⋕[d, #i] L2 → d ≤ i →
+ ∀I,K2,V. ⇩[0, i] L2 ≡ K2.ⓑ{I}V →
+ ∃∃K1. ⇩[0, i] L1 ≡ K1.ⓑ{I}V & K1 ⋕[0, V] K2.
+#L1 #L2 #d #i #H #Hdi #I #K2 #V #HLK2 elim (lleq_inv_lref … H) -H *
+[ #_ #H elim (lt_refl_false i)
+ lapply (ldrop_fwd_length_lt2 … HLK2) -HLK2
+ /2 width=3 by lt_to_le_to_lt/ (**) (* full auto too slow *)
+| -HLK2 #I1 #I2 #K11 #K22 #V1 #V2 #_ #_ #_ #_ #H elim (lt_refl_false i)
+ /2 width=3 by lt_to_le_to_lt/
+| #I0 #K1 #K0 #V0 #HLK1 #HLK0 #HK10 #_ lapply (ldrop_mono … HLK0 … HLK2) -L2
#H destruct /2 width=3 by ex2_intro/
]
qed-.
-lemma lleq_inv_lift: ∀L1,L2,U. L1 ⋕[U] L2 →
- ∀K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 →
- ∀T. ⇧[d, e] T ≡ U → K1 ⋕[T] K2.
-#L1 #L2 #U #H elim H -L1 -L2 -U
-[ #L1 #L2 #k #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H >(lift_inv_sort2 … H) -X
- lapply (ldrop_fwd_length_eq … HLK1 HLK2 HL12) -L1 -L2 -d -e
- /2 width=1 by lleq_sort/ (**) (* full auto fails *)
-| #I #L1 #L2 #K #K0 #W #i #HLK #HLK0 #HK0 #IHK0 #K1 #K2 #d #e #HLK1 #HLK2 #X #H elim (lift_inv_lref2 … H) -H
- * #Hdei #H destruct [ -HK0 | -IHK0 ]
- [ elim (ldrop_conf_lt … HLK1 … HLK) // -L1 #L1 #V #HKL1 #KL1 #HV0
- elim (ldrop_conf_lt … HLK2 … HLK0) // -Hdei -L2 #L2 #V2 #HKL2 #K0L2 #HV02
- lapply (lift_inj … HV02 … HV0) -HV02 #H destruct /3 width=11 by lleq_lref/
- | lapply (ldrop_conf_ge … HLK1 … HLK ?) // -L1
- lapply (ldrop_conf_ge … HLK2 … HLK0 ?) // -Hdei -L2
+lemma lleq_inv_lref_ge_sn: ∀L1,L2,d,i. L1 ⋕[d, #i] L2 → d ≤ i →
+ ∀I,K1,V. ⇩[0, i] L1 ≡ K1.ⓑ{I}V →
+ ∃∃K2. ⇩[0, i] L2 ≡ K2.ⓑ{I}V & K1 ⋕[0, V] K2.
+#L1 #L2 #d #i #HL12 #Hdi #I #K1 #V #HLK1 elim (lleq_inv_lref_ge_dx L2 … Hdi … HLK1) -Hdi -HLK1
+/3 width=3 by lleq_sym, ex2_intro/
+qed-.
+
+fact lleq_inv_S_aux: ∀L1,L2,T,d0. L1 ⋕[d0, T] L2 → ∀d. d0 = d + 1 →
+ ∀K1,K2,I,V. ⇩[0, d] L1 ≡ K1.ⓑ{I}V → ⇩[0, d] L2 ≡ K2.ⓑ{I}V →
+ L1 ⋕[d, T] L2.
+#L1 #L2 #T #d0 #H elim H -L1 -L2 -T -d0
+/2 width=1 by lleq_sort, lleq_free, lleq_gref/
+[ #I1 #I2 #L1 #L2 #K11 #K22 #V1 #V2 #d0 #i #Hid0 #HLK11 #HLK22 #HV1 #_ #IHV1 #IHV2 #d #H #K1 #K2 #J #W #HLK1 #HLK2 destruct
+ elim (le_to_or_lt_eq i d) /2 width=1 by lleq_skip, monotonic_pred/ -Hid0
+ [ -HV1 #Hid
+ lapply (ldrop_fwd_ldrop2 … HLK11) #H1
+ lapply (ldrop_fwd_ldrop2 … HLK22) #H2
+ lapply (ldrop_conf_ge … H1 … HLK1 ?) // -H1 -HLK1
+ lapply (ldrop_conf_ge … H2 … HLK2 ?) // -H2 -HLK2
+ <minus_plus /4 width=10 by lleq_skip, arith_i/
+ | -IHV1 -IHV2 #H destruct
+ lapply (ldrop_mono … HLK11 … HLK1) -HLK11 #H destruct
+ lapply (ldrop_mono … HLK22 … HLK2) -HLK22 #H destruct
/2 width=7 by lleq_lref/
]
-| #L1 #L2 #i #HL1 #HL2 #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H elim (lift_inv_lref2 … H) -H
+| #I #L1 #L2 #K11 #K22 #V #d0 #i #Hid0 #HLK11 #HLK22 #HV #_ #d #H #K1 #K2 #J #W #HLK1 #HLK2 destruct
+ /3 width=7 by lleq_lref, lt_to_le/
+| #a #I #L1 #L2 #V #T #d0 #_ #_ #IHV #IHT #d #H #K1 #K2 #J #W #HLK1 #HLK2 destruct
+ /4 width=6 by lleq_bind, ldrop_ldrop/
+| #I #L1 #L2 #V #T #d0 #_ #_ #IHV #IHT #d #H #K1 #K2 #J #W #HLK1 #HLK2 destruct
+ /3 width=6 by lleq_flat/
+]
+qed-.
+
+lemma lleq_inv_S: ∀T,L1,L2,d. L1 ⋕[d+1, T] L2 →
+ ∀K1,K2,I,V. ⇩[0, d] L1 ≡ K1.ⓑ{I}V → ⇩[0, d] L2 ≡ K2.ⓑ{I}V →
+ L1 ⋕[d, T] L2.
+/2 width=6 by lleq_inv_S_aux/ qed-.
+
+lemma lleq_inv_bind_O: ∀a,I,L1,L2,V,T. L1 ⋕[0, ⓑ{a,I}V.T] L2 →
+ L1 ⋕[0, V] L2 ∧ L1.ⓑ{I}V ⋕[0, T] L2.ⓑ{I}V.
+#a #I #L1 #L2 #V #T #H elim (lleq_inv_bind … H) -H
+/3 width=6 by ldrop_pair, conj, lleq_inv_S/
+qed-.
+
+lemma lleq_inv_lift_le: ∀L1,L2,U,d0. L1 ⋕[d0, U] L2 →
+ ∀K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 →
+ ∀T. ⇧[d, e] T ≡ U → d0 ≤ d → K1 ⋕[d0, T] K2.
+#L1 #L2 #U #d0 #H elim H -L1 -L2 -U -d0
+[ #L1 #L2 #d0 #k #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_sort2 … H) -X
+ lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -d -e
+ /2 width=1 by lleq_sort/
+| #I1 #I2 #L1 #L2 #K11 #K22 #W1 #W2 #d0 #i #Hid0 #HLK11 #HLK22 #HW1 #HW2 #IHW1 #IHW2 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref2 … H) -H
+ * #Hid #H destruct [ -HW1 -HW2 | -IHW1 -IHW2 ]
+ [ elim (ldrop_conf_lt … HLK1 … HLK11) // -L1
+ elim (ldrop_conf_lt … HLK2 … HLK22) // -Hid -L2
+ #L2 #V2 #HKL2 #HKL22 #HVW2 #L1 #V1 #HKL1 #HKL11 #HVW1
+ @(lleq_skip … HKL1 HKL2) -HKL1 -HKL2 /3 width=6 by monotonic_le_minus_l2/ (**) (* full auto fails *)
+ | lapply (ldrop_conf_ge … HLK1 … HLK11 ?) // -L1
+ lapply (ldrop_conf_ge … HLK2 … HLK22 ?) // -Hid -L2
+ #HK22 #HK11 @(lleq_skip … HK11 HK22) -HK11 -HK22
+ /2 width=3 by lleq_ge, le_to_lt_to_lt/ (**) (* full auto fails *)
+ ]
+| #I #L1 #L2 #K11 #K22 #W #d0 #i #Hid0 #HLK11 #HLK22 #HW #IHW #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref2 … H) -H
+ * #Hid #H destruct [ -HW | -IHW ]
+ [ elim (ldrop_conf_lt … HLK1 … HLK11) // -L1 #L1 #V #HKL1 #KL11 #HVW
+ elim (ldrop_conf_lt … HLK2 … HLK22) // -Hid -L2 #L2 #V0 #HKL2 #KL22 #HV0
+ lapply (lift_inj … HV0 … HVW) -HV0 #H destruct /3 width=12 by lleq_lref/
+ | lapply (ldrop_conf_ge … HLK1 … HLK11 ?) // -L1
+ lapply (ldrop_conf_ge … HLK2 … HLK22 ?) // -L2 -Hid0
+ elim (le_inv_plus_l … Hid) -Hid /3 width=7 by lleq_lref, transitive_le/
+ ]
+| #L1 #L2 #d0 #i #HL1 #HL2 #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref2 … H) -H
+ * #_ #H destruct
+ lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12)
+ [ lapply (ldrop_fwd_length_le4 … HLK1) -HLK1
+ lapply (ldrop_fwd_length_le4 … HLK2) -HLK2
+ #HKL2 #HKL1 #HK12 @lleq_free // /2 width=3 by transitive_le/ (**) (* full auto too slow *)
+ | lapply (ldrop_fwd_length … HLK1) -HLK1 #H >H in HL1; -H
+ lapply (ldrop_fwd_length … HLK2) -HLK2 #H >H in HL2; -H
+ /3 width=1 by lleq_free, le_plus_to_minus_r/
+ ]
+| #L1 #L2 #d0 #p #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_gref2 … H) -X
+ lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -d -e
+ /2 width=1 by lleq_gref/
+| #a #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_bind2 … H) -H
+ #V #T #HVW #HTU #H destruct /4 width=6 by lleq_bind, ldrop_skip, le_S_S/
+| #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_flat2 … H) -H
+ #V #T #HVW #HTU #H destruct /3 width=6 by lleq_flat/
+]
+qed-.
+
+lemma lleq_inv_lift_ge: ∀L1,L2,U,d0. L1 ⋕[d0, U] L2 →
+ ∀K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 →
+ ∀T. ⇧[d, e] T ≡ U → d+e ≤ d0 → K1 ⋕[d0-e, T] K2.
+#L1 #L2 #U #d0 #H elim H -L1 -L2 -U -d0
+[ #L1 #L2 #d0 #k #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_sort2 … H) -X
+ lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -d
+ /2 width=1 by lleq_sort/
+| #I1 #I2 #L1 #L2 #K11 #K22 #W1 #W2 #d0 #i #Hid0 #HLK11 #HLK22 #HW1 #HW2 #IHW1 #IHW2 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hded0 elim (lift_inv_lref2 … H) -H
+ * #Hid #H destruct [ -HW1 -HW2 | -IHW1 -IHW2 ]
+ [ elim (ldrop_conf_lt … HLK1 … HLK11) // -L1
+ elim (ldrop_conf_lt … HLK2 … HLK22) // -L2
+ elim (le_inv_plus_l … Hded0) #Hdd0e #_
+ #L2 #V2 #HKL2 #HKL22 #HVW2 #L1 #V1 #HKL1 #HKL11 #HVW1
+ @(lleq_skip … HKL1 HKL2) -HKL1 -HKL2 [ /2 width=3 by lt_to_le_to_lt/ ] (**) (* explicit constructor *)
+ >minus_minus_comm3 /3 width=6 by arith_k_sn/ (**) (* slow *)
+ | lapply (ldrop_conf_ge … HLK1 … HLK11 ?) // -L1
+ lapply (ldrop_conf_ge … HLK2 … HLK22 ?) // -L2 -Hded0
+ elim (le_inv_plus_l … Hid) -Hid #_ #Hei
+ #HK22 #HK11 @(lleq_skip … HK11 HK22) -HK11 -HK22 (**) (* explicit constructor *)
+ [ /2 width=1 by monotonic_lt_minus_l/ ] >arith_b1 //
+ ]
+| #I #L1 #L2 #K11 #K22 #W #d0 #i #Hid0 #HLK11 #HLK22 #HW #_ #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hded0 elim (lift_inv_lref2 … H) -H
+ * #Hid #H destruct
+ [ -I -L1 -L2 -K11 -K22 -W elim (le_plus_xySz_x_false e 0 d)
+ /3 width=3 by transitive_le, le_to_lt_to_lt/
+ | lapply (ldrop_conf_ge … HLK1 … HLK11 ?) // -L1
+ lapply (ldrop_conf_ge … HLK2 … HLK22 ?) // -L2 -Hded0
+ /3 width=7 by lleq_lref, monotonic_le_minus_l/
+ ]
+| #L1 #L2 #d0 #i #HL1 #HL2 #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hded0 elim (lift_inv_lref2 … H) -H
* #_ #H destruct
- lapply (ldrop_fwd_length_eq … HLK1 HLK2 HL12)
- [ /4 width=3 by lleq_free, ldrop_fwd_length_le4, transitive_le/
+ lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12)
+ [ lapply (ldrop_fwd_length_le4 … HLK1) -HLK1
+ lapply (ldrop_fwd_length_le4 … HLK2) -HLK2
+ #HKL2 #HKL1 #HK12 @lleq_free // /2 width=3 by transitive_le/ (**) (* full auto too slow *)
| lapply (ldrop_fwd_length … HLK1) -HLK1 #H >H in HL1; -H
lapply (ldrop_fwd_length … HLK2) -HLK2 #H >H in HL2; -H
/3 width=1 by lleq_free, le_plus_to_minus_r/
]
-| #L1 #L2 #p #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H >(lift_inv_gref2 … H) -X
- lapply (ldrop_fwd_length_eq … HLK1 HLK2 HL12) -L1 -L2 -d -e
- /2 width=1 by lleq_gref/ (**) (* full auto fails *)
-| #a #I #L1 #L2 #W #U #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H elim (lift_inv_bind2 … H) -H
- #V #T #HVW #HTU #H destruct /4 width=5 by lleq_bind, ldrop_skip/
-| #I #L1 #L2 #W #U #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H elim (lift_inv_flat2 … H) -H
+| #L1 #L2 #d0 #p #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_gref2 … H) -X
+ lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -d
+ /2 width=1 by lleq_gref/
+| #a #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hded0 elim (lift_inv_bind2 … H) -H
+ #V #T #HVW #HTU #H destruct
+ elim (le_inv_plus_l … Hded0) #_ #Hed0
+ @lleq_bind [ /2 width=5 by/ ] -IHW (**) (* explicit constructor *)
+ >plus_minus /3 width=5 by ldrop_skip, le_minus_to_plus/
+| #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hded0 elim (lift_inv_flat2 … H) -H
#V #T #HVW #HTU #H destruct /3 width=5 by lleq_flat/
]
qed-.
+lemma lleq_inv_lift_be: ∀L1,L2,U,d0. L1 ⋕[d0, U] L2 →
+ ∀K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 →
+ ∀T. ⇧[d, e] T ≡ U → d ≤ d0 → d0 ≤ d + e → K1 ⋕[d, T] K2.
+#L1 #L2 #U #d0 #H elim H -L1 -L2 -U -d0
+[ #L1 #L2 #d0 #k #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ #_ >(lift_inv_sort2 … H) -X
+ lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -d0 -e
+ /2 width=1 by lleq_sort/
+| #I1 #I2 #L1 #L2 #K11 #K22 #W1 #W2 #d0 #i #Hid0 #HLK11 #HLK22 #_ #_ #IHW1 #IHW2 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hde elim (lift_inv_lref2 … H) -H
+ * #Hid #H destruct
+ [ elim (ldrop_conf_lt … HLK1 … HLK11) // -L1
+ elim (ldrop_conf_lt … HLK2 … HLK22) // -L2 -Hid0
+ #L2 #V2 #HKL2 #HKL22 #HVW2 #L1 #V1 #HKL1 #HKL11 #HVW1
+ @(lleq_skip … HKL1 HKL2) -HKL1 -HKL2 //
+ /3 width=6 by arith_k_dx, monotonic_le_minus_l2/ (**) (* full auto fails *)
+ | -I1 -I2 -L1 -L2 -K11 -K22 -W1 -W2 -Hd0 elim (lt_refl_false i)
+ /3 width=3 by lt_to_le_to_lt, transitive_le/ (**) (* slow *)
+ ]
+| #I #L1 #L2 #K11 #K22 #W #d0 #i #Hid0 #HLK11 #HLK22 #HW #_ #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hde elim (lift_inv_lref2 … H) -H
+ * #Hid #H destruct
+ [ -I -L1 -L2 -K11 -K22 -W -Hde elim (lt_refl_false i)
+ /3 width=3 by lt_to_le_to_lt, transitive_le/ (**) (* slow *)
+ | lapply (ldrop_conf_ge … HLK1 … HLK11 ?) // -L1
+ lapply (ldrop_conf_ge … HLK2 … HLK22 ?) // -L2 -Hid0 -Hd0 -Hde
+ elim (le_inv_plus_l … Hid) -Hid /2 width=7 by lleq_lref/
+ ]
+| #L1 #L2 #d0 #i #HL1 #HL2 #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hde elim (lift_inv_lref2 … H) -H
+ * #_ #H destruct
+ lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12)
+ [ lapply (ldrop_fwd_length_le4 … HLK1) -HLK1
+ lapply (ldrop_fwd_length_le4 … HLK2) -HLK2
+ #HKL2 #HKL1 #HK12 @lleq_free // /2 width=3 by transitive_le/ (**) (* full auto too slow *)
+ | lapply (ldrop_fwd_length … HLK1) -HLK1 #H >H in HL1; -H
+ lapply (ldrop_fwd_length … HLK2) -HLK2 #H >H in HL2; -H
+ /3 width=1 by lleq_free, le_plus_to_minus_r/
+ ]
+| #L1 #L2 #d0 #p #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ #_ >(lift_inv_gref2 … H) -X
+ lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -d0 -e
+ /2 width=1 by lleq_gref/
+| #a #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hde elim (lift_inv_bind2 … H) -H
+ #V #T #HVW #HTU #H destruct
+ @lleq_bind [ /2 width=5 by/ ] -IHW
+ @(IHU … HTU) -IHU -HTU /2 width=1 by ldrop_skip, le_S_S/ (**) (* full auto too slow *)
+| #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hde elim (lift_inv_flat2 … H) -H
+ #V #T #HVW #HTU #H destruct /3 width=6 by lleq_flat/
+]
+qed-.
+
(* Advanced properties ******************************************************)
-lemma lleq_dec: ∀T,L1,L2. Decidable (L1 ⋕[T] L2).
+lemma lleq_lift_le: ∀K1,K2,T,d0. K1 ⋕[d0, T] K2 →
+ ∀L1,L2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 →
+ ∀U. ⇧[d, e] T ≡ U → d0 ≤ d → L1 ⋕[d0, U] L2.
+#K1 #K2 #T #d0 #H elim H -K1 -K2 -T -d0
+[ #K1 #K2 #d0 #k #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_sort1 … H) -X
+ lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -d
+ /2 width=1 by lleq_sort/
+| #I1 #I2 #K1 #K2 #K11 #K22 #V1 #V2 #d0 #i #Hid0 #HK11 #HK22 #_ #_ #IHV1 #IHV2 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H
+ * #Hdi #H destruct
+ [ elim (ldrop_trans_lt … HLK1 … HK11) // -K1
+ elim (ldrop_trans_lt … HLK2 … HK22) // -K2
+ #K2 #W2 #HLK2 #HK22 #HVW2 #K1 #W1 #HLK1 #HK11 #HVW1 -Hdi
+ @(lleq_skip … HLK1 HLK2) // /3 width=6 by monotonic_le_minus_l2/ (**) (* full auto fails *)
+ | elim (lt_refl_false i) -I1 -I2 -L1 -L2 -K1 -K2 -K11 -K22 -V1 -V2 -e
+ /3 width=3 by lt_to_le_to_lt, transitive_le/ (**) (* slow *)
+ ]
+| #I #K1 #K2 #K11 #K22 #V #d0 #i #Hid0 #HK11 #HK22 #HV #IHV #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H
+ * #Hdi #H destruct [ -HV | -IHV ]
+ [ elim (ldrop_trans_lt … HLK1 … HK11) // -K1 #K1 #W #HLK1 #HK11 #HVW
+ elim (ldrop_trans_lt … HLK2 … HK22) // -Hdi -K2 #K2 #W2 #HLK2 #HK22 #HVW2
+ lapply (lift_mono … HVW2 … HVW) -HVW2 #H destruct /3 width=12 by lleq_lref/
+ | lapply (ldrop_trans_ge … HLK1 … HK11 ?) // -K1
+ lapply (ldrop_trans_ge … HLK2 … HK22 ?) // -Hdi -K2
+ /3 width=7 by lleq_lref, transitive_le/
+ ]
+| #K1 #K2 #d0 #i #HK1 #HK2 #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H
+ * #Hid #H destruct
+ lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -HK12
+ [ /3 width=6 by lleq_free, ldrop_fwd_be/
+ | lapply (ldrop_fwd_length … HLK1) -HLK1 #HLK1
+ lapply (ldrop_fwd_length … HLK2) -HLK2 #HLK2
+ @lleq_free [ >HLK1 | >HLK2 ] -Hid -HLK1 -HLK2 /2 width=1 by monotonic_le_plus_r/ (**) (* explicit constructor *)
+ ]
+| #K1 #K2 #d0 #p #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_gref1 … H) -X
+ lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -d -e
+ /2 width=1 by lleq_gref/
+| #a #I #K1 #K2 #V #T #d0 #_ #_ #IHV #IHT #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_bind1 … H) -H
+ #W #U #HVW #HTU #H destruct /4 width=6 by lleq_bind, ldrop_skip, le_S_S/
+| #I #K1 #K2 #V #T #d0 #_ #_ #IHV #IHT #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_flat1 … H) -H
+ #W #U #HVW #HTU #H destruct /3 width=6 by lleq_flat/
+]
+qed-.
+
+lemma lleq_lift_ge: ∀K1,K2,T,d0. K1 ⋕[d0, T] K2 →
+ ∀L1,L2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 →
+ ∀U. ⇧[d, e] T ≡ U → d ≤ d0 → L1 ⋕[d0+e, U] L2.
+#K1 #K2 #T #d0 #H elim H -K1 -K2 -T -d0
+[ #K1 #K2 #d0 #k #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_sort1 … H) -X
+ lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -d
+ /2 width=1 by lleq_sort/
+| #I1 #I2 #K1 #K2 #K11 #K22 #V1 #V2 #d0 #i #hid0 #HK11 #HK22 #HV1 #HV2 #IHV1 #IHV2 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H
+ * #Hdi #H destruct [ -HV1 -HV2 | -IHV1 -IHV2 ]
+ [ elim (ldrop_trans_lt … HLK1 … HK11) // -K1 #K1 #W1 #HLK1 #HK11 #HVW1
+ elim (ldrop_trans_lt … HLK2 … HK22) // -K2 #K2 #W2 #HLK2 #HK22 #HVW2
+ @(lleq_skip … HLK1 HLK2) -HLK1 -HLK2 (**) (* explicit constructor *)
+ [ /2 width=3 by lt_to_le_to_lt/ ]
+ >arith_i /3 width=5 by monotonic_le_minus_l2/
+ | lapply (ldrop_trans_ge_comm … HLK1 … HK11 ?) // -K1
+ lapply (ldrop_trans_ge_comm … HLK2 … HK22 ?) // -K2
+ /4 width=10 by lleq_skip, monotonic_lt_plus_l/
+ ]
+| #I #K1 #K2 #K11 #K22 #V #d0 #i #Hid0 #HK11 #HK22 #HV #_ #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H
+ * #Hid #H destruct
+ [ elim (lt_refl_false i) -I -L1 -L2 -K1 -K2 -K11 -K22 -V -e
+ /3 width=3 by lt_to_le_to_lt, transitive_le/ (**) (* slow *)
+ | lapply (ldrop_trans_ge … HLK1 … HK11 ?) // -K1
+ lapply (ldrop_trans_ge … HLK2 … HK22 ?) // -Hid -K2
+ /3 width=7 by lleq_lref, monotonic_le_plus_l/
+ ]
+| #K1 #K2 #d0 #i #HK1 #HK2 #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H
+ * #Hid #H destruct
+ lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -HK12
+ [ /3 width=6 by lleq_free, ldrop_fwd_be/
+ | lapply (ldrop_fwd_length … HLK1) -HLK1 #HLK1
+ lapply (ldrop_fwd_length … HLK2) -HLK2 #HLK2
+ @lleq_free [ >HLK1 | >HLK2 ] -Hid -HLK1 -HLK2 /2 width=1 by monotonic_le_plus_r/ (**) (* explicit constructor *)
+ ]
+| #K1 #K2 #d0 #p #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_gref1 … H) -X
+ lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -d
+ /2 width=1 by lleq_gref/
+| #a #I #K1 #K2 #V #T #d0 #_ #_ #IHV #IHT #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_bind1 … H) -H
+ #W #U #HVW #HTU #H destruct /4 width=5 by lleq_bind, ldrop_skip, le_minus_to_plus/
+| #I #K1 #K2 #V #T #d0 #_ #_ #IHV #IHT #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_flat1 … H) -H
+ #W #U #HVW #HTU #H destruct /3 width=5 by lleq_flat/
+]
+qed-.
+
+lemma lleq_be: ∀L1,L2,U,d0. L1 ⋕[d0, U] L2 →
+ ∀K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 →
+ ∀T. ⇧[d, e] T ≡ U → d ≤ d0 → d0 ≤ d + e → L1 ⋕[d, U] L2.
+#L1 #L2 #U #d0 #H elim H -L1 -L2 -U -d0
+/2 width=1 by lleq_sort, lleq_free, lleq_gref/
+[ #I1 #I2 #L1 #L2 #K11 #K22 #W1 #W2 #d0 #i #Hid0 #HLK11 #HLK22 #_ #_ #IHW1 #IHW2 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hd0de elim (lift_inv_lref2 … H) -H
+ * #Hid #H destruct [ -Hid0 | -Hd0 ]
+ [ elim (ldrop_conf_lt … HLK1 … HLK11) // -HLK1
+ elim (ldrop_conf_lt … HLK2 … HLK22) // -HLK2
+ #L2 #V2 #_ #HKL22 #HVW2 #L1 #V1 #_ #HKL21 #HVW1
+ @(lleq_skip … HLK11 HLK22) -HLK11 -HLK22 //
+ /3 width=8 by arith_k_dx, monotonic_le_minus_l2/ (**) (* full auto fails *)
+ | -I1 -I2 -K11 -K22 -K1 -K2 -W1 -W2 elim (lt_refl_false … i) -L1 -L2
+ @(lt_to_le_to_lt … Hid0) -Hid0 /2 width=3 by transitive_le/ (**) (* full auto too slow *)
+ ]
+| #I #L1 #L2 #K11 #K22 #W #d0 #i #Hid0 #HLK11 #HLK22 #HW #_ #K1 #K2 #d #e #_ #_ #X #H #Hd0 #_ elim (lift_inv_lref2 … H) -H
+ * #Hid #H destruct
+ [ -I -K1 -K2 -K11 -K22 -W elim (lt_refl_false i)
+ @(lt_to_le_to_lt … Hid) -Hid /2 width=3 by transitive_le/ (**) (* full auto too slow *)
+ | -d0 /3 width=7 by lleq_lref, le_plus_b/
+ ]
+| #a #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hde elim (lift_inv_bind2 … H) -H
+ #V #T #HVW #HTU #H destruct
+ @lleq_bind [ /2 width=8 by/ ] -IHW
+ @(IHU … HTU) -IHU -HTU /2 width=2 by ldrop_skip, le_S_S/ (**) (* full auto too slow *)
+| #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hde elim (lift_inv_flat2 … H) -H
+ #V #T #HVW #HTU #H destruct /3 width=8 by lleq_flat/
+]
+qed-.
+
+axiom- lleq_dec: ∀T,L1,L2,d. Decidable (L1 ⋕[d, T] L2).
+(*
#T #L1 @(f2_ind … rfw … L1 T) -L1 -T
#n #IH #L1 * *
[ #k #Hn #L2 elim (eq_nat_dec (|L1|) (|L2|)) /3 width=1 by or_introl, lleq_sort/
| #i #H1 #L2 elim (eq_nat_dec (|L1|) (|L2|))
- [ #HL12 elim (lt_or_ge i (|L1|))
+ [ #HL12 #d elim (lt_or_ge i d) /3 width=1 by lleq_skip, or_introl/
+ #Hdi elim (lt_or_ge i (|L1|))
#HiL1 elim (lt_or_ge i (|L2|)) /3 width=1 by or_introl, lleq_free/
#HiL2 elim (ldrop_O1_lt … HiL2)
#I2 #K2 #V2 #HLK2 elim (ldrop_O1_lt … HiL1)
#I1 #K1 #V1 #HLK1 elim (eq_bind2_dec I2 I1)
[ #H2 elim (eq_term_dec V2 V1)
- [ #H3 elim (IH K1 V1 … K2) destruct
+ [ #H3 elim (IH K1 V1 … K2 0) destruct
/3 width=7 by lleq_lref, ldrop_fwd_rfw, or_introl/
]
]
-IH #H3 @or_intror
- #H elim (lleq_inv_lref … H) -H *
- [1,3,5: /3 width=4 by lt_to_le_to_lt, lt_refl_false/ ]
+ #H elim (lleq_inv_lref … H) -H [1,3,4,6,7,9: * ]
+ [1,3,5,7,8,9: /3 width=4 by lt_to_le_to_lt, lt_refl_false/ ]
#I0 #X1 #X2 #V0 #HLX1 #HLX2 #HX12
lapply (ldrop_mono … HLX1 … HLK1) -HLX1 -HLK1
lapply (ldrop_mono … HLX2 … HLK2) -HLX2 -HLK2
#H #H0 destruct /2 width=1 by/
]
| #p #Hn #L2 elim (eq_nat_dec (|L1|) (|L2|)) /3 width=1 by or_introl, lleq_gref/
-| #a #I #V #T #Hn #L2 destruct
- elim (IH L1 V … L2) /2 width=1 by/
- elim (IH (L1.ⓑ{I}V) T … (L2.ⓑ{I}V)) -IH /3 width=1 by or_introl, lleq_bind/
+| #a #I #V #T #Hn #L2 #d destruct
+ elim (IH L1 V … L2 d) /2 width=1 by/
+ elim (IH (L1.ⓑ{I}V) T … (L2.ⓑ{I}V) (d+1)) -IH /3 width=1 by or_introl, lleq_bind/
#H1 #H2 @or_intror
#H elim (lleq_inv_bind … H) -H /2 width=1 by/
-| #I #V #T #Hn #L2 destruct
- elim (IH L1 V … L2) /2 width=1 by/
- elim (IH L1 T … L2) -IH /3 width=1 by or_introl, lleq_flat/
+| #I #V #T #Hn #L2 #d destruct
+ elim (IH L1 V … L2 d) /2 width=1 by/
+ elim (IH L1 T … L2 d) -IH /3 width=1 by or_introl, lleq_flat/
#H1 #H2 @or_intror
#H elim (lleq_inv_flat … H) -H /2 width=1 by/
]
--n /4 width=2 by lleq_fwd_length, or_intror/
+-n /4 width=3 by lleq_fwd_length, or_intror/
qed-.
-
+*)
(* Main properties **********************************************************)
-theorem lleq_trans: ∀T. Transitive … (lleq T).
-#T #L1 #L #H elim H -T -L1 -L
-/4 width=4 by lleq_fwd_length, lleq_gref, lleq_sort, trans_eq/
-[ #I #L1 #L #K1 #K #V #i #HLK1 #HLK #_ #IHK1 #L2 #H elim (lleq_inv_lref … H) -H *
- [ -HLK1 -IHK1 #HLi #_ elim (lt_refl_false i)
- /3 width=5 by ldrop_fwd_length_lt2, lt_to_le_to_lt/
- | #I0 #K0 #K2 #V0 #HLK0 #HLK2 #HK12 lapply (ldrop_mono … HLK0 … HLK) -L
+axiom- lleq_trans: ∀d,T. Transitive … (lleq d T).
+(*
+#d #T #L1 #L #H elim H -d -T -L1 -L
+/4 width=5 by lleq_fwd_length, lleq_gref, lleq_sort, trans_eq/
+[ #L1 #L #d #i #Hid #HL1 #L2 #H lapply (lleq_fwd_length … H)
+ #HL2 elim (lleq_inv_lref … H) -H /2 width=1 by lleq_skip/
+| #I #L1 #L #K1 #K #V #d #i #Hdi #HLK1 #HLK #_ #IHK1 #L2 #H elim (lleq_inv_lref … H) -H
+ [ -HLK1 -IHK1 * #HLi #_ elim (lt_refl_false i)
+ /3 width=5 by ldrop_fwd_length_lt2, lt_to_le_to_lt/ (**) (* slow *)
+ | -K1 -K #Hid elim (lt_refl_false i) /2 width=3 by lt_to_le_to_lt/
+ | * #I0 #K0 #K2 #V0 #HLK0 #HLK2 #HK12 lapply (ldrop_mono … HLK0 … HLK) -L
#H destruct /3 width=7 by lleq_lref/
]
-| #L1 #L #i #HL1i #HLi #HL #L2 #H lapply (lleq_fwd_length … H)
- #HL2 elim (lleq_inv_lref … H) -H * /2 width=1 by lleq_free/
-| #a #I #L1 #L #V #T #_ #_ #IHV #IHT #L2 #H elim (lleq_inv_bind … H) -H
+| #L1 #L #d #i #HL1i #HLi #HL #L2 #H lapply (lleq_fwd_length … H)
+ #HL2 elim (lleq_inv_lref … H) -H /2 width=1 by lleq_free/
+| #a #I #L1 #L #V #T #d #_ #_ #IHV #IHT #L2 #H elim (lleq_inv_bind … H) -H
/3 width=1 by lleq_bind/
-| #I #L1 #L #V #T #_ #_ #IHV #IHT #L2 #H elim (lleq_inv_flat … H) -H
+| #I #L1 #L #V #T #d #_ #_ #IHV #IHT #L2 #H elim (lleq_inv_flat … H) -H
/3 width=1 by lleq_flat/
]
qed-.
-
-theorem lleq_canc_sn: ∀L,L1,L2,T. L ⋕[T] L1→ L ⋕[T] L2 → L1 ⋕[T] L2.
+*)
+theorem lleq_canc_sn: ∀L,L1,L2,T,d. L ⋕[d, T] L1→ L ⋕[d, T] L2 → L1 ⋕[d, T] L2.
/3 width=3 by lleq_trans, lleq_sym/ qed-.
-theorem lleq_canc_dx: ∀L1,L2,L,T. L1 ⋕[T] L → L2 ⋕[T] L → L1 ⋕[T] L2.
+theorem lleq_canc_dx: ∀L1,L2,L,T,d. L1 ⋕[d, T] L → L2 ⋕[d, T] L → L1 ⋕[d, T] L2.
/3 width=3 by lleq_trans, lleq_sym/ qed-.
(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
-notation "hvbox( ⫰ term 55 T )"
- non associative with precedence 55
+notation "hvbox( ⫰ term 70 T )"
+ non associative with precedence 70
for @{ 'Predecessor $T }.
(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
-notation "hvbox( ⫯ term 55 T )"
- non associative with precedence 55
+notation "hvbox( ⫯ term 70 T )"
+ non associative with precedence 70
for @{ 'Successor $T }.
#x #Hx #H destruct //
qed-.
+(* Forward lemmas on successor **********************************************)
+
+lemma yle_fwd_succ1: ∀m,n. ⫯m ≤ n → m ≤ ⫰n.
+#m #x #H elim (yle_inv_succ1 … H) -H
+#n #Hmn #H destruct //
+qed-.
+
(* Basic properties *********************************************************)
+lemma le_O1: ∀n:ynat. 0 ≤ n.
+* /2 width=1 by yle_inj/
+qed.
+
lemma yle_refl: reflexive … yle.
* /2 width=1 by le_n, yle_inj/
qed.
(* Properties on successor **************************************************)
+lemma yle_succ: ∀m,n. m ≤ n → ⫯m ≤ ⫯n.
+#m #n * -m -n /3 width=1 by yle_inj, le_S_S/
+qed.
+
lemma yle_succ_dx: ∀m,n. m ≤ n → m ≤ ⫯n.
#m #n * -m -n /3 width=1 by le_S, yle_inj/
qed.
lemma ylt_inv_Y2: ∀x. x < ∞ → ∃m. x = yinj m.
/2 width=3 by ylt_inv_Y2_aux/ qed-.
+lemma ylt_inv_O1: ∀n. 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 → ∃∃n. m < n & y = ⫯n.
lemma ylt_inv_succ1: ∀m,y. ⫯m < y → ∃∃n. m < n & y = ⫯n.
/2 width=3 by ylt_inv_succ1_aux/ qed-.
-lemma yle_inv_succ: ∀m,n. ⫯m < ⫯n → m < n.
+lemma ylt_inv_succ: ∀m,n. ⫯m < ⫯n → m < n.
#m #n #H elim (ylt_inv_succ1 … H) -H
#x #Hx #H destruct //
qed-.
]
qed-.
-lemma ylt_inv_succ2: ∀m,n. m < ⫯n → m ≤ n.
+(* Forward lemmas on successor **********************************************)
+
+lemma ylt_fwd_succ2: ∀m,n. m < ⫯n → m ≤ n.
/2 width=3 by ylt_inv_succ2_aux/ qed-.
(* inversion and forward lemmas on yle **************************************)
]
qed-.
+(* Properties on successor **************************************************)
+
+lemma ylt_O_succ: ∀n. 0 < ⫯n.
+* /2 width=1 by ylt_inj/
+qed.
+
(* Properties on yle ********************************************************)
lemma yle_to_ylt_or_eq: ∀m:ynat. ∀n:ynat. m ≤ n → m < n ∨ m = n.
--- /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".
+
+(* NATURAL NUMBERS WITH INFINITY ********************************************)
+
+(* subtraction *)
+definition yminus: ynat → ynat → ynat ≝ λx,y. match y with
+[ yinj n ⇒ ypred^n x
+| Y ⇒ yinj 0
+].
+
+interpretation "ynat minus" 'minus x y = (yminus x y).
+
+(* Basic properties *********************************************************)
+
+lemma yminus_inj: ∀n,m. yinj m - yinj n = yinj (m - n).
+#n elim n -n /2 width=3 by trans_eq/
+qed.
+
+lemma yminus_Y_inj: ∀n. ∞ - yinj n = ∞.
+#n elim n -n // normalize
+#n #IHn >IHn //
+qed.
+
+(* Properties on successor **************************************************)
+
+lemma yminus_succ: ∀n,m. ⫯m - ⫯n = m - n.
+* // #n * [2: >yminus_Y_inj // ]
+#m >yminus_inj //
+qed.
+
+(* Properties on order ******************************************************)
+
+lemma yle_minus_sn: ∀n,m. m - n ≤ m.
+* // #n * /2 width=1 by yle_inj/
+qed.
+
+lemma yle_to_minus: ∀m:ynat. ∀n:ynat. m ≤ n → m - n = 0.
+#m #n * -m -n /3 width=3 by eq_minus_O, eq_f/
+qed-.
+
+lemma yminus_to_le: ∀n:ynat. ∀m:ynat. m - n = 0 → m ≤ n.
+* // #n *
+[ #m >yminus_inj #H lapply (yinj_inj … H) -H (**) (* destruct lemma needed *)
+ /2 width=1 by yle_inj/
+| >yminus_Y_inj #H destruct
+]
+qed.
(* *)
(**************************************************************************)
-include "ground_2/ynat/ynat_lt.ma".
+include "ground_2/ynat/ynat_minus.ma".
(* NATURAL NUMBERS WITH INFINITY ********************************************)
(* addition *)
-definition yplus: ynat → ynat → ynat ≝ λx,y. match x with
-[ yinj m ⇒ ysucc^m y
+definition yplus: ynat → ynat → ynat ≝ λx,y. match y with
+[ yinj n ⇒ ysucc^n x
| Y ⇒ Y
].
(* Properties on successor **************************************************)
-lemma yplus_succ1: ∀m,n. (⫯m) + n = ⫯(m + n).
-* //
+lemma yplus_succ2: ∀m,n. m + ⫯n = ⫯(m + n).
+#m * //
+qed.
+
+lemma yplus_succ1: ∀m,n. ⫯m + n = ⫯(m + n).
+#m * normalize //
qed.
-lemma yplus_SO1: ∀m. 1 + m = ⫯m.
+lemma yplus_succ_swap: ∀m,n. m + ⫯n = ⫯m + n.
+// qed.
+
+lemma yplus_SO2: ∀m. m + 1 = ⫯m.
* //
-qed.
+qed.
(* Basic properties *********************************************************)
-lemma yplus_inj: ∀m,n. yinj m + yinj n = yinj (m + n).
-#m elim m -m //
-#m #IHm #n >(yplus_succ1 m) >IHm -IHm //
+lemma yplus_inj: ∀n,m. yinj m + yinj n = yinj (m + n).
+#n elim n -n [ normalize // ]
+#n #IHn #m >(yplus_succ2 ? n) >IHn -IHn
+<plus_n_Sm //
qed.
-lemma yplus_Y2: ∀m. (m + ∞) = ∞.
+lemma yplus_Y1: ∀m. ∞ + m = ∞.
* normalize //
qed.
qed.
lemma yplus_assoc: associative … yplus.
-* // #x * //
-#y #z >yplus_inj whd in ⊢ (??%%); >iter_plus //
+#x #y * // #z cases y -y
+[ #y >yplus_inj whd in ⊢ (??%%); <iter_plus //
+| >yplus_Y1 //
+]
qed.
+lemma yplus_O_sn: ∀n:ynat. 0 + n = n.
+#n >yplus_comm // qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma yplus_inv_inj: ∀z,y,x. x + y = yinj z →
+ ∃∃m,n. m + n = z & x = yinj m & y = yinj n.
+#z * [2: normalize #x #H destruct ]
+#y * [2: >yplus_Y1 #H destruct ]
+/3 width=5 by yinj_inj, ex3_2_intro/
+qed-.
+
+(* Properties on order ******************************************************)
+
+lemma yle_plus_dx2: ∀n,m. n ≤ m + n.
+* //
+#n elim n -n //
+#n #IHn #m >(yplus_succ2 ? n) @(yle_succ n) // (**) (* full auto fails *)
+qed.
+
+lemma yle_plus_dx1: ∀n,m. m ≤ m + n.
+// qed.
+
+(* Forward lemmas on order **************************************************)
+
+lemma yle_fwd_plus_sn2: ∀x,y,z. x + y ≤ z → y ≤ z.
+/2 width=3 by yle_trans/ qed-.
+
+lemma yle_fwd_plus_sn1: ∀x,y,z. x + y ≤ z → x ≤ z.
+/2 width=3 by yle_trans/ qed-.
projects / helm.git / commitdiff