From 1fc01f9de46cd1d5db5253f5cb6dafd07f3f00f1 Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Wed, 31 Mar 2021 15:50:38 +0200
Subject: [PATCH] More lemmas for list's prefix_of and suffix_of

---
 theories/list.v | 24 ++++++++++++++++++++----
 1 file changed, 20 insertions(+), 4 deletions(-)

diff --git a/theories/list.v b/theories/list.v
index 68ca3f6e..122ed46a 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -1848,14 +1848,20 @@ Proof.
 Qed.
 
 (** ** Properties of the [prefix] and [suffix] predicates *)
-Global Instance: PreOrder (@prefix A).
+Global Instance: PartialOrder (@prefix A).
 Proof.
-  split.
+  split; [split|].
   - intros ?. eexists []. by rewrite (right_id_L [] (++)).
   - intros ???[k1->] [k2->]. exists (k1 ++ k2). by rewrite (assoc_L (++)).
+  - intros x y [x1 H1] [y1 H2].
+    rewrite H2, <-(assoc_L (++)) in H1. rewrite <-(app_nil_r y) in H1 at 1.
+    simplify_eq. symmetry in H1. apply app_nil in H1 as [].
+    subst y1. by apply app_nil_r.
 Qed.
 Lemma prefix_nil l : [] `prefix_of` l.
 Proof. by exists l. Qed.
+Lemma prefix_nil_inv l : l `prefix_of` [] → l = [].
+Proof. intros [[|?] Eq]; symmetry in Eq; by apply app_nil in Eq as []. Qed.
 Lemma prefix_nil_not x l : ¬x :: l `prefix_of` [].
 Proof. by intros [k ?]. Qed.
 Lemma prefix_cons x l1 l2 : l1 `prefix_of` l2 → x :: l1 `prefix_of` x :: l2.
@@ -1884,11 +1890,21 @@ Lemma prefix_length l1 l2 : l1 `prefix_of` l2 → length l1 ≤ length l2.
 Proof. intros [? ->]. rewrite app_length. lia. Qed.
 Lemma prefix_snoc_not l x : ¬l ++ [x] `prefix_of` l.
 Proof. intros [??]. discriminate_list. Qed.
-Global Instance: PreOrder (@suffix A).
+Lemma prefix_of_down_total l1 l2 l3 :
+  l1 `prefix_of` l3 → l2 `prefix_of` l3 → l1 `prefix_of` l2 ∨ l2 `prefix_of` l1.
 Proof.
-  split.
+  intros [k1 H1] [k2 H2]. rewrite H2 in H1.
+  apply app_eq_inv in H1 as [(k&?&?)|(k&?&?)]; [left|right]; exists k; eauto.
+Qed.
+Global Instance: PartialOrder (@suffix A).
+Proof.
+  split; [split|].
   - intros ?. by eexists [].
   - intros ???[k1->] [k2->]. exists (k2 ++ k1). by rewrite (assoc_L (++)).
+  - intros x y [x1 H1] [y1 H2].
+    rewrite H2, (assoc_L (++)) in H1. rewrite <-(app_nil_l y) in H1 at 1.
+    apply app_inv_tail in H1. symmetry in H1. apply app_nil in H1 as [].
+    simplify_eq. by apply app_nil_l.
 Qed.
 Global Instance prefix_dec `{!EqDecision A} : RelDecision prefix :=
   fix go l1 l2 :=
-- 
GitLab