matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs.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 "basic_2/notation/relations/relationstarstar_4.ma".
  16 include "basic_2/static/lfxs.ma".
  17
  18 (* ITERATED EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ***)
  19
  20 definition tc_lfxs (R): term → relation lenv ≝ LTC … (lfxs R).
  21
  22 interpretation "iterated extension on referred entries (local environment)"
  23    'RelationStarStar R T L1 L2 = (tc_lfxs R T L1 L2).
  24
  25 (* Basic properties *********************************************************)
  26
  27 lemma tc_lfxs_step_dx: ∀R,L1,L,T. L1 ⦻**[R, T] L →
  28                        ∀L2. L ⦻*[R, T] L2 → L1 ⦻**[R, T] L2.
  29 #R #L1 #L2 #T #HL1 #L2 @step @HL1 (**) (* auto fails *)
  30 qed-.
  31
  32 lemma tc_lfxs_step_sn: ∀R,L1,L,T. L1 ⦻*[R, T] L →
  33                        ∀L2. L ⦻**[R, T] L2 → L1 ⦻**[R, T] L2.
  34 #R #L1 #L2 #T #HL1 #L2 @TC_strap @HL1 (**) (* auto fails *)
  35 qed-.
  36
  37 lemma tc_lfxs_atom: ∀R,I. ⋆ ⦻**[R, ⓪{I}] ⋆.
  38 /2 width=1 by inj/ qed.
  39
  40 lemma tc_lfxs_sort: ∀R,I,L1,L2,V1,V2,s.
  41                     L1 ⦻**[R, ⋆s] L2 → L1.ⓑ{I}V1 ⦻**[R, ⋆s] L2.ⓑ{I}V2.
  42 #R #I #L1 #L2 #V1 #V2 #s #H elim H -L2
  43 /3 width=4 by lfxs_sort, tc_lfxs_step_dx, inj/
  44 qed.
  45
  46 lemma tc_lfxs_zero: ∀R. (∀L. reflexive … (R L)) →
  47                     ∀I,L1,L2,V. L1 ⦻**[R, V] L2 →
  48                     L1.ⓑ{I}V ⦻**[R, #0] L2.ⓑ{I}V.
  49 #R #HR #I #L1 #L2 #V #H elim H -L2
  50 /3 width=5 by lfxs_zero, tc_lfxs_step_dx, inj/
  51 qed.
  52
  53 lemma tc_lfxs_lref: ∀R,I,L1,L2,V1,V2,i.
  54                     L1 ⦻**[R, #i] L2 → L1.ⓑ{I}V1 ⦻**[R, #⫯i] L2.ⓑ{I}V2.
  55 #R #I #L1 #L2 #V1 #V2 #i #H elim H -L2
  56 /3 width=4 by lfxs_lref, tc_lfxs_step_dx, inj/
  57 qed.
  58
  59 lemma tc_lfxs_gref: ∀R,I,L1,L2,V1,V2,l.
  60                     L1 ⦻**[R, §l] L2 → L1.ⓑ{I}V1 ⦻**[R, §l] L2.ⓑ{I}V2.
  61 #R #I #L1 #L2 #V1 #V2 #l #H elim H -L2
  62 /3 width=4 by lfxs_gref, tc_lfxs_step_dx, inj/
  63 qed.
  64
  65 lemma tc_lfxs_sym: ∀R. lexs_frees_confluent R cfull →
  66                    (∀L1,L2,T1,T2. R L1 T1 T2 → R L2 T2 T1) →
  67                    ∀T. symmetric … (tc_lfxs R T).
  68 #R #H1R #H2R #T #L1 #L2 #H elim H -L2
  69 /4 width=3 by lfxs_sym, tc_lfxs_step_sn, inj/
  70 qed-.
  71
  72 lemma tc_lfxs_co: ∀R1,R2. (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) →
  73                   ∀L1,L2,T. L1 ⦻**[R1, T] L2 → L1 ⦻**[R2, T] L2.
  74 #R1 #R2 #HR #L1 #L2 #T #H elim H -L2
  75 /4 width=5 by lfxs_co, tc_lfxs_step_dx, inj/
  76 qed-.
  77
  78 (* Basic inversion lemmas ***************************************************)
  79
  80 (* Basic_2A1: uses: TC_lpx_sn_inv_atom1 *)
  81 lemma tc_lfxs_inv_atom_sn: ∀R,I,Y2. ⋆ ⦻**[R, ⓪{I}] Y2 → Y2 = ⋆.
  82 #R #I #Y2 #H elim H -Y2 /3 width=3 by inj, lfxs_inv_atom_sn/
  83 qed-.
  84
  85 (* Basic_2A1: uses: TC_lpx_sn_inv_atom2 *)
  86 lemma tc_lfxs_inv_atom_dx: ∀R,I,Y1. Y1 ⦻**[R, ⓪{I}] ⋆ → Y1 = ⋆.
  87 #R #I #Y1 #H @(TC_ind_dx ??????? H) -Y1
  88 /3 width=3 by inj, lfxs_inv_atom_dx/
  89 qed-.
  90
  91 lemma tc_lfxs_inv_sort: ∀R,Y1,Y2,s. Y1 ⦻**[R, ⋆s] Y2 →
  92                         (Y1 = ⋆ ∧ Y2 = ⋆) ∨
  93                         ∃∃I,L1,L2,V1,V2. L1 ⦻**[R, ⋆s] L2 &
  94                                          Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2.
  95 #R #Y1 #Y2 #s #H elim H -Y2
  96 [ #Y2 #H elim (lfxs_inv_sort … H) -H *
  97   /4 width=8 by ex3_5_intro, inj, or_introl, or_intror, conj/
  98 | #Y #Y2 #_ #H elim (lfxs_inv_sort … H) -H *
  99   [ #H #H2 * * /3 width=8 by ex3_5_intro, or_introl, or_intror, conj/
 100   | #I #L #L2 #V #V2 #HL2 #H #H2 * *
 101     [ #H1 #H0 destruct
 102     | #I0 #L1 #L0 #V1 #V0 #HL10 #H1 #H0 destruct
 103       /4 width=8 by ex3_5_intro, tc_lfxs_step_dx, or_intror/
 104     ]
 105   ]
 106 ]
 107 qed-.
 108
 109 lemma tc_lfxs_inv_gref: ∀R,Y1,Y2,l. Y1 ⦻**[R, §l] Y2 →
 110                         (Y1 = ⋆ ∧ Y2 = ⋆) ∨
 111                         ∃∃I,L1,L2,V1,V2. L1 ⦻**[R, §l] L2 &
 112                                          Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2.
 113 #R #Y1 #Y2 #l #H elim H -Y2
 114 [ #Y2 #H elim (lfxs_inv_gref … H) -H *
 115   /4 width=8 by ex3_5_intro, inj, or_introl, or_intror, conj/
 116 | #Y #Y2 #_ #H elim (lfxs_inv_gref … H) -H *
 117   [ #H #H2 * * /3 width=8 by ex3_5_intro, or_introl, or_intror, conj/
 118   | #I #L #L2 #V #V2 #HL2 #H #H2 * *
 119     [ #H1 #H0 destruct
 120     | #I0 #L1 #L0 #V1 #V0 #HL10 #H1 #H0 destruct
 121       /4 width=8 by ex3_5_intro, tc_lfxs_step_dx, or_intror/
 122     ]
 123   ]
 124 ]
 125 qed-.
 126
 127 lemma tc_lfxs_inv_bind: ∀R. (∀L. reflexive … (R L)) →
 128                         ∀p,I,L1,L2,V,T. L1 ⦻**[R, ⓑ{p,I}V.T] L2 →
 129                         L1 ⦻**[R, V] L2 ∧ L1.ⓑ{I}V ⦻**[R, T] L2.ⓑ{I}V.
 130 #R #HR #p #I #L1 #L2 #V #T #H elim H -L2
 131 [ #L2 #H elim (lfxs_inv_bind … V ? H) -H /3 width=1 by inj, conj/
 132 | #L #L2 #_ #H * elim (lfxs_inv_bind … V ? H) -H /3 width=3 by tc_lfxs_step_dx, conj/
 133 ]
 134 qed-.
 135
 136 lemma tc_lfxs_inv_flat: ∀R,I,L1,L2,V,T. L1 ⦻**[R, ⓕ{I}V.T] L2 →
 137                         L1 ⦻**[R, V] L2 ∧ L1 ⦻**[R, T] L2.
 138 #R #I #L1 #L2 #V #T #H elim H -L2
 139 [ #L2 #H elim (lfxs_inv_flat … H) -H /3 width=1 by inj, conj/
 140 | #L #L2 #_ #H * elim (lfxs_inv_flat … H) -H /3 width=3 by tc_lfxs_step_dx, conj/
 141 ]
 142 qed-.
 143
 144 (* Advanced inversion lemmas ************************************************)
 145
 146 lemma tc_lfxs_inv_sort_pair_sn: ∀R,I,Y2,L1,V1,s. L1.ⓑ{I}V1 ⦻**[R, ⋆s] Y2 →
 147                                 ∃∃L2,V2. L1 ⦻**[R, ⋆s] L2 & Y2 = L2.ⓑ{I}V2.
 148 #R #I #Y2 #L1 #V1 #s #H elim (tc_lfxs_inv_sort … H) -H *
 149 [ #H destruct
 150 | #J #Y1 #L2 #X1 #V2 #Hs #H1 #H2 destruct /2 width=4 by ex2_2_intro/
 151 ]
 152 qed-.
 153
 154 lemma tc_lfxs_inv_sort_pair_dx: ∀R,I,Y1,L2,V2,s. Y1 ⦻**[R, ⋆s] L2.ⓑ{I}V2 →
 155                                 ∃∃L1,V1. L1 ⦻**[R, ⋆s] L2 & Y1 = L1.ⓑ{I}V1.
 156 #R #I #Y1 #L2 #V2 #s #H elim (tc_lfxs_inv_sort … H) -H *
 157 [ #_ #H destruct
 158 | #J #L1 #Y2 #V1 #X2 #Hs #H1 #H2 destruct /2 width=4 by ex2_2_intro/
 159 ]
 160 qed-.
 161
 162 lemma tc_lfxs_inv_gref_pair_sn: ∀R,I,Y2,L1,V1,l. L1.ⓑ{I}V1 ⦻**[R, §l] Y2 →
 163                                 ∃∃L2,V2. L1 ⦻**[R, §l] L2 & Y2 = L2.ⓑ{I}V2.
 164 #R #I #Y2 #L1 #V1 #l #H elim (tc_lfxs_inv_gref … H) -H *
 165 [ #H destruct
 166 | #J #Y1 #L2 #X1 #V2 #Hl #H1 #H2 destruct /2 width=4 by ex2_2_intro/
 167 ]
 168 qed-.
 169
 170 lemma tc_lfxs_inv_gref_pair_dx: ∀R,I,Y1,L2,V2,l. Y1 ⦻**[R, §l] L2.ⓑ{I}V2 →
 171                                 ∃∃L1,V1. L1 ⦻**[R, §l] L2 & Y1 = L1.ⓑ{I}V1.
 172 #R #I #Y1 #L2 #V2 #l #H elim (tc_lfxs_inv_gref … H) -H *
 173 [ #_ #H destruct
 174 | #J #L1 #Y2 #V1 #X2 #Hl #H1 #H2 destruct /2 width=4 by ex2_2_intro/
 175 ]
 176 qed-.
 177
 178 (* Basic forward lemmas *****************************************************)
 179
 180 lemma tc_lfxs_fwd_pair_sn: ∀R,I,L1,L2,V,T. L1 ⦻**[R, ②{I}V.T] L2 → L1 ⦻**[R, V] L2.
 181 #R #I #L1 #L2 #V #T #H elim H -L2
 182 /3 width=5 by lfxs_fwd_pair_sn, tc_lfxs_step_dx, inj/
 183 qed-.
 184
 185 lemma tc_lfxs_fwd_bind_dx: ∀R. (∀L. reflexive … (R L)) →
 186                            ∀p,I,L1,L2,V,T. L1 ⦻**[R, ⓑ{p,I}V.T] L2 →
 187                            L1.ⓑ{I}V ⦻**[R, T] L2.ⓑ{I}V.
 188 #R #HR #p #I #L1 #L2 #V #T #H elim (tc_lfxs_inv_bind … H) -H //
 189 qed-.
 190
 191 lemma tc_lfxs_fwd_flat_dx: ∀R,I,L1,L2,V,T. L1 ⦻**[R, ⓕ{I}V.T] L2 → L1 ⦻**[R, T] L2.
 192 #R #I #L1 #L2 #V #T #H elim (tc_lfxs_inv_flat … H) -H //
 193 qed-.
 194
 195 (* Basic_2A1: removed theorems 2:
 196               TC_lpx_sn_inv_pair1 TC_lpx_sn_inv_pair2
 197 *)