chore: extends Membership (#47)

Author: astrainfinita

Algorithm/Data/Classes/Bag.lean

@@ -21,6 +21,7 @@ variable {C α : Type*} [Bag.ReadOnly C α] (c : C)
 attribute [local instance] Bag.ReadOnly.decidableMem in
 instance : MultiBag.ReadOnly C α where
   count a c := if a ∈ c then 1 else 0
-  count_eq_count_toMultiset a c := by symm; convert Multiset.count_eq_of_nodup (nodup_toMultiset c)
+  count_eq_count_toMultiset a c := by
+    simp [Multiset.count_eq_of_nodup (nodup_toMultiset c)]
 
 end Bag.ReadOnly

Algorithm/Data/Classes/IndexedMinHeap.lean

@@ -192,10 +192,9 @@ def mk [DecidableEq α] (assocArray : C) (minHeap : C')
       simpa [h, size_eq_card_toMultiset, Multiset.card_erase_lt_of_mem, - MinHeap.head_def] using
         Multiset.card_erase_lt_of_mem (MinHeap.head_mem_toMultiset _ _)
     mk assocArray (MinHeap.tail minHeap) fun i hi ↦ by
-      simp? [ToMultiset.mem_iff, h] says
-        simp only [ToMultiset.mem_iff, MinHeap.toMultiset_tail, h, Bool.false_eq_true, ↓reduceDIte,
-          MinHeap.head_def]
-      rw [Multiset.mem_erase_of_ne]
+      simp only [← mem_toMultiset, MinHeap.toMultiset_tail, h, Bool.false_eq_true, ↓reduceDIte,
+        MinHeap.head_def]
+      rw [Multiset.mem_erase_of_ne, mem_toMultiset]
       · exact mem_minHeap _ _
       · intro h''
         apply h'
@@ -238,7 +237,8 @@ instance [DecidableEq α] :
           rw [ite_eq_left_iff, Classical.not_imp] at hj
           simp only [hj.1, ↓reduceIte]
           exact c.mem_minHeap j hj.2
-        · rw [ToMultiset.mem_iff, toMultiset_insert, Multiset.mem_cons]
+        · -- TODO: `mem_insert`
+          rw [← mem_toMultiset, toMultiset_insert, Multiset.mem_cons, mem_toMultiset]
           split_ifs at hj ⊢ with hji
           · simp [hji]
           · exact .inr <| c.mem_minHeap j hj

Algorithm/Data/Classes/ToFinset.lean

@@ -6,10 +6,16 @@ Authors: Yuyang Zhao
 import Algorithm.Data.Classes.ToMultiset
 import Mathlib.Data.Finset.Card
 
-class ToFinset (C : Type*) (α : outParam Type*) extends Size C where
+variable {C α : Type*}
+
+class ToFinset (C : Type*) (α : outParam Type*) extends Membership α C, Size C where
   toFinset : C → Finset α
+  mem c a := a ∈ toFinset c
+  mem_toFinset {x c} : x ∈ toFinset c ↔ x ∈ c := by rfl
   size_eq_card_toFinset c : size c = (toFinset c).card
-export ToFinset (toFinset size_eq_card_toFinset)
+export ToFinset (toFinset mem_toFinset size_eq_card_toFinset)
+
+attribute [simp] mem_toFinset
 
 class ToFinset.LawfulInsert (C : Type*) (α : outParam Type*)
     [ToFinset C α] [Insert α C] : Prop where
@@ -18,38 +24,31 @@ export ToFinset.LawfulInsert (toFinset_insert)
 
 attribute [simp] toFinset_insert
 
-section
-variable {α : Type*}
-
 section ToFinset
-variable {C α : Type*} [ToFinset C α] (c : C)
 
-instance (priority := 100) ToFinset.toMultiset : ToMultiset C α where
+variable [ToFinset C α] (c : C)
+
+instance (priority := 100) ToFinset.toToMultiset : ToMultiset C α where
   toMultiset c := (toFinset c).val
+  mem_toMultiset := mem_toFinset
   size_eq_card_toMultiset c := size_eq_card_toFinset c
 
 section LawfulEmptyCollection
 variable [EmptyCollection C]
 
-lemma ToFinset.lawfulEmptyCollection_iff :
+lemma lawfulEmptyCollection_iff_toFinset :
     LawfulEmptyCollection C α ↔ toFinset (∅ : C) = ∅ := by
-  rw [ToMultiset.lawfulEmptyCollection_iff]
-  change (toFinset (∅ : C)).val = ∅ ↔ _
-  simp
+  simp_rw [lawfulEmptyCollection_iff, Finset.eq_empty_iff_forall_not_mem, mem_toFinset]
 
-alias ⟨_, LawfulEmptyCollection.ofToFinset⟩ := ToFinset.lawfulEmptyCollection_iff
+alias ⟨_, LawfulEmptyCollection.of_toFinset⟩ := lawfulEmptyCollection_iff_toFinset
 
 @[simp]
-lemma toFinset_empty [inst : LawfulEmptyCollection C α] :
+lemma toFinset_empty [LawfulEmptyCollection C α] :
     toFinset (∅ : C) = ∅ := by
-  rwa [ToFinset.lawfulEmptyCollection_iff] at inst
+  rwa [← lawfulEmptyCollection_iff_toFinset]
 
 end LawfulEmptyCollection
 
-lemma ToFinset.mem_iff {c : C} {v : α} : v ∈ c ↔ v ∈ toFinset c := .rfl
-
-lemma mem_toFinset {c : C} {v : α} : v ∈ toFinset c ↔ v ∈ c := .rfl
-
 @[simp]
 lemma toFinset_val : (toFinset c).val = toMultiset c := rfl
 

Algorithm/Data/Classes/ToList.lean

@@ -77,36 +77,52 @@ lemma dropLast_toList : a.toList.dropLast = a.pop.toList := by
 
 end Array
 
-class ToList (C : Type*) (α : outParam Type*) extends Size C where
+class ToList (C : Type*) (α : outParam Type*) extends Membership α C, Size C where
   toList : C → List α
   toArray : C → Array α
   toArray_eq_mk_toList a : toArray a = Array.mk (toList a)
+  mem c a := a ∈ toList c
+  mem_toList {x c} : x ∈ toList c ↔ x ∈ c := by rfl
   size_eq_length_toList c : size c = (toList c).length
-export ToList (toList toArray toArray_eq_mk_toList size_eq_length_toList)
+export ToList (toList toArray toArray_eq_mk_toList mem_toList size_eq_length_toList)
 
-attribute [simp] toArray_eq_mk_toList
+attribute [simp] toArray_eq_mk_toList mem_toList
 
 section ToList
+
+instance : ToList (List α) α where
+  toList := id
+  toArray := Array.mk
+  toArray_eq_mk_toList _ := rfl
+  size_eq_length_toList _ := rfl
+
+instance : ToList (Array α) α where
+  toList := Array.toList
+  toArray := id
+  toArray_eq_mk_toList _ := rfl
+  mem_toList := Array.mem_def.symm
+  size_eq_length_toList _ := rfl
+
 variable [ToList C α]
 
-instance (priority := 100) ToList.toMultiset : ToMultiset C α where
+instance (priority := 100) ToList.toToMultiset : ToMultiset C α where
   toMultiset c := ↑(toList c)
+  mem_toMultiset := mem_toList
   size_eq_card_toMultiset c := size_eq_length_toList c
 
 section LawfulEmptyCollection
 variable [EmptyCollection C]
 
-lemma ToList.lawfulEmptyCollection_iff :
+lemma lawfulEmptyCollection_iff_toList :
     LawfulEmptyCollection C α ↔ toList (∅ : C) = [] := by
-  rw [ToMultiset.lawfulEmptyCollection_iff]
-  simp [toMultiset]
+  simp_rw [lawfulEmptyCollection_iff, List.eq_nil_iff_forall_not_mem, mem_toList]
 
-alias ⟨_, LawfulEmptyCollection.ofToList⟩ := ToList.lawfulEmptyCollection_iff
+alias ⟨_, LawfulEmptyCollection.of_toList⟩ := lawfulEmptyCollection_iff_toList
 
 @[simp]
-lemma toList_empty [inst : LawfulEmptyCollection C α] :
+lemma toList_empty [LawfulEmptyCollection C α] :
     toList (∅ : C) = [] := by
-  rwa [ToList.lawfulEmptyCollection_iff] at inst
+  rwa [← lawfulEmptyCollection_iff_toList]
 
 end LawfulEmptyCollection
 
@@ -127,11 +143,6 @@ lemma coe_toList : ↑(toList c) = toMultiset c := rfl
 lemma isEmpty_toList : (toList c).isEmpty = isEmpty c := by
   rw [isEmpty_eq_decide_size, List.isEmpty_eq_decide_length, size_eq_length_toList]
 
-lemma ToList.mem_iff {c : C} {v : α} : v ∈ c ↔ v ∈ toList c := .rfl
-
-@[simp]
-lemma mem_toList {c : C} {v : α} : v ∈ toList c ↔ v ∈ c := .rfl
-
 end ToList
 
 class Front (C : Type*) (α : outParam Type*) [ToList C α] where
@@ -235,12 +246,6 @@ end ToList
 
 section List
 
-instance : ToList (List α) α where
-  toList := id
-  toArray := Array.mk
-  toArray_eq_mk_toList _ := rfl
-  size_eq_length_toList _ := rfl
-
 instance : Front (List α) α where
   front? := List.head?
   front?_def _ := rfl
@@ -264,12 +269,6 @@ end List
 
 section Array
 
-instance : ToList (Array α) α where
-  toList := Array.toList
-  toArray := id
-  toArray_eq_mk_toList _ := rfl
-  size_eq_length_toList _ := rfl
-
 instance : Front (Array α) α where
   front? c := c.get? 0
   front?_def c := by

Algorithm/Data/Classes/ToMultiset.lean

@@ -6,18 +6,22 @@ Authors: Yuyang Zhao
 import Algorithm.Data.Classes.Size
 import Mathlib.Data.Multiset.Basic
 
-class ToMultiset (C : Type*) (α : outParam Type*) extends Size C where
-  toMultiset : C → Multiset α
-  size_eq_card_toMultiset c : size c = Multiset.card (toMultiset c)
-export ToMultiset (toMultiset size_eq_card_toMultiset)
+variable {C α : Type*}
 
-@[mk_iff ToMultiset.lawfulEmptyCollection_iff]
+@[mk_iff]
 class LawfulEmptyCollection (C : Type*) (α : outParam Type*)
-    [ToMultiset C α] [EmptyCollection C] : Prop where
-  toMultiset_empty : toMultiset (∅ : C) = 0
-export LawfulEmptyCollection (toMultiset_empty)
+    [Membership α C] [EmptyCollection C] : Prop where
+  not_mem_empty (x : α) : x ∉ (∅ : C)
+export LawfulEmptyCollection (not_mem_empty)
+
+class ToMultiset (C : Type*) (α : outParam Type*) extends Membership α C, Size C where
+  toMultiset : C → Multiset α
+  mem c a := a ∈ toMultiset c
+  mem_toMultiset {x c} : x ∈ toMultiset c ↔ x ∈ c := by rfl
+  size_eq_card_toMultiset c : size c = Multiset.card (toMultiset c)
+export ToMultiset (toMultiset mem_toMultiset size_eq_card_toMultiset)
 
-attribute [simp] toMultiset_empty
+attribute [simp] mem_toMultiset
 
 class ToMultiset.LawfulInsert (C : Type*) (α : outParam Type*)
     [ToMultiset C α] [Insert α C] : Prop where
@@ -26,42 +30,51 @@ export ToMultiset.LawfulInsert (toMultiset_insert)
 
 attribute [simp] toMultiset_insert
 
-section
-variable {α : Type*}
+section ToMultiset
 
 instance : ToMultiset (List α) α where
   toMultiset := (↑)
+  mem_toMultiset := .rfl
   size_eq_card_toMultiset _ := rfl
 
 instance : ToMultiset (Array α) α where
   toMultiset c := ↑c.toList
+  mem_toMultiset := Array.mem_def.symm
   size_eq_card_toMultiset _ := by simp [size]
 
-section ToMultiset
-variable {C α : Type*} [ToMultiset C α] (c : C)
+variable [ToMultiset C α]
 
-instance (priority := 100) : Membership α C where
-  mem c a := a ∈ toMultiset c
+section LawfulEmptyCollection
+variable [EmptyCollection C]
 
-lemma ToMultiset.mem_iff {c : C} {v : α} : v ∈ c ↔ v ∈ toMultiset c := .rfl
+lemma lawfulEmptyCollection_iff_toMultiset :
+    LawfulEmptyCollection C α ↔ toMultiset (∅ : C) = 0 := by
+  simp_rw [lawfulEmptyCollection_iff, Multiset.eq_zero_iff_forall_not_mem, mem_toMultiset]
+
+alias ⟨_, LawfulEmptyCollection.of_toMultiset⟩ := lawfulEmptyCollection_iff_toMultiset
+
+@[simp]
+lemma toMultiset_empty [LawfulEmptyCollection C α] :
+    toMultiset (∅ : C) = 0 := by
+  rwa [← lawfulEmptyCollection_iff_toMultiset]
 
-lemma mem_toMultiset {c : C} {v : α} : v ∈ toMultiset c ↔ v ∈ c := .rfl
+end LawfulEmptyCollection
 
 @[simp]
-lemma toMultiset_of_isEmpty (h : isEmpty c) : toMultiset c = 0 := by
+lemma toMultiset_of_isEmpty {c : C} (h : isEmpty c) : toMultiset c = 0 := by
   simpa [size_eq_card_toMultiset] using h
 
 @[simp]
 lemma toMultiset_list (l : List α) : toMultiset l = ↑l := rfl
 
 @[simp]
-lemma ToMultiset.not_isEmpty_of_mem {c : C} {v} (hv : v ∈ c) : ¬isEmpty c := by
-  simpa [size_eq_card_toMultiset, Multiset.eq_zero_iff_forall_not_mem] using ⟨v, hv⟩
+lemma ToMultiset.not_isEmpty_of_mem {c : C} {x} (hx : x ∈ c) : ¬isEmpty c := by
+  simpa [size_eq_card_toMultiset, Multiset.eq_zero_iff_forall_not_mem] using ⟨x, hx⟩
 
 variable [DecidableEq α]
 
-theorem count_toMultiset_eq_zero {a : α} {c : C} : (toMultiset c).count a = 0 ↔ a ∉ c :=
-  Multiset.count_eq_zero
+theorem count_toMultiset_eq_zero {a : α} {c : C} : (toMultiset c).count a = 0 ↔ a ∉ c := by
+  simp
 
 theorem count_toMultiset_ne_zero {a : α} {c : C} : (toMultiset c).count a ≠ 0 ↔ a ∈ c := by
   simp [count_toMultiset_eq_zero, mem_toMultiset]

Algorithm/Data/PairingHeap.lean

@@ -180,8 +180,8 @@ instance : ToMultiset (PairingHeap α le) α where
 instance : EmptyCollection (PairingHeap α le) where
   emptyCollection := empty
 
-instance : LawfulEmptyCollection (PairingHeap α le) α where
-  toMultiset_empty := rfl
+instance : LawfulEmptyCollection (PairingHeap α le) α :=
+  .of_toMultiset rfl
 
 @[simp]
 lemma size_eq_zero_iff (x : PairingHeap α le) : x.size = 0 ↔ x = ∅ := by
@@ -213,12 +213,12 @@ instance [Preorder α] [IsTotal α (· ≤ ·)] [DecidableRel (α := α) (· ≤
     simp only [isEmpty_iff_size_eq_zero] at hx
     match x, hx with
     | ⟨.node a c .nil, _⟩, _ =>
-      simpa using ⟨a, by
+      simpa [- mem_toMultiset] using ⟨a, by
         simp [toMultiset, toListUnordered, PairingHeapImp.Heap.toListUnordered_node], rfl⟩
   head?_le x b hb := by
     match x with
     | ⟨.node a c .nil, hwf⟩ =>
-      simp_rw [ToMultiset.mem_iff, toMultiset, toListUnordered,
+      simp_rw [← mem_toMultiset, toMultiset, toListUnordered,
         PairingHeapImp.Heap.toListUnordered_node, PairingHeapImp.Heap.toListUnordered_nil,
         List.append_nil, ← Multiset.cons_coe, Multiset.mem_cons] at hb
       obtain (rfl | hb) := hb; · rfl

Algorithm/Graph/Dijkstra.lean

@@ -445,8 +445,9 @@ lemma dijkstraStep_fst_getElem' (g : G) (c : Info → CostType)
   split_ifs with h
   · simp? [Function.update_apply] says
       simp only [Function.update_apply, min_eq_top, ite_eq_left_iff, Multiset.inf_eq_top,
-        Multiset.mem_filterMap, Option.ite_none_right_eq_some, Option.some.injEq, Prod.exists,
-        Prod.mk.injEq, exists_eq_right_right, exists_eq_right, forall_exists_index, and_imp]
+        Multiset.mem_filterMap, mem_toMultiset, Option.ite_none_right_eq_some, Option.some.injEq,
+        Prod.exists, Prod.mk.injEq, exists_eq_right_right, exists_eq_right, forall_exists_index,
+        and_imp]
     use fun hv ↦ (spec₁ v).resolve_right (h.resolve_left hv)
     rintro - e - h' ⟨rfl⟩ ⟨rfl⟩
     split_ifs at h' with snde
@@ -482,8 +483,9 @@ lemma dijkstraStep_fst_getElem (g : G) (c : Info → CostType)
   apply Multiset.inf_congr
   intro d
   simp? says
-    simp only [Multiset.mem_dedup, Multiset.mem_filterMap, Option.ite_none_right_eq_some,
-      Option.some.injEq, Multiset.mem_map, Finset.mem_val, Finset.mem_univ, true_and]
+    simp only [Multiset.mem_dedup, Multiset.mem_filterMap, mem_toMultiset,
+      Option.ite_none_right_eq_some, Option.some.injEq, Multiset.mem_map, Finset.mem_val,
+      Finset.mem_univ, true_and]
   constructor
   · rintro ⟨x, hx, rfl, rfl, rfl⟩
     exact ⟨homOfStar x hx, rfl⟩