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 AND IRREDUCIBLE TERMS *****************************)
  18
  19 (* reducible terms *)
  20 inductive trf: term → Prop ≝
  21 | trf_abst_sn: ∀V,T.   trf V → trf (𝕔{Abst} V. T)
  22 | trf_abst_dx: ∀V,T.   trf T → trf (𝕔{Abst} V. T)
  23 | trf_appl_sn: ∀V,T.   trf V → trf (𝕔{Appl} V. T)
  24 | trf_appl_dx: ∀V,T.   trf T → trf (𝕔{Appl} V. T)
  25 | trf_abbr   : ∀V,T.           trf (𝕔{Abbr} V. T)
  26 | trf_cast   : ∀V,T.           trf (𝕔{Cast} V. T)
  27 | trf_beta   : ∀V,W,T. trf (𝕔{Appl} V. 𝕔{Abst} W. T)
  28 .
  29
  30 interpretation
  31    "context-free reducibility (term)"
  32    'Reducible T = (trf T).
  33
  34 (* irreducible terms *)
  35 definition tif: term → Prop ≝
  36    λT. ℝ[T] → False.
  37
  38 interpretation
  39    "context-free irreducibility (term)"
  40    'NotReducible T = (tif T).
  41
  42 (* Basic inversion lemmas ***************************************************)
  43
  44 fact trf_inv_atom_aux: ∀I,T. ℝ[T] → T =  𝕒{I} → False.
  45 #I #T * -T
  46 [ #V #T #_ #H destruct
  47 | #V #T #_ #H destruct
  48 | #V #T #_ #H destruct
  49 | #V #T #_ #H destruct
  50 | #V #T #H destruct
  51 | #V #T #H destruct
  52 | #V #W #T #H destruct
  53 ]
  54 qed.
  55
  56 lemma trf_inv_atom: ∀I. ℝ[𝕒{I}] → False.
  57 /2/ qed-.
  58
  59 fact trf_inv_abst_aux: ∀W,U,T. ℝ[T] → T =  𝕔{Abst} W. U → ℝ[W] ∨ ℝ[U].
  60 #W #U #T * -T
  61 [ #V #T #HV #H destruct -V T /2/
  62 | #V #T #HT #H destruct -V T /2/
  63 | #V #T #_ #H destruct
  64 | #V #T #_ #H destruct
  65 | #V #T #H destruct
  66 | #V #T #H destruct
  67 | #V #W0 #T #H destruct
  68 ]
  69 qed.
  70
  71 lemma trf_inv_abst: ∀V,T. ℝ[𝕔{Abst}V.T] → ℝ[V] ∨ ℝ[T].
  72 /2/ qed-.
  73
  74 fact trf_inv_appl_aux: ∀W,U,T. ℝ[T] → T =  𝕔{Appl} W. U →
  75                        ∨∨ ℝ[W] | ℝ[U] | (𝕊[U] → False).
  76 #W #U #T * -T
  77 [ #V #T #_ #H destruct
  78 | #V #T #_ #H destruct
  79 | #V #T #HV #H destruct -V T /2/
  80 | #V #T #HT #H destruct -V T /2/
  81 | #V #T #H destruct
  82 | #V #T #H destruct
  83 | #V #W0 #T #H destruct -V U
  84   @or3_intro2 #H elim (simple_inv_bind … H)
  85 ]
  86 qed.
  87
  88 lemma trf_inv_appl: ∀W,U. ℝ[𝕔{Appl}W.U] → ∨∨ ℝ[W] | ℝ[U] | (𝕊[U] → False).
  89 /2/ qed-.
  90
  91 lemma tif_inv_abbr: ∀V,T. 𝕀[𝕔{Abbr}V.T] → False.
  92 /2/ qed-.
  93
  94 lemma tif_inv_abst: ∀V,T. 𝕀[𝕔{Abst}V.T] → 𝕀[V] ∧ 𝕀[T].
  95 /4/ qed-.
  96
  97 lemma tif_inv_appl: ∀V,T. 𝕀[𝕔{Appl}V.T] → ∧∧ 𝕀[V] & 𝕀[T] & 𝕊[T].
  98 #V #T #HVT @and3_intro /3/
  99 generalize in match HVT -HVT; elim T -T //
 100 * // * #U #T #_ #_ #H elim (H ?) -H /2/
 101 qed-.
 102
 103 lemma tif_inv_cast: ∀V,T. 𝕀[𝕔{Cast}V.T] → False.
 104 /2/ qed-.
 105
 106 (* Basic properties *********************************************************)
 107
 108 lemma tif_atom: ∀I. 𝕀[𝕒{I}].
 109 /2/ qed.
 110
 111 lemma tif_abst: ∀V,T. 𝕀[V] →  𝕀[T] →  𝕀[𝕔 {Abst}V.T].
 112 #V #T #HV #HT #H
 113 elim (trf_inv_abst … H) -H /2/
 114 qed.
 115
 116 lemma tif_appl: ∀V,T. 𝕀[V] →  𝕀[T] →  𝕊[T] → 𝕀[𝕔{Appl}V.T].
 117 #V #T #HV #HT #S #H
 118 elim (trf_inv_appl … H) -H /2/
 119 qed.