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