1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "paths/path.ma".
17 (* TRACE ********************************************************************)
19 (* Policy: trace metavariables: r, s *)
20 definition trace: Type[0] ≝ list path.
22 (* Note: a "whd" computation contracts just redexes in the whd *)
23 definition is_whd: predicate trace ≝ All … in_whd.
25 lemma is_whd_dx: ∀s. is_whd s → is_whd (dx:::s).
27 #p #s #IHs * /3 width=1/
30 lemma is_whd_append: ∀r. is_whd r → ∀s. is_whd s → is_whd (r@s).
31 /2 width=1 by All_append/
34 lemma is_whd_inv_append: ∀r,s. is_whd (r@s) → is_whd r ∧ is_whd s.
35 /2 width=1 by All_inv_append/
38 definition ho_compatible_rc: predicate (trace→relation term) ≝ λR.
39 ∀s,A1,A2. R s A1 A2 → R (rc:::s) (𝛌.A1) (𝛌.A2).
41 definition ho_compatible_sn: predicate (trace→relation term) ≝ λR.
42 ∀s,B1,B2,A. R s B1 B2 → R (sn:::s) (@B1.A) (@B2.A).
44 definition ho_compatible_dx: predicate (trace→relation term) ≝ λR.
45 ∀s,B,A1,A2. R s A1 A2 → R (dx:::s) (@B.A1) (@B.A2).
47 lemma lstar_compatible_rc: ∀R. compatible_rc R → ho_compatible_rc (lstar … R).
48 #R #HR #s #A1 #A2 #H @(lstar_ind_l … s A1 H) -s -A1 // /3 width=3/
51 lemma lstar_compatible_sn: ∀R. compatible_sn R → ho_compatible_sn (lstar … R).
52 #R #HR #s #B1 #B2 #A #H @(lstar_ind_l … s B1 H) -s -B1 // /3 width=3/
55 lemma lstar_compatible_dx: ∀R. compatible_dx R → ho_compatible_dx (lstar … R).
56 #R #HR #s #B #A1 #A2 #H @(lstar_ind_l … s A1 H) -s -A1 // /3 width=3/