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