Derive a more constructive `StepFunction` definition.

Common.lean

@@ -1,4 +1,5 @@
 import Common.Combinator
+import Common.Finset
 import Common.List
 import Common.Real
 import Common.Set

Common/Finset.lean

@@ -0,0 +1,17 @@
+import Mathlib.Data.Finset.Basic
+
+/-! # Common.Finset
+
+Additional theorems and definitions useful in the context of `Finset`s.
+-/
+
+namespace Finset
+
+/--
+An alternative `Finset.range` function that returns `Fin` indices instead of `ℕ`
+indices.
+-/
+def finRange (n : ℕ) : Finset (Fin n) :=
+  ⟨sorry, sorry⟩
+
+end Finset

Common/Geometry/Area.lean

@@ -1,5 +1,5 @@
 import Common.Geometry.Basic
-import Common.Geometry.Rectangle.Skew
+import Common.Geometry.Rectangle.Orthogonal
 import Common.Geometry.StepFunction
 
 /-! # Common.Geometry.Area

Common/Geometry/Rectangle/Orthogonal.lean

@@ -46,6 +46,13 @@ The bottom-right corner of the `Orthogonal` rectangle.
 -/
 def br (r : Orthogonal) : Point := ⟨r.bl.x + r.width, r.bl.y⟩
 
+/--
+The `Set` of `Point`s enclosed in the region determined by the edges of the
+`Orthogonal` rectangle. Edges of the rectangle are included in the result set.
+-/
+def toSet (r : Orthogonal) : Set Point :=
+  { p | r.bl.x ≤ p.x ∧ p.x ≤ r.br.x ∧ r.bl.y ≤ p.y ∧ p.y ≤ r.tl.y }
+
 /--
 An `Orthogonal` rectangle's top side is equal in length to its bottom side.
 -/

Common/Geometry/StepFunction.lean

@@ -1,4 +1,7 @@
+import Common.Finset
 import Common.Geometry.Point
+import Common.Geometry.Rectangle.Orthogonal
+import Common.List.Basic
 import Common.Set.Partition
 
 /-! # Common.Geometry.StepFunction
@@ -14,20 +17,24 @@ open Set Partition
 A function `f`, whose domain is a closed interval `[a, b]`, is a `StepFunction`
 if there exists a `Partition` `P = {x₀, x₁, …, xₙ}` of `[a, b]` such that `f` is
 constant on each open subinterval of `P`.
+
+Instead of maintaining a function from `[a, b]` to `ℝ`, we instead maintain a
+function that maps each `Partition` index to some constant value. 
 -/
 structure StepFunction where
   p : Partition ℝ
-  toFun : ∀ x ∈ p.toIcc, ℝ
+  toFun : Fin p.ivls.length → ℝ
-  const_open_subintervals :
-    ∀ (hI : I ∈ p.openSubintervals), ∃ c, ∀ (hy : y ∈ I),
-      toFun y (mem_open_subinterval_mem_closed_interval hI hy) = c
 
 namespace StepFunction
 
 /--
-The ordinate set of the function.
+The ordinate set of the `StepFunction`.
 -/
-def toSet (s : StepFunction) : Set Point := sorry
+def toSet (sf : StepFunction) : Set Point :=
+  ⋃ i ∈ Finset.finRange sf.p.ivls.length,
+    let I := sf.p.ivls[i]
+    Rectangle.Orthogonal.toSet
+      ⟨{ x := I.left, y := 0 }, { x := I.right, y := sf.toFun i }⟩
 
 end StepFunction
 

Common/List.lean

@@ -1 +1,2 @@
 import Common.List.Basic
+import Common.List.NonEmpty

Common/List/NonEmpty.lean

@@ -0,0 +1,81 @@
+import Mathlib.Algebra.Group.Defs
+import Mathlib.Data.Nat.Basic
+import Mathlib.Tactic.NormNum
+
+/-! # Common.List.NonEmpty
+
+A `List` with at least one member.
+-/
+
+namespace List
+
+structure NonEmpty (α : Type _) : Type _ where
+  head : α
+  tail : List α
+
+instance : Coe (NonEmpty α) (List α) where
+  coe (xs : NonEmpty α) := xs.head :: xs.tail
+
+instance : CoeDep (List α) (cons x xs : List α) (NonEmpty α) where
+  coe := { head := x, tail := xs }
+
+namespace NonEmpty
+
+/--
+The length of a `List.NonEmpty`.
+-/
+def length (xs : NonEmpty α) : Nat := 1 + xs.tail.length
+
+/--
+The length of a `List.NonEmpty` is always one plus the length of its tail.
+-/
+theorem length_self_eq_one_add_length_tail (xs : NonEmpty α)
+  : xs.length = 1 + xs.tail.length := rfl
+
+/--
+A proof that an index is within the bounds of the `List.NonEmpty`.
+-/
+abbrev inBounds (xs : NonEmpty α) (i : Nat) : Prop :=
+  i < xs.length
+
+/--
+Retrieves the member of the `List.NonEmpty` at the specified index.
+-/
+def get (xs : NonEmpty α) : (i : Nat) → (h : xs.inBounds i) → α
+  | 0, _ => xs.head
+  | n + 1, h =>
+    have : n < xs.tail.length := by
+      unfold inBounds at h
+      rw [length_self_eq_one_add_length_tail, add_comm] at h
+      norm_num at h
+      exact h
+    xs.tail[n]
+
+/--
+Variant of `get` that returns an `Option α` in the case of an invalid index.
+-/
+def get? : NonEmpty α → Nat → Option α
+  | xs, 0 => some xs.head
+  | xs, n + 1 => xs.tail.get? n
+
+/--
+Type class instance for allowing direct indexing notation.
+-/
+instance : GetElem (NonEmpty α) Nat α inBounds where
+  getElem := get
+
+/--
+Convert a `List.NonEmpty` into a plain `List`.
+-/
+def toList (xs : NonEmpty α) : List α := xs
+
+/--
+Retrieve the last member of the `List.NonEmpty`.
+-/
+def last : NonEmpty α → α
+  | ⟨head, []⟩ => head
+  | ⟨_, cons x xs⟩ => last (cons x xs)
+
+end NonEmpty
+
+end List

Common/Set/Basic.lean

@@ -2,7 +2,7 @@ import Mathlib.Data.Set.Basic
 
 /-! # Common.Set.Basic
 
-Additional theorems and definitions useful in the context of sets.
+Additional theorems and definitions useful in the context of `Set`s.
 -/
 
 namespace Set

Common/Set/Interval.lean

@@ -0,0 +1,58 @@
+import Mathlib.Data.Real.Basic
+import Mathlib.Data.Set.Intervals.Basic
+
+import Common.List.Basic
+
+/-! # Common.Set.Interval
+
+A representation of a range of values.
+-/
+
+namespace Set
+
+/--
+An interval defines a range of values, characterized by a "left" value and a
+"right" value. We require these values to be distinct; we do not support the
+notion of an empty interval.
+-/
+structure Interval (α : Type _) [LT α] where
+  left : α
+  right : α
+  h : left < right
+
+namespace Interval
+
+/--
+Computes the size of the interval.
+-/
+def size [LT α] [Sub α] (i : Interval α) : α := i.right - i.left
+
+/--
+Computes the midpoint of the interval.
+-/
+def midpoint [LT α] [Add α] [HDiv α ℝ α] (i : Interval α) : α :=
+  (i.left + i.right) / (2 : ℝ)
+
+/--
+Convert an `Interval` into a `Set.Ico`.
+-/
+def toIco [Preorder α] (i : Interval α) : Set α := Set.Ico i.left i.right
+
+/--
+Convert an `Interval` into a `Set.Ioc`.
+-/
+def toIoc [Preorder α] (i : Interval α) : Set α := Set.Ioc i.left i.right
+
+/--
+Convert an `Interval` into a `Set.Icc`.
+-/
+def toIcc [Preorder α] (i : Interval α) : Set α := Set.Icc i.left i.right
+
+/--
+Convert an `Interval` into a `Set.Ioo`.
+-/
+def toIoo [Preorder α] (i : Interval α) : Set α := Set.Ioo i.left i.right
+
+end Interval
+
+end Set

Common/Set/Partition.lean

@@ -3,6 +3,8 @@ import Mathlib.Data.List.Sort
 import Mathlib.Data.Set.Intervals.Basic
 
 import Common.List.Basic
+import Common.List.NonEmpty
+import Common.Set.Interval
 
 /-! # Common.Set.Partition
 
@@ -11,126 +13,28 @@ Additional theorems and definitions useful in the context of sets.
 
 namespace Set
 
-open List
-
 /--
 A `Partition` is a finite subset of `[a, b]` containing points `a` and `b`.
+
+We use a `List.NonEmpty` internally to ensure the existence of at least one
+`Interval`, which cannot be empty. Thus our `Partition` can never be empty.
+The intervals are sorted via the `connected` proposition.
 -/
-structure Partition (α : Type _) [Preorder α] [@DecidableRel α LT.lt] where
+structure Partition (α : Type _) [LT α] where
-  /- The left-most endpoint of the partition. -/
+  ivls : List.NonEmpty (Interval α)
-  a : α
+  connected : ∀ I ∈ ivls.toList.pairwise (·.right = ·.left), I
-  /- The right-most endpoint of the partition. -/
-  b : α
-  /- The subdivision points. -/
-  xs : List α
-  /- Ensure the subdivision points are in sorted order. -/
-  sorted_xs : Sorted LT.lt xs
-  /- Ensure each subdivision point is in our defined interval. -/
-  within_xs : ∀ x ∈ xs, x ∈ Ioo a b
 
 namespace Partition
 
 /--
-An object `x` is a member of a `Partition` `p` if `x` is an endpoint of `p` or a
+Return the left-most endpoint of the `Partition`.
-subdivision point of `p`.
-
-Notice that being a member of `p` is different from being a member of some
-(sub)interval determined by `p`.
 -/
-instance [Preorder α] [@DecidableRel α LT.lt] : Membership α (Partition α) where
+def left [LT α] (p : Partition α) := p.ivls.head.left
-  mem (x : α) (p : Partition α) := x = p.a ∨ x ∈ p.xs ∨ x = p.b
 
 /--
-Return the endpoints and subdivision points of a `Partition` as a sorted `List`.
+Return the right-most endpoint of the `Partition`.
 -/
-def toList [Preorder α] [@DecidableRel α LT.lt] (p : Partition α) : List α :=
+def right [LT α] (p : Partition α) := p.ivls.last.right
-  (p.a :: p.xs) ++ [p.b]
-
-/--
-`x` is a member of `Partition` `p` **iff** `x` is a member of `p.List`.
--/
-theorem mem_self_iff_mem_toList [Preorder α] [@DecidableRel α LT.lt]
-  (p : Partition α) : x ∈ p ↔ x ∈ p.toList := by
-  apply Iff.intro
-  · sorry
-  · sorry
-
-/--
-Every member of a `Partition` is greater than or equal to its left-most point.
--/
-theorem left_le_mem_self [Preorder α] [@DecidableRel α LT.lt]
-  (p : Partition α) : ∀ x ∈ p, p.a ≤ x := by
-  sorry
-
-/--
-Every member of a `Partition` is less than or equal to its right-most point.
--/
-theorem right_ge_mem_self [Preorder α] [@DecidableRel α LT.lt]
-  (p : Partition α) : ∀ x ∈ p, x ≤ p.b := by
-  sorry
-
-/--
-The closed interval determined by the endpoints of the `Partition`.
--/
-abbrev toIcc [Preorder α] [@DecidableRel α LT.lt]
-  (p : Partition α) := Set.Icc p.a p.b
-
-/-
-Return the closed subintervals determined by the `Partition`.
--/
-def closedSubintervals [Preorder α] [@DecidableRel α LT.lt]
-  (p : Partition α) : List (Set α) :=
-  p.toList.pairwise (fun x₁ x₂ => Icc x₁ x₂)
-
-/--
-The open interval determined by the endpoints of the `Partition`.
--/
-abbrev toIoo [Preorder α] [@DecidableRel α LT.lt]
-  (p : Partition α) := Set.Ioo p.a p.b
-
-/-
-Return the open subintervals determined by the `Partition`.
--/
-def openSubintervals [Preorder α] [@DecidableRel α LT.lt]
-  (p : Partition α) : List (Set α) :=
-  p.toList.pairwise (fun x₁ x₂ => Ioo x₁ x₂)
-
-/--
-A member of an open subinterval of a `Partition` `p` is a member of the entire
-open interval determined by `p`.
--/
-theorem mem_open_subinterval_mem_open_interval
-  [Preorder α] [@DecidableRel α LT.lt] {p : Partition α}
-  (hI : I ∈ p.openSubintervals) (hy : y ∈ I) : y ∈ Ioo p.a p.b := by
-  have ⟨i, ⟨x₁, ⟨x₂, ⟨hx₁, ⟨hx₂, hI'⟩⟩⟩⟩⟩ :=
-    List.mem_pairwise_imp_exists_adjacent hI
-  have hx₁' : p.a ≤ x₁ := by
-    refine p.left_le_mem_self x₁ ?_
-    rw [p.mem_self_iff_mem_toList]
-    have : ↑i < p.toList.length := calc ↑i
-      _ < p.toList.length - 1 := i.2
-      _ < p.toList.length := by
-        unfold List.length Partition.toList
-        simp
-    exact List.mem_iff_exists_get.mpr ⟨⟨↑i, this⟩, Eq.symm hx₁⟩
-  have hx₂' : x₂ ≤ p.b := by
-    refine p.right_ge_mem_self x₂ ?_
-    rw [p.mem_self_iff_mem_toList]
-    have : ↑i + 1 < p.toList.length := add_lt_add_right i.2 1
-    exact List.mem_iff_exists_get.mpr ⟨⟨↑i + 1, this⟩, Eq.symm hx₂⟩
-  have hx_sub := Set.Ioo_subset_Ioo hx₁' hx₂'
-  rw [hI'] at hy
-  exact Set.mem_of_subset_of_mem hx_sub hy
-
-/--
-A member of an open subinterval of a `Partition` `p` is a member of the entire
-closed interval determined by `p`.
--/
-theorem mem_open_subinterval_mem_closed_interval
-  [Preorder α] [@DecidableRel α LT.lt] {p : Partition α}
-  (hI : I ∈ p.openSubintervals) (hy : y ∈ I) : y ∈ Icc p.a p.b := by
-  have := mem_open_subinterval_mem_open_interval hI hy
-  exact Set.mem_of_subset_of_mem Set.Ioo_subset_Icc_self this
 
 end Partition