matita/matita/contribs/lambdadelta/basic_2/reduction/crx.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/reducible_4.ma".
  16 include "basic_2/static/sd.ma".
  17 include "basic_2/reduction/crr.ma".
  18
  19 (* CONTEXT-SENSITIVE EXTENDED REDUCIBLE TERMS *******************************)
  20
  21 (* extended reducible terms *)
  22 inductive crx (h) (g): lenv → predicate term ≝
  23 | crx_sort   : ∀L,k,l. deg h g k (l+1) → crx h g L (⋆k)
  24 | crx_delta  : ∀I,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → crx h g L (#i)
  25 | crx_appl_sn: ∀L,V,T. crx h g L V → crx h g L (ⓐV.T)
  26 | crx_appl_dx: ∀L,V,T. crx h g L T → crx h g L (ⓐV.T)
  27 | crx_ri2    : ∀I,L,V,T. ri2 I → crx h g L (②{I}V.T)
  28 | crx_ib2_sn : ∀a,I,L,V,T. ib2 a I → crx h g L V → crx h g L (ⓑ{a,I}V.T)
  29 | crx_ib2_dx : ∀a,I,L,V,T. ib2 a I → crx h g (L.ⓑ{I}V) T → crx h g L (ⓑ{a,I}V.T)
  30 | crx_beta   : ∀a,L,V,W,T. crx h g L (ⓐV. ⓛ{a}W.T)
  31 | crx_theta  : ∀a,L,V,W,T. crx h g L (ⓐV. ⓓ{a}W.T)
  32 .
  33
  34 interpretation
  35    "context-sensitive extended reducibility (term)"
  36    'Reducible h g L T = (crx h g L T).
  37
  38 (* Basic properties *********************************************************)
  39
  40 lemma crr_crx: ∀h,g,L,T. L ⊢ 𝐑⦃T⦄ → ⦃h, L⦄ ⊢ 𝐑[g]⦃T⦄.
  41 #h #g #L #T #H elim H -L -T // /2 width=1/ /2 width=4/
  42 qed.
  43
  44 (* Basic inversion lemmas ***************************************************)
  45
  46 fact crx_inv_sort_aux: ∀h,g,L,T,k. ⦃h, L⦄ ⊢ 𝐑[g]⦃T⦄ → T = ⋆k →
  47                        ∃l. deg h g k (l+1).
  48 #h #g #L #T #k0 * -L -T
  49 [ #L #k #l #Hkl #H destruct /2 width=2/
  50 | #I #L #K #V #i #HLK #H destruct
  51 | #L #V #T #_ #H destruct
  52 | #L #V #T #_ #H destruct
  53 | #I #L #V #T #_ #H destruct
  54 | #a #I #L #V #T #_ #_ #H destruct
  55 | #a #I #L #V #T #_ #_ #H destruct
  56 | #a #L #V #W #T #H destruct
  57 | #a #L #V #W #T #H destruct
  58 ]
  59 qed-.
  60
  61 lemma crx_inv_sort: ∀h,g,L,k. ⦃h, L⦄ ⊢ 𝐑[g]⦃⋆k⦄ → ∃l. deg h g k (l+1).
  62 /2 width=4 by crx_inv_sort_aux/ qed-.
  63
  64 fact crx_inv_lref_aux: ∀h,g,L,T,i. ⦃h, L⦄ ⊢ 𝐑[g]⦃T⦄ → T = #i →
  65                        ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V.
  66 #h #g #L #T #j * -L -T
  67 [ #L #k #l #_ #H destruct
  68 | #I #L #K #V #i #HLK #H destruct /2 width=4/
  69 | #L #V #T #_ #H destruct
  70 | #L #V #T #_ #H destruct
  71 | #I #L #V #T #_ #H destruct
  72 | #a #I #L #V #T #_ #_ #H destruct
  73 | #a #I #L #V #T #_ #_ #H destruct
  74 | #a #L #V #W #T #H destruct
  75 | #a #L #V #W #T #H destruct
  76 ]
  77 qed-.
  78
  79 lemma crx_inv_lref: ∀h,g,L,i. ⦃h, L⦄ ⊢ 𝐑[g]⦃#i⦄ → ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V.
  80 /2 width=5 by crx_inv_lref_aux/ qed-.
  81
  82 fact crx_inv_gref_aux: ∀h,g,L,T,p. ⦃h, L⦄ ⊢ 𝐑[g]⦃T⦄ → T = §p → ⊥.
  83 #h #g #L #T #q * -L -T
  84 [ #L #k #l #_ #H destruct
  85 | #I #L #K #V #i #HLK #H destruct
  86 | #L #V #T #_ #H destruct
  87 | #L #V #T #_ #H destruct
  88 | #I #L #V #T #_ #H destruct
  89 | #a #I #L #V #T #_ #_ #H destruct
  90 | #a #I #L #V #T #_ #_ #H destruct
  91 | #a #L #V #W #T #H destruct
  92 | #a #L #V #W #T #H destruct
  93 ]
  94 qed-.
  95
  96 lemma crx_inv_gref: ∀h,g,L,p. ⦃h, L⦄ ⊢ 𝐑[g]⦃§p⦄ → ⊥.
  97 /2 width=7 by crx_inv_gref_aux/ qed-.
  98
  99 lemma trx_inv_atom: ∀h,g,I. ⦃h, ⋆⦄ ⊢ 𝐑[g]⦃⓪{I}⦄ →
 100                     ∃∃k,l. deg h g k (l+1) & I = Sort k.
 101 #h #g * #i #H
 102 [ elim (crx_inv_sort … H) -H /2 width=4/
 103 | elim (crx_inv_lref … H) -H #I #L #V #H
 104   elim (ldrop_inv_atom1 … H) -H #H destruct
 105 | elim (crx_inv_gref … H)
 106 ]
 107 qed-.
 108
 109 fact crx_inv_ib2_aux: ∀h,g,a,I,L,W,U,T. ib2 a I → ⦃h, L⦄ ⊢ 𝐑[g]⦃T⦄ →
 110                       T = ⓑ{a,I}W.U → ⦃h, L⦄ ⊢ 𝐑[g]⦃W⦄ ∨ ⦃h, L.ⓑ{I}W⦄ ⊢ 𝐑[g]⦃U⦄.
 111 #h #g #b #J #L #W0 #U #T #HI * -L -T
 112 [ #L #k #l #_ #H destruct
 113 | #I #L #K #V #i #_ #H destruct
 114 | #L #V #T #_ #H destruct
 115 | #L #V #T #_ #H destruct
 116 | #I #L #V #T #H1 #H2 destruct
 117   elim H1 -H1 #H destruct
 118   elim HI -HI #H destruct
 119 | #a #I #L #V #T #_ #HV #H destruct /2 width=1/
 120 | #a #I #L #V #T #_ #HT #H destruct /2 width=1/
 121 | #a #L #V #W #T #H destruct
 122 | #a #L #V #W #T #H destruct
 123 ]
 124 qed-.
 125
 126 lemma crx_inv_ib2: ∀h,g,a,I,L,W,T. ib2 a I → ⦃h, L⦄ ⊢ 𝐑[g]⦃ⓑ{a,I}W.T⦄ →
 127                    ⦃h, L⦄ ⊢ 𝐑[g]⦃W⦄ ∨ ⦃h, L.ⓑ{I}W⦄ ⊢ 𝐑[g]⦃T⦄.
 128 /2 width=5 by crx_inv_ib2_aux/ qed-.
 129
 130 fact crx_inv_appl_aux: ∀h,g,L,W,U,T. ⦃h, L⦄ ⊢ 𝐑[g]⦃T⦄ → T = ⓐW.U →
 131                        ∨∨ ⦃h, L⦄ ⊢ 𝐑[g]⦃W⦄ | ⦃h, L⦄ ⊢ 𝐑[g]⦃U⦄ | (𝐒⦃U⦄ → ⊥).
 132 #h #g #L #W0 #U #T * -L -T
 133 [ #L #k #l #_ #H destruct
 134 | #I #L #K #V #i #_ #H destruct
 135 | #L #V #T #HV #H destruct /2 width=1/
 136 | #L #V #T #HT #H destruct /2 width=1/
 137 | #I #L #V #T #H1 #H2 destruct
 138   elim H1 -H1 #H destruct
 139 | #a #I #L #V #T #_ #_ #H destruct
 140 | #a #I #L #V #T #_ #_ #H destruct
 141 | #a #L #V #W #T #H destruct
 142   @or3_intro2 #H elim (simple_inv_bind … H)
 143 | #a #L #V #W #T #H destruct
 144   @or3_intro2 #H elim (simple_inv_bind … H)
 145 ]
 146 qed-.
 147
 148 lemma crx_inv_appl: ∀h,g,L,V,T. ⦃h, L⦄ ⊢ 𝐑[g]⦃ⓐV.T⦄ →
 149                     ∨∨ ⦃h, L⦄ ⊢ 𝐑[g]⦃V⦄ | ⦃h, L⦄ ⊢ 𝐑[g]⦃T⦄ | (𝐒⦃T⦄ → ⊥).
 150 /2 width=3 by crx_inv_appl_aux/ qed-.