matita/matita/contribs/lambdadelta/basic_2A/etc/lleq_alt/lleq_lleq.etc

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "basic_2/substitution/cpys_cpys.ma".
  16 include "basic_2/substitution/lleq_ldrop.ma".
  17
  18 (* Advanced forward lemmas **************************************************)
  19
  20 lemma lleq_fwd_lref: ∀L1,L2. ∀d:ynat. ∀i:nat. L1 ⋕[#i, d] L2 →
  21                      ∨∨ |L1| ≤ i ∧ |L2| ≤ i
  22                       | yinj i < d
  23                       | ∃∃I1,I2,K1,K2,V. ⇩[i] L1 ≡ K1.ⓑ{I1}V &
  24                                          ⇩[i] L2 ≡ K2.ⓑ{I2}V &
  25                                          K1 ⋕[V, yinj 0] K2 & d ≤ yinj i.
  26 #L1 #L2 #d #i * #HL12 #IH elim (lt_or_ge i (|L1|)) /3 width=3 by or3_intro0, conj/
  27 elim (ylt_split i d) /2 width=1 by or3_intro1/ #Hdi #Hi
  28 elim (ldrop_O1_lt … Hi) #I1 #K1 #V1 #HLK1
  29 elim (ldrop_O1_lt L2 i) // -Hi #I2 #K2 #V2 #HLK2
  30 lapply (ldrop_fwd_length_minus2 … HLK2) #H
  31 lapply (ldrop_fwd_length_minus2 … HLK1) >HL12 <H -HL12 -H
  32 #H lapply (injective_plus_l … H) -H #HK12
  33 elim (lift_total V1 0 (i+1)) #W1 #HVW1
  34 elim (lift_total V2 0 (i+1)) #W2 #HVW2
  35 elim (IH W1) elim (IH W2) #_ #H2 #H1 #_
  36 elim (cpys_inv_lref1_ldrop … (H1 ?) … HLK2 … HVW1) -H1
  37 [ elim (cpys_inv_lref1_ldrop … (H2 ?) … HLK1 … HVW2) -H2 ]
  38 /3 width=7 by cpys_subst, yle_inj/ -W1 -W2 #H12 #_ #_ #H21 #_ #_
  39 lapply (cpys_antisym_eq … H12 … H21) -H12 -H21 #H destruct
  40 @or3_intro2 @(ex4_5_intro … HLK1 HLK2) // @conj // -HK12
  41 #V elim (lift_total V 0 (i+1))
  42 #W #HVW elim (IH W) -IH #H12 #H21 @conj #H
  43 [ elim (cpys_inv_lref1_ldrop … (H12 ?) … HLK2 … HVW) -H12 -H21
  44 | elim (cpys_inv_lref1_ldrop … (H21 ?) … HLK1 … HVW) -H21 -H12
  45 ] [1,3: >yminus_Y_inj ] /3 width=7 by cpys_subst_Y2, yle_inj/
  46 qed-.
  47
  48 lemma lleq_fwd_lref_dx: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 →
  49                         ∀I2,K2,V. ⇩[i] L2 ≡ K2.ⓑ{I2}V →
  50                         i < d ∨
  51                         ∃∃I1,K1. ⇩[i] L1 ≡ K1.ⓑ{I1}V & K1 ⋕[V, 0] K2 & d ≤ i.
  52 #L1 #L2 #d #i #H #I2 #K2 #V #HLK2 elim (lleq_fwd_lref … H) -H [ * || * ]
  53 [ #_ #H elim (lt_refl_false i)
  54   lapply (ldrop_fwd_length_lt2 … HLK2) -HLK2
  55   /2 width=3 by lt_to_le_to_lt/ (**) (* full auto too slow *)
  56 | /2 width=1 by or_introl/
  57 | #I1 #I2 #K11 #K22 #V0 #HLK11 #HLK22 #HV0 #Hdi lapply (ldrop_mono … HLK22 … HLK2) -L2
  58   #H destruct /3 width=5 by ex3_2_intro, or_intror/
  59 ]
  60 qed-.
  61
  62 lemma lleq_fwd_lref_sn: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 →
  63                         ∀I1,K1,V. ⇩[i] L1 ≡ K1.ⓑ{I1}V →
  64                         i < d ∨
  65                         ∃∃I2,K2. ⇩[i] L2 ≡ K2.ⓑ{I2}V & K1 ⋕[V, 0] K2 & d ≤ i.
  66 #L1 #L2 #d #i #HL12 #I1 #K1 #V #HLK1 elim (lleq_fwd_lref_dx L2 … d … HLK1) -HLK1
  67 [2: * ] /4 width=6 by lleq_sym, ex3_2_intro, or_introl, or_intror/
  68 qed-.
  69
  70 (* Advanced inversion lemmas ************************************************)
  71
  72 lemma lleq_inv_lref_ge_dx: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → d ≤ i →
  73                            ∀I2,K2,V. ⇩[i] L2 ≡ K2.ⓑ{I2}V →
  74                            ∃∃I1,K1. ⇩[i] L1 ≡ K1.ⓑ{I1}V & K1 ⋕[V, 0] K2.
  75 #L1 #L2 #d #i #H #Hdi #I2 #K2 #V #HLK2 elim (lleq_fwd_lref_dx … H … HLK2) -L2
  76 [ #H elim (ylt_yle_false … H Hdi)
  77 | * /2 width=4 by ex2_2_intro/
  78 ]
  79 qed-.
  80
  81 lemma lleq_inv_lref_ge_sn: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → d ≤ i →
  82                            ∀I1,K1,V. ⇩[i] L1 ≡ K1.ⓑ{I1}V →
  83                            ∃∃I2,K2. ⇩[i] L2 ≡ K2.ⓑ{I2}V & K1 ⋕[V, 0] K2.
  84 #L1 #L2 #d #i #HL12 #Hdi #I1 #K1 #V #HLK1 elim (lleq_inv_lref_ge_dx L2 … Hdi … HLK1) -Hdi -HLK1
  85 /3 width=4 by lleq_sym, ex2_2_intro/
  86 qed-.
  87
  88 lemma lleq_inv_lref_ge_gen: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → d ≤ i →
  89                             ∀I1,I2,K1,K2,V1,V2.
  90                             ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
  91                             V1 = V2 ∧ K1 ⋕[V2, 0] K2.
  92 #L1 #L2 #d #i #HL12 #Hdi #I1 #I2 #K1 #K2 #V1 #V2 #HLK1 #HLK2
  93 elim (lleq_inv_lref_ge_sn … HL12 … HLK1) // -L1 -d
  94 #J #Y #HY lapply (ldrop_mono … HY … HLK2) -L2 -i #H destruct /2 width=1 by conj/
  95 qed-.
  96
  97 lemma lleq_inv_lref_ge: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → d ≤ i →
  98                         ∀I,K1,K2,V. ⇩[i] L1 ≡ K1.ⓑ{I}V → ⇩[i] L2 ≡ K2.ⓑ{I}V →
  99                         K1 ⋕[V, 0] K2.
 100 #L1 #L2 #d #i #HL12 #Hdi #I #K1 #K2 #V #HLK1 #HLK2
 101 elim (lleq_inv_lref_ge_gen … HL12 … HLK1 HLK2) //
 102 qed-.
 103
 104 (* Advanced properties ******************************************************)
 105
 106 lemma lleq_dec: ∀T,L1,L2,d. Decidable (L1 ⋕[T, d] L2).
 107 #T #L1 @(f2_ind … rfw … L1 T) -L1 -T
 108 #n #IH #L1 * *
 109 [ #k #Hn #L2 elim (eq_nat_dec (|L1|) (|L2|)) /3 width=1 by or_introl, lleq_sort/
 110 | #i #Hn #L2 elim (eq_nat_dec (|L1|) (|L2|))
 111   [ #HL12 #d elim (ylt_split i d) /3 width=1 by lleq_skip, or_introl/
 112     #Hdi elim (lt_or_ge i (|L1|)) #HiL1
 113     elim (lt_or_ge i (|L2|)) #HiL2 /3 width=1 by or_introl, lleq_free/
 114     elim (ldrop_O1_lt … HiL2) #I2 #K2 #V2 #HLK2
 115     elim (ldrop_O1_lt … HiL1) #I1 #K1 #V1 #HLK1
 116     elim (eq_term_dec V2 V1)
 117     [ #H3 elim (IH K1 V1 … K2 0) destruct
 118       /3 width=8 by lleq_lref, ldrop_fwd_rfw, or_introl/
 119     ]
 120     -IH #H3 @or_intror
 121     #H elim (lleq_fwd_lref … H) -H [1,3,4,6: * ]
 122     [1,3: /3 width=4 by lt_to_le_to_lt, lt_refl_false/
 123     |5,6: /2 width=4 by ylt_yle_false/
 124     ]
 125     #Z1 #Z2 #Y1 #Y2 #X #HLY1 #HLY2 #HX #_
 126     lapply (ldrop_mono … HLY1 … HLK1) -HLY1 -HLK1
 127     lapply (ldrop_mono … HLY2 … HLK2) -HLY2 -HLK2
 128     #H2 #H1 destruct /2 width=1 by/
 129   ]
 130 | #p #Hn #L2 elim (eq_nat_dec (|L1|) (|L2|)) /3 width=1 by or_introl, lleq_gref/
 131 | #a #I #V #T #Hn #L2 #d destruct
 132   elim (IH L1 V … L2 d) /2 width=1 by/
 133   elim (IH (L1.ⓑ{I}V) T … (L2.ⓑ{I}V) (d+1)) -IH /3 width=1 by or_introl, lleq_bind/
 134   #H1 #H2 @or_intror
 135   #H elim (lleq_inv_bind … H) -H /2 width=1 by/
 136 | #I #V #T #Hn #L2 #d destruct
 137   elim (IH L1 V … L2 d) /2 width=1 by/
 138   elim (IH L1 T … L2 d) -IH /3 width=1 by or_introl, lleq_flat/
 139   #H1 #H2 @or_intror
 140   #H elim (lleq_inv_flat … H) -H /2 width=1 by/
 141 ]
 142 -n /4 width=3 by lleq_fwd_length, or_intror/
 143 qed-.
 144
 145 (* Main properties **********************************************************)
 146
 147 theorem lleq_trans: ∀d,T. Transitive … (lleq d T).
 148 #d #T #L1 #L * #HL1 #IH1 #L2 * #HL2 #IH2 /3 width=3 by conj, iff_trans/
 149 qed-.
 150
 151 theorem lleq_canc_sn: ∀L,L1,L2,T,d. L ⋕[d, T] L1→ L ⋕[d, T] L2 → L1 ⋕[d, T] L2.
 152 /3 width=3 by lleq_trans, lleq_sym/ qed-.
 153
 154 theorem lleq_canc_dx: ∀L1,L2,L,T,d. L1 ⋕[d, T] L → L2 ⋕[d, T] L → L1 ⋕[d, T] L2.
 155 /3 width=3 by lleq_trans, lleq_sym/ qed-.
 156
 157 (* Inversion lemmas on negated lazy quivalence for local environments *******)
 158
 159 lemma nlleq_inv_bind: ∀a,I,L1,L2,V,T,d. (L1 ⋕[ⓑ{a,I}V.T, d] L2 → ⊥) →
 160                       (L1 ⋕[V, d] L2 → ⊥) ∨ (L1.ⓑ{I}V ⋕[T, ⫯d] L2.ⓑ{I}V → ⊥).
 161 #a #I #L1 #L2 #V #T #d #H elim (lleq_dec V L1 L2 d)
 162 /4 width=1 by lleq_bind, or_intror, or_introl/
 163 qed-.
 164
 165 lemma nlleq_inv_flat: ∀I,L1,L2,V,T,d. (L1 ⋕[ⓕ{I}V.T, d] L2 → ⊥) →
 166                       (L1 ⋕[V, d] L2 → ⊥) ∨ (L1 ⋕[T, d] L2 → ⊥).
 167 #I #L1 #L2 #V #T #d #H elim (lleq_dec V L1 L2 d)
 168 /4 width=1 by lleq_flat, or_intror, or_introl/
 169 qed-.
 170
 171 (* Note: lleq_nlleq_trans: ∀d,T,L1,L. L1⋕[T, d] L →
 172                            ∀L2. (L ⋕[T, d] L2 → ⊥) → (L1 ⋕[T, d] L2 → ⊥).
 173 /3 width=3 by lleq_canc_sn/ qed-.
 174 works with /4 width=8/ so lleq_canc_sn is more convenient
 175 *)