inductive attempt

Invariant.lean

@@ -1,47 +1,20 @@
+inductive StrictlyIncreasing : List Nat → Prop
+| empty     : StrictlyIncreasing []
+| singleton : StrictlyIncreasing [x]
+| cons : (∀a, a ∈ xs → a > x) → StrictlyIncreasing xs → StrictlyIncreasing (x::xs)
+
 -- sorted set of natural numbers
-structure NatSet where
+abbrev NatSet := { xs : List Nat // StrictlyIncreasing xs }
-  items : List Nat
-  invariant : List.Pairwise (· < ·) items
 
 namespace NatSet
 
--- TODO: binary search
+def empty : NatSet := ⟨[], .empty⟩
-instance : Membership Nat NatSet where
+def singleton (x : Nat) : NatSet := ⟨[x], .singleton⟩
-  mem l x := x ∈ l.items
 
-instance (x : Nat) (l : NatSet) : Decidable (x ∈ l) :=
+def remove (x : Nat) : NatSet → NatSet
-  List.instDecidableMemOfLawfulBEq x l.items
+| ⟨[], _⟩ => empty
-
+| ⟨a::xs, h⟩ =>
-def empty : NatSet := ⟨[], by simp⟩
+  let tail := ⟨xs, by simp⟩
-
+  if a = x then tail
-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::xs, h⟩
-  ⟨
-    a::rest,
-    by
-      simp [*]
-      sorry,
-  ⟩