1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "basic_2/notation/relations/psubststar_4.ma".
16 include "basic_2/grammar/genv.ma".
17 include "basic_2/substitution/lsuby.ma".
19 (* CONTEXT-SENSITIVE EXTENDED MULTIPLE SUBSTITUTION FOR TERMS ***************)
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)
36 "context-sensitive extended multiple substitution (term)"
37 'PSubstStar G L T1 T2 = (cpys G L T1 T2).
39 (* Basic properties *********************************************************)
41 lemma lsuby_cpys_trans: ∀G. lsub_trans … (cpys G) lsuby.
42 #G #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2
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/
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/
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/
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.
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/ ]
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/
83 (* Basic inversion lemmas ***************************************************)
85 fact cpys_inv_atom1_aux: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ▶* T2 → ∀J. T1 = ⓪{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
97 lemma cpys_inv_atom1: ∀J,G,L,T2. ⦃G, L⦄ ⊢ ⓪{J} ▶* T2 →
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-.
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
108 lemma cpys_inv_lref1: ∀G,L,T2,i. ⦃G, L⦄ ⊢ #i ▶* T2 →
110 ∃∃I,K,V,V2. ⇩[i] L ≡ K. ⓑ{I}V & ⦃G, K⦄ ⊢ V ▶* V2 &
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/
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/
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
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 &
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
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 &
142 /2 width=3 by cpys_inv_bind1_aux/ qed-.
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 &
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/
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 &
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/
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 &
168 /2 width=3 by cpys_inv_flat1_aux/ qed-.
170 (* Basic forward lemmas *****************************************************)
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 &
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/