matita/matita/contribs/lambdadelta/static_2/i_static/rexs.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/lib/star.ma".
  16 include "static_2/notation/relations/relationstar_4.ma".
  17 include "static_2/static/rex.ma".
  18
  19 (* ITERATED EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ***)
  20
  21 definition rexs (R): term → relation lenv ≝ CTC … (rex R).
  22
  23 interpretation "iterated extension on referred entries (local environment)"
  24    'RelationStar R T L1 L2 = (rexs R T L1 L2).
  25
  26 (* Basic properties *********************************************************)
  27
  28 lemma rexs_step_dx: ∀R,L1,L,T. L1 ⪤*[R,T] L →
  29                     ∀L2. L ⪤[R,T] L2 → L1 ⪤*[R,T] L2.
  30 #R #L1 #L2 #T #HL1 #L2 @step @HL1 (**) (* auto fails *)
  31 qed-.
  32
  33 lemma rexs_step_sn: ∀R,L1,L,T. L1 ⪤[R,T] L →
  34                     ∀L2. L ⪤*[R,T] L2 → L1 ⪤*[R,T] L2.
  35 #R #L1 #L2 #T #HL1 #L2 @TC_strap @HL1 (**) (* auto fails *)
  36 qed-.
  37
  38 lemma rexs_atom: ∀R,I. ⋆ ⪤*[R,⓪[I]] ⋆.
  39 /2 width=1 by inj/ qed.
  40
  41 lemma rexs_sort: ∀R,I,L1,L2,V1,V2,s.
  42                  L1 ⪤*[R,⋆s] L2 → L1.ⓑ[I]V1 ⪤*[R,⋆s] L2.ⓑ[I]V2.
  43 #R #I #L1 #L2 #V1 #V2 #s #H elim H -L2
  44 /3 width=4 by rex_sort, rexs_step_dx, inj/
  45 qed.
  46
  47 lemma rexs_pair: ∀R. (∀L. reflexive … (R L)) →
  48                  ∀I,L1,L2,V. L1 ⪤*[R,V] L2 →
  49                  L1.ⓑ[I]V ⪤*[R,#0] L2.ⓑ[I]V.
  50 #R #HR #I #L1 #L2 #V #H elim H -L2
  51 /3 width=5 by rex_pair, rexs_step_dx, inj/
  52 qed.
  53
  54 lemma rexs_unit: ∀R,f,I,L1,L2. 𝐈❨f❩ → L1 ⪤[cext2 R,cfull,f] L2 →
  55                  L1.ⓤ[I] ⪤*[R,#0] L2.ⓤ[I].
  56 /3 width=3 by rex_unit, inj/ qed.
  57
  58 lemma rexs_lref: ∀R,I,L1,L2,V1,V2,i.
  59                  L1 ⪤*[R,#i] L2 → L1.ⓑ[I]V1 ⪤*[R,#↑i] L2.ⓑ[I]V2.
  60 #R #I #L1 #L2 #V1 #V2 #i #H elim H -L2
  61 /3 width=4 by rex_lref, rexs_step_dx, inj/
  62 qed.
  63
  64 lemma rexs_gref: ∀R,I,L1,L2,V1,V2,l.
  65                  L1 ⪤*[R,§l] L2 → L1.ⓑ[I]V1 ⪤*[R,§l] L2.ⓑ[I]V2.
  66 #R #I #L1 #L2 #V1 #V2 #l #H elim H -L2
  67 /3 width=4 by rex_gref, rexs_step_dx, inj/
  68 qed.
  69
  70 lemma rexs_co: ∀R1,R2. (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) →
  71                ∀L1,L2,T. L1 ⪤*[R1,T] L2 → L1 ⪤*[R2,T] L2.
  72 #R1 #R2 #HR #L1 #L2 #T #H elim H -L2
  73 /4 width=5 by rex_co, rexs_step_dx, inj/
  74 qed-.
  75
  76 (* Basic inversion lemmas ***************************************************)
  77
  78 (* Basic_2A1: uses: TC_lpx_sn_inv_atom1 *)
  79 lemma rexs_inv_atom_sn: ∀R,I,Y2. ⋆ ⪤*[R,⓪[I]] Y2 → Y2 = ⋆.
  80 #R #I #Y2 #H elim H -Y2 /3 width=3 by inj, rex_inv_atom_sn/
  81 qed-.
  82
  83 (* Basic_2A1: uses: TC_lpx_sn_inv_atom2 *)
  84 lemma rexs_inv_atom_dx: ∀R,I,Y1. Y1 ⪤*[R,⓪[I]] ⋆ → Y1 = ⋆.
  85 #R #I #Y1 #H @(TC_ind_dx ??????? H) -Y1
  86 /3 width=3 by inj, rex_inv_atom_dx/
  87 qed-.
  88
  89 lemma rexs_inv_sort: ∀R,Y1,Y2,s. Y1 ⪤*[R,⋆s] Y2 →
  90                      ∨∨ ∧∧ Y1 = ⋆ & Y2 = ⋆
  91                       | ∃∃I1,I2,L1,L2. L1 ⪤*[R,⋆s] L2 &
  92                                        Y1 = L1.ⓘ[I1] & Y2 = L2.ⓘ[I2].
  93 #R #Y1 #Y2 #s #H elim H -Y2
  94 [ #Y2 #H elim (rex_inv_sort … H) -H *
  95   /4 width=8 by ex3_4_intro, inj, or_introl, or_intror, conj/
  96 | #Y #Y2 #_ #H elim (rex_inv_sort … H) -H *
  97   [ #H #H2 * * /3 width=7 by ex3_4_intro, or_introl, or_intror, conj/
  98   | #I #I2 #L #L2 #HL2 #H #H2 * *
  99     [ #H1 #H0 destruct
 100     | #I1 #I0 #L1 #L0 #HL10 #H1 #H0 destruct
 101       /4 width=7 by ex3_4_intro, rexs_step_dx, or_intror/
 102     ]
 103   ]
 104 ]
 105 qed-.
 106
 107 lemma rexs_inv_gref: ∀R,Y1,Y2,l. Y1 ⪤*[R,§l] Y2 →
 108                      ∨∨ ∧∧ Y1 = ⋆ & Y2 = ⋆
 109                       | ∃∃I1,I2,L1,L2. L1 ⪤*[R,§l] L2 &
 110                                        Y1 = L1.ⓘ[I1] & Y2 = L2.ⓘ[I2].
 111 #R #Y1 #Y2 #l #H elim H -Y2
 112 [ #Y2 #H elim (rex_inv_gref … H) -H *
 113   /4 width=8 by ex3_4_intro, inj, or_introl, or_intror, conj/
 114 | #Y #Y2 #_ #H elim (rex_inv_gref … H) -H *
 115   [ #H #H2 * * /3 width=7 by ex3_4_intro, or_introl, or_intror, conj/
 116   | #I #I2 #L #L2 #HL2 #H #H2 * *
 117     [ #H1 #H0 destruct
 118     | #I1 #I0 #L1 #L0 #HL10 #H1 #H0 destruct
 119       /4 width=7 by ex3_4_intro, rexs_step_dx, or_intror/
 120     ]
 121   ]
 122 ]
 123 qed-.
 124
 125 lemma rexs_inv_bind: ∀R. (∀L. reflexive … (R L)) →
 126                      ∀p,I,L1,L2,V,T. L1 ⪤*[R,ⓑ[p,I]V.T] L2 →
 127                      ∧∧ L1 ⪤*[R,V] L2 & L1.ⓑ[I]V ⪤*[R,T] L2.ⓑ[I]V.
 128 #R #HR #p #I #L1 #L2 #V #T #H elim H -L2
 129 [ #L2 #H elim (rex_inv_bind … V ? H) -H /3 width=1 by inj, conj/
 130 | #L #L2 #_ #H * elim (rex_inv_bind … V ? H) -H /3 width=3 by rexs_step_dx, conj/
 131 ]
 132 qed-.
 133
 134 lemma rexs_inv_flat: ∀R,I,L1,L2,V,T. L1 ⪤*[R,ⓕ[I]V.T] L2 →
 135                      ∧∧ L1 ⪤*[R,V] L2 & L1 ⪤*[R,T] L2.
 136 #R #I #L1 #L2 #V #T #H elim H -L2
 137 [ #L2 #H elim (rex_inv_flat … H) -H /3 width=1 by inj, conj/
 138 | #L #L2 #_ #H * elim (rex_inv_flat … H) -H /3 width=3 by rexs_step_dx, conj/
 139 ]
 140 qed-.
 141
 142 (* Advanced inversion lemmas ************************************************)
 143
 144 lemma rexs_inv_sort_bind_sn: ∀R,I1,Y2,L1,s. L1.ⓘ[I1] ⪤*[R,⋆s] Y2 →
 145                              ∃∃I2,L2. L1 ⪤*[R,⋆s] L2 & Y2 = L2.ⓘ[I2].
 146 #R #I1 #Y2 #L1 #s #H elim (rexs_inv_sort … H) -H *
 147 [ #H destruct
 148 | #Z #I2 #Y1 #L2 #Hs #H1 #H2 destruct /2 width=4 by ex2_2_intro/
 149 ]
 150 qed-.
 151
 152 lemma rexs_inv_sort_bind_dx: ∀R,I2,Y1,L2,s. Y1 ⪤*[R,⋆s] L2.ⓘ[I2] →
 153                              ∃∃I1,L1. L1 ⪤*[R,⋆s] L2 & Y1 = L1.ⓘ[I1].
 154 #R #I2 #Y1 #L2 #s #H elim (rexs_inv_sort … H) -H *
 155 [ #_ #H destruct
 156 | #I1 #Z #L1 #Y2 #Hs #H1 #H2 destruct /2 width=4 by ex2_2_intro/
 157 ]
 158 qed-.
 159
 160 lemma rexs_inv_gref_bind_sn: ∀R,I1,Y2,L1,l. L1.ⓘ[I1] ⪤*[R,§l] Y2 →
 161                              ∃∃I2,L2. L1 ⪤*[R,§l] L2 & Y2 = L2.ⓘ[I2].
 162 #R #I1 #Y2 #L1 #l #H elim (rexs_inv_gref … H) -H *
 163 [ #H destruct
 164 | #Z #I2 #Y1 #L2 #Hl #H1 #H2 destruct /2 width=4 by ex2_2_intro/
 165 ]
 166 qed-.
 167
 168 lemma rexs_inv_gref_bind_dx: ∀R,I2,Y1,L2,l. Y1 ⪤*[R,§l] L2.ⓘ[I2] →
 169                              ∃∃I1,L1. L1 ⪤*[R,§l] L2 & Y1 = L1.ⓘ[I1].
 170 #R #I2 #Y1 #L2 #l #H elim (rexs_inv_gref … H) -H *
 171 [ #_ #H destruct
 172 | #I1 #Z #L1 #Y2 #Hl #H1 #H2 destruct /2 width=4 by ex2_2_intro/
 173 ]
 174 qed-.
 175
 176 (* Basic forward lemmas *****************************************************)
 177
 178 lemma rexs_fwd_pair_sn: ∀R,I,L1,L2,V,T. L1 ⪤*[R,②[I]V.T] L2 → L1 ⪤*[R,V] L2.
 179 #R #I #L1 #L2 #V #T #H elim H -L2
 180 /3 width=5 by rex_fwd_pair_sn, rexs_step_dx, inj/
 181 qed-.
 182
 183 lemma rexs_fwd_bind_dx: ∀R. (∀L. reflexive … (R L)) →
 184                         ∀p,I,L1,L2,V,T. L1 ⪤*[R,ⓑ[p,I]V.T] L2 →
 185                         L1.ⓑ[I]V ⪤*[R,T] L2.ⓑ[I]V.
 186 #R #HR #p #I #L1 #L2 #V #T #H elim (rexs_inv_bind … H) -H //
 187 qed-.
 188
 189 lemma rexs_fwd_flat_dx: ∀R,I,L1,L2,V,T. L1 ⪤*[R,ⓕ[I]V.T] L2 → L1 ⪤*[R,T] L2.
 190 #R #I #L1 #L2 #V #T #H elim (rexs_inv_flat … H) -H //
 191 qed-.
 192
 193 (* Basic_2A1: removed theorems 2:
 194               TC_lpx_sn_inv_pair1 TC_lpx_sn_inv_pair2
 195 *)