From fd519401ff408b71fcb2eba230b231898065cf91 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 3 Mar 2022 17:19:22 -0800
Subject: [PATCH] feat: add `Membership` instance for `List`
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

and the theorem `a ∈ as -> sizeOf a < sizeOf as`.
We will use theorems like this one to improve the `decreasing_tactic`.
---
 src/Init/Data/List/Basic.lean    | 24 ++++++++++++++++++++++++
 src/Init/Data/List/BasicAux.lean |  3 +++
 src/Init/SimpLemmas.lean         |  1 +
 3 files changed, 28 insertions(+)

diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index 5e84bff599..55e359f218 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -212,6 +212,30 @@ def notElem [BEq α] (a : α) (as : List α) : Bool :=
 abbrev contains [BEq α] (as : List α) (a : α) : Bool :=
   elem a as
 
+inductive Mem : α → List α → Prop
+  | head (a : α) (as : List α) : Mem a (a::as)
+  | tail (a : α) {b : α} {as : List α} : Mem b as → Mem b (a::as)
+
+instance : Membership α (List α) where
+  mem := Mem
+
+theorem mem_of_elem_eq_true [DecidableEq α] {a : α} {as : List α} : elem a as = true → a ∈ as := by
+  match as with
+  | [] => simp [elem]
+  | a'::as =>
+    simp [elem]
+    split
+    next h => intros; simp [BEq.beq] at h; subst h; apply Mem.head
+    next _ => intro h; exact Mem.tail _ (mem_of_elem_eq_true h)
+
+theorem elem_eq_true_of_mem [DecidableEq α] {a : α} {as : List α} (h : a ∈ as) : elem a as = true := by
+  induction h with
+  | head _ => simp [elem]
+  | tail _ h ih => simp [elem]; split; rfl; assumption
+
+instance [DecidableEq α] (a : α) (as : List α) : Decidable (a ∈ as) :=
+  decidable_of_decidable_of_iff (Iff.intro mem_of_elem_eq_true elem_eq_true_of_mem)
+
 def eraseDupsAux {α} [BEq α] : List α → List α → List α
   | [],    bs => bs.reverse
   | a::as, bs => match bs.elem a with
diff --git a/src/Init/Data/List/BasicAux.lean b/src/Init/Data/List/BasicAux.lean
index bc91cb8fa5..d45c1acccb 100644
--- a/src/Init/Data/List/BasicAux.lean
+++ b/src/Init/Data/List/BasicAux.lean
@@ -116,4 +116,7 @@ theorem get_last {as : List α} {i : Fin (length (as ++ [a]))} (h : ¬ i.1 < as.
     cases i with simp_arith at h
     | succ i => apply ih; simp_arith [h]
 
+theorem sizeOf_lt_of_mem {as : List α} (h : a ∈ as) : sizeOf a < sizeOf as := by
+  cases h <;> simp_arith
+
 end List
diff --git a/src/Init/SimpLemmas.lean b/src/Init/SimpLemmas.lean
index 3971477f9a..7f396dfa2c 100644
--- a/src/Init/SimpLemmas.lean
+++ b/src/Init/SimpLemmas.lean
@@ -154,3 +154,4 @@ theorem dite_congr {s : Decidable b} [Decidable c]
 @[simp] theorem cond_false (a b : α) : cond false a b = b := rfl
 
 @[simp] theorem beq_self_eq_true [BEq α] [LawfulBEq α] (a : α) : (a == a) = true := LawfulBEq.rfl a
+@[simp] theorem beq_self_eq_true' [DecidableEq α] (a : α) : (a == a) = true := by simp [BEq.beq]