diff --git a/Invariant.lean b/Invariant.lean
index c298ab1..edb75cf 100644
--- a/Invariant.lean
+++ b/Invariant.lean
@@ -1,20 +1,116 @@
-inductive StrictlyIncreasing : List Nat → Prop
-| empty : StrictlyIncreasing []
-| singleton : StrictlyIncreasing [x]
-| cons : (∀a, a ∈ xs → a > x) → StrictlyIncreasing xs → StrictlyIncreasing (x::xs)
+import Mathlib.Data.List.Sort
--- sorted set of natural numbers
-abbrev NatSet := { xs : List Nat // StrictlyIncreasing xs }
+abbrev NatSet := { xs : List ℕ // List.Sorted (·<·) xs }
namespace NatSet
-def empty : NatSet := ⟨[], .empty⟩
-def singleton (x : Nat) : NatSet := ⟨[x], .singleton⟩
+def empty : NatSet := ⟨[], List.sorted_nil⟩
+def singleton (x : ℕ) : NatSet := ⟨[x], List.sorted_singleton x⟩
-def remove (x : Nat) : NatSet → NatSet
+def remove (x : ℕ) : NatSet → NatSet
| ⟨[], _⟩ => empty
-| ⟨a::xs, h⟩ =>
- let tail := ⟨xs, by simp⟩
- if a = x then tail
+| ⟨n::ns, h⟩ =>
+ let tail := ⟨ns, List.Sorted.of_cons h⟩
+ if n = x
+ then tail
+ else ⟨n::tail, h⟩
+
+def list_insert (x : ℕ) : List ℕ → List ℕ
+| [] => [x]
+| a::as =>
+ if x = a
+ then as
+ else if x < a
+ then x::a::as
+ else a::(list_insert x as)
+
+theorem list_insert_mem : b ∈ list_insert x xs → b = x ∨ b ∈ xs := by
+ induction xs with simp [list_insert]
+ | cons a as ih =>
+ split
+ next heq =>
+ intro hmem
+ right; right
+ assumption
+ next hne =>
+ split
+ · simp
+ · 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
+ induction xs with simp [list_insert]
+ | cons a as ih =>
+ split
+ · exact List.Sorted.of_cons hs
+ · split
+ · rename_i hnlt
+ exact List.Sorted.cons hnlt hs
+
+ have : a < x := by
+ rename_i hne hnlt
+ apply Nat.lt_of_le_of_ne
+ exact Nat.le_of_not_lt hnlt
+ exact fun a_1 => hne (Eq.symm a_1)
+
+ have h : List.Sorted (·<·) as := List.Sorted.of_cons hs
+
+ have := ih h
+ sorry
+
+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
- ⟨a::xs, h⟩
+ 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
+
+ ⟩
+
+instance : EmptyCollection NatSet where
+ emptyCollection := empty
+
+instance : Singleton ℕ NatSet where
+ singleton := singleton
+
+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]
diff --git a/lake-manifest.json b/lake-manifest.json
index f08e15f..3fb7027 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,7 +1,77 @@
{"version": "1.1.0",
"packagesDir": ".lake/packages",
"packages":
- [{"url": "https://github.com/leanprover-community/batteries",
+ [{"url": "https://github.com/leanprover-community/mathlib4",
+ "type": "git",
+ "subDir": null,
+ "scope": "leanprover-community",
+ "rev": "37f686cf27093bcbde5a9eb2f1519ef730de1828",
+ "name": "mathlib",
+ "manifestFile": "lake-manifest.json",
+ "inputRev": "master",
+ "inherited": false,
+ "configFile": "lakefile.lean"},
+ {"url": "https://github.com/leanprover-community/plausible",
+ "type": "git",
+ "subDir": null,
+ "scope": "leanprover-community",
+ "rev": "4dfba8b20a5ce570b9ef8bae969dd163782f9793",
+ "name": "plausible",
+ "manifestFile": "lake-manifest.json",
+ "inputRev": "nightly-testing",
+ "inherited": true,
+ "configFile": "lakefile.toml"},
+ {"url": "https://github.com/leanprover-community/LeanSearchClient",
+ "type": "git",
+ "subDir": null,
+ "scope": "leanprover-community",
+ "rev": "8d29bc2c3ebe1f863c2f02df816b4f3dd1b65226",
+ "name": "LeanSearchClient",
+ "manifestFile": "lake-manifest.json",
+ "inputRev": "main",
+ "inherited": true,
+ "configFile": "lakefile.toml"},
+ {"url": "https://github.com/leanprover-community/import-graph",
+ "type": "git",
+ "subDir": null,
+ "scope": "leanprover-community",
+ "rev": "c20832d6f0b3186a97ea9361cec0a5b87dd152a3",
+ "name": "importGraph",
+ "manifestFile": "lake-manifest.json",
+ "inputRev": "main",
+ "inherited": true,
+ "configFile": "lakefile.toml"},
+ {"url": "https://github.com/leanprover-community/ProofWidgets4",
+ "type": "git",
+ "subDir": null,
+ "scope": "leanprover-community",
+ "rev": "ea953247aac573c9b5adea60bacd3e085f58aca4",
+ "name": "proofwidgets",
+ "manifestFile": "lake-manifest.json",
+ "inputRev": "v0.0.56",
+ "inherited": true,
+ "configFile": "lakefile.lean"},
+ {"url": "https://github.com/leanprover-community/aesop",
+ "type": "git",
+ "subDir": null,
+ "scope": "leanprover-community",
+ "rev": "57185dfad68d78356f9462af984882d6f262aa5d",
+ "name": "aesop",
+ "manifestFile": "lake-manifest.json",
+ "inputRev": "master",
+ "inherited": true,
+ "configFile": "lakefile.toml"},
+ {"url": "https://github.com/leanprover-community/quote4",
+ "type": "git",
+ "subDir": null,
+ "scope": "leanprover-community",
+ "rev": "aa4c87abed970d9dfad2506000d99d30b02f476b",
+ "name": "Qq",
+ "manifestFile": "lake-manifest.json",
+ "inputRev": "master",
+ "inherited": true,
+ "configFile": "lakefile.toml"},
+ {"url": "https://github.com/leanprover-community/batteries",
"type": "git",
"subDir": null,
"scope": "leanprover-community",
@@ -10,6 +80,16 @@
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": false,
+ "configFile": "lakefile.toml"},
+ {"url": "https://github.com/leanprover/lean4-cli",
+ "type": "git",
+ "subDir": null,
+ "scope": "leanprover",
+ "rev": "aff4176e5c41737a0d73be74ad9feb6a889bfa98",
+ "name": "Cli",
+ "manifestFile": "lake-manifest.json",
+ "inputRev": "main",
+ "inherited": true,
"configFile": "lakefile.toml"}],
"name": "invariant",
"lakeDir": ".lake"}
diff --git a/lakefile.toml b/lakefile.toml
index 4db9bc3..bd78094 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -4,3 +4,7 @@ defaultTargets = ["Invariant"]
[[lean_lib]]
name = "Invariant"
+
+[[require]]
+name = "mathlib"
+scope = "leanprover-community"
diff --git a/lean-toolchain b/lean-toolchain
index c7e245c..9565de3 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.19.0-rc2
\ No newline at end of file
+leanprover/lean4:v4.19.0-rc2