NatSet.insert

Invariant.lean

@@ -19,7 +19,7 @@ def list_insert (x : ℕ) : List ℕ → List ℕ
 | [] => [x]
 | a::as =>
   if x = a
-  then as
+  then a::as
   else if x < a
   then x::a::as
   else a::(list_insert x as)
@@ -30,25 +30,25 @@ theorem list_insert_mem : b ∈ list_insert x xs → b = x ∨ b ∈ xs := by
     split
     next heq =>
       intro hmem
-      right; right
-      assumption
+      simp_all only [List.mem_cons, or_true]
     next hne =>
       split
       · simp
-      · next hnlt =>
-          simp [*]
-          intro h
-          cases h
-          · right; left; assumption
-          cases ih ‹_›
-          · left; assumption
-          · right; right; assumption
+      next hnlt =>
+        simp [*]
+        intro h
+        cases h
+        · right; left; assumption
+        cases ih ‹_›
+        · left; assumption
+        · right; right; assumption
 
-theorem list_insert_sorted (hs : List.Sorted (·<·) xs) : List.Sorted (·<·) (list_insert x xs) := by
+theorem list_insert_sorted (hs : List.Sorted (·<·) xs)
+    : List.Sorted (·<·) (list_insert x xs) := by
   induction xs with simp [list_insert]
   | cons a as ih =>
     split
-    · exact List.Sorted.of_cons hs
+    · simp_all only [List.sorted_cons, implies_true, and_self]
     · split
       · exact List.Sorted.cons ‹_› hs
       · have : a < x := by
@@ -65,43 +65,8 @@ theorem list_insert_sorted (hs : List.Sorted (·<·) xs) : List.Sorted (·<·) (
           <;> simp_all only [imp_self, List.sorted_cons, and_true, not_lt]
         · simp_all only [imp_self, List.sorted_cons, and_true, not_lt]
 
-def insert (x : ℕ) : NatSet → NatSet
-| ⟨[], _⟩ => singleton x
-| ⟨n::ns, h⟩ =>
-  if heq : x = n
-  then ⟨n::ns, h⟩
-  else if hlt : x < n
-  then ⟨x::n::ns, List.Sorted.cons hlt h⟩
-  else
-    let tail : NatSet := ⟨ns, List.Sorted.of_cons h⟩
-    let ⟨tail, h₂⟩ := tail.insert x
-    ⟨
-      n::tail,
-      by
-        have : ∀b ∈ tail, b = x ∨ b ∈ ns := by
-          intro b h
-          induction tail
-          · contradiction
-          · simp [*] at *
-
-            sorry
-        have : ∀b ∈ ns, n < b := by
-          simp only [List.sorted_cons] at h
-          exact h.left
-        simp only [List.sorted_cons]
-        constructor
-        · assumption
-
-        -- have : n < x := by
-        --   rw [Nat.lt_iff_le_and_ne]
-        --   constructor
-        --   · simp at hlt
-        --     assumption
-        --   · intro h
-        --     exact heq h.symm
-        sorry
-
-    ⟩
+def insert (x : ℕ) (s : NatSet) : NatSet :=
+  ⟨list_insert x s.val, list_insert_sorted s.prop⟩
 
 instance : EmptyCollection NatSet where
   emptyCollection := empty
@@ -113,5 +78,25 @@ instance : Insert ℕ NatSet where
   insert := insert
 
 instance : LawfulSingleton ℕ NatSet where
-  insert_empty_eq := by simp [Insert.insert, EmptyCollection.emptyCollection, empty, insert,
-    Singleton.singleton, implies_true]
+  insert_empty_eq := by intro; rfl
+
+instance : Membership ℕ NatSet where
+  -- this is still an optimization over typical list membership, but
+  -- TODO: binary search
+  mem s n := n ∈ s.val.takeWhile (· ≤ n)
+
+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
+
+#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)
+
+end NatSet

README.md

@@ -1 +1,3 @@
-# invariant
+# invariant
+basic examples of formally enforcing invariants in data structures, inspired by [`Batteries.dlist`](https://leanprover-community.github.io/mathlib4_docs/Batteries/Data/DList/Basic.html#Batteries.DList)'s `invariant` field.
+