commit 592a4b45e6cb0515a024049849a064539dea31d4
Author: mehbark <terezi@pyrope.net>
Date:   Thu Apr 3 17:42:08 2025 -0400

    pairwise attempt

diff --git a/Invariant.lean b/Invariant.lean
new file mode 100644
index 0000000..f7b0335
--- /dev/null
+++ b/Invariant.lean
@@ -0,0 +1,47 @@
+-- sorted set of natural numbers
+structure NatSet where
+  items : List Nat
+  invariant : List.Pairwise (· < ·) items
+
+namespace NatSet
+
+-- TODO: binary search
+instance : Membership Nat NatSet where
+  mem l x := x ∈ l.items
+
+instance (x : Nat) (l : NatSet) : Decidable (x ∈ l) :=
+  List.instDecidableMemOfLawfulBEq x l.items
+
+def empty : NatSet := ⟨[], by simp⟩
+
+def singleton (x : Nat) : NatSet :=
+  ⟨[x], by simp⟩
+
+def remove (x : Nat) (l : NatSet) : NatSet where
+  items := l.items.erase x
+  invariant := List.Pairwise.erase x l.invariant
+
+def insert (x : Nat) : NatSet → NatSet
+| ⟨[], h⟩ => ⟨[x], List.pairwise_singleton ..⟩
+| l@⟨a::as, h⟩ =>
+  if a = x
+  then l
+  else if hlt : x < a
+  then ⟨
+    x::a::as,
+    by
+      apply List.pairwise_cons.mpr
+      constructor
+      · intro a' hmem
+        have := List.Pairwise.iff
+        sorry
+      · assumption
+  ⟩
+  else
+  let ⟨rest, hr⟩ := (NatSet.mk as (List.Pairwise.of_cons h)).insert x
+  ⟨
+    a::rest,
+    by
+      simp [*]
+      sorry,
+  ⟩
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..0548d4d
--- /dev/null
+++ b/README.md
@@ -0,0 +1 @@
+# invariant
\ No newline at end of file
diff --git a/lake-manifest.json b/lake-manifest.json
new file mode 100644
index 0000000..f08e15f
--- /dev/null
+++ b/lake-manifest.json
@@ -0,0 +1,15 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "ff4cd734811e5ab091cef2acb4d805737670eced",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.toml"}],
+ "name": "invariant",
+ "lakeDir": ".lake"}
diff --git a/lakefile.toml b/lakefile.toml
new file mode 100644
index 0000000..4db9bc3
--- /dev/null
+++ b/lakefile.toml
@@ -0,0 +1,6 @@
+name = "invariant"
+version = "0.1.0"
+defaultTargets = ["Invariant"]
+
+[[lean_lib]]
+name = "Invariant"
diff --git a/lean-toolchain b/lean-toolchain
new file mode 100644
index 0000000..c7e245c
--- /dev/null
+++ b/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.19.0-rc2
\ No newline at end of file