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 inductive fqu: tri_relation genv lenv term ≝
  25 | fqu_lref_O : ∀I,G,L,V. fqu G (L.ⓑ{I}V) (#0) G L V
  26 | fqu_pair_sn: ∀I,G,L,V,T. fqu G L (②{I}V.T) G L V
  27 | fqu_bind_dx: ∀p,I,G,L,V,T. fqu G L (ⓑ{p,I}V.T) G (L.ⓑ{I}V) T
  28 | fqu_flat_dx: ∀I,G,L,V,T. fqu G L (ⓕ{I}V.T) G L T
  29 | fqu_drop   : ∀I,I1,I2,G,L,V. ⬆*[1] ⓪{I2} ≡ ⓪{I1} →
  30                fqu G (L.ⓑ{I}V) (⓪{I1}) G L (⓪{I2})
  31 .
  32
  33 interpretation
  34    "structural successor (closure)"
  35    'SupTerm G1 L1 T1 G2 L2 T2 = (fqu G1 L1 T1 G2 L2 T2).
  36
  37 (* Basic properties *********************************************************)
  38
  39 lemma fqu_lref_S: ∀I,G,L,V,i. ⦃G, L.ⓑ{I}V, #(⫯i)⦄ ⊐ ⦃G, L, #(i)⦄.
  40 /2 width=1 by fqu_drop/ qed.
  41
  42 (* Basic inversion lemmas ***************************************************)
  43
  44 fact fqu_inv_atom1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
  45                         ∀I. L1 = ⋆ → T1 = ⓪{I} → ⊥.
  46 #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
  47 [ #I #G #L #T #J #H destruct
  48 | #I #G #L #V #T #J #_ #H destruct
  49 | #p #I #G #L #V #T #J #_ #H destruct
  50 | #I #G #L #V #T #J  #_ #H destruct
  51 | #I #I1 #I2 #G #L #V #_ #J #H destruct
  52 ]
  53 qed-.
  54
  55 lemma fqu_inv_atom1: ∀I,G1,G2,L2,T2. ⦃G1, ⋆, ⓪{I}⦄ ⊐ ⦃G2, L2, T2⦄ → ⊥.
  56 /2 width=10 by fqu_inv_atom1_aux/ qed-.
  57
  58 fact fqu_inv_sort1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
  59                         ∀I,K,V,s. L1 = K.ⓑ{I}V → T1 = ⋆s →
  60                         ∧∧ G1 = G2 & L2 = K & T2 = ⋆s.
  61 #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
  62 [ #I #G #L #T #J #K #W #s #_ #H destruct
  63 | #I #G #L #V #T #J #K #W #s #_ #H destruct
  64 | #p #I #G #L #V #T #J #K #W #s #_ #H destruct
  65 | #I #G #L #V #T #J #K #W #s #_ #H destruct
  66 | #I #I1 #I2 #G #L #V #HI12 #J #K #W #s #H1 #H2 destruct
  67   lapply (lifts_inv_sort2 … HI12) -HI12 /2 width=1 by and3_intro/
  68 ]
  69 qed-.
  70
  71 lemma fqu_inv_sort1: ∀I,G1,G2,K,L2,V,T2,s. ⦃G1, K.ⓑ{I}V, ⋆s⦄ ⊐ ⦃G2, L2, T2⦄ →
  72                      ∧∧ G1 = G2 & L2 = K & T2 = ⋆s.
  73 /2 width=7 by fqu_inv_sort1_aux/ qed-.
  74
  75 fact fqu_inv_zero1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
  76                         ∀I,K,V. L1 = K.ⓑ{I}V → T1 = #0 →
  77                         ∧∧ G1 = G2 & L2 = K & T2 = V.
  78 #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
  79 [ #I #G #L #T #J #K #W #H1 #H2 destruct /2 width=1 by and3_intro/
  80 | #I #G #L #V #T #J #K #W #_ #H destruct
  81 | #p #I #G #L #V #T #J #K #W #_ #H destruct
  82 | #I #G #L #V #T #J #K #W #_ #H destruct
  83 | #I #I1 #I2 #G #L #V #HI12 #J #K #W #H1 #H2 destruct
  84   elim (lifts_inv_lref2_uni_lt … HI12) -HI12 //
  85 ]
  86 qed-.
  87
  88 lemma fqu_inv_zero1: ∀I,G1,G2,K,L2,V,T2. ⦃G1, K.ⓑ{I}V, #0⦄ ⊐ ⦃G2, L2, T2⦄ →
  89                      ∧∧ G1 = G2 & L2 = K & T2 = V.
  90 /2 width=9 by fqu_inv_zero1_aux/ qed-.
  91
  92 fact fqu_inv_lref1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
  93                         ∀I,K,V,i. L1 = K.ⓑ{I}V → T1 = #(⫯i) →
  94                         ∧∧ G1 = G2 & L2 = K & T2 = #i.
  95 #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
  96 [ #I #G #L #T #J #K #W #i #_ #H destruct
  97 | #I #G #L #V #T #J #K #W #i #_ #H destruct
  98 | #p #I #G #L #V #T #J #K #W #i #_ #H destruct
  99 | #I #G #L #V #T #J #K #W #i #_ #H destruct
 100 | #I #I1 #I2 #G #L #V #HI12 #J #K #W #i #H1 #H2 destruct
 101   lapply (lifts_inv_lref2_uni_ge … HI12) -HI12 /2 width=1 by and3_intro/
 102 ]
 103 qed-.
 104
 105 lemma fqu_inv_lref1: ∀I,G1,G2,K,L2,V,T2,i. ⦃G1, K.ⓑ{I}V, #(⫯i)⦄ ⊐ ⦃G2, L2, T2⦄ →
 106                      ∧∧ G1 = G2 & L2 = K & T2 = #i.
 107 /2 width=9 by fqu_inv_lref1_aux/ qed-.
 108
 109 fact fqu_inv_gref1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
 110                         ∀I,K,V,l. L1 = K.ⓑ{I}V → T1 = §l →
 111                         ∧∧ G1 = G2 & L2 = K & T2 = §l.
 112 #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
 113 [ #I #G #L #T #J #K #W #l #_ #H destruct
 114 | #I #G #L #V #T #J #K #W #l #_ #H destruct
 115 | #p #I #G #L #V #T #J #K #W #l #_ #H destruct
 116 | #I #G #L #V #T #J #K #W #l #_ #H destruct
 117 | #I #I1 #I2 #G #L #V #HI12 #J #K #W #l #H1 #H2 destruct
 118   lapply (lifts_inv_gref2 … HI12) -HI12 /2 width=1 by and3_intro/
 119 ]
 120 qed-.
 121
 122 lemma fqu_inv_gref1: ∀I,G1,G2,K,L2,V,T2,l. ⦃G1, K.ⓑ{I}V, §l⦄ ⊐ ⦃G2, L2, T2⦄ →
 123                      ∧∧ G1 = G2 & L2 = K & T2 = §l.
 124 /2 width=7 by fqu_inv_gref1_aux/ qed-.
 125
 126 fact fqu_inv_bind1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
 127                         ∀p,I,V1,U1. T1 = ⓑ{p,I}V1.U1 →
 128                         (∧∧ G1 = G2 & L1 = L2 & V1 = T2) ∨
 129                         (∧∧ G1 = G2 & L1.ⓑ{I}V1 = L2 & U1 = T2).
 130 #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
 131 [ #I #G #L #T #q #J #W #U #H destruct
 132 | #I #G #L #V #T #q #J #W #U #H destruct /3 width=1 by and3_intro, or_introl/
 133 | #p #I #G #L #V #T #q #J #W #U #H destruct /3 width=1 by and3_intro, or_intror/
 134 | #I #G #L #V #T #q #J #W #U #H destruct
 135 | #I #I1 #I2 #G #L #V #_ #q #J #W #U #H destruct
 136 ]
 137 qed-.
 138
 139 lemma fqu_inv_bind1: ∀p,I,G1,G2,L1,L2,V1,U1,T2. ⦃G1, L1, ⓑ{p,I}V1.U1⦄ ⊐ ⦃G2, L2, T2⦄ →
 140                      (∧∧ G1 = G2 & L1 = L2 & V1 = T2) ∨
 141                      (∧∧ G1 = G2 & L1.ⓑ{I}V1 = L2 & U1 = T2).
 142 /2 width=4 by fqu_inv_bind1_aux/ qed-.
 143
 144 fact fqu_inv_flat1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
 145                         ∀I,V1,U1. T1 = ⓕ{I}V1.U1 →
 146                         (∧∧ G1 = G2 & L1 = L2 & V1 = T2) ∨
 147                         (∧∧ G1 = G2 & L1 = L2 & U1 = T2).
 148 #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
 149 [ #I #G #L #T #J #W #U #H destruct
 150 | #I #G #L #V #T #J #W #U #H destruct /3 width=1 by and3_intro, or_introl/
 151 | #p #I #G #L #V #T #J #W #U #H destruct
 152 | #I #G #L #V #T #J #W #U #H destruct /3 width=1 by and3_intro, or_intror/
 153 | #I #I1 #I2 #G #L #V #_ #J #W #U #H destruct
 154 ]
 155 qed-.
 156
 157 lemma fqu_inv_flat1: ∀I,G1,G2,L1,L2,V1,U1,T2. ⦃G1, L1, ⓕ{I}V1.U1⦄ ⊐ ⦃G2, L2, T2⦄ →
 158                      (∧∧ G1 = G2 & L1 = L2 & V1 = T2) ∨
 159                      (∧∧ G1 = G2 & L1 = L2 & U1 = T2).
 160 /2 width=4 by fqu_inv_flat1_aux/ qed-.
 161
 162 (* Basic_2A1: removed theorems 3:
 163               fqu_drop fqu_drop_lt fqu_lref_S_lt
 164 *)