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: predicate term ≝
  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: predicate term ≝ λT. ℝ[T] → False.
  36
  37 interpretation
  38    "context-free irreducibility (term)"
  39    'NotReducible T = (tif T).
  40
  41 (* Basic inversion lemmas ***************************************************)
  42
  43 fact trf_inv_atom_aux: ∀I,T. ℝ[T] → T =  𝕒{I} → False.
  44 #I #T * -T
  45 [ #V #T #_ #H destruct
  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 #W #T #H destruct
  52 ]
  53 qed.
  54
  55 lemma trf_inv_atom: ∀I. ℝ[𝕒{I}] → False.
  56 /2/ qed-.
  57
  58 fact trf_inv_abst_aux: ∀W,U,T. ℝ[T] → T =  𝕔{Abst} W. U → ℝ[W] ∨ ℝ[U].
  59 #W #U #T * -T
  60 [ #V #T #HV #H destruct -V T /2/
  61 | #V #T #HT #H destruct -V T /2/
  62 | #V #T #_ #H destruct
  63 | #V #T #_ #H destruct
  64 | #V #T #H destruct
  65 | #V #T #H destruct
  66 | #V #W0 #T #H destruct
  67 ]
  68 qed.
  69
  70 lemma trf_inv_abst: ∀V,T. ℝ[𝕔{Abst}V.T] → ℝ[V] ∨ ℝ[T].
  71 /2/ qed-.
  72
  73 fact trf_inv_appl_aux: ∀W,U,T. ℝ[T] → T =  𝕔{Appl} W. U →
  74                        ∨∨ ℝ[W] | ℝ[U] | (𝕊[U] → False).
  75 #W #U #T * -T
  76 [ #V #T #_ #H destruct
  77 | #V #T #_ #H destruct
  78 | #V #T #HV #H destruct -V T /2/
  79 | #V #T #HT #H destruct -V T /2/
  80 | #V #T #H destruct
  81 | #V #T #H destruct
  82 | #V #W0 #T #H destruct -V U
  83   @or3_intro2 #H elim (simple_inv_bind … H)
  84 ]
  85 qed.
  86
  87 lemma trf_inv_appl: ∀W,U. ℝ[𝕔{Appl}W.U] → ∨∨ ℝ[W] | ℝ[U] | (𝕊[U] → False).
  88 /2/ qed-.
  89
  90 lemma tif_inv_abbr: ∀V,T. 𝕀[𝕔{Abbr}V.T] → False.
  91 /2/ qed-.
  92
  93 lemma tif_inv_abst: ∀V,T. 𝕀[𝕔{Abst}V.T] → 𝕀[V] ∧ 𝕀[T].
  94 /4/ qed-.
  95
  96 lemma tif_inv_appl: ∀V,T. 𝕀[𝕔{Appl}V.T] → ∧∧ 𝕀[V] & 𝕀[T] & 𝕊[T].
  97 #V #T #HVT @and3_intro /3/
  98 generalize in match HVT -HVT; elim T -T //
  99 * // * #U #T #_ #_ #H elim (H ?) -H /2/
 100 qed-.
 101
 102 lemma tif_inv_cast: ∀V,T. 𝕀[𝕔{Cast}V.T] → False.
 103 /2/ qed-.
 104
 105 (* Basic properties *********************************************************)
 106
 107 lemma tif_atom: ∀I. 𝕀[𝕒{I}].
 108 /2/ qed.
 109
 110 lemma tif_abst: ∀V,T. 𝕀[V] →  𝕀[T] →  𝕀[𝕔 {Abst}V.T].
 111 #V #T #HV #HT #H
 112 elim (trf_inv_abst … H) -H /2/
 113 qed.
 114
 115 lemma tif_appl: ∀V,T. 𝕀[V] →  𝕀[T] →  𝕊[T] → 𝕀[𝕔{Appl}V.T].
 116 #V #T #HV #HT #S #H
 117 elim (trf_inv_appl … H) -H /2/
 118 qed.