matita/matita/contribs/lambda_delta/basic_2/reducibility/crf.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/grammar/term_simple.ma".
  16 include "basic_2/substitution/ldrop.ma".
  17
  18 (* CONTEXT-SENSITIVE REDUCIBLE TERMS ****************************************)
  19
  20 (* reducible binary items *)
  21 definition ri2: item2 → Prop ≝
  22                 λI. I = Bind2 true Abbr ∨ I = Flat2 Cast.
  23
  24 (* irreducible binary binders *)
  25 definition ib2: bool → bind2 → Prop ≝
  26                 λa,I. I = Abst ∨ Bind2 a I = Bind2 false Abbr.
  27
  28 (* reducible terms *)
  29 inductive crf: lenv → predicate term ≝
  30 | crf_delta  : ∀L,K,V,i. ⇩[0, i] L ≡ K.ⓓV → crf L (#i)
  31 | crf_appl_sn: ∀L,V,T. crf L V → crf L (ⓐV. T)
  32 | crf_appl_dx: ∀L,V,T. crf L T → crf L (ⓐV. T)
  33 | crf_ri2    : ∀I,L,V,T. ri2 I → crf L (②{I}V. T)
  34 | crf_ib2_sn : ∀a,I,L,V,T. ib2 a I → crf L V → crf L (ⓑ{a,I}V. T)
  35 | crf_ib2_dx : ∀a,I,L,V,T. ib2 a I → crf (L.ⓑ{I}V) T → crf L (ⓑ{a,I}V. T)
  36 | crf_beta   : ∀a,L,V,W,T. crf L (ⓐV. ⓛ{a}W. T)
  37 | crf_theta  : ∀a,L,V,W,T. crf L (ⓐV. ⓓ{a}W. T)
  38 .
  39
  40 interpretation
  41    "context-sensitive reducibility (term)"
  42    'Reducible L T = (crf L T).
  43
  44 (* Basic inversion lemmas ***************************************************)
  45
  46 fact trf_inv_atom_aux: ∀I,L,T. L ⊢ 𝐑⦃T⦄ → L = ⋆ → T = ⓪{I} → ⊥.
  47 #I #L #T * -L -T
  48 [ #L #K #V #i #HLK #H1 #H2 destruct
  49   lapply (ldrop_inv_atom1 … HLK) -HLK #H destruct
  50 | #L #V #T #_ #_ #H destruct
  51 | #L #V #T #_ #_ #H destruct
  52 | #J #L #V #T #_ #_ #H destruct
  53 | #a #J #L #V #T #_ #_ #_ #H destruct
  54 | #a #J #L #V #T #_ #_ #_ #H destruct
  55 | #a #L #V #W #T #_ #H destruct
  56 | #a #L #V #W #T #_ #H destruct
  57 ]
  58 qed.
  59
  60 lemma trf_inv_atom: ∀I. ⋆ ⊢ 𝐑⦃⓪{I}⦄ → ⊥.
  61 /2 width=6/ qed-.
  62
  63 fact trf_inv_lref_aux: ∀L,T. L ⊢ 𝐑⦃T⦄ → ∀i. T = #i → ∃∃K,V. ⇩[0, i] L ≡ K.ⓓV.
  64 #L #T * -L -T
  65 [ #L #K #V #j #HLK #i #H destruct /2 width=3/
  66 | #L #V #T #_ #i #H destruct
  67 | #L #V #T #_ #i #H destruct
  68 | #J #L #V #T #_ #i #H destruct
  69 | #a #J #L #V #T #_ #_ #i #H destruct
  70 | #a #J #L #V #T #_ #_ #i #H destruct
  71 | #a #L #V #W #T #i #H destruct
  72 | #a #L #V #W #T #i #H destruct
  73 ]
  74 qed.
  75
  76 lemma trf_inv_lref: ∀L,i. L ⊢ 𝐑⦃#i⦄ → ∃∃K,V. ⇩[0, i] L ≡ K.ⓓV.
  77 /2 width=3/ qed-.
  78
  79 fact crf_inv_ib2_aux: ∀a,I,L,W,U,T. ib2 a I → L ⊢ 𝐑⦃T⦄ → T = ⓑ{a,I}W. U →
  80                       L ⊢ 𝐑⦃W⦄ ∨ L.ⓑ{I}W ⊢ 𝐑⦃U⦄.
  81 #a #I #L #W #U #T #HI * -T
  82 [ #L #K #V #i #_ #H destruct
  83 | #L #V #T #_ #H destruct
  84 | #L #V #T #_ #H destruct
  85 | #J #L #V #T #H1 #H2 destruct
  86   elim H1 -H1 #H destruct
  87   elim HI -HI #H destruct
  88 | #b #J #L #V #T #_ #HV #H destruct /2 width=1/
  89 | #b #J #L #V #T #_ #HT #H destruct /2 width=1/
  90 | #b #L #V #W #T #H destruct
  91 | #b #L #V #W #T #H destruct
  92 ]
  93 qed.
  94
  95 lemma crf_inv_ib2: ∀a,I,L,W,T. ib2 a I → L ⊢ 𝐑⦃ⓑ{a,I}W.T⦄ →
  96                    L ⊢ 𝐑⦃W⦄ ∨ L.ⓑ{I}W ⊢ 𝐑⦃T⦄.
  97 /2 width=5/ qed-.
  98
  99 fact crf_inv_appl_aux: ∀L,W,U,T. L ⊢ 𝐑⦃T⦄ → T = ⓐW. U →
 100                        ∨∨ L ⊢ 𝐑⦃W⦄ | L ⊢ 𝐑⦃U⦄ | (𝐒⦃U⦄ → ⊥).
 101 #L #W #U #T * -T
 102 [ #L #K #V #i #_ #H destruct
 103 | #L #V #T #HV #H destruct /2 width=1/
 104 | #L #V #T #HT #H destruct /2 width=1/
 105 | #J #L #V #T #H1 #H2 destruct
 106   elim H1 -H1 #H destruct
 107 | #a #I #L #V #T #_ #_ #H destruct
 108 | #a #I #L #V #T #_ #_ #H destruct
 109 | #a #L #V #W0 #T #H destruct
 110   @or3_intro2 #H elim (simple_inv_bind … H)
 111 | #a #L #V #W0 #T #H destruct
 112   @or3_intro2 #H elim (simple_inv_bind … H)
 113 ]
 114 qed.
 115
 116 lemma crf_inv_appl: ∀L,V,T. L ⊢ 𝐑⦃ⓐV.T⦄ → ∨∨ L ⊢ 𝐑⦃V⦄ | L ⊢ 𝐑⦃T⦄ | (𝐒⦃T⦄ → ⊥).
 117 /2 width=3/ qed-.