matita/matita/contribs/lambda_delta/basic_2/etc/csup/csup.etc

   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 notation "hvbox( ⦃ L1, break T1 ⦄ > break ⦃ L2 , break T2 ⦄ )"
  16    non associative with precedence 45
  17    for @{ 'SupTerm $L1 $T1 $L2 $T2 }.
  18
  19 include "basic_2/substitution/ldrop.ma".
  20
  21 (* SUPCLOSURE ***************************************************************)
  22
  23 inductive csup: bi_relation lenv term ≝
  24 | csup_lref   : ∀I,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → csup L (#i) K V
  25 | csup_bind_sn: ∀a,I,L,V,T. csup L (ⓑ{a,I}V.T) L V
  26 | csup_bind_dx: ∀a,I,L,V,T. csup L (ⓑ{a,I}V.T) (L.ⓑ{I}V) T
  27 | csup_flat_sn: ∀I,L,V,T.   csup L (ⓕ{I}V.T) L V
  28 | csup_flat_dx: ∀I,L,V,T.   csup L (ⓕ{I}V.T) L T
  29 .
  30
  31 interpretation
  32    "structural predecessor (closure)"
  33    'SupTerm L1 T1 L2 T2 = (csup L1 T1 L2 T2).
  34
  35 (* Basic inversion lemmas ***************************************************)
  36
  37 fact csup_inv_atom1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ → ∀J. T1 = ⓪{J} →
  38                          ∃∃I,i. ⇩[0, i] L1 ≡ L2.ⓑ{I}T2 & J = LRef i.
  39 #L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2
  40 [ #I #L #K #V #i #HLK #J #H destruct /2 width=4/
  41 | #a #I #L #V #T #J #H destruct
  42 | #a #I #L #V #T #J #H destruct
  43 | #I #L #V #T #J #H destruct
  44 | #I #L #V #T #J #H destruct
  45 ]
  46 qed-.
  47
  48 lemma csup_inv_atom1: ∀J,L1,L2,T2. ⦃L1, ⓪{J}⦄ > ⦃L2, T2⦄ →
  49                       ∃∃I,i. ⇩[0, i] L1 ≡ L2.ⓑ{I}T2 & J = LRef i.
  50 /2 width=3 by csup_inv_atom1_aux/ qed-.
  51
  52 fact csup_inv_bind1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ →
  53                          ∀b,J,W,U. T1 = ⓑ{b,J}W.U →
  54                          (L2 = L1 ∧ T2 = W) ∨
  55                          (L2 = L1.ⓑ{J}W ∧ T2 = U).
  56 #L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2
  57 [ #I #L #K #V #i #_ #b #J #W #U #H destruct
  58 | #a #I #L #V #T #b #J #W #U #H destruct /3 width=1/
  59 | #a #I #L #V #T #b #J #W #U #H destruct /3 width=1/
  60 | #I #L #V #T #b #J #W #U #H destruct
  61 | #I #L #V #T #b #J #W #U #H destruct
  62 ]
  63 qed-.
  64
  65 lemma csup_inv_bind1: ∀b,J,L1,L2,W,U,T2. ⦃L1, ⓑ{b,J}W.U⦄ > ⦃L2, T2⦄ →
  66                       (L2 = L1 ∧ T2 = W) ∨
  67                       (L2 = L1.ⓑ{J}W ∧ T2 = U).
  68 /2 width=4 by csup_inv_bind1_aux/ qed-.
  69
  70 fact csup_inv_flat1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ →
  71                          ∀J,W,U. T1 = ⓕ{J}W.U →
  72                          L2 = L1 ∧ (T2 = W ∨ T2 = U).
  73 #L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2
  74 [ #I #L #K #V #i #_ #J #W #U #H destruct
  75 | #a #I #L #V #T #J #W #U #H destruct
  76 | #a #I #L #V #T #J #W #U #H destruct
  77 | #I #L #V #T #J #W #U #H destruct /3 width=1/
  78 | #I #L #V #T #J #W #U #H destruct /3 width=1/
  79 ]
  80 qed-.
  81
  82 lemma csup_inv_flat1: ∀J,L1,L2,W,U,T2. ⦃L1, ⓕ{J}W.U⦄ > ⦃L2, T2⦄ →
  83                       L2 = L1 ∧ (T2 = W ∨ T2 = U).
  84 /2 width=4 by csup_inv_flat1_aux/ qed-.
  85
  86 (* Basic forward lemmas *****************************************************)
  87
  88 lemma csup_fwd_cw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ → #{L2, T2} < #{L1, T1}.
  89 #L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 /width=1/ /2 width=4 by ldrop_pair2_fwd_cw/
  90 qed-.
  91
  92 lemma csup_fwd_ldrop: ∀L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ →
  93                       ∃i. ⇩[0, i] L1 ≡ L2 ∨ ⇩[0, i] L2 ≡ L1.
  94 #L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 /3 width=2/ /4 width=2/
  95 #I #L1 #K1 #V1 #i #HLK1
  96 lapply (ldrop_fwd_ldrop2 … HLK1) -HLK1 /3 width=2/
  97 qed-.
  98
  99 (* Advanced forward lemmas **************************************************)
 100
 101 lemma lift_csup_trans_eq: ∀T1,U1,d,e. ⇧[d, e] T1 ≡ U1 →
 102                           ∀L,U2. ⦃L, U1⦄ > ⦃L, U2⦄ →
 103                           ∃T2. ⇧[d, e] T2 ≡ U2.
 104 #T1 #U1 #d #e * -T1 -U1 -d -e
 105 [5: #a #I #V1 #W1 #T1 #U1 #d #e #HVW1 #_ #L #X #H
 106     elim (csup_inv_bind1 … H) -H *
 107     [ #_ #H destruct /2 width=2/
 108     | #H elim (discr_lpair_x_xy … H)
 109     ]
 110 |6: #I #V1 #W1 #T1 #U1 #d #e #HVW1 #HUT1 #L #X #H
 111     elim (csup_inv_flat1 … H) -H #_ * #H destruct /2 width=2/
 112 ]
 113 #i #d #e [2,3: #_ ] #L #X #H
 114 elim (csup_inv_atom1 … H) -H #I #j #HL #H destruct
 115 lapply (ldrop_pair2_fwd_cw … HL X) -HL #H
 116 elim (lt_refl_false … H)
 117 qed-.
 118 (*
 119 lemma lift_csup_trans_gt: ∀L1,L2,U1,U2. ⦃L1, U1⦄ > ⦃L2, U2⦄ →
 120                           ⇩[0, 1] L2 ≡ L1 → ∀T1,d,e. ⇧[d, e] T1 ≡ U1 →
 121                           ∃T2. ⇧[d + 1, e] T2 ≡ U2.
 122 #L1 #L2 #U1 #U2 * -L1 -L2 -U1 -U2
 123 [ #I #L1 #K1 #V #i #HLK1 #HKL1
 124   lapply (ldrop_fwd_lw … HLK1) -HLK1 #HLK1
 125   lapply (ldrop_fwd_lw … HKL1) -HKL1 #HKL1
 126   lapply (transitive_le … HLK1 HKL1) -L1 normalize #H
 127
 128
 129 | #a
 130 | #a
 131 ]
 132 #I #L1 #W1 #U1 #HL1
 133
 134
 135
 136  #X #d #e #H
 137   lapply (ldrop_inv_refl … HL1) -HL1
 138 | #a #I #L1 #W1 #U1 #j #HL1 #X #d #e #H
 139   lapply (ldrop_inv_ldrop1 … HL1)
 140
 141   elim (lift_inv_bind2 … H) -H #W2 #U2 #HW21 #HU21 #H destruct
 142
 143
 144  /3 width=2/ /4 width=2/
 145
 146 *)
 147
 148
 149
 150 (* Advanced inversion lemmas ************************************************)
 151
 152 lemma csup_inv_lref2_be: ∀L,U,i. ⦃L, U⦄ > ⦃L, #i⦄ →
 153                          ∀T,d,e. ⇧[d, e] T ≡ U → d ≤ i → i < d + e → ⊥.
 154 #L #U #i #H #T #d #e #HTU #Hdi #Hide
 155 elim (lift_csup_trans_eq … HTU … H) -H -T #T #H
 156 elim (lift_inv_lref2_be … H ? ?) //
 157 qed-.