NatSet.mem_insert

Invariant.lean

@@ -88,15 +88,37 @@ instance : Membership ℕ NatSet where
 instance (n : ℕ) (s : NatSet) : Decidable (n ∈ s) :=
   List.instDecidableMemOfLawfulBEq n (s.val.takeWhile (· ≤ n))
 
--- TODO: (tricky!)
-theorem mem_insert (x : ℕ) (s : NatSet) : x ∈ s.insert x := by
-  sorry
+theorem mem_insert_cons (hmem : x ∈ insert x ⟨ns, h₁⟩)
+    : x ∈ insert x ⟨n::ns, h₂⟩ := by
+  induction ns
+  <;> (
+    simp only [Membership.mem, insert, list_insert]
+    split
+    next heq =>
+      simp [heq]
+      exact List.Mem.head _
+    next hne =>
+      split
+      · simp
+        exact List.Mem.head ..
+      next hnlt =>
+        have hle : n ≤ x := by simp at hnlt; assumption
+        simp only [List.takeWhile, hle, decide_true, le_refl]
+        apply List.Mem.tail n
+        try exact List.Mem.head []
+        try exact hmem
+  )
 
-#eval 3 ∈ ({1, 2, 3} : NatSet)
-#eval 3 ∈ ({1, 2} : NatSet)
-#eval 3 ∈ ({} : NatSet)
-#eval ({1, 2} : NatSet) == {3, 4}
-#eval ({2, 2, 3, 4} : NatSet) == {4, 3, 2}
-#eval ({2, 2, 3, 4} : NatSet)
+theorem mem_insert (x : ℕ) (s : NatSet) : x ∈ s.insert x := by
+  let ⟨xs, h⟩ := s
+  induction xs with
+  | nil =>
+    simp [Membership.mem, insert, list_insert, List.Mem.head]
+  | cons a as ih =>
+    rw [List.sorted_cons] at h
+    have hmem := ih h.right
+    exact mem_insert_cons hmem
+
+-- TODO: set operation instances
 
 end NatSet