matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.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
  17 (* CONTEXT-FREE REDUCIBLE TERMS *********************************************)
  18
  19 (* reducible terms *)
  20 inductive trf: predicate term ≝
  21 | trf_abst_sn: ∀V,T.   trf V → trf (ⓛV. T)
  22 | trf_abst_dx: ∀V,T.   trf T → trf (ⓛV. T)
  23 | trf_appl_sn: ∀V,T.   trf V → trf (ⓐV. T)
  24 | trf_appl_dx: ∀V,T.   trf T → trf (ⓐV. T)
  25 | trf_abbr   : ∀V,T.           trf (ⓓV. T)
  26 | trf_cast   : ∀V,T.           trf (ⓝV. T)
  27 | trf_beta   : ∀V,W,T. trf (ⓐV. ⓛW. T)
  28 .
  29
  30 interpretation
  31    "context-free reducibility (term)"
  32    'Reducible T = (trf T).
  33
  34 (* Basic inversion lemmas ***************************************************)
  35
  36 fact trf_inv_atom_aux: ∀I,T. 𝐑⦃T⦄ → T =  ⓪{I} → ⊥.
  37 #I #T * -T
  38 [ #V #T #_ #H destruct
  39 | #V #T #_ #H destruct
  40 | #V #T #_ #H destruct
  41 | #V #T #_ #H destruct
  42 | #V #T #H destruct
  43 | #V #T #H destruct
  44 | #V #W #T #H destruct
  45 ]
  46 qed.
  47
  48 lemma trf_inv_atom: ∀I. 𝐑⦃⓪{I}⦄ → ⊥.
  49 /2 width=4/ qed-.
  50
  51 fact trf_inv_abst_aux: ∀W,U,T. 𝐑⦃T⦄ → T =  ⓛW. U → 𝐑⦃W⦄ ∨ 𝐑⦃U⦄.
  52 #W #U #T * -T
  53 [ #V #T #HV #H destruct /2 width=1/
  54 | #V #T #HT #H destruct /2 width=1/
  55 | #V #T #_ #H destruct
  56 | #V #T #_ #H destruct
  57 | #V #T #H destruct
  58 | #V #T #H destruct
  59 | #V #W0 #T #H destruct
  60 ]
  61 qed.
  62
  63 lemma trf_inv_abst: ∀V,T. 𝐑⦃ⓛV.T⦄ → 𝐑⦃V⦄ ∨ 𝐑⦃T⦄.
  64 /2 width=3/ qed-.
  65
  66 fact trf_inv_appl_aux: ∀W,U,T. 𝐑⦃T⦄ → T =  ⓐW. U →
  67                        ∨∨ 𝐑⦃W⦄ | 𝐑⦃U⦄ | (𝐒⦃U⦄ → ⊥).
  68 #W #U #T * -T
  69 [ #V #T #_ #H destruct
  70 | #V #T #_ #H destruct
  71 | #V #T #HV #H destruct /2 width=1/
  72 | #V #T #HT #H destruct /2 width=1/
  73 | #V #T #H destruct
  74 | #V #T #H destruct
  75 | #V #W0 #T #H destruct
  76   @or3_intro2 #H elim (simple_inv_bind … H)
  77 ]
  78 qed.
  79
  80 lemma trf_inv_appl: ∀W,U. 𝐑⦃ⓐW.U⦄ → ∨∨ 𝐑⦃W⦄ | 𝐑⦃U⦄ | (𝐒⦃U⦄ → ⊥).
  81 /2 width=3/ qed-.