matita/matita/contribs/lambdadelta/static_2/s_transition/fqu.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_2/xoa/and_4.ma".
  16 include "ground_2/xoa/ex_4_2.ma".
  17 include "ground_2/xoa/or_4.ma".
  18 include "static_2/notation/relations/supterm_6.ma".
  19 include "static_2/notation/relations/supterm_7.ma".
  20 include "static_2/syntax/lenv.ma".
  21 include "static_2/syntax/genv.ma".
  22 include "static_2/relocation/lifts.ma".
  23
  24 (* SUPCLOSURE ***************************************************************)
  25
  26 (* activate genv *)
  27 (* Note: frees_total requires fqu_drop for all atoms
  28          fqu_cpx_trans requires fqu_drop for all terms
  29          frees_fqus_drops requires fqu_drop restricted on atoms
  30 *)
  31 inductive fqu (b:bool): tri_relation genv lenv term ≝
  32 | fqu_lref_O : ∀I,G,L,V. fqu b G (L.ⓑ[I]V) (#0) G L V
  33 | fqu_pair_sn: ∀I,G,L,V,T. fqu b G L (②[I]V.T) G L V
  34 | fqu_bind_dx: ∀p,I,G,L,V,T. b = Ⓣ → fqu b G L (ⓑ[p,I]V.T) G (L.ⓑ[I]V) T
  35 | fqu_clear  : ∀p,I,G,L,V,T. b = Ⓕ → fqu b G L (ⓑ[p,I]V.T) G (L.ⓧ) T
  36 | fqu_flat_dx: ∀I,G,L,V,T. fqu b G L (ⓕ[I]V.T) G L T
  37 | fqu_drop   : ∀I,G,L,T,U. ⇧*[1] T ≘ U → fqu b G (L.ⓘ[I]) U G L T
  38 .
  39
  40 interpretation
  41    "extended structural successor (closure)"
  42    'SupTerm b G1 L1 T1 G2 L2 T2 = (fqu b G1 L1 T1 G2 L2 T2).
  43
  44 interpretation
  45    "structural successor (closure)"
  46    'SupTerm G1 L1 T1 G2 L2 T2 = (fqu true G1 L1 T1 G2 L2 T2).
  47
  48 (* Basic properties *********************************************************)
  49
  50 lemma fqu_sort: ∀b,I,G,L,s. ❪G,L.ⓘ[I],⋆s❫ ⬂[b] ❪G,L,⋆s❫.
  51 /2 width=1 by fqu_drop/ qed.
  52
  53 lemma fqu_lref_S: ∀b,I,G,L,i. ❪G,L.ⓘ[I],#↑i❫ ⬂[b] ❪G,L,#i❫.
  54 /2 width=1 by fqu_drop/ qed.
  55
  56 lemma fqu_gref: ∀b,I,G,L,l. ❪G,L.ⓘ[I],§l❫ ⬂[b] ❪G,L,§l❫.
  57 /2 width=1 by fqu_drop/ qed.
  58
  59 (* Basic inversion lemmas ***************************************************)
  60
  61 fact fqu_inv_sort1_aux: ∀b,G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂[b] ❪G2,L2,T2❫ →
  62                         ∀s. T1 = ⋆s →
  63                         ∃∃J. G1 = G2 & L1 = L2.ⓘ[J] & T2 = ⋆s.
  64 #b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
  65 [ #I #G #L #T #s #H destruct
  66 | #I #G #L #V #T #s #H destruct
  67 | #p #I #G #L #V #T #_ #s #H destruct
  68 | #p #I #G #L #V #T #_ #s #H destruct
  69 | #I #G #L #V #T #s #H destruct
  70 | #I #G #L #T #U #HI12 #s #H destruct
  71   lapply (lifts_inv_sort2 … HI12) -HI12 /2 width=2 by ex3_intro/
  72 ]
  73 qed-.
  74
  75 lemma fqu_inv_sort1: ∀b,G1,G2,L1,L2,T2,s. ❪G1,L1,⋆s❫ ⬂[b] ❪G2,L2,T2❫ →
  76                      ∃∃J. G1 = G2 & L1 = L2.ⓘ[J] & T2 = ⋆s.
  77 /2 width=4 by fqu_inv_sort1_aux/ qed-.
  78
  79 fact fqu_inv_lref1_aux: ∀b,G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂[b] ❪G2,L2,T2❫ →
  80                         ∀i. T1 = #i →
  81                         (∃∃J,V. G1 = G2 & L1 = L2.ⓑ[J]V & T2 = V & i = 0) ∨
  82                         ∃∃J,j. G1 = G2 & L1 = L2.ⓘ[J] & T2 = #j & i = ↑j.
  83 #b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
  84 [ #I #G #L #T #i #H destruct /3 width=4 by ex4_2_intro, or_introl/
  85 | #I #G #L #V #T #i #H destruct
  86 | #p #I #G #L #V #T #_ #i #H destruct
  87 | #p #I #G #L #V #T #_ #i #H destruct
  88 | #I #G #L #V #T #i #H destruct
  89 | #I #G #L #T #U #HI12 #i #H destruct
  90   elim (lifts_inv_lref2_uni … HI12) -HI12 /3 width=3 by ex4_2_intro, or_intror/
  91 ]
  92 qed-.
  93
  94 lemma fqu_inv_lref1: ∀b,G1,G2,L1,L2,T2,i. ❪G1,L1,#i❫ ⬂[b] ❪G2,L2,T2❫ →
  95                      (∃∃J,V. G1 = G2 & L1 = L2.ⓑ[J]V & T2 = V & i = 0) ∨
  96                      ∃∃J,j. G1 = G2 & L1 = L2.ⓘ[J] & T2 = #j & i = ↑j.
  97 /2 width=4 by fqu_inv_lref1_aux/ qed-.
  98
  99 fact fqu_inv_gref1_aux: ∀b,G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂[b] ❪G2,L2,T2❫ →
 100                         ∀l. T1 = §l →
 101                         ∃∃J. G1 = G2 & L1 = L2.ⓘ[J] & T2 = §l.
 102 #b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
 103 [ #I #G #L #T #l #H destruct
 104 | #I #G #L #V #T #l #H destruct
 105 | #p #I #G #L #V #T #_ #l #H destruct
 106 | #p #I #G #L #V #T #_ #l #H destruct
 107 | #I #G #L #V #T #s #H destruct
 108 | #I #G #L #T #U #HI12 #l #H destruct
 109   lapply (lifts_inv_gref2 … HI12) -HI12 /2 width=3 by ex3_intro/
 110 ]
 111 qed-.
 112
 113 lemma fqu_inv_gref1: ∀b,G1,G2,L1,L2,T2,l. ❪G1,L1,§l❫ ⬂[b] ❪G2,L2,T2❫ →
 114                      ∃∃J. G1 = G2 & L1 = L2.ⓘ[J] & T2 = §l.
 115 /2 width=4 by fqu_inv_gref1_aux/ qed-.
 116
 117 fact fqu_inv_bind1_aux: ∀b,G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂[b] ❪G2,L2,T2❫ →
 118                         ∀p,I,V1,U1. T1 = ⓑ[p,I]V1.U1 →
 119                         ∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2
 120                          | ∧∧ G1 = G2 & L1.ⓑ[I]V1 = L2 & U1 = T2 & b = Ⓣ
 121                          | ∧∧ G1 = G2 & L1.ⓧ = L2 & U1 = T2 & b = Ⓕ
 122                          | ∃∃J. G1 = G2 & L1 = L2.ⓘ[J] & ⇧*[1] T2 ≘ ⓑ[p,I]V1.U1.
 123 #b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
 124 [ #I #G #L #T #q #J #V0 #U0 #H destruct
 125 | #I #G #L #V #T #q #J #V0 #U0 #H destruct /3 width=1 by and3_intro, or4_intro0/
 126 | #p #I #G #L #V #T #Hb #q #J #V0 #U0 #H destruct /3 width=1 by and4_intro, or4_intro1/
 127 | #p #I #G #L #V #T #Hb #q #J #V0 #U0 #H destruct /3 width=1 by and4_intro, or4_intro2/
 128 | #I #G #L #V #T #q #J #V0 #U0 #H destruct
 129 | #I #G #L #T #U #HTU #q #J #V0 #U0 #H destruct /3 width=2 by or4_intro3, ex3_intro/
 130 ]
 131 qed-.
 132
 133 lemma fqu_inv_bind1: ∀b,p,I,G1,G2,L1,L2,V1,U1,T2. ❪G1,L1,ⓑ[p,I]V1.U1❫ ⬂[b] ❪G2,L2,T2❫ →
 134                      ∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2
 135                       | ∧∧ G1 = G2 & L1.ⓑ[I]V1 = L2 & U1 = T2 & b = Ⓣ
 136                       | ∧∧ G1 = G2 & L1.ⓧ = L2 & U1 = T2 & b = Ⓕ
 137                       | ∃∃J. G1 = G2 & L1 = L2.ⓘ[J] & ⇧*[1] T2 ≘ ⓑ[p,I]V1.U1.
 138 /2 width=4 by fqu_inv_bind1_aux/ qed-.
 139
 140 lemma fqu_inv_bind1_true: ∀p,I,G1,G2,L1,L2,V1,U1,T2. ❪G1,L1,ⓑ[p,I]V1.U1❫ ⬂ ❪G2,L2,T2❫ →
 141                           ∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2
 142                            | ∧∧ G1 = G2 & L1.ⓑ[I]V1 = L2 & U1 = T2
 143                            | ∃∃J. G1 = G2 & L1 = L2.ⓘ[J] & ⇧*[1] T2 ≘ ⓑ[p,I]V1.U1.
 144 #p #I #G1 #G2 #L1 #L2 #V1 #U1 #T2 #H elim (fqu_inv_bind1 … H) -H
 145 /3 width=1 by or3_intro0, or3_intro2/
 146 * #HG #HL #HU #H destruct
 147 /3 width=1 by and3_intro, or3_intro1/
 148 qed-.
 149
 150 fact fqu_inv_flat1_aux: ∀b,G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂[b] ❪G2,L2,T2❫ →
 151                         ∀I,V1,U1. T1 = ⓕ[I]V1.U1 →
 152                         ∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2
 153                          | ∧∧ G1 = G2 & L1 = L2 & U1 = T2
 154                          | ∃∃J. G1 = G2 & L1 = L2.ⓘ[J] & ⇧*[1] T2 ≘ ⓕ[I]V1.U1.
 155 #b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
 156 [ #I #G #L #T #J #V0 #U0 #H destruct
 157 | #I #G #L #V #T #J #V0 #U0 #H destruct /3 width=1 by and3_intro, or3_intro0/
 158 | #p #I #G #L #V #T #_ #J #V0 #U0 #H destruct
 159 | #p #I #G #L #V #T #_ #J #V0 #U0 #H destruct
 160 | #I #G #L #V #T #J #V0 #U0 #H destruct /3 width=1 by and3_intro, or3_intro1/
 161 | #I #G #L #T #U #HTU #J #V0 #U0 #H destruct /3 width=2 by or3_intro2, ex3_intro/
 162 ]
 163 qed-.
 164
 165 lemma fqu_inv_flat1: ∀b,I,G1,G2,L1,L2,V1,U1,T2. ❪G1,L1,ⓕ[I]V1.U1❫ ⬂[b] ❪G2,L2,T2❫ →
 166                      ∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2
 167                       | ∧∧ G1 = G2 & L1 = L2 & U1 = T2
 168                       | ∃∃J. G1 = G2 & L1 = L2.ⓘ[J] & ⇧*[1] T2 ≘ ⓕ[I]V1.U1.
 169 /2 width=4 by fqu_inv_flat1_aux/ qed-.
 170
 171 (* Advanced inversion lemmas ************************************************)
 172
 173 lemma fqu_inv_atom1: ∀b,I,G1,G2,L2,T2. ❪G1,⋆,⓪[I]❫ ⬂[b] ❪G2,L2,T2❫ → ⊥.
 174 #b * #x #G1 #G2 #L2 #T2 #H
 175 [ elim (fqu_inv_sort1 … H) | elim (fqu_inv_lref1 … H) * | elim (fqu_inv_gref1 … H) ] -H
 176 #I [2: #V |3: #i ] #_ #H destruct
 177 qed-.
 178
 179 lemma fqu_inv_sort1_bind: ∀b,I,G1,G2,K,L2,T2,s. ❪G1,K.ⓘ[I],⋆s❫ ⬂[b] ❪G2,L2,T2❫ →
 180                           ∧∧ G1 = G2 & L2 = K & T2 = ⋆s.
 181 #b #I #G1 #G2 #K #L2 #T2 #s #H elim (fqu_inv_sort1 … H) -H
 182 #Z #X #H1 #H2 destruct /2 width=1 by and3_intro/
 183 qed-.
 184
 185 lemma fqu_inv_zero1_pair: ∀b,I,G1,G2,K,L2,V,T2. ❪G1,K.ⓑ[I]V,#0❫ ⬂[b] ❪G2,L2,T2❫ →
 186                           ∧∧ G1 = G2 & L2 = K & T2 = V.
 187 #b #I #G1 #G2 #K #L2 #V #T2 #H elim (fqu_inv_lref1 … H) -H *
 188 #Z #X #H1 #H2 #H3 #H4 destruct /2 width=1 by and3_intro/
 189 qed-.
 190
 191 lemma fqu_inv_lref1_bind: ∀b,I,G1,G2,K,L2,T2,i. ❪G1,K.ⓘ[I],#(↑i)❫ ⬂[b] ❪G2,L2,T2❫ →
 192                           ∧∧ G1 = G2 & L2 = K & T2 = #i.
 193 #b #I #G1 #G2 #K #L2 #T2 #i #H elim (fqu_inv_lref1 … H) -H *
 194 #Z #X #H1 #H2 #H3 #H4 destruct /2 width=1 by and3_intro/
 195 qed-.
 196
 197 lemma fqu_inv_gref1_bind: ∀b,I,G1,G2,K,L2,T2,l. ❪G1,K.ⓘ[I],§l❫ ⬂[b] ❪G2,L2,T2❫ →
 198                           ∧∧ G1 = G2 & L2 = K & T2 = §l.
 199 #b #I #G1 #G2 #K #L2 #T2 #l #H elim (fqu_inv_gref1 … H) -H
 200 #Z #H1 #H2 #H3 destruct /2 width=1 by and3_intro/
 201 qed-.
 202
 203 (* Basic_2A1: removed theorems 3:
 204               fqu_drop fqu_drop_lt fqu_lref_S_lt
 205 *)