matita/matita/contribs/lambdadelta/basic_2/etc/cpys/cpys.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/notation/relations/extpsubststar_4.ma".
  16 include "basic_2/grammar/genv.ma".
  17 include "basic_2/grammar/cl_shift.ma".
  18 include "basic_2/relocation/ldrop_append.ma".
  19 include "basic_2/relocation/lsuby.ma".
  20
  21 (* CONTEXT-SENSITIVE EXTENDED MULTIPLE SUBSTITUTION FOR TERMS ***************)
  22
  23 (* avtivate genv *)
  24 inductive cpys: relation4 genv lenv term term ≝
  25 | cpys_atom : ∀I,G,L. cpys G L (⓪{I}) (⓪{I})
  26 | cpys_delta: ∀I,G,L,K,V,V2,W2,i.
  27               ⇩[0, i] L ≡ K.ⓑ{I}V → cpys G K V V2 →
  28               ⇧[0, i + 1] V2 ≡ W2 → cpys G L (#i) W2
  29 | cpys_bind : ∀a,I,G,L,V1,V2,T1,T2.
  30               cpys G L V1 V2 → cpys G (L.ⓑ{I}V1) T1 T2 →
  31               cpys G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
  32 | cpys_flat : ∀I,G,L,V1,V2,T1,T2.
  33               cpys G L V1 V2 → cpys G L T1 T2 →
  34               cpys G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
  35 .
  36
  37 interpretation
  38    "context-sensitive extended multiple substitution (term)"
  39    'ExtPSubstStar G L T1 T2 = (cpys G L T1 T2).
  40
  41 (* Basic properties *********************************************************)
  42
  43 lemma lsuby_cpys_trans: ∀G. lsub_trans … (cpys G) lsuby.
  44 #G #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2
  45 [ //
  46 | #I #G #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
  47   elim (lsuby_fwd_ldrop2_pair … HL12 … HLK1) -HL12 -HLK1 *
  48   /3 width=7 by cpys_delta/
  49 | /4 width=1 by lsuby_pair, cpys_bind/
  50 | /3 width=1 by cpys_flat/
  51 ]
  52 qed-.
  53
  54 (* Note: this is "∀L. reflexive … (cpys L)" *)
  55 lemma cpys_refl: ∀G,T,L. ⦃G, L⦄ ⊢ T ▶*× T.
  56 #G #T elim T -T // * /2 width=1 by cpys_bind, cpys_flat/
  57 qed.
  58
  59 lemma cpys_pair_sn: ∀I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ▶*× V2 →
  60                     ∀T. ⦃G, L⦄ ⊢ ②{I}V1.T ▶*× ②{I}V2.T.
  61 * /2 width=1 by cpys_bind, cpys_flat/
  62 qed.
  63
  64 lemma cpys_bind_ext: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ▶*× V2 →
  65                      ∀J,T1,T2. ⦃G, L.ⓑ{J}V1⦄ ⊢ T1 ▶*× T2 →
  66                      ∀a,I. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*× ⓑ{a,I}V2.T2.
  67 /4 width=4 by lsuby_cpys_trans, cpys_bind, lsuby_pair/ qed.
  68
  69 lemma cpys_delift: ∀I,G,K,V,T1,L,d. ⇩[0, d] L ≡ (K.ⓑ{I}V) →
  70                    ∃∃T2,T.  ⦃G, L⦄ ⊢ T1 ▶*× T2 & ⇧[d, 1] T ≡ T2.
  71 #I #G #K #V #T1 elim T1 -T1
  72 [ * /2 width=4 by cpys_atom, lift_sort, lift_gref, ex2_2_intro/
  73   #i #L #d elim (lt_or_eq_or_gt i d) #Hid [1,3: /3 width=4 by cpys_atom, lift_lref_ge_minus, lift_lref_lt, ex2_2_intro/ ]
  74   destruct
  75   elim (lift_total V 0 (i+1)) #W #HVW
  76   elim (lift_split … HVW i i) /3 width=7 by cpys_delta, ex2_2_intro/
  77 | * [ #a ] #I #W1 #U1 #IHW1 #IHU1 #L #d #HLK
  78   elim (IHW1 … HLK) -IHW1 #W2 #W #HW12 #HW2
  79   [ elim (IHU1 (L. ⓑ{I}W1) (d+1)) -IHU1 /3 width=9 by cpys_bind, ldrop_ldrop, lift_bind, ex2_2_intro/
  80   | elim (IHU1 … HLK) -IHU1 -HLK /3 width=8 by cpys_flat, lift_flat, ex2_2_intro/
  81   ]
  82 ]
  83 qed-.
  84
  85 lemma cpys_append: ∀G. l_appendable_sn … (cpys G).
  86 #G #K #T1 #T2 #H elim H -G -K -T1 -T2
  87 /2 width=3 by cpys_bind, cpys_flat/
  88 #I #G #K #K0 #V1 #V2 #W2 #i #HK0 #_ #HVW2 #IHV12 #L
  89 lapply (ldrop_fwd_length_lt2 … HK0) #H
  90 @(cpys_delta … I … (L@@K0) V1 … HVW2) //
  91 @(ldrop_O1_append_sn_le … HK0) /2 width=2 by lt_to_le/ (**) (* /3/ does not work *)
  92 qed.
  93
  94 (* Basic inversion lemmas ***************************************************)
  95
  96 fact cpys_inv_atom1_aux: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ▶*× T2 → ∀J. T1 = ⓪{J} →
  97                          T2 = ⓪{J} ∨
  98                          ∃∃I,K,V,V2,i. ⇩[O, i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ▶*× V2 &
  99                                        ⇧[O, i + 1] V2 ≡ T2 & J = LRef i.
 100 #G #L #T1 #T2 * -L -T1 -T2
 101 [ #I #G #L #J #H destruct /2 width=1 by or_introl/
 102 | #I #G #L #K #V #V2 #T2 #i #HLK #HV2 #HVT2 #J #H destruct /3 width=9 by ex4_5_intro, or_intror/
 103 | #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct
 104 | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct
 105 ]
 106 qed-.
 107
 108 lemma cpys_inv_atom1: ∀J,G,L,T2. ⦃G, L⦄ ⊢ ⓪{J} ▶*× T2 →
 109                       T2 = ⓪{J} ∨
 110                       ∃∃I,K,V,V2,i. ⇩[O, i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ▶*× V2 &
 111                                     ⇧[O, i + 1] V2 ≡ T2 & J = LRef i.
 112 /2 width=3 by cpys_inv_atom1_aux/ qed-.
 113
 114 lemma cpys_inv_sort1: ∀G,L,T2,k. ⦃G, L⦄ ⊢ ⋆k ▶*× T2 → T2 = ⋆k.
 115 #G #L #T2 #k #H elim (cpys_inv_atom1 … H) -H // *
 116 #I #K #V #V2 #i #_ #_ #_ #H destruct
 117 qed-.
 118
 119 lemma cpys_inv_lref1: ∀G,L,T2,i. ⦃G, L⦄ ⊢ #i ▶*× T2 →
 120                       T2 = #i ∨
 121                       ∃∃I,K,V,V2. ⇩[O, i] L ≡ K. ⓑ{I}V & ⦃G, K⦄ ⊢ V ▶*× V2 &
 122                                   ⇧[O, i + 1] V2 ≡ T2.
 123 #G #L #T2 #i #H elim (cpys_inv_atom1 … H) -H /2 width=1 by or_introl/ *
 124 #I #K #V #V2 #j #HLK #HV2 #HVT2 #H destruct /3 width=7 by ex3_4_intro, or_intror/
 125 qed-.
 126
 127 lemma cpys_inv_lref1_ge: ∀G,L,T2,i. ⦃G, L⦄ ⊢ #i ▶*× T2 → |L| ≤ i → T2 = #i.
 128 #G #L #T2 #i #H elim (cpys_inv_lref1 … H) -H // *
 129 #I #K #V1 #V2 #HLK #_ #_ #HL -V2 lapply (ldrop_fwd_length_lt2 … HLK) -K -I -V1
 130 #H elim (lt_refl_false i) /2 width=3 by lt_to_le_to_lt/
 131 qed-.
 132
 133 lemma cpys_inv_gref1: ∀G,L,T2,p.  ⦃G, L⦄ ⊢ §p ▶*× T2 → T2 = §p.
 134 #G #L #T2 #p #H elim (cpys_inv_atom1 … H) -H // *
 135 #I #K #V #V2 #i #_ #_ #_ #H destruct
 136 qed-.
 137
 138 fact cpys_inv_bind1_aux: ∀G,L,U1,U2. ⦃G, L⦄ ⊢ U1 ▶*× U2 →
 139                          ∀a,J,V1,T1. U1 = ⓑ{a,J}V1.T1 →
 140                          ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*× V2 & ⦃G, L.ⓑ{J}V1⦄ ⊢ T1 ▶*× T2 &
 141                                   U2 = ⓑ{a,J}V2.T2.
 142 #G #L #U1 #U2 * -L -U1 -U2
 143 [ #I #G #L #b #J #W #U1 #H destruct
 144 | #I #G #L #K #V #V2 #W2 #i #_ #_ #_ #b #J #W #U1 #H destruct
 145 | #a #I #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #b #J #W #U1 #H destruct /2 width=5 by ex3_2_intro/
 146 | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #b #J #W #U1 #H destruct
 147 ]
 148 qed-.
 149
 150 lemma cpys_inv_bind1: ∀a,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*× U2 →
 151                       ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*× V2 & ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶*× T2 &
 152                                U2 = ⓑ{a,I}V2.T2.
 153 /2 width=3 by cpys_inv_bind1_aux/ qed-.
 154
 155 lemma cpys_inv_bind1_ext: ∀a,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*× U2 → ∀J.
 156                           ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*× V2 & ⦃G, L.ⓑ{J}V1⦄ ⊢ T1 ▶*× T2 &
 157                                    U2 = ⓑ{a,I}V2.T2.
 158 #a #I #G #L #V1 #T1 #U2 #H #J elim (cpys_inv_bind1 … H) -H
 159 #V2 #T2 #HV12 #HT12 #H destruct
 160 /4 width=5 by lsuby_cpys_trans, lsuby_pair, ex3_2_intro/
 161 qed-.
 162
 163 fact cpys_inv_flat1_aux: ∀G,L,U,U2. ⦃G, L⦄ ⊢ U ▶*× U2 →
 164                          ∀J,V1,U1. U = ⓕ{J}V1.U1 →
 165                          ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*× V2 & ⦃G, L⦄ ⊢ U1 ▶*× T2 &
 166                                   U2 = ⓕ{J}V2.T2.
 167 #G #L #U #U2 * -L -U -U2
 168 [ #I #G #L #J #W #U1 #H destruct
 169 | #I #G #L #K #V #V2 #W2 #i #_ #_ #_ #J #W #U1 #H destruct
 170 | #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #J #W #U1 #H destruct
 171 | #I #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #J #W #U1 #H destruct /2 width=5 by ex3_2_intro/
 172 ]
 173 qed-.
 174
 175 lemma cpys_inv_flat1: ∀I,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓕ{I}V1.U1 ▶*× U2 →
 176                       ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*× V2 & ⦃G, L⦄ ⊢ U1 ▶*× T2 &
 177                                U2 = ⓕ{I}V2.T2.
 178 /2 width=3 by cpys_inv_flat1_aux/ qed-.
 179
 180 (* Basic forward lemmas *****************************************************)
 181
 182 lemma cpys_fwd_bind1: ∀a,I,G,L,V1,T1,T. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*× T → ∀b,J.
 183                       ∃∃V2,T2. ⦃G, L⦄ ⊢ ⓑ{b,J}V1.T1 ▶*× ⓑ{b,J}V2.T2 &
 184                                T = ⓑ{a,I}V2.T2.
 185 #a #I #G #L #V1 #T1 #T #H #b #J elim (cpys_inv_bind1_ext … H J) -H
 186 #V2 #T2 #HV12 #HT12 #H destruct /3 width=4 by cpys_bind, ex2_2_intro/
 187 qed-.
 188
 189 lemma cpys_fwd_shift1: ∀G,L1,L,T1,T. ⦃G, L⦄ ⊢ L1 @@ T1 ▶*× T →
 190                        ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2.
 191 #G #L1 @(lenv_ind_dx … L1) -L1 normalize
 192 [ #L #T1 #T #HT1 @(ex2_2_intro … (⋆)) // (**) (* explicit constructor *)
 193 | #I #L1 #V1 #IH #L #T1 #X >shift_append_assoc normalize
 194   #H elim (cpys_inv_bind1 … H) -H
 195   #V0 #T0 #_ #HT10 #H destruct
 196   elim (IH … HT10) -IH -HT10 #L2 #T2 #HL12 #H destruct
 197   >append_length >HL12 -HL12
 198   @(ex2_2_intro … (⋆.ⓑ{I}V0@@L2) T2) [ >append_length ] /2 width=3 by trans_eq/ (**) (* explicit constructor *)
 199 ]
 200 qed-.