- ynat: some additions

- lleq: we are ready to remove the old definition :)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma
index 80688b96309012bbb0e888c7c2041ad70f688ca1..05b77349e21a65356138862f6dc7620a1f4d20fa 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma
@@ -103,6 +103,37 @@ lapply (cpy_weak … HT12 0 (d + e) ? ?) -HT12
 /2 width=2 by cpy_weak_top/
 qed-.
 
+lemma cpy_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 →
+              ∀T1,d,e. ⇧[d, e] T1 ≡ U1 →
+              d ≤ dt → d + e ≤ dt + et →
+              ∃∃T2. ⦃G, L⦄ ⊢ U1 ▶×[d+e, dt+et-(d+e)] U2 & ⇧[d, e] T2 ≡ U2.
+#G #L #U1 #U2 #dt #et #H elim H -G -L -U1 -U2 -dt -et
+[ * #i #G #L #dt #et #T1 #d #e #H #_
+  [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by ex2_intro/
+  | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3 by lift_lref_ge_minus, lift_lref_lt, ex2_intro/
+  | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by ex2_intro/
+  ]
+| #I #G #L #K #V #W #i #dt #et #Hdti #Hidet #HLK #HVW #T1 #d #e #H #Hddt #Hdedet
+  elim (lift_inv_lref2 … H) -H * #Hid #H destruct [ -V -Hidet -Hdedet | -Hdti -Hddt ]
+  [ elim (ylt_yle_false … Hddt) -Hddt /3 width=3 by yle_ylt_trans, ylt_inj/
+  | elim (le_inv_plus_l … Hid) #Hdie #Hei
+    elim (lift_split … HVW d (i-e+1) ? ? ?) [2,3,4: /2 width=1 by le_S_S, le_S/ ] -Hdie
+    #T2 #_ >plus_minus // <minus_minus /2 width=1 by le_S/ <minus_n_n <plus_n_O #H -Hei
+    @(ex2_intro … H) -H @(cpy_subst … HLK HVW) /2 width=1 by yle_inj/ >ymax_pre_sn_comm // (**) (* explicit constructor *)
+  ]
+| #a #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #X #d #e #H #Hddt #Hdedet
+  elim (lift_inv_bind2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct
+  elim (IHW12 … HVW1) -V1 -IHW12 //
+  elim (IHU12 … HTU1) -T1 -IHU12 /2 width=1 by yle_succ/
+  <yplus_inj >yplus_SO2 >yplus_succ1 >yplus_succ1
+  /3 width=2 by cpy_bind, lift_bind, ex2_intro/
+| #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #X #d #e #H #Hddt #Hdedet
+  elim (lift_inv_flat2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct
+  elim (IHW12 … HVW1) -V1 -IHW12 // elim (IHU12 … HTU1) -T1 -IHU12
+  /3 width=2 by cpy_flat, lift_flat, ex2_intro/
+]
+qed-.
+
 lemma cpy_split_up: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶×[d, e] T2 → ∀i. i ≤ d + e →
                     ∃∃T. ⦃G, L⦄ ⊢ T1 ▶×[d, i-d] T & ⦃G, L⦄ ⊢ T ▶×[i, d+e-i] T2.
 #G #L #T1 #T2 #d #e #H elim H -G -L -T1 -T2 -d -e
@@ -248,6 +279,12 @@ qed-.
 lemma cpy_inv_refl_O2: ∀G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 ▶×[d, 0] T2 → T1 = T2.
 /2 width=6 by cpy_inv_refl_O2_aux/ qed-.
 
+lemma cpy_inv_lift1_eq: ∀G,T1,U1,d,e. ⇧[d, e] T1 ≡ U1 →
+                        ∀L,U2. ⦃G, L⦄ ⊢ U1 ▶×[d, e] U2 → U1 = U2.
+#G #T1 #U1 #d #e #HTU1 #L #U2 #HU12 elim (cpy_up … HU12 … HTU1) -HU12 -HTU1
+/2 width=4 by cpy_inv_refl_O2/
+qed-.
+
 (* Basic forward lemmas *****************************************************)
 
 lemma cpy_fwd_tw: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶×[d, e] T2 → ♯{T1} ≤ ♯{T2}.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_lift.ma
index 7cb26f477db1a7fa5dce2a154039de8773bbcca1..85203f2031091017a97e5073f530aa3d5f5aa25d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_lift.ma
@@ -17,7 +17,7 @@ include "basic_2/relocation/cpy.ma".
 
 (* CONTEXT-SENSITIVE EXTENDED ORDINARY SUBSTITUTION FOR TERMS ***************)
 
-(* Relocation properties ****************************************************)
+(* Properties on relocation *************************************************)
 
 lemma cpy_lift_le: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶×[dt, et] T2 →
                    ∀L,U1,U2,d,e. ⇩[d, e] L ≡ K →
@@ -103,15 +103,17 @@ lemma cpy_lift_ge: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶×[dt, et] T2 →
 ]
 qed-.
 
+(* Inversion lemmas on relocation *******************************************)
+
 lemma cpy_inv_lift1_le: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 →
                         ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
                         dt + et ≤ d →
                         ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶×[dt, et] T2 & ⇧[d, e] T2 ≡ U2.
 #G #L #U1 #U2 #dt #et #H elim H -G -L -U1 -U2 -dt -et
-[ * #G #L #i #dt #et #K #d #e #_ #T1 #H #_
-  [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by cpy_atom, lift_sort, ex2_intro/
-  | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3 by cpy_atom, lift_lref_ge_minus, lift_lref_lt, ex2_intro/
-  | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by cpy_atom, lift_gref, ex2_intro/
+[ * #i #G #L #dt #et #K #d #e #_ #T1 #H #_
+  [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by ex2_intro/
+  | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3 by lift_lref_ge_minus, lift_lref_lt, ex2_intro/
+  | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by ex2_intro/
   ]
 | #I #G #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #d #e #HLK #T1 #H #Hdetd
   lapply (ylt_yle_trans … Hdetd … Hidet) -Hdetd #Hid
@@ -119,14 +121,14 @@ lemma cpy_inv_lift1_le: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 
   lapply (lift_inv_lref2_lt … H … Hid) -H #H destruct
   elim (ldrop_conf_lt … HLK … HLKV) -L // #L #U #HKL #_ #HUV
   elim (lift_trans_le … HUV … HVW) -V // >minus_plus <plus_minus_m_m // -Hid /3 width=5 by cpy_subst, ex2_intro/
-| #a #I #G #L #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdetd
-  elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
-  elim (IHV12 … HLK … HWV1) -V1 // #W2 #HW12 #HWV2
+| #a #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #d #e #HLK #X #H #Hdetd
+  elim (lift_inv_bind2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct
+  elim (IHW12 … HLK … HVW1) -W1 // #V2 #HV12 #HVW2
   elim (IHU12 … HTU1) -IHU12 -HTU1
   /3 width=5 by cpy_bind, yle_succ, ldrop_skip, lift_bind, ex2_intro/
-| #I #G #L #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdetd
-  elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
-  elim (IHV12 … HLK … HWV1) -V1 //
+| #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #d #e #HLK #X #H #Hdetd
+  elim (lift_inv_flat2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct
+  elim (IHW12 … HLK … HVW1) -W1 //
   elim (IHU12 … HLK … HTU1) -U1 -HLK
   /3 width=5 by cpy_flat, lift_flat, ex2_intro/
 ]
@@ -137,10 +139,10 @@ lemma cpy_inv_lift1_be: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 
                         dt ≤ d → d + e ≤ dt + et →
                         ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶×[dt, et-e] T2 & ⇧[d, e] T2 ≡ U2.
 #G #L #U1 #U2 #dt #et #H elim H -G -L -U1 -U2 -dt -et
-[ * #G #L #i #dt #et #K #d #e #_ #T1 #H #_
-  [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by cpy_atom, lift_sort, ex2_intro/
-  | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3 by cpy_atom, lift_lref_ge_minus, lift_lref_lt, ex2_intro/
-  | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by cpy_atom, lift_gref, ex2_intro/
+[ * #i #G #L #dt #et #K #d #e #_ #T1 #H #_ #_
+  [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by ex2_intro/
+  | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3 by lift_lref_ge_minus, lift_lref_lt, ex2_intro/
+  | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by ex2_intro/
   ]
 | #I #G #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #d #e #HLK #T1 #H #Hdtd #Hdedet
   lapply (yle_fwd_plus_ge_inj … Hdtd Hdedet) #Heet
@@ -158,14 +160,14 @@ lemma cpy_inv_lift1_be: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 
     @(ex2_intro … H) @(cpy_subst … HKV HV1) // (**) (* explicit constructor *)
     >yplus_minus_assoc_inj /3 width=1 by monotonic_ylt_minus_dx, yle_inj/
   ]
-| #a #I #G #L #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdtd #Hdedet
-  elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
-  elim (IHV12 … HLK … HWV1) -V1 // #W2 #HW12 #HWV2
+| #a #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #d #e #HLK #X #H #Hdtd #Hdedet
+  elim (lift_inv_bind2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct
+  elim (IHW12 … HLK … HVW1) -W1 // #V2 #HV12 #HVW2
   elim (IHU12 … HTU1) -U1
   /3 width=5 by cpy_bind, ldrop_skip, lift_bind, yle_succ, ex2_intro/
-| #I #G #L #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdtd #Hdedet
-  elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
-  elim (IHV12 … HLK … HWV1) -V1 //
+| #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #d #e #HLK #X #H #Hdtd #Hdedet
+  elim (lift_inv_flat2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct
+  elim (IHW12 … HLK … HVW1) -W1 //
   elim (IHU12 … HLK … HTU1) -U1 -HLK //
   /3 width=5 by cpy_flat, lift_flat, ex2_intro/
 ]
@@ -176,10 +178,10 @@ lemma cpy_inv_lift1_ge: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 
                         d + e ≤ dt →
                         ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶×[dt-e, et] T2 & ⇧[d, e] T2 ≡ U2.
 #G #L #U1 #U2 #dt #et #H elim H -G -L -U1 -U2 -dt -et
-[ * #G #L #i #dt #et #K #d #e #_ #T1 #H #_
-  [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by cpy_atom, lift_sort, ex2_intro/
-  | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3 by cpy_atom, lift_lref_ge_minus, lift_lref_lt, ex2_intro/
-  | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by cpy_atom, lift_gref, ex2_intro/
+[ * #i #G #L #dt #et #K #d #e #_ #T1 #H #_
+  [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by ex2_intro/
+  | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3 by lift_lref_ge_minus, lift_lref_lt, ex2_intro/
+  | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by ex2_intro/
   ]
 | #I #G #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #d #e #HLK #T1 #H #Hdedt
   lapply (yle_trans … Hdedt … Hdti) #Hdei
@@ -193,35 +195,20 @@ lemma cpy_inv_lift1_ge: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 
   [ /2 width=1 by monotonic_yle_minus_dx/
   | <yplus_minus_comm_inj /2 width=1 by monotonic_ylt_minus_dx/
   ]
-| #a #I #G #L #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdetd
-  elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
+| #a #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #d #e #HLK #X #H #Hdetd
+  elim (lift_inv_bind2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct
   elim (yle_inv_plus_inj2 … Hdetd) #_ #Hedt
-  elim (IHV12 … HLK … HWV1) -V1 // #W2 #HW12 #HWV2
+  elim (IHW12 … HLK … HVW1) -W1 // #V2 #HV12 #HVW2
   elim (IHU12 … HTU1) -U1 [4: @ldrop_skip // |2: skip |3: /2 width=1 by yle_succ/ ]
   >yminus_succ1_inj /3 width=5 by cpy_bind, lift_bind, ex2_intro/
-| #I #G #L #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdetd
-  elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
-  elim (IHV12 … HLK … HWV1) -V1 //
+| #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #d #e #HLK #X #H #Hdetd
+  elim (lift_inv_flat2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct
+  elim (IHW12 … HLK … HVW1) -W1 //
   elim (IHU12 … HLK … HTU1) -U1 -HLK /3 width=5 by cpy_flat, lift_flat, ex2_intro/
 ]
 qed-.
 
-lemma cpy_inv_lift1_eq: ∀G,T1,U1,d,e. ⇧[d, e] T1 ≡ U1 →
-                        ∀L,U2. ⦃G, L⦄ ⊢ U1 ▶×[d, e] U2 → U1 = U2.
-#G #T1 #U1 #d #e #H elim H -T1 -U1 -d -e
-[ #k #d #e #L #X #H >(cpy_inv_sort1 … H) -H //
-| #i #d #e #Hid #L #X #H elim (cpy_inv_lref1 … H) -H //
-  * #I #K #V #H elim (ylt_yle_false … H) -H /2 width=1 by ylt_inj/
-| #i #d #e #Hdi #L #X #H elim (cpy_inv_lref1 … H) -H //
-  * #I #K #V #_ #H elim (ylt_yle_false i d)
-  /2 width=2 by ylt_inv_monotonic_plus_dx, yle_inj/
-| #p #d #e #L #X #H >(cpy_inv_gref1 … H) -H //
-| #a #I #V1 #W1 #T1 #U1 #d #e #_ #_ #IHVW1 #IHTU1 #L #X #H elim (cpy_inv_bind1 … H) -H
-  #W2 #U2 #HW12 #HU12 #H destruct /3 width=2 by eq_f2/
-| #I #V1 #W1 #T1 #U1 #d #e #_ #_ #IHVW1 #IHTU1 #L #X #H elim (cpy_inv_flat1 … H) -H
-  #W2 #U2 #HW12 #HU12 #H destruct /3 width=2 by eq_f2/
-]
-qed-.
+(* Advancd inversion lemmas on relocation ***********************************)
 
 lemma cpy_inv_lift1_ge_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 →
                            ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys.ma
index 594c34062abd5c4f6da806a5bcc0e7a783d1885c..885bce34471bbb75e3f560be4829cede13de1fec 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys.ma
@@ -97,6 +97,17 @@ lemma cpys_weak_full: ∀G,L,T1,T2,d,e.
 /3 width=5 by cpys_strap1, cpy_weak_full/
 qed-.
 
+lemma cpys_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 →
+               ∀T1,d,e. ⇧[d, e] T1 ≡ U1 →
+               d ≤ dt → d + e ≤ dt + et →
+               ∃∃T2. ⦃G, L⦄ ⊢ U1 ▶*×[d+e, dt+et-(d+e)] U2 & ⇧[d, e] T2 ≡ U2.
+#G #L #U1 #U2 #dt #et #H #T1 #d #e #HTU1 #Hddt #Hdedet @(cpys_ind … H) -U2
+[ /2 width=3 by ex2_intro/
+| -HTU1 #U #U2 #_ #HU2 * #T #HU1 #HTU
+  elim (cpy_up … HU2 … HTU) -HU2 -HTU /3 width=3 by cpys_strap1, ex2_intro/
+]
+qed-.
+
 lemma cpys_append: ∀G,d,e. l_appendable_sn … (cpys d e G).
 #G #d #e #K #T1 #T2 #H @(cpys_ind … H) -T2
 /3 width=3 by cpys_strap1, cpy_append/
@@ -147,6 +158,12 @@ lemma cpys_inv_refl_O2: ∀G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 ▶*×[d, 0] T2 → T1
 #T #T2 #_ #HT2 #IHT1 <(cpy_inv_refl_O2 … HT2) -HT2 //
 qed-.
 
+lemma cpys_inv_lift1_eq: ∀G,L,U1,U2. ∀d,e:nat.
+                         ⦃G, L⦄ ⊢ U1 ▶*×[d, e] U2 → ∀T1. ⇧[d, e] T1 ≡ U1 → U1 = U2.
+#G #L #U1 #U2 #d #e #H #T1 #HTU1 @(cpys_ind … H) -U2
+/2 width=7 by cpy_inv_lift1_eq/
+qed-.
+
 (* Basic forward lemmas *****************************************************)
 
 lemma cpys_fwd_tw: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2 → ♯{T1} ≤ ♯{T2}.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma
index 69683612c42380285216a2c6b9a9f3699dcf87a9..c4b9518e6c6f1595e02256a52fd228fe4ec42199 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma
@@ -92,7 +92,7 @@ lemma cpys_inv_lref1_ldrop: ∀G,L,T2,i,d,e. ⦃G, L⦄ ⊢ #i ▶*×[d, e] T2 
 ]
 qed-.
 
-(* Relocation properties ****************************************************)
+(* Properties on relocation *************************************************)
 
 lemma cpys_lift_le: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*×[dt, et] T2 →
                     ∀L,U1,d,e. dt + et ≤ yinj d → ⇩[d, e] L ≡ K →
@@ -133,6 +133,8 @@ lemma cpys_lift_ge: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*×[dt, et] T2 →
 ]
 qed-.
 
+(* Inversion lemmas for relocation ******************************************)
+
 lemma cpys_inv_lift1_le: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 →
                          ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
                          dt + et ≤ d →
@@ -166,12 +168,7 @@ lemma cpys_inv_lift1_ge: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2
 ]
 qed-.
 
-lemma cpys_inv_lift1_eq: ∀G,L,U1,U2. ∀d,e:nat.
-                         ⦃G, L⦄ ⊢ U1 ▶*×[d, e] U2 → ∀T1. ⇧[d, e] T1 ≡ U1 → U1 = U2.
-#G #L #U1 #U2 #d #e #H #T1 #HTU1 @(cpys_ind … H) -U2 //
-#U #U2 #_ #HU2 #IHU destruct
-<(cpy_inv_lift1_eq … HTU1 … HU2) -HU2 -HTU1 //
-qed-.
+(* Advanced inversion lemmas on relocation **********************************)
 
 lemma cpys_inv_lift1_ge_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 →
                             ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma
index 7e48dbca0c27f98d18a3fadea23cf14d6d430a26..75833e23bb2d42a63d8cb1a8c7e3669744c79e9b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma
@@ -27,6 +27,13 @@ interpretation
 
 (* Basic properties *********************************************************)
 
+lemma lleq_refl: ∀d,T. reflexive … (lleq d T).
+/3 width=1 by conj/ qed.
+
+lemma lleq_sym: ∀d,T. symmetric … (lleq d T).
+#d #T #L1 #L2 * /3 width=1 by iff_sym, conj/
+qed-.
+
 lemma lleq_sort: ∀L1,L2,d,k. |L1| = |L2| → L1 ⋕[⋆k, d] L2.
 #L1 #L2 #d #k #HL12 @conj // -HL12
 #U @conj #H >(cpys_inv_sort1 … H) -H //
@@ -60,12 +67,29 @@ elim (IHV W) -IHV elim (IHT U) -IHT
 /3 width=1 by cpys_flat/
 qed.
 
+lemma lleq_be: ∀L1,L2,U,dt. L1 ⋕[U, dt] L2 → ∀T,d,e. ⇧[d, e] T ≡ U →
+               d ≤ dt → dt ≤ d + e → L1 ⋕[U, d] L2.
+#L1 #L2 #U #dt * #HL12 #IH #T #d #e #HTU #Hddt #Hdtde @conj // -HL12
+#U0 elim (IH U0) -IH #H12 #H21 @conj
+#HU0 elim (cpys_up … HU0 … HTU) // -HU0 /4 width=5 by cpys_weak/
+qed-.
+
 (* Basic forward lemmas *****************************************************)
 
 lemma lleq_fwd_length: ∀L1,L2,T,d. L1 ⋕[T, d] L2 → |L1| = |L2|.
 #L1 #L2 #T #d * //
 qed-.
 
+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 #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-.
+
 lemma lleq_fwd_bind_sn: ∀a,I,L1,L2,V,T,d.
                         L1 ⋕[ⓑ{a,I}V.T, d] L2 → L1 ⋕[V, d] L2.
 #a #I #L1 #L2 #V #T #d * #HL12 #H @conj // -HL12

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma
index 10370818ce5a5d589212e81a933a7e1bc2b87bc8..c7bb1a8a715b7f1180d90b3bc2ebaf44765e015f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma
@@ -13,7 +13,6 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/lazyeqalt_4.ma".
-include "basic_2/substitution/lleq_ldrop.ma".
 include "basic_2/substitution/lleq_lleq.ma".
 
 inductive lleqa: relation4 ynat term lenv lenv ≝
@@ -53,3 +52,80 @@ theorem lleq_lleqa: ∀L1,T,L2,d. L1 ⋕[T, d] L2 → L1 ⋕⋕[T, d] L2.
 | #I #V #T #Hn #L2 #d #H elim (lleq_inv_flat … H) -H /3 width=1 by lleqa_flat/
 ]
 qed.
+
+(* Advanced eliminators *****************************************************)
+
+lemma lleq_ind_alt: ∀R:relation4 ynat term lenv lenv. (
+                       ∀L1,L2,d,k. |L1| = |L2| → R d (⋆k) L1 L2
+                    ) → (
+                       ∀L1,L2,d,i. |L1| = |L2| → yinj i < d → R d (#i) L1 L2
+                    ) → (
+                       ∀I1,I2,L1,L2,K1,K2,V,d,i. d ≤ yinj i →
+                       ⇩[O, i] L1 ≡ K1.ⓑ{I1}V → ⇩[O, i] L2 ≡ K2.ⓑ{I2}V →
+                       K1 ⋕[V, yinj O] K2 → R (yinj O) V K1 K2 → R d (#i) L1 L2
+                    ) → (
+                       ∀L1,L2,d,i. |L1| = |L2| → |L1| ≤ i → |L2| ≤ i → R d (#i) L1 L2
+                    ) → (
+                       ∀L1,L2,d,p. |L1| = |L2| → R d (§p) L1 L2
+                    ) → (
+                       ∀a,I,L1,L2,V,T,d.
+                       L1 ⋕[V, d]L2 → L1.ⓑ{I}V ⋕[T, ⫯d] L2.ⓑ{I}V →
+                       R d V L1 L2 → R (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) → R d (ⓑ{a,I}V.T) L1 L2
+                    ) → (
+                       ∀I,L1,L2,V,T,d.
+                       L1 ⋕[V, d]L2 → L1 ⋕[T, d] L2 →
+                       R d V L1 L2 → R d T L1 L2 → R d (ⓕ{I}V.T) L1 L2
+                    ) →
+                    ∀d,T,L1,L2. L1 ⋕[T, d] L2 → R d T L1 L2.
+#R #H1 #H2 #H3 #H4 #H5 #H6 #H7 #d #T #L1 #L2 #H elim (lleq_lleqa … H) -H
+/3 width=9 by lleqa_inv_lleq/
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma lleq_ge: ∀L1,L2,T,d1. L1 ⋕[T, d1] L2 → ∀d2. d1 ≤ d2 → L1 ⋕[T, d2] L2.
+#L1 #L2 #T #d1 #H @(lleq_ind_alt … H) -L1 -L2 -T -d1
+/4 width=1 by lleq_sort, lleq_free, lleq_gref, lleq_bind, lleq_flat, yle_succ/
+[ /3 width=3 by lleq_skip, ylt_yle_trans/
+| #I1 #I2 #L1 #L2 #K1 #K2 #V #d1 #i #Hi #HLK1 #HLK2 #HV #IHV #d2 #Hd12 elim (ylt_split i d2)
+  [ lapply (lleq_fwd_length … HV) #HK12 #Hid2
+    lapply (ldrop_fwd_length … HLK1) lapply (ldrop_fwd_length … HLK2)
+    normalize in ⊢ (%→%→?); -I1 -I2 -V -d1 /2 width=1 by lleq_skip/ 
+  | /3 width=8 by lleq_lref, yle_trans/
+  ]
+]
+qed-.
+
+lemma lleq_bind_O: ∀a,I,L1,L2,V,T. L1 ⋕[V, 0] L2 → L1.ⓑ{I}V ⋕[T, 0] L2.ⓑ{I}V →
+                   L1 ⋕[ⓑ{a,I}V.T, 0] L2.
+/3 width=3 by lleq_ge, lleq_bind/ qed.
+
+(* Advanced inversion lemmas ************************************************)
+
+fact lleq_inv_S_aux: ∀L1,L2,T,d0. L1 ⋕[T, d0] L2 → ∀d. d0 = d + 1 →
+                     ∀K1,K2,I,V. ⇩[0, d] L1 ≡ K1.ⓑ{I}V → ⇩[0, d] L2 ≡ K2.ⓑ{I}V →
+                     K1 ⋕[V, 0] K2 → L1 ⋕[T, d] L2.
+#L1 #L2 #T #d0 #H @(lleq_ind_alt … H) -L1 -L2 -T -d0
+/2 width=1 by lleq_gref, lleq_free, lleq_sort/
+[ #L1 #L2 #d0 #i #HL12 #Hid #d #H #K1 #K2 #I #V #HLK1 #HLK2 #HV destruct
+  elim (yle_split_eq i d) /2 width=1 by lleq_skip, ylt_fwd_succ2/ -HL12 -Hid
+  #H destruct /2 width=8 by lleq_lref/
+| #I1 #I2 #L1 #L2 #K11 #K22 #V #d0 #i #Hd0i #HLK11 #HLK22 #HV #_ #d #H #K1 #K2 #J #W #_ #_ #_ destruct
+  /3 width=8 by lleq_lref, yle_pred_sn/
+| #a #I #L1 #L2 #V #T #d0 #_ #_ #IHV #IHT #d #H #K1 #K2 #J #W #HLK1 #HLK2 destruct
+  /4 width=7 by lleq_bind, ldrop_ldrop/
+| #I #L1 #L2 #V #T #d0 #_ #_ #IHV #IHT #d #H #K1 #K2 #J #W #HLK1 #HLK2 destruct
+  /3 width=7 by lleq_flat/
+]
+qed-.
+
+lemma lleq_inv_S: ∀T,L1,L2,d. L1 ⋕[T, d+1] L2 →
+                  ∀K1,K2,I,V. ⇩[0, d] L1 ≡ K1.ⓑ{I}V → ⇩[0, d] L2 ≡ K2.ⓑ{I}V →
+                  K1 ⋕[V, 0] K2 → L1 ⋕[T, d] L2.
+/2 width=7 by lleq_inv_S_aux/ qed-.
+
+lemma lleq_inv_bind_O: ∀a,I,L1,L2,V,T. L1 ⋕[ⓑ{a,I}V.T, 0] L2 →
+                       L1 ⋕[V, 0] L2 ∧ L1.ⓑ{I}V ⋕[T, 0] L2.ⓑ{I}V.
+#a #I #L1 #L2 #V #T #H elim (lleq_inv_bind … H) -H
+/3 width=7 by ldrop_pair, conj, lleq_inv_S/
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ldrop.ma
index 69c0f84b12ba4d5d74daeaad8929fc06a9a2ca03..126da3dd362571f9dfd49f686a2a8dc78681c389 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ldrop.ma
@@ -46,3 +46,78 @@ lemma lleq_free: ∀L1,L2,d,i. |L1| ≤ i → |L2| ≤ i → |L1| = |L2| → L1
 #I #Z #Y #X #_ #_ #H lapply (ldrop_fwd_length_lt2 … H) -H
 #H elim (lt_refl_false i) /2 width=3 by lt_to_le_to_lt/
 qed.
+
+(* Properties on relocation *************************************************)
+
+lemma lleq_lift_le: ∀K1,K2,T,dt. K1 ⋕[T, dt] K2 →
+                    ∀L1,L2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 →
+                    ∀U. ⇧[d, e] T ≡ U → dt ≤ d → L1 ⋕[U, dt] L2.
+#K1 #K2 #T #dt * #HK12 #IHT #L1 #L2 #d #e #HLK1 #HLK2 #U #HTU #Hdtd
+lapply (ldrop_fwd_length … HLK1) lapply (ldrop_fwd_length … HLK2)
+#H2 #H1 @conj // -HK12 -H1 -H2 #U0 @conj #HU0
+[ letin HLKA ≝ HLK1 letin HLKB ≝ HLK2 | letin HLKA ≝ HLK2 letin HLKB ≝ HLK1 ]
+elim (cpys_inv_lift1_be … HU0 … HLKA … HTU) // -HU0 >yminus_Y_inj #T0 #HT0 #HTU0
+elim (IHT T0) [ #H #_ | #_ #H ] -IHT /3 width=11 by cpys_lift_be/
+qed-.
+
+lemma lleq_lift_ge: ∀K1,K2,T,dt. K1 ⋕[T, dt] K2 →
+                    ∀L1,L2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 →
+                    ∀U. ⇧[d, e] T ≡ U → d ≤ dt → L1 ⋕[U, dt+e] L2.
+#K1 #K2 #T #dt * #HK12 #IHT #L1 #L2 #d #e #HLK1 #HLK2 #U #HTU #Hddt
+lapply (ldrop_fwd_length … HLK1) lapply (ldrop_fwd_length … HLK2)
+#H2 #H1 @conj // -HK12 -H1 -H2 #U0 @conj #HU0
+[ letin HLKA ≝ HLK1 letin HLKB ≝ HLK2 | letin HLKA ≝ HLK2 letin HLKB ≝ HLK1 ]
+elim (cpys_inv_lift1_ge … HU0 … HLKA … HTU) /2 width=1 by monotonic_yle_plus_dx/ -HU0 >yplus_minus_inj #T0 #HT0 #HTU0
+elim (IHT T0) [ #H #_ | #_ #H ] -IHT /3 width=9 by cpys_lift_ge/
+qed-.
+
+(* Inversion lemmas on relocation *******************************************)
+
+lemma lleq_inv_lift_le: ∀L1,L2,U,dt. L1 ⋕[U, dt] L2 →
+                        ∀K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 →
+                        ∀T. ⇧[d, e] T ≡ U → dt ≤ d → K1 ⋕[T, dt] K2.
+#L1 #L2 #U #dt * #HL12 #IH #K1 #K2 #d #e #HLK1 #HLK2 #T #HTU #Hdtd
+lapply (ldrop_fwd_length_minus2 … HLK1) lapply (ldrop_fwd_length_minus2 … HLK2)
+#H2 #H1 @conj // -HL12 -H1 -H2
+#T0 elim (lift_total T0 d e)
+#U0 #HTU0 elim (IH U0) -IH
+#H12 #H21 @conj #HT0
+[ letin HLKA ≝ HLK1 letin HLKB ≝ HLK2 letin H0 ≝ H12 | letin HLKA ≝ HLK2 letin HLKB ≝ HLK1 letin H0 ≝ H21 ]
+lapply (cpys_lift_be … HT0 … HLKA … HTU … HTU0) // -HT0
+>yplus_Y1 #HU0 elim (cpys_inv_lift1_be … (H0 HU0) … HLKB … HTU) // -L1 -L2 -U -Hdtd
+#X #HT0 #HX lapply (lift_inj … HX … HTU0) -U0 //
+qed-.
+
+lemma lleq_inv_lift_ge: ∀L1,L2,U,dt. L1 ⋕[U, dt] L2 →
+                        ∀K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 →
+                        ∀T. ⇧[d, e] T ≡ U → d+e ≤ dt → K1 ⋕[T, dt-e] K2.
+#L1 #L2 #U #dt * #HL12 #IH #K1 #K2 #d #e #HLK1 #HLK2 #T #HTU #Hdedt
+lapply (ldrop_fwd_length_minus2 … HLK1) lapply (ldrop_fwd_length_minus2 … HLK2)
+#H2 #H1 @conj // -HL12 -H1 -H2
+elim (yle_inv_plus_inj2 … Hdedt) #Hddt #Hedt
+#T0 elim (lift_total T0 d e)
+#U0 #HTU0 elim (IH U0) -IH
+#H12 #H21 @conj #HT0
+[ letin HLKA ≝ HLK1 letin HLKB ≝ HLK2 letin H0 ≝ H12 | letin HLKA ≝ HLK2 letin HLKB ≝ HLK1 letin H0 ≝ H21 ]
+lapply (cpys_lift_ge … HT0 … HLKA … HTU … HTU0) // -HT0 -Hddt
+>ymax_pre_sn // #HU0 elim (cpys_inv_lift1_ge … (H0 HU0) … HLKB … HTU) // -L1 -L2 -U -Hdedt -Hedt
+#X #HT0 #HX lapply (lift_inj … HX … HTU0) -U0 //
+qed-.
+
+lemma lleq_inv_lift_be: ∀L1,L2,U,dt. L1 ⋕[U, dt] L2 →
+                        ∀K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 →
+                        ∀T. ⇧[d, e] T ≡ U → d ≤ dt → dt ≤ d + e → K1 ⋕[T, d] K2.
+#L1 #L2 #U #dt * #HL12 #IH #K1 #K2 #d #e #HLK1 #HLK2 #T #HTU #Hddt #Hdtde
+lapply (ldrop_fwd_length_minus2 … HLK1) lapply (ldrop_fwd_length_minus2 … HLK2)
+#H2 #H1 @conj // -HL12 -H1 -H2
+#T0 elim (lift_total T0 d e)
+#U0 #HTU0 elim (IH U0) -IH
+#H12 #H21 @conj #HT0
+[ letin HLKA ≝ HLK1 letin HLKB ≝ HLK2 letin H0 ≝ H12 | letin HLKA ≝ HLK2 letin HLKB ≝ HLK1 letin H0 ≝ H21 ]
+lapply (cpys_lift_ge … HT0 … HLKA … HTU … HTU0) // -HT0
+#HU0 lapply (cpys_weak … HU0 dt (∞) ? ?) // -HU0
+#HU0 lapply (H0 HU0)
+#HU0 lapply (cpys_weak … HU0 d (∞) ? ?) // -HU0
+#HU0 elim (cpys_inv_lift1_ge_up … HU0 … HLKB … HTU) // -L1 -L2 -U -Hddt -Hdtde
+#X #HT0 #HX lapply (lift_inj … HX … HTU0) -U0 //
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma
index 7405011e040a2489d26b998b71ab07c5d6e75051..0694be69cc970278d774ac50c88c392e0a9bef36 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/substitution/cpys_cpys.ma".
-include "basic_2/substitution/lleq.ma".
+include "basic_2/substitution/lleq_ldrop.ma".
 
 (* Advanced forward lemmas **************************************************)
 
@@ -44,3 +44,96 @@ lapply (cpys_antisym_eq … H12 … H21) -H12 -H21 #H destruct
 | elim (cpys_inv_lref1_ldrop … (H21 ?) … HLK1 … HVW) -H21 -H12
 ] [1,3: >yminus_Y_inj ] /3 width=7 by cpys_subst_Y2, yle_inj/
 qed-.
+
+lemma lleq_fwd_lref_dx: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 →
+                        ∀I2,K2,V. ⇩[0, i] L2 ≡ K2.ⓑ{I2}V →
+                        i < d ∨
+                        ∃∃I1,K1. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V & K1 ⋕[V, 0] K2 & d ≤ i.
+#L1 #L2 #d #i #H #I2 #K2 #V #HLK2 elim (lleq_fwd_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 *)
+| /2 width=1 by or_introl/
+| #I1 #I2 #K11 #K22 #V0 #HLK11 #HLK22 #HV0 #Hdi lapply (ldrop_mono … HLK22 … HLK2) -L2
+  #H destruct /3 width=5 by ex3_2_intro, or_intror/
+]
+qed-.
+
+lemma lleq_fwd_lref_sn: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 →
+                        ∀I1,K1,V. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V →
+                        i < d ∨
+                        ∃∃I2,K2. ⇩[0, i] L2 ≡ K2.ⓑ{I2}V & K1 ⋕[V, 0] K2 & d ≤ i.
+#L1 #L2 #d #i #HL12 #I1 #K1 #V #HLK1 elim (lleq_fwd_lref_dx L2 … d … HLK1) -HLK1
+[2: * ] /4 width=6 by lleq_sym, ex3_2_intro, or_introl, or_intror/
+qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma lleq_inv_lref_ge_dx: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → d ≤ i →
+                           ∀I2,K2,V. ⇩[0, i] L2 ≡ K2.ⓑ{I2}V →
+                           ∃∃I1,K1. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V & K1 ⋕[V, 0] K2.
+#L1 #L2 #d #i #H #Hdi #I2 #K2 #V #HLK2 elim (lleq_fwd_lref_dx … H … HLK2) -L2
+[ #H elim (ylt_yle_false … H Hdi)
+| * /2 width=4 by ex2_2_intro/
+]
+qed-.
+
+lemma lleq_inv_lref_ge_sn: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → d ≤ i →
+                           ∀I1,K1,V. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V →
+                           ∃∃I2,K2. ⇩[0, i] L2 ≡ K2.ⓑ{I2}V & K1 ⋕[V, 0] K2.
+#L1 #L2 #d #i #HL12 #Hdi #I1 #K1 #V #HLK1 elim (lleq_inv_lref_ge_dx L2 … Hdi … HLK1) -Hdi -HLK1
+/3 width=4 by lleq_sym, ex2_2_intro/
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma lleq_dec: ∀T,L1,L2,d. Decidable (L1 ⋕[T, d] 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 #Hn #L2 elim (eq_nat_dec (|L1|) (|L2|))
+  [ #HL12 #d elim (ylt_split i d) /3 width=1 by lleq_skip, or_introl/
+    #Hdi elim (lt_or_ge i (|L1|)) #HiL1
+    elim (lt_or_ge i (|L2|)) #HiL2 /3 width=1 by or_introl, lleq_free/
+    elim (ldrop_O1_lt … HiL2) #I2 #K2 #V2 #HLK2
+    elim (ldrop_O1_lt … HiL1) #I1 #K1 #V1 #HLK1
+    elim (eq_term_dec V2 V1)
+    [ #H3 elim (IH K1 V1 … K2 0) destruct
+      /3 width=8 by lleq_lref, ldrop_fwd_rfw, or_introl/
+    ]
+    -IH #H3 @or_intror
+    #H elim (lleq_fwd_lref … H) -H [1,3,4,6: * ]
+    [1,3: /3 width=4 by lt_to_le_to_lt, lt_refl_false/
+    |5,6: /2 width=4 by ylt_yle_false/
+    ]
+    #Z1 #Z2 #Y1 #Y2 #X #HLY1 #HLY2 #HX #_
+    lapply (ldrop_mono … HLY1 … HLK1) -HLY1 -HLK1
+    lapply (ldrop_mono … HLY2 … HLK2) -HLY2 -HLK2
+    #H2 #H1 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 #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 #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=3 by lleq_fwd_length, or_intror/
+qed-.
+
+(* Main properties **********************************************************)
+
+theorem lleq_trans: ∀d,T. Transitive … (lleq d T).
+#d #T #L1 #L * #HL1 #IH1 #L2 * #HL2 #IH2 /3 width=3 by conj, iff_trans/
+qed-.
+
+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,d. L1 ⋕[d, T] L → L2 ⋕[d, T] L → L1 ⋕[d, T] L2.
+/3 width=3 by lleq_trans, lleq_sym/ qed-.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_minus.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_minus.ma
index 10a841cbd4f04ba980dc611a0cef4e1b73ced275..596885cf0b55361d538c47008099f3759520aa73 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_minus.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_minus.ma
@@ -38,6 +38,9 @@ qed.
 lemma yminus_O1: ∀x:ynat. 0 - x = 0.
 * // qed.
 
+lemma yminus_refl: ∀x:ynat. x - x = 0.
+* // qed.
+
 lemma yminus_minus_comm: ∀y,z,x. x - y - z = x - z - y.
 * #y [ * #z [ * // ] ] >yminus_O1 //
 qed.