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])
32 interpretation "generic entrywise extension (local environment)"
33 'Relation RN RP f L1 L2 = (sex RN RP f L1 L2).
35 definition sex_transitive: relation3 lenv bind bind → relation3 lenv bind bind →
36 relation3 lenv bind bind →
37 relation3 lenv bind bind → relation3 lenv bind bind →
38 relation3 rtmap lenv bind ≝
39 λR1,R2,R3,RN,RP,f,L1,I1.
40 ∀I. R1 L1 I1 I → ∀L2. L1 ⪤[RN,RP,f] L2 →
41 ∀I2. R2 L2 I I2 → R3 L1 I1 I2.
43 definition R_pw_confluent2_sex: relation3 lenv bind bind → relation3 lenv bind bind →
44 relation3 lenv bind bind → relation3 lenv bind bind →
45 relation3 lenv bind bind → relation3 lenv bind bind →
46 relation3 rtmap lenv bind ≝
47 λR1,R2,RN1,RP1,RN2,RP2,f,L0,I0.
48 ∀I1. R1 L0 I0 I1 → ∀I2. R2 L0 I0 I2 →
49 ∀L1. L0 ⪤[RN1,RP1,f] L1 → ∀L2. L0 ⪤[RN2,RP2,f] L2 →
50 ∃∃I. R2 L1 I1 I & R1 L2 I2 I.
52 definition R_pw_replace3_sex: relation3 lenv bind bind → relation3 lenv bind bind →
53 relation3 lenv bind bind → relation3 lenv bind bind →
54 relation3 lenv bind bind → relation3 lenv bind bind →
55 relation3 rtmap lenv bind ≝
56 λR1,R2,RN1,RP1,RN2,RP2,f,L0,I0.
57 ∀I1. R1 L0 I0 I1 → ∀I2. R2 L0 I0 I2 →
58 ∀L1. L0 ⪤[RN1,RP1,f] L1 → ∀L2. L0 ⪤[RN2,RP2,f] L2 →
59 ∀I. R2 L1 I1 I → R1 L2 I2 I.
61 (* Basic inversion lemmas ***************************************************)
63 fact sex_inv_atom1_aux: ∀RN,RP,f,X,Y. X ⪤[RN,RP,f] Y → X = ⋆ → Y = ⋆.
64 #RN #RP #f #X #Y * -f -X -Y //
65 #f #I1 #I2 #L1 #L2 #_ #_ #H destruct
68 (* Basic_2A1: includes lpx_sn_inv_atom1 *)
69 lemma sex_inv_atom1: ∀RN,RP,f,Y. ⋆ ⪤[RN,RP,f] Y → Y = ⋆.
70 /2 width=6 by sex_inv_atom1_aux/ qed-.
72 fact sex_inv_next1_aux: ∀RN,RP,f,X,Y. X ⪤[RN,RP,f] Y → ∀g,J1,K1. X = K1.ⓘ[J1] → f = ↑g →
73 ∃∃J2,K2. K1 ⪤[RN,RP,g] K2 & RN K1 J1 J2 & Y = K2.ⓘ[J2].
74 #RN #RP #f #X #Y * -f -X -Y
75 [ #f #g #J1 #K1 #H destruct
76 | #f #I1 #I2 #L1 #L2 #HL #HI #g #J1 #K1 #H1 #H2 <(injective_next … H2) -g destruct
77 /2 width=5 by ex3_2_intro/
78 | #f #I1 #I2 #L1 #L2 #_ #_ #g #J1 #K1 #_ #H elim (discr_push_next … H)
82 (* Basic_2A1: includes lpx_sn_inv_pair1 *)
83 lemma sex_inv_next1: ∀RN,RP,g,J1,K1,Y. K1.ⓘ[J1] ⪤[RN,RP,↑g] Y →
84 ∃∃J2,K2. K1 ⪤[RN,RP,g] K2 & RN K1 J1 J2 & Y = K2.ⓘ[J2].
85 /2 width=7 by sex_inv_next1_aux/ qed-.
87 fact sex_inv_push1_aux: ∀RN,RP,f,X,Y. X ⪤[RN,RP,f] Y → ∀g,J1,K1. X = K1.ⓘ[J1] → f = ⫯g →
88 ∃∃J2,K2. K1 ⪤[RN,RP,g] K2 & RP K1 J1 J2 & Y = K2.ⓘ[J2].
89 #RN #RP #f #X #Y * -f -X -Y
90 [ #f #g #J1 #K1 #H destruct
91 | #f #I1 #I2 #L1 #L2 #_ #_ #g #J1 #K1 #_ #H elim (discr_next_push … H)
92 | #f #I1 #I2 #L1 #L2 #HL #HI #g #J1 #K1 #H1 #H2 <(injective_push … H2) -g destruct
93 /2 width=5 by ex3_2_intro/
97 lemma sex_inv_push1: ∀RN,RP,g,J1,K1,Y. K1.ⓘ[J1] ⪤[RN,RP,⫯g] Y →
98 ∃∃J2,K2. K1 ⪤[RN,RP,g] K2 & RP K1 J1 J2 & Y = K2.ⓘ[J2].
99 /2 width=7 by sex_inv_push1_aux/ qed-.
101 fact sex_inv_atom2_aux: ∀RN,RP,f,X,Y. X ⪤[RN,RP,f] Y → Y = ⋆ → X = ⋆.
102 #RN #RP #f #X #Y * -f -X -Y //
103 #f #I1 #I2 #L1 #L2 #_ #_ #H destruct
106 (* Basic_2A1: includes lpx_sn_inv_atom2 *)
107 lemma sex_inv_atom2: ∀RN,RP,f,X. X ⪤[RN,RP,f] ⋆ → X = ⋆.
108 /2 width=6 by sex_inv_atom2_aux/ qed-.
110 fact sex_inv_next2_aux: ∀RN,RP,f,X,Y. X ⪤[RN,RP,f] Y → ∀g,J2,K2. Y = K2.ⓘ[J2] → f = ↑g →
111 ∃∃J1,K1. K1 ⪤[RN,RP,g] K2 & RN K1 J1 J2 & X = K1.ⓘ[J1].
112 #RN #RP #f #X #Y * -f -X -Y
113 [ #f #g #J2 #K2 #H destruct
114 | #f #I1 #I2 #L1 #L2 #HL #HI #g #J2 #K2 #H1 #H2 <(injective_next … H2) -g destruct
115 /2 width=5 by ex3_2_intro/
116 | #f #I1 #I2 #L1 #L2 #_ #_ #g #J2 #K2 #_ #H elim (discr_push_next … H)
120 (* Basic_2A1: includes lpx_sn_inv_pair2 *)
121 lemma sex_inv_next2: ∀RN,RP,g,J2,X,K2. X ⪤[RN,RP,↑g] K2.ⓘ[J2] →
122 ∃∃J1,K1. K1 ⪤[RN,RP,g] K2 & RN K1 J1 J2 & X = K1.ⓘ[J1].
123 /2 width=7 by sex_inv_next2_aux/ qed-.
125 fact sex_inv_push2_aux: ∀RN,RP,f,X,Y. X ⪤[RN,RP,f] Y → ∀g,J2,K2. Y = K2.ⓘ[J2] → f = ⫯g →
126 ∃∃J1,K1. K1 ⪤[RN,RP,g] K2 & RP K1 J1 J2 & X = K1.ⓘ[J1].
127 #RN #RP #f #X #Y * -f -X -Y
128 [ #f #J2 #K2 #g #H destruct
129 | #f #I1 #I2 #L1 #L2 #_ #_ #g #J2 #K2 #_ #H elim (discr_next_push … H)
130 | #f #I1 #I2 #L1 #L2 #HL #HI #g #J2 #K2 #H1 #H2 <(injective_push … H2) -g destruct
131 /2 width=5 by ex3_2_intro/
135 lemma sex_inv_push2: ∀RN,RP,g,J2,X,K2. X ⪤[RN,RP,⫯g] K2.ⓘ[J2] →
136 ∃∃J1,K1. K1 ⪤[RN,RP,g] K2 & RP K1 J1 J2 & X = K1.ⓘ[J1].
137 /2 width=7 by sex_inv_push2_aux/ qed-.
139 (* Basic_2A1: includes lpx_sn_inv_pair *)
140 lemma sex_inv_next: ∀RN,RP,f,I1,I2,L1,L2.
141 L1.ⓘ[I1] ⪤[RN,RP,↑f] L2.ⓘ[I2] →
142 L1 ⪤[RN,RP,f] L2 ∧ RN L1 I1 I2.
143 #RN #RP #f #I1 #I2 #L1 #L2 #H elim (sex_inv_next1 … H) -H
144 #I0 #L0 #HL10 #HI10 #H destruct /2 width=1 by conj/
147 lemma sex_inv_push: ∀RN,RP,f,I1,I2,L1,L2.
148 L1.ⓘ[I1] ⪤[RN,RP,⫯f] L2.ⓘ[I2] →
149 L1 ⪤[RN,RP,f] L2 ∧ RP L1 I1 I2.
150 #RN #RP #f #I1 #I2 #L1 #L2 #H elim (sex_inv_push1 … H) -H
151 #I0 #L0 #HL10 #HI10 #H destruct /2 width=1 by conj/
154 lemma sex_inv_tl: ∀RN,RP,f,I1,I2,L1,L2. L1 ⪤[RN,RP,⫱f] L2 →
155 RN L1 I1 I2 → RP L1 I1 I2 →
156 L1.ⓘ[I1] ⪤[RN,RP,f] L2.ⓘ[I2].
157 #RN #RP #f #I1 #I2 #L2 #L2 elim (pn_split f) *
158 /2 width=1 by sex_next, sex_push/
161 (* Basic forward lemmas *****************************************************)
163 lemma sex_fwd_bind: ∀RN,RP,f,I1,I2,L1,L2.
164 L1.ⓘ[I1] ⪤[RN,RP,f] L2.ⓘ[I2] →
166 #RN #RP #f #I1 #I2 #L1 #L2 #Hf
167 elim (pn_split f) * #g #H destruct
168 [ elim (sex_inv_push … Hf) | elim (sex_inv_next … Hf) ] -Hf //
171 (* Basic properties *********************************************************)
173 lemma sex_eq_repl_back: ∀RN,RP,L1,L2. eq_repl_back … (λf. L1 ⪤[RN,RP,f] L2).
174 #RN #RP #L1 #L2 #f1 #H elim H -f1 -L1 -L2 //
175 #f1 #I1 #I2 #L1 #L2 #_ #HI #IH #f2 #H
176 [ elim (eq_inv_nx … H) -H /3 width=3 by sex_next/
177 | elim (eq_inv_px … H) -H /3 width=3 by sex_push/
181 lemma sex_eq_repl_fwd: ∀RN,RP,L1,L2. eq_repl_fwd … (λf. L1 ⪤[RN,RP,f] L2).
182 #RN #RP #L1 #L2 @eq_repl_sym /2 width=3 by sex_eq_repl_back/ (**) (* full auto fails *)
185 lemma sex_refl: ∀RN,RP. c_reflexive … RN → c_reflexive … RP →
186 ∀f.reflexive … (sex RN RP f).
187 #RN #RP #HRN #HRP #f #L generalize in match f; -f elim L -L //
188 #L #I #IH #f elim (pn_split f) *
189 #g #H destruct /2 width=1 by sex_next, sex_push/
192 lemma sex_sym: ∀RN,RP.
193 (∀L1,L2,I1,I2. RN L1 I1 I2 → RN L2 I2 I1) →
194 (∀L1,L2,I1,I2. RP L1 I1 I2 → RP L2 I2 I1) →
195 ∀f. symmetric … (sex RN RP f).
196 #RN #RP #HRN #HRP #f #L1 #L2 #H elim H -L1 -L2 -f
197 /3 width=2 by sex_next, sex_push/
200 lemma sex_pair_repl: ∀RN,RP,f,I1,I2,L1,L2.
201 L1.ⓘ[I1] ⪤[RN,RP,f] L2.ⓘ[I2] →
202 ∀J1,J2. RN L1 J1 J2 → RP L1 J1 J2 →
203 L1.ⓘ[J1] ⪤[RN,RP,f] L2.ⓘ[J2].
204 /3 width=3 by sex_inv_tl, sex_fwd_bind/ qed-.
206 lemma sex_co: ∀RN1,RP1,RN2,RP2. RN1 ⊆ RN2 → RP1 ⊆ RP2 →
207 ∀f,L1,L2. L1 ⪤[RN1,RP1,f] L2 → L1 ⪤[RN2,RP2,f] L2.
208 #RN1 #RP1 #RN2 #RP2 #HRN #HRP #f #L1 #L2 #H elim H -f -L1 -L2
209 /3 width=1 by sex_atom, sex_next, sex_push/
212 lemma sex_co_isid: ∀RN1,RP1,RN2,RP2. RP1 ⊆ RP2 →
213 ∀f,L1,L2. L1 ⪤[RN1,RP1,f] L2 → 𝐈❪f❫ →
215 #RN1 #RP1 #RN2 #RP2 #HR #f #L1 #L2 #H elim H -f -L1 -L2 //
216 #f #I1 #I2 #K1 #K2 #_ #HI12 #IH #H
217 [ elim (isid_inv_next … H) -H //
218 | /4 width=3 by sex_push, isid_inv_push/
222 lemma sex_sdj: ∀RN,RP. RP ⊆ RN →
223 ∀f1,L1,L2. L1 ⪤[RN,RP,f1] L2 →
224 ∀f2. f1 ∥ f2 → L1 ⪤[RP,RN,f2] L2.
225 #RN #RP #HR #f1 #L1 #L2 #H elim H -f1 -L1 -L2 //
226 #f1 #I1 #I2 #L1 #L2 #_ #HI12 #IH #f2 #H12
227 [ elim (sdj_inv_nx … H12) -H12 [2,3: // ]
228 #g2 #H #H2 destruct /3 width=1 by sex_push/
229 | elim (sdj_inv_px … H12) -H12 [2,4: // ] *
230 #g2 #H #H2 destruct /3 width=1 by sex_next, sex_push/
234 lemma sle_sex_trans: ∀RN,RP. RN ⊆ RP →
235 ∀f2,L1,L2. L1 ⪤[RN,RP,f2] L2 →
236 ∀f1. f1 ⊆ f2 → L1 ⪤[RN,RP,f1] L2.
237 #RN #RP #HR #f2 #L1 #L2 #H elim H -f2 -L1 -L2 //
238 #f2 #I1 #I2 #L1 #L2 #_ #HI12 #IH #f1 #H12
239 [ elim (pn_split f1) * ]
240 [ /4 width=5 by sex_push, sle_inv_pn/
241 | /4 width=5 by sex_next, sle_inv_nn/
242 | elim (sle_inv_xp … H12) -H12 [2,3: // ]
243 #g1 #H #H1 destruct /3 width=5 by sex_push/
247 lemma sle_sex_conf: ∀RN,RP. RP ⊆ RN →
248 ∀f1,L1,L2. L1 ⪤[RN,RP,f1] L2 →
249 ∀f2. f1 ⊆ f2 → L1 ⪤[RN,RP,f2] L2.
250 #RN #RP #HR #f1 #L1 #L2 #H elim H -f1 -L1 -L2 //
251 #f1 #I1 #I2 #L1 #L2 #_ #HI12 #IH #f2 #H12
252 [2: elim (pn_split f2) * ]
253 [ /4 width=5 by sex_push, sle_inv_pp/
254 | /4 width=5 by sex_next, sle_inv_pn/
255 | elim (sle_inv_nx … H12) -H12 [2,3: // ]
256 #g2 #H #H2 destruct /3 width=5 by sex_next/
260 lemma sex_sle_split: ∀R1,R2,RP. c_reflexive … R1 → c_reflexive … R2 →
261 ∀f,L1,L2. L1 ⪤[R1,RP,f] L2 → ∀g. f ⊆ g →
262 ∃∃L. L1 ⪤[R1,RP,g] L & L ⪤[R2,cfull,f] L2.
263 #R1 #R2 #RP #HR1 #HR2 #f #L1 #L2 #H elim H -f -L1 -L2
264 [ /2 width=3 by sex_atom, ex2_intro/ ]
265 #f #I1 #I2 #L1 #L2 #_ #HI12 #IH #y #H
266 [ elim (sle_inv_nx … H ??) -H [ |*: // ] #g #Hfg #H destruct
267 elim (IH … Hfg) -IH -Hfg /3 width=5 by sex_next, ex2_intro/
268 | elim (sle_inv_px … H ??) -H [1,3: * |*: // ] #g #Hfg #H destruct
269 elim (IH … Hfg) -IH -Hfg /3 width=5 by sex_next, sex_push, ex2_intro/
273 lemma sex_sdj_split: ∀R1,R2,RP. c_reflexive … R1 → c_reflexive … R2 →
274 ∀f,L1,L2. L1 ⪤[R1,RP,f] L2 → ∀g. f ∥ g →
275 ∃∃L. L1 ⪤[RP,R1,g] L & L ⪤[R2,cfull,f] L2.
276 #R1 #R2 #RP #HR1 #HR2 #f #L1 #L2 #H elim H -f -L1 -L2
277 [ /2 width=3 by sex_atom, ex2_intro/ ]
278 #f #I1 #I2 #L1 #L2 #_ #HI12 #IH #y #H
279 [ elim (sdj_inv_nx … H ??) -H [ |*: // ] #g #Hfg #H destruct
280 elim (IH … Hfg) -IH -Hfg /3 width=5 by sex_next, sex_push, ex2_intro/
281 | elim (sdj_inv_px … H ??) -H [1,3: * |*: // ] #g #Hfg #H destruct
282 elim (IH … Hfg) -IH -Hfg /3 width=5 by sex_next, sex_push, ex2_intro/
286 lemma sex_dec: ∀RN,RP.
287 (∀L,I1,I2. Decidable (RN L I1 I2)) →
288 (∀L,I1,I2. Decidable (RP L I1 I2)) →
289 ∀L1,L2,f. Decidable (L1 ⪤[RN,RP,f] L2).
290 #RN #RP #HRN #HRP #L1 elim L1 -L1 [ * | #L1 #I1 #IH * ]
291 [ /2 width=1 by sex_atom, or_introl/
292 | #L2 #I2 #f @or_intror #H
293 lapply (sex_inv_atom1 … H) -H #H destruct
295 lapply (sex_inv_atom2 … H) -H #H destruct
296 | #L2 #I2 #f elim (IH L2 (⫱f)) -IH #HL12
297 [2: /4 width=3 by sex_fwd_bind, or_intror/ ]
298 elim (pn_split f) * #g #H destruct
299 [ elim (HRP L1 I1 I2) | elim (HRN L1 I1 I2) ] -HRP -HRN #HV12
300 [1,3: /3 width=1 by sex_push, sex_next, or_introl/ ]
302 [ elim (sex_inv_push … H) | elim (sex_inv_next … H) ] -H