(* *)
(**************************************************************************)
-include "paths/path.ma".
+include "paths/standard_precedence.ma".
(* STANDARD ORDER ************************************************************)
-(* Note: standard precedence relation on paths: p ≺ q
- to serve as base for the order relations: p < q and p ≤ q *)
-inductive sprec: relation path ≝
-| sprec_nil : ∀c,q. sprec (◊) (c::q)
-| sprec_rc : ∀p,q. sprec (dx::p) (rc::q)
-| sprec_sn : ∀p,q. sprec (rc::p) (sn::q)
-| sprec_comp: ∀c,p,q. sprec p q → sprec (c::p) (c::q)
-| sprec_skip: sprec (dx::◊) ◊
-.
-
-interpretation "standard 'precedes' on paths"
- 'prec p q = (sprec p q).
-
-lemma sprec_inv_sn: ∀p,q. p ≺ q → ∀p0. sn::p0 = p →
- ∃∃q0. p0 ≺ q0 & sn::q0 = q.
-#p #q * -p -q
-[ #c #q #p0 #H destruct
-| #p #q #p0 #H destruct
-| #p #q #p0 #H destruct
-| #c #p #q #Hpq #p0 #H destruct /2 width=3/
-| #p0 #H destruct
-]
-qed-.
-
-lemma sprec_fwd_in_whd: ∀p,q. p ≺ q → in_whd q → in_whd p.
-#p #q #H elim H -p -q // /2 width=1/
-[ #p #q * #H destruct
-| #p #q * #H destruct
-| #c #p #q #_ #IHpq * #H destruct /3 width=1/
-]
-qed-.
-
-(* Note: this is p < q *)
-definition slt: relation path ≝ TC … sprec.
-
-interpretation "standard 'less than' on paths"
- 'lt p q = (slt p q).
-
-lemma slt_step_rc: ∀p,q. p ≺ q → p < q.
-/2 width=1/
-qed.
-
-lemma slt_nil: ∀c,p. ◊ < c::p.
-/2 width=1/
-qed.
-
-lemma slt_skip: dx::◊ < ◊.
-/2 width=1/
-qed.
-
-lemma slt_comp: ∀c,p,q. p < q → c::p < c::q.
-#c #p #q #H elim H -q /3 width=1/ /3 width=3/
-qed.
-
-theorem slt_trans: transitive … slt.
-/2 width=3/
-qed-.
-
-lemma slt_refl: ∀p. p < p.
-#p elim p -p /2 width=1/
-@(slt_trans … (dx::◊)) //
-qed.
-
(* Note: this is p ≤ q *)
definition sle: relation path ≝ star … sprec.
* // /2 width=1/
qed.
-lemma sle_comp: ∀p1,p2. p1 ≤ p2 → ∀c. (c::p1) ≤ (c::p2).
+lemma sle_comp: ∀p1,p2. p1 ≤ p2 → ∀o. (o::p1) ≤ (o::p2).
#p1 #p2 #H elim H -p2 // /3 width=3/
qed.
lemma sle_skip_sle: ∀p. p ≤ ◊ → dx::p ≤ ◊.
-#p #H @(star_ind_l ??????? H) -p //
+#p #H @(star_ind_l … p H) -p //
#p #q #Hpq #_ #H @(sle_step_sn … H) -H /2 width=1/
qed.
lemma sle_dichotomy: ∀p1,p2:path. p1 ≤ p2 ∨ p2 ≤ p1.
#p1 elim p1 -p1
[ * /2 width=1/
-| #c1 #p1 #IHp1 * /2 width=1/
- * #p2 cases c1 -c1 /2 width=1/
+| #o1 #p1 #IHp1 * /2 width=1/
+ * #p2 cases o1 -o1 /2 width=1/
elim (IHp1 p2) -IHp1 /3 width=1/
]
qed-.
+lemma sle_inv_dx: ∀p,q. p ≤ q → ∀q0. dx::q0 = q →
+ in_whd p ∨ ∃∃p0. p0 ≤ q0 & dx::p0 = p.
+#p #q #H @(star_ind_l … p H) -p [ /3 width=3/ ]
+#p0 #p #Hp0 #_ #IHpq #q1 #H destruct
+elim (IHpq ??) -IHpq [4: // |3: skip ] (**) (* simplify line *)
+[ lapply (sprec_fwd_in_whd … Hp0) -Hp0 /3 width=1/
+| * #p1 #Hpq1 #H elim (sprec_inv_dx … Hp0 … H) -p
+ [ #H destruct /2 width=1/
+ | * /4 width=3/
+ ]
+]
+qed-.
+
+lemma sle_inv_rc: ∀p,q. p ≤ q → ∀p0. rc::p0 = p →
+ (∃∃q0. p0 ≤ q0 & rc::q0 = q) ∨
+ ∃q0. sn::q0 = q.
+#p #q #H elim H -q /3 width=3/
+#q #q0 #_ #Hq0 #IHpq #p0 #H destruct
+elim (IHpq p0 ?) -IHpq // *
+[ #p1 #Hp01 #H
+ elim (sprec_inv_rc … Hq0 … H) -q * /3 width=3/ /4 width=3/
+| #p1 #H elim (sprec_inv_sn … Hq0 … H) -q /3 width=2/
+]
+qed-.
+
lemma sle_inv_sn: ∀p,q. p ≤ q → ∀p0. sn::p0 = p →
∃∃q0. p0 ≤ q0 & sn::q0 = q.
#p #q #H elim H -q /2 width=3/
qed.
lemma sle_nil_inv_in_whd: ∀p. p ≤ ◊ → in_whd p.
-#p #H @(star_ind_l ??????? H) -p // /2 width=3 by sprec_fwd_in_whd/
+#p #H @(star_ind_l … p H) -p // /2 width=3 by sprec_fwd_in_whd/
qed-.
lemma sle_inv_in_whd: ∀p. (∀q. p ≤ q) → in_whd p.
/2 width=1 by sle_nil_inv_in_whd/
qed-.
+
+lemma sle_fwd_in_whd: ∀p,q. p ≤ q → in_whd q → in_whd p.
+#p #q #H @(star_ind_l … p H) -p // /3 width=3 by sprec_fwd_in_whd/
+qed-.
+
+lemma sle_fwd_in_inner: ∀p,q. p ≤ q → in_inner p → in_inner q.
+/3 width=3 by sle_fwd_in_whd/
+qed-.