matita/matita/contribs/lambdadelta/static_2/relocation/sex.ma

   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 "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".
  19
  20 (* GENERIC ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****)
  21
  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])
  30 .
  31
  32 interpretation
  33   "generic entrywise extension (local environment)"
  34   'Relation RN RP f L1 L2 = (sex RN RP f L1 L2).
  35
  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.
  44
  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 ≝
  49            λR1,R2,RN,RP,f,L1,I1.
  50            ∀I2. R1 L1 I1 I2 → ∀L2. L1 ⪤[RN,RP,f] L2 → R2 L2 I1 I2.
  51
  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.
  61
  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.
  71
  72 (* Basic inversion lemmas ***************************************************)
  73
  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
  78 qed-.
  79
  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-.
  84
  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)
  93 ]
  94 qed-.
  95
  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-.
 101
 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/
 110 ]
 111 qed-.
 112
 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-.
 117
 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
 122 qed-.
 123
 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-.
 128
 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)
 137 ]
 138 qed-.
 139
 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-.
 145
 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/
 154 ]
 155 qed-.
 156
 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-.
 161
 162 (* Basic_2A1: includes lpx_sn_inv_pair *)
 163 lemma sex_inv_next (RN) (RP):
 164       ∀f,I1,I2,L1,L2.
 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/
 169 qed-.
 170
 171 lemma sex_inv_push (RN) (RP):
 172       ∀f,I1,I2,L1,L2.
 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/
 177 qed-.
 178
 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/
 185 qed-.
 186
 187 (* Basic forward lemmas *****************************************************)
 188
 189 lemma sex_fwd_bind (RN) (RP):
 190       ∀f,I1,I2,L1,L2.
 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 //
 195 qed-.
 196
 197 (* Basic properties *********************************************************)
 198
 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/
 205 ]
 206 qed-.
 207
 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 *)
 211 qed-.
 212
 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/
 219 qed.
 220
 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/
 227 qed-.
 228
 229 lemma sex_pair_repl (RN) (RP):
 230       ∀f,I1,I2,L1,L2.
 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-.
 235
 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/
 241 qed-.
 242
 243 lemma sex_co_isid (RN1) (RP1) (RN2) (RP2):
 244       RP1 ⊆ RP2 →
 245       ∀f,L1,L2. L1 ⪤[RN1,RP1,f] L2 → 𝐈❪f❫ →
 246       L1 ⪤[RN2,RP2,f] L2.
 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/
 251 ]
 252 qed-.
 253
 254 lemma sex_sdj (RN) (RP):
 255       RP ⊆ RN →
 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/
 264 ]
 265 qed-.
 266
 267 lemma sle_sex_trans (RN) (RP):
 268       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/
 278 ]
 279 qed-.
 280
 281 lemma sle_sex_conf (RN) (RP):
 282       RP ⊆ RN →
 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/
 292 ]
 293 qed-.
 294
 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/
 306 ]
 307 qed-.
 308
 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/
 320 ]
 321 qed-.
 322
 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
 331 | #f @or_intror #H
 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/ ]
 338   @or_intror #H
 339   [ elim (sex_inv_push … H) | elim (sex_inv_next … H) ] -H
 340   /2 width=1 by/
 341 ]
 342 qed-.