matita/matita/contribs/lambda/pointer.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 "term.ma".
  16
  17 (* POINTER ******************************************************************)
  18
  19 (* Policy: pointer step metavariables: c *)
  20 (* Note: this is a step of a path in the tree representation of a term:
  21          rc (rectus)  : not needed (we use sn instead)
  22          sn (sinister): proceed on the left argument of an application
  23                         or on the argument of an abstraction (this would be rc)
  24          dx (dexter)  : proceed on the right argument of an application
  25 *)
  26 (* Remark: the following breaks destruct because of δ-expansions
  27            definition ptr_step: Type[0] ≝ bool.
  28            definition sn: bool ≝ true.
  29            definition dx: bool ≝ false.
  30 *)
  31 inductive ptr_step: Type[0] ≝
  32 | sn: ptr_step
  33 | dx: ptr_step
  34 .
  35
  36 definition is_dx: predicate ptr_step ≝ λc. dx = c.
  37
  38 (* Policy: pointer metavariables: p, q *)
  39 (* Note: this is a path in the tree representation of a term, heading to a redex *)
  40 definition ptr: Type[0] ≝ list ptr_step.
  41
  42 (* Note: a redex is "in whd" when is not under an abstraction nor in the lefr argument of an application *)
  43 definition in_whd: predicate ptr ≝ All … is_dx.
  44
  45 lemma in_whd_ind: ∀R:predicate ptr. R (◊) →
  46                   (∀p. in_whd p → R p → R (dx::p)) →
  47                   ∀p. in_whd p → R p.
  48 #R #H #IH #p elim p -p // -H *
  49 #p #IHp * #H1 #H2 destruct /3 width=1/
  50 qed-.
  51
  52 definition compatible_rc: predicate (ptr→relation term) ≝ λR.
  53                           ∀p,A1,A2. R p A1 A2 → R (sn::p) (𝛌.A1) (𝛌.A2).
  54
  55 definition compatible_sn: predicate (ptr→relation term) ≝ λR.
  56                           ∀p,B1,B2,A. R p B1 B2 → R (sn::p) (@B1.A) (@B2.A).
  57
  58 definition compatible_dx: predicate (ptr→relation term) ≝ λR.
  59                           ∀p,B,A1,A2. R p A1 A2 → R (dx::p) (@B.A1) (@B.A2).