From 349457177de56ac95d55670fceb24334cb9973b1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 12 Jan 2022 16:40:29 +0100
Subject: [PATCH] Shorten proof and make lemma name consistent.

---
 theories/list.v | 14 ++------------
 1 file changed, 2 insertions(+), 12 deletions(-)

diff --git a/theories/list.v b/theories/list.v
index fb2339c8..8fe36bb0 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -1971,19 +1971,9 @@ Section filter.
     intros [k ->]%elem_of_Permutation ?; simpl.
     rewrite decide_False, Nat.lt_succ_r by done. apply filter_length.
   Qed.
-  Lemma not_elem_of_filter_nil `{EqDecision A} l x :
-    filter P l = [] → P x → x ∉ l.
-  Proof.
-    intros Hfilter HP Hin.
-    induction l as [|y l IHl]; [by inversion Hin|].
-    destruct (decide (x = y)) as [<-|Hneq].
-    { by rewrite filter_cons_True in Hfilter. }
-    apply elem_of_cons in Hin.
-    destruct Hin as [<-|Hin]; [done|].
-    destruct (decide (P y)); [by rewrite filter_cons_True in Hfilter|].
-    apply IHl; [|done]. by rewrite filter_cons_False in Hfilter.
-  Qed.
 
+  Lemma filter_nil_not_elem_of l x : filter P l = [] → P x → x ∉ l.
+  Proof. induction 3; simplify_eq/=; case_decide; naive_solver. Qed.
 End filter.
 
 Lemma list_filter_iff (P1 P2 : A → Prop)
-- 
GitLab