matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma

   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/notation/relations/extlrsubeq_4.ma".
  16 include "basic_2/relocation/ldrop.ma".
  17
  18 (* LOCAL ENVIRONMENT REFINEMENT FOR EXTENDED SUBSTITUTION *******************)
  19
  20 inductive lsuby: relation4 nat nat lenv lenv ≝
  21 | lsuby_atom: ∀L,d,e. lsuby d e L (⋆)
  22 | lsuby_zero: ∀I1,I2,L1,L2,V1,V2.
  23               lsuby 0 0 L1 L2 → lsuby 0 0 (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2)
  24 | lsuby_pair: ∀I1,I2,L1,L2,V,e. lsuby 0 e L1 L2 →
  25               lsuby 0 (e + 1) (L1.ⓑ{I1}V) (L2.ⓑ{I2}V)
  26 | lsuby_succ: ∀I1,I2,L1,L2,V1,V2,d,e.
  27               lsuby d e L1 L2 → lsuby (d + 1) e (L1. ⓑ{I1}V1) (L2. ⓑ{I2} V2)
  28 .
  29
  30 interpretation
  31   "local environment refinement (extended substitution)"
  32   'ExtLRSubEq L1 d e L2 = (lsuby d e L1 L2).
  33
  34 (* Basic properties *********************************************************)
  35
  36 lemma lsuby_pair_lt: ∀I1,I2,L1,L2,V,e. L1 ⊑×[0, e-1] L2 → 0 < e →
  37                      L1.ⓑ{I1}V ⊑×[0, e] L2.ⓑ{I2}V.
  38 #I1 #I2 #L1 #L2 #V #e #HL12 #He >(plus_minus_m_m e 1) /2 width=1 by lsuby_pair/
  39 qed.
  40
  41 lemma lsuby_succ_lt: ∀I1,I2,L1,L2,V1,V2,d,e. L1 ⊑×[d-1, e] L2 → 0 < d →
  42                      L1.ⓑ{I1}V1 ⊑×[d, e] L2. ⓑ{I2}V2.
  43 #I1 #I2 #L1 #L2 #V1 #V2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) /2 width=1 by lsuby_succ/
  44 qed.
  45
  46 lemma lsuby_refl: ∀L,d,e. L ⊑×[d, e] L.
  47 #L elim L -L //
  48 #L #I #V #IHL #d @(nat_ind_plus … d) -d /2 width=1 by lsuby_succ/
  49 #e @(nat_ind_plus … e) -e /2 width=2 by lsuby_pair, lsuby_zero/
  50 qed.
  51
  52 lemma lsuby_length: ∀L1,L2. |L2| ≤ |L1| → L1 ⊑×[0, 0] L2.
  53 #L1 elim L1 -L1
  54 [ #X #H lapply (le_n_O_to_eq … H) -H
  55   #H lapply (length_inv_zero_sn … H) #H destruct /2 width=1 by lsuby_atom/
  56 | #L1 #I1 #V1 #IHL1 * normalize
  57   /4 width=2 by lsuby_zero, le_S_S_to_le/
  58 ]
  59 qed.
  60
  61 (* Basic inversion lemmas ***************************************************)
  62
  63 fact lsuby_inv_atom1_aux: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 → L1 = ⋆ → L2 = ⋆.
  64 #L1 #L2 #d #e * -L1 -L2 -d -e //
  65 [ #I1 #I2 #L1 #L2 #V1 #V2 #_ #H destruct
  66 | #I1 #I2 #L1 #L2 #V #e #_ #H destruct
  67 | #I1 #I2 #L1 #L2 #V1 #V2 #d #e #_ #H destruct
  68 ]
  69 qed-.
  70
  71 lemma lsuby_inv_atom1: ∀L2,d,e. ⋆ ⊑×[d, e] L2 → L2 = ⋆.
  72 /2 width=5 by lsuby_inv_atom1_aux/ qed-.
  73
  74 fact lsuby_inv_zero1_aux: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 →
  75                           ∀J1,K1,W1. L1 = K1.ⓑ{J1}W1 → d = 0 → e = 0 →
  76                           L2 = ⋆ ∨
  77                           ∃∃J2,K2,W2. K1 ⊑×[0, 0] K2 & L2 = K2.ⓑ{J2}W2.
  78 #L1 #L2 #d #e * -L1 -L2 -d -e /2 width=1 by or_introl/
  79 [ #I1 #I2 #L1 #L2 #V1 #V2 #HL12 #J1 #K1 #W1 #H #_ #_ destruct
  80   /3 width=5 by ex2_3_intro, or_intror/
  81 | #I1 #I2 #L1 #L2 #V #e #_ #J1 #K1 #W1 #_ #_
  82   <plus_n_Sm #H destruct
  83 | #I1 #I2 #L1 #L2 #V1 #V2 #d #e #_ #J1 #K1 #W1 #_
  84   <plus_n_Sm #H destruct
  85 ]
  86 qed-.
  87
  88 lemma lsuby_inv_zero1: ∀I1,K1,L2,V1. K1.ⓑ{I1}V1 ⊑×[0, 0] L2 →
  89                        L2 = ⋆ ∨
  90                        ∃∃I2,K2,V2. K1 ⊑×[0, 0] K2 & L2 = K2.ⓑ{I2}V2.
  91 /2 width=9 by lsuby_inv_zero1_aux/ qed-.
  92
  93 fact lsuby_inv_pair1_aux: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 →
  94                           ∀J1,K1,W. L1 = K1.ⓑ{J1}W → d = 0 → 0 < e →
  95                           L2 = ⋆ ∨
  96                           ∃∃J2,K2. K1 ⊑×[0, e-1] K2 & L2 = K2.ⓑ{J2}W.
  97 #L1 #L2 #d #e * -L1 -L2 -d -e /2 width=1 by or_introl/
  98 [ #I1 #I2 #L1 #L2 #V1 #V2 #_ #J1 #K1 #W #_ #_ #H
  99   elim (lt_zero_false … H)
 100 | #I1 #I2 #L1 #L2 #V #e #HL12 #J1 #K1 #W #H #_ #_ destruct
 101   /3 width=4 by ex2_2_intro, or_intror/
 102 | #I1 #I2 #L1 #L2 #V1 #V2 #d #e #_ #J1 #K1 #W #_
 103   <plus_n_Sm #H destruct
 104 ]
 105 qed-.
 106
 107 lemma lsuby_inv_pair1: ∀I1,K1,L2,V,e. K1.ⓑ{I1}V ⊑×[0, e] L2 → 0 < e →
 108                        L2 = ⋆ ∨
 109                        ∃∃I2,K2. K1 ⊑×[0, e-1] K2 & L2 = K2.ⓑ{I2}V.
 110 /2 width=6 by lsuby_inv_pair1_aux/ qed-.
 111
 112
 113 fact lsuby_inv_succ1_aux: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 →
 114                           ∀J1,K1,W1. L1 = K1.ⓑ{J1}W1 → 0 < d →
 115                           L2 = ⋆ ∨
 116                           ∃∃J2,K2,W2. K1 ⊑×[d-1, e] K2 & L2 = K2.ⓑ{J2}W2.
 117 #L1 #L2 #d #e * -L1 -L2 -d -e /2 width=1 by or_introl/
 118 [ #I1 #I2 #L1 #L2 #V1 #V2 #_ #J1 #K1 #W1 #_ #H
 119   elim (lt_zero_false … H)
 120 | #I1 #I2 #L1 #L2 #V #e #_ #J1 #K1 #W1 #_ #H
 121   elim (lt_zero_false … H)
 122 | #I1 #I2 #L1 #L2 #V1 #V2 #d #e #HL12 #J1 #K1 #W1 #H #_ destruct
 123   /3 width=5 by ex2_3_intro, or_intror/
 124 ]
 125 qed-.
 126
 127 lemma lsuby_inv_succ1: ∀I1,K1,L2,V1,d,e. K1.ⓑ{I1}V1 ⊑×[d, e] L2 → 0 < d →
 128                        L2 = ⋆ ∨
 129                        ∃∃I2,K2,V2. K1 ⊑×[d - 1, e] K2 & L2 = K2.ⓑ{I2}V2.
 130 /2 width=5 by lsuby_inv_succ1_aux/ qed-.
 131
 132 fact lsuby_inv_zero2_aux: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 →
 133                           ∀J2,K2,W2. L2 = K2.ⓑ{J2}W2 → d = 0 → e = 0 →
 134                           ∃∃J1,K1,W1. K1 ⊑×[0, 0] K2 & L1 = K1.ⓑ{J1}W1.
 135 #L1 #L2 #d #e * -L1 -L2 -d -e
 136 [ #L1 #d #e #J2 #K2 #W1 #H destruct
 137 | #I1 #I2 #L1 #L2 #V1 #V2 #HL12 #J2 #K2 #W2 #H #_ #_ destruct
 138   /2 width=5 by ex2_3_intro/
 139 | #I1 #I2 #L1 #L2 #V #e #_ #J2 #K2 #W2 #_ #_
 140   <plus_n_Sm #H destruct
 141 | #I1 #I2 #L1 #L2 #V1 #V2 #d #e #_ #J2 #K2 #W2 #_
 142   <plus_n_Sm #H destruct
 143 ]
 144 qed-.
 145
 146 lemma lsuby_inv_zero2: ∀I2,K2,L1,V2. L1 ⊑×[0, 0] K2.ⓑ{I2}V2 →
 147                        ∃∃I1,K1,V1. K1 ⊑×[0, 0] K2 & L1 = K1.ⓑ{I1}V1.
 148 /2 width=9 by lsuby_inv_zero2_aux/ qed-.
 149
 150 fact lsuby_inv_pair2_aux: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 →
 151                           ∀J2,K2,W. L2 = K2.ⓑ{J2}W → d = 0 → 0 < e →
 152                           ∃∃J1,K1. K1 ⊑×[0, e-1] K2 & L1 = K1.ⓑ{J1}W.
 153 #L1 #L2 #d #e * -L1 -L2 -d -e
 154 [ #L1 #d #e #J2 #K2 #W #H destruct
 155 | #I1 #I2 #L1 #L2 #V1 #V2 #_ #J2 #K2 #W #_ #_ #H
 156   elim (lt_zero_false … H)
 157 | #I1 #I2 #L1 #L2 #V #e #HL12 #J2 #K2 #W #H #_ #_ destruct
 158   /2 width=4 by ex2_2_intro/
 159 | #I1 #I2 #L1 #L2 #V1 #V2 #d #e #_ #J2 #K2 #W #_
 160   <plus_n_Sm #H destruct
 161 ]
 162 qed-.
 163
 164 lemma lsuby_inv_pair2: ∀I2,K2,L1,V,e. L1 ⊑×[0, e] K2.ⓑ{I2}V → 0 < e →
 165                        ∃∃I1,K1. K1 ⊑×[0, e-1] K2 & L1 = K1.ⓑ{I1}V.
 166 /2 width=6 by lsuby_inv_pair2_aux/ qed-.
 167
 168 fact lsuby_inv_succ2_aux: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 →
 169                           ∀J2,K2,W2. L2 = K2.ⓑ{J2}W2 → 0 < d →
 170                           ∃∃J1,K1,W1. K1 ⊑×[d-1, e] K2 & L1 = K1.ⓑ{J1}W1.
 171 #L1 #L2 #d #e * -L1 -L2 -d -e
 172 [ #L1 #d #e #J2 #K2 #W2 #H destruct
 173 | #I1 #I2 #L1 #L2 #V1 #V2 #_ #J2 #K2 #W2 #_ #H
 174   elim (lt_zero_false … H)
 175 | #I1 #I2 #L1 #L2 #V #e #_ #J2 #K1 #W2 #_ #H
 176   elim (lt_zero_false … H)
 177 | #I1 #I2 #L1 #L2 #V1 #V2 #d #e #HL12 #J2 #K2 #W2 #H #_ destruct
 178   /2 width=5 by ex2_3_intro/
 179 ]
 180 qed-.
 181
 182 lemma lsuby_inv_succ2: ∀I2,K2,L1,V2,d,e. L1 ⊑×[d, e] K2.ⓑ{I2}V2 → 0 < d →
 183                        ∃∃I1,K1,V1. K1 ⊑×[d-1, e] K2 & L1 = K1.ⓑ{I1}V1.
 184 /2 width=5 by lsuby_inv_succ2_aux/ qed-.
 185
 186 (* Basic forward lemmas *****************************************************)
 187
 188 lemma lsuby_fwd_length: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 → |L2| ≤ |L1|.
 189 #L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize /2 width=1 by le_S_S/
 190 qed-.
 191
 192 lemma lsuby_fwd_ldrop2_be: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 →
 193                            ∀I2,K2,W,i. ⇩[0, i] L2 ≡ K2.ⓑ{I2}W →
 194                            d ≤ i → i < d + e →
 195                            ∃∃I1,K1. K1 ⊑×[0, d+e-i-1] K2 & ⇩[0, i] L1 ≡ K1.ⓑ{I1}W.
 196 #L1 #L2 #d #e #H elim H -L1 -L2 -d -e
 197 [ #L1 #d #e #J2 #K2 #W #i #H
 198   elim (ldrop_inv_atom1 … H) -H #H destruct
 199 | #I1 #I2 #L1 #L2 #V1 #V2 #_ #_ #J2 #K2 #W #i #_ #_ #H
 200   elim (lt_zero_false … H)
 201 | #I1 #I2 #L1 #L2 #V #e #HL12 #IHL12 #J2 #K2 #W #i #H #_ #Hie
 202   elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK1
 203   [ -IHL12 -Hie destruct normalize -I2
 204     <minus_n_O <minus_plus_m_m /2 width=4 by ldrop_pair, ex2_2_intro/
 205   | -HL12
 206     elim (IHL12 … HLK1) -IHL12 -HLK1 // [2: /2 width=1 by lt_plus_to_minus/ ] -Hie normalize
 207     >minus_minus_comm >arith_b1 /3 width=4 by ldrop_ldrop_lt, ex2_2_intro/
 208   ]
 209 | #I1 #I2 #L1 #L2 #V1 #V2 #d #e #_ #IHL12 #J2 #K2 #W #i #H #Hdi >plus_plus_comm_23 #Hide
 210   elim (le_inv_plus_l … Hdi) #_ #Hi
 211   lapply (ldrop_inv_ldrop1_lt … H ?) -H // #HLK1
 212   elim (IHL12 … HLK1) -IHL12 -HLK1
 213   [2,3: /2 width=1 by lt_plus_to_minus, monotonic_pred/ ] -Hdi -Hide
 214   >minus_minus_comm >arith_b1 /3 width=4 by ldrop_ldrop_lt, ex2_2_intro/
 215 ]
 216 qed-.