X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambda%2Fpaths%2Ftrace.ma;h=fb042bdf65b70b6b18b9417e1016c7bd4e4805b9;hb=f7da48c844105a52a705872dfa0d4104de010c82;hp=53b979809efa4743ee979073215bf9aba00e9a6b;hpb=5c792a695677f2857e1984ababc9998d42fc8033;p=helm.git

diff --git a/matita/matita/contribs/lambda/paths/trace.ma b/matita/matita/contribs/lambda/paths/trace.ma
index 53b979809..fb042bdf6 100644
--- a/matita/matita/contribs/lambda/paths/trace.ma
+++ b/matita/matita/contribs/lambda/paths/trace.ma
@@ -19,19 +19,6 @@ include "paths/path.ma".
 (* Policy: trace metavariables: r, s *)
 definition trace: Type[0] ≝ list path.
 
-(* Note: a "whd" computation contracts just redexes in the whd *)
-definition is_whd: predicate trace ≝ All … in_whd.
-
-lemma is_whd_dx: ∀s. is_whd s → is_whd (dx:::s).
-#s elim s -s //
-#p #s #IHs * /3 width=1/ 
-qed.
-
-lemma is_whd_append: ∀r. is_whd r → ∀s. is_whd s → is_whd (r@s).
-#r elim r -r //
-#q #r #IHr * /3 width=1/
-qed.
-
 definition ho_compatible_rc: predicate (trace→relation term) ≝ λR.
                              ∀s,A1,A2. R s A1 A2 → R (rc:::s) (𝛌.A1) (𝛌.A2).
 
@@ -42,13 +29,45 @@ definition ho_compatible_dx: predicate (trace→relation term) ≝ λR.
                              ∀s,B,A1,A2. R s A1 A2 → R (dx:::s) (@B.A1) (@B.A2).
 
 lemma lstar_compatible_rc: ∀R. compatible_rc R → ho_compatible_rc (lstar … R).
-#R #HR #s #A1 #A2 #H @(lstar_ind_l ????????? H) -s -A1 // /3 width=3/
+#R #HR #s #A1 #A2 #H @(lstar_ind_l … s A1 H) -s -A1 // /3 width=3/
 qed.
 
 lemma lstar_compatible_sn: ∀R. compatible_sn R → ho_compatible_sn (lstar … R).
-#R #HR #s #B1 #B2 #A #H @(lstar_ind_l ????????? H) -s -B1 // /3 width=3/
+#R #HR #s #B1 #B2 #A #H @(lstar_ind_l … s B1 H) -s -B1 // /3 width=3/
 qed.
 
 lemma lstar_compatible_dx: ∀R. compatible_dx R → ho_compatible_dx (lstar … R).
-#R #HR #s #B #A1 #A2 #H @(lstar_ind_l ????????? H) -s -A1 // /3 width=3/
+#R #HR #s #B #A1 #A2 #H @(lstar_ind_l … s A1 H) -s -A1 // /3 width=3/
 qed.
+
+(* Note: a "whd" computation contracts just redexes in the whd *)
+definition is_whd: predicate trace ≝ All … in_whd.
+
+lemma is_whd_dx: ∀s. is_whd s → is_whd (dx:::s).
+#s elim s -s //
+#p #s #IHs * /3 width=1/
+qed.
+
+lemma is_whd_append: ∀r. is_whd r → ∀s. is_whd s → is_whd (r@s).
+/2 width=1 by All_append/
+qed.
+
+lemma is_whd_inv_dx: ∀s. is_whd (dx:::s) → is_whd s.
+#s elim s -s //
+#p #s #IHs * * #_ /3 width=1/
+qed-.
+
+lemma is_whd_inv_append: ∀r,s. is_whd (r@s) → is_whd r ∧ is_whd s.
+/2 width=1 by All_inv_append/
+qed-.
+
+(* Note: an "inner" computation contracts just redexes not in the whd *)
+definition is_inner: predicate trace ≝ All … in_inner.
+
+lemma is_inner_append: ∀r. is_inner r → ∀s. is_inner s → is_inner (r@s).
+/2 width=1 by All_append/
+qed.
+
+lemma is_whd_is_inner_inv: ∀s. is_whd s → is_inner s → ◊ = s.
+* // #p #s * #H1p #_ * #H2p #_ elim (H2p …) -H2p //
+qed-.