matita/matita/lib/lambda/paths/path.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 "lambda/terms/term.ma".
  16
  17 (* PATH *********************************************************************)
  18
  19 (* Policy: path step metavariables: o *)
  20 (* Note: this is a step of a path in the tree representation of a term:
  21          rc (rectus)  : proceed on the argument of an abstraction
  22          sn (sinister): proceed on the left argument of an application
  23          dx (dexter)  : proceed on the right argument of an application
  24 *)
  25 inductive step: Type[0] ≝
  26 | rc: step
  27 | sn: step
  28 | dx: step
  29 .
  30
  31 definition is_dx: predicate step ≝ λo. dx = o.
  32
  33 (* Policy: path metavariables: p, q *)
  34 (* Note: this is a path in the tree representation of a term, heading to a redex *)
  35 definition path: Type[0] ≝ list step.
  36
  37 definition compatible_rc: predicate (path→relation term) ≝ λR.
  38                           ∀p,A1,A2. R p A1 A2 → R (rc::p) (𝛌.A1) (𝛌.A2).
  39
  40 definition compatible_sn: predicate (path→relation term) ≝ λR.
  41                           ∀p,B1,B2,A. R p B1 B2 → R (sn::p) (@B1.A) (@B2.A).
  42
  43 definition compatible_dx: predicate (path→relation term) ≝ λR.
  44                           ∀p,B,A1,A2. R p A1 A2 → R (dx::p) (@B.A1) (@B.A2).
  45
  46 (* Note: a redex is "in the whd" when is not under an abstraction nor in the left argument of an application *)
  47 definition in_whd: predicate path ≝ All … is_dx.
  48
  49 lemma in_whd_ind: ∀R:predicate path. R (◊) →
  50                   (∀p. in_whd p → R p → R (dx::p)) →
  51                   ∀p. in_whd p → R p.
  52 #R #H #IH #p elim p -p // -H *
  53 #p #IHp * #H1 #H2 destruct /3 width=1/
  54 qed-.
  55
  56 (* Note: a redex is "inner" when is not in the whd *)
  57 definition in_inner: predicate path ≝ λp. in_whd p → ⊥.
  58
  59 lemma in_inner_rc: ∀p. in_inner (rc::p).
  60 #p * normalize #H destruct
  61 qed.
  62
  63 lemma in_inner_sn: ∀p. in_inner (sn::p).
  64 #p * normalize #H destruct
  65 qed.
  66
  67 lemma in_inner_cons: ∀o,p. in_inner p → in_inner (o::p).
  68 #o #p #H1p * /2 width=1/
  69 qed.
  70
  71 lemma in_inner_inv_dx: ∀p. in_inner (dx::p) → in_inner p.
  72 /3 width=1/
  73 qed-.
  74
  75 lemma in_whd_or_in_inner: ∀p. in_whd p ∨ in_inner p.
  76 #p elim p -p /2 width=1/ #o #p * #Hp /3 width=1/ cases o -o /2 width=1/ /3 width=1/
  77 qed-.
  78
  79 lemma in_inner_ind: ∀R:predicate path.
  80                     (∀p. R (rc::p)) → (∀p. R (sn::p)) →
  81                     (∀p. in_inner p → R p → R (dx::p)) →
  82                     ∀p. in_inner p → R p.
  83 #R #H1 #H2 #IH #p elim p -p
  84 [ #H elim (H …) -H //
  85 | * #p #IHp // #H
  86   lapply (in_inner_inv_dx … H) -H /3 width=1/
  87 ]
  88 qed-.
  89
  90 lemma in_inner_inv: ∀p. in_inner p →
  91                     ∨∨ ∃q. rc::q = p | ∃q. sn::q = p
  92                      | ∃∃q. in_inner q & dx::q = p.
  93 @in_inner_ind /3 width=2/ /3 width=3/
  94 qed-.