matita/matita/lib/lambda/paths/trace.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 "paths/path.ma".
  16
  17 (* TRACE ********************************************************************)
  18
  19 (* Policy: trace metavariables: r, s *)
  20 definition trace: Type[0] ≝ list path.
  21
  22 definition ho_compatible_rc: predicate (trace→relation term) ≝ λR.
  23                              ∀s,A1,A2. R s A1 A2 → R (rc:::s) (𝛌.A1) (𝛌.A2).
  24
  25 definition ho_compatible_sn: predicate (trace→relation term) ≝ λR.
  26                              ∀s,B1,B2,A. R s B1 B2 → R (sn:::s) (@B1.A) (@B2.A).
  27
  28 definition ho_compatible_dx: predicate (trace→relation term) ≝ λR.
  29                              ∀s,B,A1,A2. R s A1 A2 → R (dx:::s) (@B.A1) (@B.A2).
  30
  31 lemma lstar_compatible_rc: ∀R. compatible_rc R → ho_compatible_rc (lstar … R).
  32 #R #HR #s #A1 #A2 #H @(lstar_ind_l … s A1 H) -s -A1 // /3 width=3/
  33 qed.
  34
  35 lemma lstar_compatible_sn: ∀R. compatible_sn R → ho_compatible_sn (lstar … R).
  36 #R #HR #s #B1 #B2 #A #H @(lstar_ind_l … s B1 H) -s -B1 // /3 width=3/
  37 qed.
  38
  39 lemma lstar_compatible_dx: ∀R. compatible_dx R → ho_compatible_dx (lstar … R).
  40 #R #HR #s #B #A1 #A2 #H @(lstar_ind_l … s A1 H) -s -A1 // /3 width=3/
  41 qed.
  42
  43 (* Note: a "whd" computation contracts just redexes in the whd *)
  44 definition is_whd: predicate trace ≝ All … in_whd.
  45
  46 lemma is_whd_dx: ∀s. is_whd s → is_whd (dx:::s).
  47 #s elim s -s //
  48 #p #s #IHs * /3 width=1/
  49 qed.
  50
  51 lemma is_whd_append: ∀r. is_whd r → ∀s. is_whd s → is_whd (r@s).
  52 /2 width=1 by All_append/
  53 qed.
  54
  55 lemma is_whd_inv_dx: ∀s. is_whd (dx:::s) → is_whd s.
  56 #s elim s -s //
  57 #p #s #IHs * * #_ /3 width=1/
  58 qed-.
  59
  60 lemma is_whd_inv_append: ∀r,s. is_whd (r@s) → is_whd r ∧ is_whd s.
  61 /2 width=1 by All_inv_append/
  62 qed-.
  63
  64 (* Note: an "inner" computation contracts just redexes not in the whd *)
  65 definition is_inner: predicate trace ≝ All … in_inner.
  66
  67 lemma is_inner_append: ∀r. is_inner r → ∀s. is_inner s → is_inner (r@s).
  68 /2 width=1 by All_append/
  69 qed.
  70
  71 lemma is_whd_is_inner_inv: ∀s. is_whd s → is_inner s → ◊ = s.
  72 * // #p #s * #H1p #_ * #H2p #_ elim (H2p …) -H2p //
  73 qed-.