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 "generic entrywise extension (local environment)"
  33    'Relation RN RP f L1 L2 = (sex RN RP f L1 L2).
  34
  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.
  42
  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.
  51
  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.
  60
  61 (* Basic inversion lemmas ***************************************************)
  62
  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
  66 qed-.
  67
  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-.
  71
  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)
  79 ]
  80 qed-.
  81
  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-.
  86
  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/
  94 ]
  95 qed-.
  96
  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-.
 100
 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
 104 qed-.
 105
 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-.
 109
 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)
 117 ]
 118 qed-.
 119
 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-.
 124
 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/
 132 ]
 133 qed-.
 134
 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-.
 138
 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/
 145 qed-.
 146
 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/
 152 qed-.
 153
 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/
 159 qed-.
 160
 161 (* Basic forward lemmas *****************************************************)
 162
 163 lemma sex_fwd_bind: ∀RN,RP,f,I1,I2,L1,L2.
 164                     L1.ⓘ[I1] ⪤[RN,RP,f] L2.ⓘ[I2] →
 165                     L1 ⪤[RN,RP,⫱f] L2.
 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 //
 169 qed-.
 170
 171 (* Basic properties *********************************************************)
 172
 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/
 178 ]
 179 qed-.
 180
 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 *)
 183 qed-.
 184
 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/
 190 qed.
 191
 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/
 198 qed-.
 199
 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-.
 205
 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/
 210 qed-.
 211
 212 lemma sex_co_isid: ∀RN1,RP1,RN2,RP2. RP1 ⊆ RP2 →
 213                    ∀f,L1,L2. L1 ⪤[RN1,RP1,f] L2 → 𝐈❪f❫ →
 214                    L1 ⪤[RN2,RP2,f] L2.
 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/
 219 ]
 220 qed-.
 221
 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/
 231 ]
 232 qed-.
 233
 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/
 244 ]
 245 qed-.
 246
 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/
 257 ]
 258 qed-.
 259
 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/
 270 ]
 271 qed-.
 272
 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/
 283 ]
 284 qed-.
 285
 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
 294 | #f @or_intror #H
 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/ ]
 301   @or_intror #H
 302   [ elim (sex_inv_push … H) | elim (sex_inv_next … H) ] -H
 303   /2 width=1 by/
 304 ]
 305 qed-.