- ng_refiner:

[helm.git] / matita / matita / contribs / lambda / paths / path.ma

diff --git a/matita/matita/contribs/lambda/paths/path.ma b/matita/matita/contribs/lambda/paths/path.ma
index 7105c519ff3dede78304ac4e2a978a49d69559e9..743ec4c348f12b1985f07b6e9186ca3ba1884876 100644 (file)
--- a/matita/matita/contribs/lambda/paths/path.ma
+++ b/matita/matita/contribs/lambda/paths/path.ma
@@ -34,7 +34,16 @@ definition is_dx: predicate step ≝ λo. dx = o.
 (* Note: this is a path in the tree representation of a term, heading to a redex *)
 definition path: Type[0] ≝ list step.
 
-(* Note: a redex is "in whd" when is not under an abstraction nor in the lefr argument of an application *)
+definition compatible_rc: predicate (path→relation term) ≝ λR.
+                          ∀p,A1,A2. R p A1 A2 → R (rc::p) (𝛌.A1) (𝛌.A2).
+
+definition compatible_sn: predicate (path→relation term) ≝ λR.
+                          ∀p,B1,B2,A. R p B1 B2 → R (sn::p) (@B1.A) (@B2.A).
+
+definition compatible_dx: predicate (path→relation term) ≝ λR.
+                          ∀p,B,A1,A2. R p A1 A2 → R (dx::p) (@B.A1) (@B.A2).
+
+(* Note: a redex is "in the whd" when is not under an abstraction nor in the left argument of an application *)
 definition in_whd: predicate path ≝ All … is_dx.
 
 lemma in_whd_ind: ∀R:predicate path. R (◊) →
@@ -44,11 +53,42 @@ lemma in_whd_ind: ∀R:predicate path. R (◊) →
 #p #IHp * #H1 #H2 destruct /3 width=1/
 qed-.
 
-definition compatible_rc: predicate (path→relation term) ≝ λR.
-                          ∀p,A1,A2. R p A1 A2 → R (rc::p) (𝛌.A1) (𝛌.A2).
+(* Note: a redex is "inner" when is not in the whd *)
+definition in_inner: predicate path ≝ λp. in_whd p → ⊥.
 
-definition compatible_sn: predicate (path→relation term) ≝ λR.
-                          ∀p,B1,B2,A. R p B1 B2 → R (sn::p) (@B1.A) (@B2.A).
+lemma in_inner_rc: ∀p. in_inner (rc::p).
+#p * normalize #H destruct
+qed.
 
-definition compatible_dx: predicate (path→relation term) ≝ λR.
-                          ∀p,B,A1,A2. R p A1 A2 → R (dx::p) (@B.A1) (@B.A2).
+lemma in_inner_sn: ∀p. in_inner (sn::p).
+#p * normalize #H destruct
+qed.
+
+lemma in_inner_cons: ∀o,p. in_inner p → in_inner (o::p).
+#o #p #H1p * /2 width=1/
+qed.
+
+lemma in_inner_inv_dx: ∀p. in_inner (dx::p) → in_inner p.
+/3 width=1/
+qed-.
+
+lemma in_whd_or_in_inner: ∀p. in_whd p ∨ in_inner p.
+#p elim p -p /2 width=1/ #o #p * #Hp /3 width=1/ cases o -o /2 width=1/ /3 width=1/
+qed-.
+
+lemma in_inner_ind: ∀R:predicate path.
+                    (∀p. R (rc::p)) → (∀p. R (sn::p)) →
+                    (∀p. in_inner p → R p → R (dx::p)) →
+                    ∀p. in_inner p → R p.
+#R #H1 #H2 #IH #p elim p -p
+[ #H elim (H …) -H //
+| * #p #IHp // #H
+  lapply (in_inner_inv_dx … H) -H /3 width=1/
+]
+qed-.
+
+lemma in_inner_inv: ∀p. in_inner p →
+                    ∨∨ ∃q. rc::q = p | ∃q. sn::q = p
+                     | ∃∃q. in_inner q & dx::q = p.
+@in_inner_ind /3 width=2/ /3 width=3/
+qed-.