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 "ground/relocation/rtmap_sle.ma".
16 include "ground/relocation/rtmap_sdj.ma".
17 include "static_2/notation/relations/relation_5.ma".
18 include "static_2/syntax/lenv.ma".
20 (* GENERIC ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****)
22 inductive sex (RN,RP:relation3 lenv bind bind): rtmap → relation lenv ≝
23 | sex_atom: ∀f. sex RN RP f (⋆) (⋆)
24 | sex_next: ∀f,I1,I2,L1,L2.
25 sex RN RP f L1 L2 → RN L1 I1 I2 →
26 sex RN RP (↑f) (L1.ⓘ[I1]) (L2.ⓘ[I2])
27 | sex_push: ∀f,I1,I2,L1,L2.
28 sex RN RP f L1 L2 → RP L1 I1 I2 →
29 sex RN RP (⫯f) (L1.ⓘ[I1]) (L2.ⓘ[I2])
33 "generic entrywise extension (local environment)"
34 'Relation RN RP f L1 L2 = (sex RN RP f L1 L2).
36 definition R_pw_transitive_sex:
37 relation3 lenv bind bind → relation3 lenv bind bind →
38 relation3 lenv bind bind →
39 relation3 lenv bind bind → relation3 lenv bind bind →
40 relation3 rtmap lenv bind ≝
41 λR1,R2,R3,RN,RP,f,L1,I1.
42 ∀I. R1 L1 I1 I → ∀L2. L1 ⪤[RN,RP,f] L2 →
43 ∀I2. R2 L2 I I2 → R3 L1 I1 I2.
45 definition R_pw_confluent1_sex:
46 relation3 lenv bind bind → relation3 lenv bind bind →
47 relation3 lenv bind bind → relation3 lenv bind bind →
48 relation3 rtmap lenv bind ≝
50 ∀I2. R1 L1 I1 I2 → ∀L2. L1 ⪤[RN,RP,f] L2 → R2 L2 I1 I2.
52 definition R_pw_confluent2_sex:
53 relation3 lenv bind bind → relation3 lenv bind bind →
54 relation3 lenv bind bind → relation3 lenv bind bind →
55 relation3 lenv bind bind → relation3 lenv bind bind →
56 relation3 rtmap lenv bind ≝
57 λR1,R2,RN1,RP1,RN2,RP2,f,L0,I0.
58 ∀I1. R1 L0 I0 I1 → ∀I2. R2 L0 I0 I2 →
59 ∀L1. L0 ⪤[RN1,RP1,f] L1 → ∀L2. L0 ⪤[RN2,RP2,f] L2 →
60 ∃∃I. R2 L1 I1 I & R1 L2 I2 I.
62 definition R_pw_replace3_sex:
63 relation3 lenv bind bind → relation3 lenv bind bind →
64 relation3 lenv bind bind → relation3 lenv bind bind →
65 relation3 lenv bind bind → relation3 lenv bind bind →
66 relation3 rtmap lenv bind ≝
67 λR1,R2,RN1,RP1,RN2,RP2,f,L0,I0.
68 ∀I1. R1 L0 I0 I1 → ∀I2. R2 L0 I0 I2 →
69 ∀L1. L0 ⪤[RN1,RP1,f] L1 → ∀L2. L0 ⪤[RN2,RP2,f] L2 →
70 ∀I. R2 L1 I1 I → R1 L2 I2 I.
72 (* Basic inversion lemmas ***************************************************)
74 fact sex_inv_atom1_aux (RN) (RP):
75 ∀f,X,Y. X ⪤[RN,RP,f] Y → X = ⋆ → Y = ⋆.
76 #RN #RP #f #X #Y * -f -X -Y //
77 #f #I1 #I2 #L1 #L2 #_ #_ #H destruct
80 (* Basic_2A1: includes lpx_sn_inv_atom1 *)
81 lemma sex_inv_atom1 (RN) (RP):
82 ∀f,Y. ⋆ ⪤[RN,RP,f] Y → Y = ⋆.
83 /2 width=6 by sex_inv_atom1_aux/ qed-.
85 fact sex_inv_next1_aux (RN) (RP):
86 ∀f,X,Y. X ⪤[RN,RP,f] Y → ∀g,J1,K1. X = K1.ⓘ[J1] → f = ↑g →
87 ∃∃J2,K2. K1 ⪤[RN,RP,g] K2 & RN K1 J1 J2 & Y = K2.ⓘ[J2].
88 #RN #RP #f #X #Y * -f -X -Y
89 [ #f #g #J1 #K1 #H destruct
90 | #f #I1 #I2 #L1 #L2 #HL #HI #g #J1 #K1 #H1 #H2 <(injective_next … H2) -g destruct
91 /2 width=5 by ex3_2_intro/
92 | #f #I1 #I2 #L1 #L2 #_ #_ #g #J1 #K1 #_ #H elim (discr_push_next … H)
96 (* Basic_2A1: includes lpx_sn_inv_pair1 *)
97 lemma sex_inv_next1 (RN) (RP):
98 ∀g,J1,K1,Y. K1.ⓘ[J1] ⪤[RN,RP,↑g] Y →
99 ∃∃J2,K2. K1 ⪤[RN,RP,g] K2 & RN K1 J1 J2 & Y = K2.ⓘ[J2].
100 /2 width=7 by sex_inv_next1_aux/ qed-.
102 fact sex_inv_push1_aux (RN) (RP):
103 ∀f,X,Y. X ⪤[RN,RP,f] Y → ∀g,J1,K1. X = K1.ⓘ[J1] → f = ⫯g →
104 ∃∃J2,K2. K1 ⪤[RN,RP,g] K2 & RP K1 J1 J2 & Y = K2.ⓘ[J2].
105 #RN #RP #f #X #Y * -f -X -Y
106 [ #f #g #J1 #K1 #H destruct
107 | #f #I1 #I2 #L1 #L2 #_ #_ #g #J1 #K1 #_ #H elim (discr_next_push … H)
108 | #f #I1 #I2 #L1 #L2 #HL #HI #g #J1 #K1 #H1 #H2 <(injective_push … H2) -g destruct
109 /2 width=5 by ex3_2_intro/
113 lemma sex_inv_push1 (RN) (RP):
114 ∀g,J1,K1,Y. K1.ⓘ[J1] ⪤[RN,RP,⫯g] Y →
115 ∃∃J2,K2. K1 ⪤[RN,RP,g] K2 & RP K1 J1 J2 & Y = K2.ⓘ[J2].
116 /2 width=7 by sex_inv_push1_aux/ qed-.
118 fact sex_inv_atom2_aux (RN) (RP):
119 ∀f,X,Y. X ⪤[RN,RP,f] Y → Y = ⋆ → X = ⋆.
120 #RN #RP #f #X #Y * -f -X -Y //
121 #f #I1 #I2 #L1 #L2 #_ #_ #H destruct
124 (* Basic_2A1: includes lpx_sn_inv_atom2 *)
125 lemma sex_inv_atom2 (RN) (RP):
126 ∀f,X. X ⪤[RN,RP,f] ⋆ → X = ⋆.
127 /2 width=6 by sex_inv_atom2_aux/ qed-.
129 fact sex_inv_next2_aux (RN) (RP):
130 ∀f,X,Y. X ⪤[RN,RP,f] Y → ∀g,J2,K2. Y = K2.ⓘ[J2] → f = ↑g →
131 ∃∃J1,K1. K1 ⪤[RN,RP,g] K2 & RN K1 J1 J2 & X = K1.ⓘ[J1].
132 #RN #RP #f #X #Y * -f -X -Y
133 [ #f #g #J2 #K2 #H destruct
134 | #f #I1 #I2 #L1 #L2 #HL #HI #g #J2 #K2 #H1 #H2 <(injective_next … H2) -g destruct
135 /2 width=5 by ex3_2_intro/
136 | #f #I1 #I2 #L1 #L2 #_ #_ #g #J2 #K2 #_ #H elim (discr_push_next … H)
140 (* Basic_2A1: includes lpx_sn_inv_pair2 *)
141 lemma sex_inv_next2 (RN) (RP):
142 ∀g,J2,X,K2. X ⪤[RN,RP,↑g] K2.ⓘ[J2] →
143 ∃∃J1,K1. K1 ⪤[RN,RP,g] K2 & RN K1 J1 J2 & X = K1.ⓘ[J1].
144 /2 width=7 by sex_inv_next2_aux/ qed-.
146 fact sex_inv_push2_aux (RN) (RP):
147 ∀f,X,Y. X ⪤[RN,RP,f] Y → ∀g,J2,K2. Y = K2.ⓘ[J2] → f = ⫯g →
148 ∃∃J1,K1. K1 ⪤[RN,RP,g] K2 & RP K1 J1 J2 & X = K1.ⓘ[J1].
149 #RN #RP #f #X #Y * -f -X -Y
150 [ #f #J2 #K2 #g #H destruct
151 | #f #I1 #I2 #L1 #L2 #_ #_ #g #J2 #K2 #_ #H elim (discr_next_push … H)
152 | #f #I1 #I2 #L1 #L2 #HL #HI #g #J2 #K2 #H1 #H2 <(injective_push … H2) -g destruct
153 /2 width=5 by ex3_2_intro/
157 lemma sex_inv_push2 (RN) (RP):
158 ∀g,J2,X,K2. X ⪤[RN,RP,⫯g] K2.ⓘ[J2] →
159 ∃∃J1,K1. K1 ⪤[RN,RP,g] K2 & RP K1 J1 J2 & X = K1.ⓘ[J1].
160 /2 width=7 by sex_inv_push2_aux/ qed-.
162 (* Basic_2A1: includes lpx_sn_inv_pair *)
163 lemma sex_inv_next (RN) (RP):
165 L1.ⓘ[I1] ⪤[RN,RP,↑f] L2.ⓘ[I2] →
166 L1 ⪤[RN,RP,f] L2 ∧ RN L1 I1 I2.
167 #RN #RP #f #I1 #I2 #L1 #L2 #H elim (sex_inv_next1 … H) -H
168 #I0 #L0 #HL10 #HI10 #H destruct /2 width=1 by conj/
171 lemma sex_inv_push (RN) (RP):
173 L1.ⓘ[I1] ⪤[RN,RP,⫯f] L2.ⓘ[I2] →
174 L1 ⪤[RN,RP,f] L2 ∧ RP L1 I1 I2.
175 #RN #RP #f #I1 #I2 #L1 #L2 #H elim (sex_inv_push1 … H) -H
176 #I0 #L0 #HL10 #HI10 #H destruct /2 width=1 by conj/
179 lemma sex_inv_tl (RN) (RP):
180 ∀f,I1,I2,L1,L2. L1 ⪤[RN,RP,⫱f] L2 →
181 RN L1 I1 I2 → RP L1 I1 I2 →
182 L1.ⓘ[I1] ⪤[RN,RP,f] L2.ⓘ[I2].
183 #RN #RP #f #I1 #I2 #L2 #L2 elim (pn_split f) *
184 /2 width=1 by sex_next, sex_push/
187 (* Basic forward lemmas *****************************************************)
189 lemma sex_fwd_bind (RN) (RP):
191 L1.ⓘ[I1] ⪤[RN,RP,f] L2.ⓘ[I2] → L1 ⪤[RN,RP,⫱f] L2.
192 #RN #RP #f #I1 #I2 #L1 #L2 #Hf
193 elim (pn_split f) * #g #H destruct
194 [ elim (sex_inv_push … Hf) | elim (sex_inv_next … Hf) ] -Hf //
197 (* Basic properties *********************************************************)
199 lemma sex_eq_repl_back (RN) (RP):
200 ∀L1,L2. eq_repl_back … (λf. L1 ⪤[RN,RP,f] L2).
201 #RN #RP #L1 #L2 #f1 #H elim H -f1 -L1 -L2 //
202 #f1 #I1 #I2 #L1 #L2 #_ #HI #IH #f2 #H
203 [ elim (eq_inv_nx … H) -H /3 width=3 by sex_next/
204 | elim (eq_inv_px … H) -H /3 width=3 by sex_push/
208 lemma sex_eq_repl_fwd (RN) (RP):
209 ∀L1,L2. eq_repl_fwd … (λf. L1 ⪤[RN,RP,f] L2).
210 #RN #RP #L1 #L2 @eq_repl_sym /2 width=3 by sex_eq_repl_back/ (**) (* full auto fails *)
213 lemma sex_refl (RN) (RP):
214 c_reflexive … RN → c_reflexive … RP →
215 ∀f.reflexive … (sex RN RP f).
216 #RN #RP #HRN #HRP #f #L generalize in match f; -f elim L -L //
217 #L #I #IH #f elim (pn_split f) *
218 #g #H destruct /2 width=1 by sex_next, sex_push/
221 lemma sex_sym (RN) (RP):
222 (∀L1,L2,I1,I2. RN L1 I1 I2 → RN L2 I2 I1) →
223 (∀L1,L2,I1,I2. RP L1 I1 I2 → RP L2 I2 I1) →
224 ∀f. symmetric … (sex RN RP f).
225 #RN #RP #HRN #HRP #f #L1 #L2 #H elim H -L1 -L2 -f
226 /3 width=2 by sex_next, sex_push/
229 lemma sex_pair_repl (RN) (RP):
231 L1.ⓘ[I1] ⪤[RN,RP,f] L2.ⓘ[I2] →
232 ∀J1,J2. RN L1 J1 J2 → RP L1 J1 J2 →
233 L1.ⓘ[J1] ⪤[RN,RP,f] L2.ⓘ[J2].
234 /3 width=3 by sex_inv_tl, sex_fwd_bind/ qed-.
236 lemma sex_co (RN1) (RP1) (RN2) (RP2):
237 RN1 ⊆ RN2 → RP1 ⊆ RP2 →
238 ∀f,L1,L2. L1 ⪤[RN1,RP1,f] L2 → L1 ⪤[RN2,RP2,f] L2.
239 #RN1 #RP1 #RN2 #RP2 #HRN #HRP #f #L1 #L2 #H elim H -f -L1 -L2
240 /3 width=1 by sex_atom, sex_next, sex_push/
243 lemma sex_co_isid (RN1) (RP1) (RN2) (RP2):
245 ∀f,L1,L2. L1 ⪤[RN1,RP1,f] L2 → 𝐈❪f❫ →
247 #RN1 #RP1 #RN2 #RP2 #HR #f #L1 #L2 #H elim H -f -L1 -L2 //
248 #f #I1 #I2 #K1 #K2 #_ #HI12 #IH #H
249 [ elim (isid_inv_next … H) -H //
250 | /4 width=3 by sex_push, isid_inv_push/
254 lemma sex_sdj (RN) (RP):
256 ∀f1,L1,L2. L1 ⪤[RN,RP,f1] L2 →
257 ∀f2. f1 ∥ f2 → L1 ⪤[RP,RN,f2] L2.
258 #RN #RP #HR #f1 #L1 #L2 #H elim H -f1 -L1 -L2 //
259 #f1 #I1 #I2 #L1 #L2 #_ #HI12 #IH #f2 #H12
260 [ elim (sdj_inv_nx … H12) -H12 [2,3: // ]
261 #g2 #H #H2 destruct /3 width=1 by sex_push/
262 | elim (sdj_inv_px … H12) -H12 [2,4: // ] *
263 #g2 #H #H2 destruct /3 width=1 by sex_next, sex_push/
267 lemma sle_sex_trans (RN) (RP):
269 ∀f2,L1,L2. L1 ⪤[RN,RP,f2] L2 →
270 ∀f1. f1 ⊆ f2 → L1 ⪤[RN,RP,f1] L2.
271 #RN #RP #HR #f2 #L1 #L2 #H elim H -f2 -L1 -L2 //
272 #f2 #I1 #I2 #L1 #L2 #_ #HI12 #IH #f1 #H12
273 [ elim (pn_split f1) * ]
274 [ /4 width=5 by sex_push, sle_inv_pn/
275 | /4 width=5 by sex_next, sle_inv_nn/
276 | elim (sle_inv_xp … H12) -H12 [2,3: // ]
277 #g1 #H #H1 destruct /3 width=5 by sex_push/
281 lemma sle_sex_conf (RN) (RP):
283 ∀f1,L1,L2. L1 ⪤[RN,RP,f1] L2 →
284 ∀f2. f1 ⊆ f2 → L1 ⪤[RN,RP,f2] L2.
285 #RN #RP #HR #f1 #L1 #L2 #H elim H -f1 -L1 -L2 //
286 #f1 #I1 #I2 #L1 #L2 #_ #HI12 #IH #f2 #H12
287 [2: elim (pn_split f2) * ]
288 [ /4 width=5 by sex_push, sle_inv_pp/
289 | /4 width=5 by sex_next, sle_inv_pn/
290 | elim (sle_inv_nx … H12) -H12 [2,3: // ]
291 #g2 #H #H2 destruct /3 width=5 by sex_next/
295 lemma sex_sle_split_sn (R1) (R2) (RP):
296 c_reflexive … R1 → c_reflexive … R2 →
297 ∀f,L1,L2. L1 ⪤[R1,RP,f] L2 → ∀g. f ⊆ g →
298 ∃∃L. L1 ⪤[R1,RP,g] L & L ⪤[R2,cfull,f] L2.
299 #R1 #R2 #RP #HR1 #HR2 #f #L1 #L2 #H elim H -f -L1 -L2
300 [ /2 width=3 by sex_atom, ex2_intro/ ]
301 #f #I1 #I2 #L1 #L2 #_ #HI12 #IH #y #H
302 [ elim (sle_inv_nx … H ??) -H [ |*: // ] #g #Hfg #H destruct
303 elim (IH … Hfg) -IH -Hfg /3 width=5 by sex_next, ex2_intro/
304 | elim (sle_inv_px … H ??) -H [1,3: * |*: // ] #g #Hfg #H destruct
305 elim (IH … Hfg) -IH -Hfg /3 width=5 by sex_next, sex_push, ex2_intro/
309 lemma sex_sdj_split_sn (R1) (R2) (RP):
310 c_reflexive … R1 → c_reflexive … R2 →
311 ∀f,L1,L2. L1 ⪤[R1,RP,f] L2 → ∀g. f ∥ g →
312 ∃∃L. L1 ⪤[RP,R1,g] L & L ⪤[R2,cfull,f] L2.
313 #R1 #R2 #RP #HR1 #HR2 #f #L1 #L2 #H elim H -f -L1 -L2
314 [ /2 width=3 by sex_atom, ex2_intro/ ]
315 #f #I1 #I2 #L1 #L2 #_ #HI12 #IH #y #H
316 [ elim (sdj_inv_nx … H ??) -H [ |*: // ] #g #Hfg #H destruct
317 elim (IH … Hfg) -IH -Hfg /3 width=5 by sex_next, sex_push, ex2_intro/
318 | elim (sdj_inv_px … H ??) -H [1,3: * |*: // ] #g #Hfg #H destruct
319 elim (IH … Hfg) -IH -Hfg /3 width=5 by sex_next, sex_push, ex2_intro/
323 lemma sex_dec (RN) (RP):
324 (∀L,I1,I2. Decidable (RN L I1 I2)) →
325 (∀L,I1,I2. Decidable (RP L I1 I2)) →
326 ∀L1,L2,f. Decidable (L1 ⪤[RN,RP,f] L2).
327 #RN #RP #HRN #HRP #L1 elim L1 -L1 [ * | #L1 #I1 #IH * ]
328 [ /2 width=1 by sex_atom, or_introl/
329 | #L2 #I2 #f @or_intror #H
330 lapply (sex_inv_atom1 … H) -H #H destruct
332 lapply (sex_inv_atom2 … H) -H #H destruct
333 | #L2 #I2 #f elim (IH L2 (⫱f)) -IH #HL12
334 [2: /4 width=3 by sex_fwd_bind, or_intror/ ]
335 elim (pn_split f) * #g #H destruct
336 [ elim (HRP L1 I1 I2) | elim (HRN L1 I1 I2) ] -HRP -HRN #HV12
337 [1,3: /3 width=1 by sex_push, sex_next, or_introl/ ]
339 [ elim (sex_inv_push … H) | elim (sex_inv_next … H) ] -H