From 7363e2ccc1c19196e46755349e169ded7cf3fdf9 Mon Sep 17 00:00:00 2001
From: Dmitry Khalanskiy <Dmitry.Khalanskiy@jetbrains.com>
Date: Tue, 21 Jan 2020 16:21:51 +0300
Subject: [PATCH] Add list_lookup_singletonM_{lt,gt}

`list_lookup_singletonM_ne` is not sufficient when we need to
compare a singleton with another list, for example, to see if one
is included in the other.
---
 theories/algebra/list.v | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index 669500516..b1685f2eb 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -363,6 +363,12 @@ Section properties.
   Qed.
   Lemma list_lookup_singletonM i x : ({[ i := x ]} : list A) !! i = Some x.
   Proof. induction i; by f_equal/=. Qed.
+  Lemma list_lookup_singletonM_lt i i' x:
+    (i' < i)%nat → ({[ i := x ]} : list A) !! i' = Some ε.
+  Proof. move: i'. induction i; intros [|i']; naive_solver auto with lia. Qed.
+  Lemma list_lookup_singletonM_gt i i' x:
+    (i < i')%nat → ({[ i := x ]} : list A) !! i' = None.
+  Proof. move: i'. induction i; intros [|i']; naive_solver auto with lia. Qed.
   Lemma list_lookup_singletonM_ne i j x :
     i ≠ j →
     ({[ i := x ]} : list A) !! j = None ∨ ({[ i := x ]} : list A) !! j = Some ε.
-- 
GitLab