list_insert_mem

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]

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"}

lakefile.toml

@@ -4,3 +4,7 @@ defaultTargets = ["Invariant"]
 
 [[lean_lib]]
 name = "Invariant"
+
+[[require]]
+name = "mathlib"
+scope = "leanprover-community"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.19.0-rc2
+leanprover/lean4:v4.19.0-rc2