Commit 74d21e01 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Move `elem_of_suffix` to other suffix lemmas.

parent e58dd720
...@@ -2078,9 +2078,6 @@ Proof. intros [??]. discriminate_list. Qed. ...@@ -2078,9 +2078,6 @@ Proof. intros [??]. discriminate_list. Qed.
Lemma elem_of_prefix l1 l2 x : Lemma elem_of_prefix l1 l2 x :
x l1 l1 `prefix_of` l2 x l2. x l1 l1 `prefix_of` l2 x l2.
Proof. intros Hin [l' ->]. apply elem_of_app. by left. Qed. Proof. intros Hin [l' ->]. apply elem_of_app. by left. Qed.
Lemma elem_of_suffix l1 l2 x :
x l1 l1 `suffix_of` l2 x l2.
Proof. intros Hin [l' ->]. apply elem_of_app. by right. Qed.
(* [prefix] is not a total order, but [l1] and [l2] are always comparable if (* [prefix] is not a total order, but [l1] and [l2] are always comparable if
they are both prefixes of some [l3]. *) they are both prefixes of some [l3]. *)
Lemma prefix_weak_total l1 l2 l3 : Lemma prefix_weak_total l1 l2 l3 :
...@@ -2230,6 +2227,9 @@ Lemma suffix_length l1 l2 : l1 `suffix_of` l2 → length l1 ≤ length l2. ...@@ -2230,6 +2227,9 @@ Lemma suffix_length l1 l2 : l1 `suffix_of` l2 → length l1 ≤ length l2.
Proof. intros [? ->]. rewrite app_length. lia. Qed. Proof. intros [? ->]. rewrite app_length. lia. Qed.
Lemma suffix_cons_not x l : ¬x :: l `suffix_of` l. Lemma suffix_cons_not x l : ¬x :: l `suffix_of` l.
Proof. intros [??]. discriminate_list. Qed. Proof. intros [??]. discriminate_list. Qed.
Lemma elem_of_suffix l1 l2 x :
x l1 l1 `suffix_of` l2 x l2.
Proof. intros Hin [l' ->]. apply elem_of_app. by right. Qed.
(* [suffix] is not a total order, but [l1] and [l2] are always comparable if (* [suffix] is not a total order, but [l1] and [l2] are always comparable if
they are both suffixes of some [l3]. *) they are both suffixes of some [l3]. *)
Lemma suffix_weak_total l1 l2 l3 : Lemma suffix_weak_total l1 l2 l3 :
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment