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