Proved open projection set characterization

PolyhedralCombinatorics/LinearSystem/Basic.lean

@@ -1,37 +1,56 @@
 import PolyhedralCombinatorics.LinearSystem.Defs
 
+import Mathlib.Analysis.Convex.Basic
+
+/-!
+# Theorems about linear systems
+
+This file contains theorems about linear systems.
+
+## Main results
+
+* `LinearSystem.solutions_concat`: Characterizes the set of solutions of the
+  concatenation of two linear systems.
+* `LinearSystem.solutions_convex`: The set of solutions of a linear system is convex.
+-/
+
 namespace LinearSystem
 open Matrix
 
 variable {𝔽 n} [LinearOrderedField 𝔽] (p q : LinearSystem 𝔽 n)
 
 open Matrix
 
-@[simp] lemma mem_toSet : x ∈ p.toSet ↔ p.mat *ᵥ x ≤ p.vec := Set.mem_setOf
+@[simp] lemma mem_solutions : x ∈ p.solutions ↔ p.mat *ᵥ x ≤ p.vec := Set.mem_setOf
+
+@[simp] lemma mem_solutions_of {x : Fin n → 𝔽} : x ∈ (of A b).solutions ↔ A *ᵥ x ≤ b := Set.mem_setOf
 
-@[simp] theorem toSet_concat : (p.concat q).toSet = p.toSet ∩ q.toSet := by
+/-- The set of solutions of the concatenation of two linear systems is the intersection of their
+  sets of solutions. -/
+@[simp] theorem solutions_concat : (p.concat q).solutions = p.solutions ∩ q.solutions := by
   simp_rw [Set.ext_iff, Set.mem_inter_iff]
   intro x
   constructor <;> intro h
-  . simp_rw [concat, mem_toSet, Pi.le_def] at h
-    constructor <;> (rw [mem_toSet, Pi.le_def]; intro i)
+  . simp_rw [concat, mem_solutions, Pi.le_def] at h
+    constructor <;> (rw [mem_solutions, Pi.le_def]; intro i)
     . have := h (i.castLE $ Nat.le_add_right ..)
       simp_all [mulVec]
     . have := h ⟨p.m + i, Nat.add_lt_add_left i.prop ..⟩
       simp_all [mulVec]
-  . simp_rw [concat, mem_toSet, Pi.le_def]
+  . simp_rw [concat, mem_solutions, Pi.le_def]
     intro i
     by_cases hi : i < p.m <;> simp only [hi, mulVec, ↓reduceDIte, of_apply]
     . apply h.1
     . apply h.2
 
--- section repr
--- open Std.Format
-
--- instance repr [Repr 𝔽] : Repr (LinearSystem 𝔽 n) where
---   reprPrec p _p :=
---     (text "!!{ x | "
---       ++ (nest 2 <| reprArg p.mat ++ text " x ≤ " ++ reprArg p.vec)
---       ++ text "}")
-
--- end repr
+/-- The set of solutions of a linear system is convex. -/
+theorem solutions_convex : Convex 𝔽 p.solutions := by
+  intro x x_mem_p y y_mem_p α β α_nonneg β_nonneg αβ_affine
+  calc
+    p.mat *ᵥ (α • x + β • y) = α • p.mat *ᵥ x + β • p.mat *ᵥ y := by
+      simp_rw [mulVec_add, mulVec_smul]
+    _ ≤ α • p.vec + β • p.vec :=
+      add_le_add
+        (smul_le_smul_of_nonneg_left x_mem_p α_nonneg)
+        (smul_le_smul_of_nonneg_left y_mem_p β_nonneg)
+    _ = p.vec := by rw [←add_smul, αβ_affine, one_smul]

PolyhedralCombinatorics/LinearSystem/Defs.lean

@@ -1,6 +1,23 @@
 import Mathlib.Data.Matrix.Basic
 import Mathlib.Data.Matrix.Notation
 
+/-!
+# Linear systems
+
+This file defines basic properties of linear systems.
+
+Linear systems of `n` variables over a linear ordered field `𝔽` are represented
+with `LinearSystem 𝔽 n`.
+
+## Main definitions
+
+* `LinearSystem`: The type of linear systems.
+* `LinearSystem.of`: The linear system defined by a `m × n` coefficient matrix
+  and an `m × 1` column vector.
+* `LinearSystem.concat`: Concatenation of linear systems.
+* `LinearSystem.solutions`: Set of solutions of a linear system.
+-/
+
 variable
   (𝔽 : Type*) [LinearOrderedField 𝔽] -- Field type
   (n : ℕ) -- Dimension of the space
@@ -18,31 +35,33 @@ structure LinearSystem where
 namespace LinearSystem
 open Matrix
 
-variable {𝔽 n} (p q : LinearSystem 𝔽 n)
+variable {𝔽 m n} (p q : LinearSystem 𝔽 n)
 
-abbrev of {m} (A : Matrix (Fin m) (Fin n) 𝔽) (b : Fin m → 𝔽) : LinearSystem 𝔽 n := ⟨m, A, b⟩
+/-- Constructs a linear system defined by a `m × n` coefficient matrix `A` and an `m × 1` column
+  vector `b`. -/
+abbrev of (A : Matrix (Fin m) (Fin n) 𝔽) (b : Fin m → 𝔽) : LinearSystem 𝔽 n := ⟨m, A, b⟩
 
 /-- The concatenation of two linear systems. -/
 def concat : LinearSystem 𝔽 n :=
   {
     m := p.m + q.m,
-    mat := Matrix.of fun i j =>
+    mat := Matrix.of fun i j ↦
       if h : i < p.m then
         p.mat ⟨i, h⟩ j
       else
         q.mat ⟨i - p.m, Nat.sub_lt_left_of_lt_add (not_lt.mp h) i.prop⟩ j
-    vec := fun i =>
+    vec := fun i ↦
       if h : i < p.m then
         p.vec ⟨i, h⟩
       else
         q.vec ⟨i - p.m, Nat.sub_lt_left_of_lt_add (not_lt.mp h) i.prop⟩
   }
 
 /-- The set of solutions of the linear system. -/
-@[coe,simp] def toSet : Set (Fin n → 𝔽) := { x | p.mat *ᵥ x ≤ p.vec }
+@[simp] def solutions : Set (Fin n → 𝔽) := { x | p.mat *ᵥ x ≤ p.vec }
 
 /-- Two linear systems are said to be equivalent when their sets of solutions are equal. -/
-instance : HasEquiv (LinearSystem 𝔽 n) := ⟨(·.toSet = ·.toSet)⟩
+instance : HasEquiv (LinearSystem 𝔽 n) := ⟨(·.solutions = ·.solutions)⟩
 
 instance isSetoid (𝔽 n) [LinearOrderedField 𝔽] : Setoid (LinearSystem 𝔽 n) :=
   ⟨instHasEquiv.Equiv, fun _ ↦ rfl, Eq.symm, Eq.trans⟩

PolyhedralCombinatorics/LinearSystem/LinearConstraints.lean

@@ -1,11 +1,35 @@
 import PolyhedralCombinatorics.LinearSystem.Basic
 
-inductive LinearConstraint.Comparator | le | eq | ge
+/-!
+# Linear constraints in linear systems
+
+Although inequalities of the form `yᵀ x ≤ b` (where `y` is a coefficient vector
+and `b` is a scalar) are sufficient to represent all linear systems, it is
+often convenient to be able to use equalities (`yᵀ x = b`) or inequalities in
+the other direction (`yᵀ x ≥ b`).
+
+To this end, we hereby define the type of linear constraints and prove some
+relevant theorems about how linear systems defined by a set of constraints
+behave.
+
+## Main definitions
+
+* `LinearConstraint`: The type of linear constraints.
+* `LinearSystem.ofConstraints`: The linear system corresponding to a list of
+  constraints.
+
+## Main results
+
+* `LinearSystem.solutions_ofConstraints`: Characterization of the solutions of
+  a linear system in terms of the constraints that define it.
+-/
 
 variable
   (𝔽 : Type*) [LinearOrderedField 𝔽] -- Field type
   (n : ℕ) -- Dimension of the space
 
+inductive LinearConstraint.Comparator | le | eq | ge
+
 /-- `LinearConstraint n` is the type of linear constraints on `n` variables. -/
 structure LinearConstraint where
   coefficients : Fin n → 𝔽
@@ -17,38 +41,42 @@ variable {𝔽 n} {y : Fin n → 𝔽} {b : 𝔽}
 namespace LinearConstraint
 open Matrix
 
+@[match_pattern] abbrev le (y : Fin n → 𝔽) (b : 𝔽) : LinearConstraint 𝔽 n := ⟨y, .le, b⟩
+@[match_pattern] abbrev eq (y : Fin n → 𝔽) (b : 𝔽) : LinearConstraint 𝔽 n := ⟨y, .eq, b⟩
+@[match_pattern] abbrev ge (y : Fin n → 𝔽) (b : 𝔽) : LinearConstraint 𝔽 n := ⟨y, .ge, b⟩
+
 /-- Converts a linear constraint into a list o extended matrix rows for a
   linear system. -/
 def toExtendedRows : LinearConstraint 𝔽 n → List ((Fin n → 𝔽) × 𝔽)
-| ⟨y, .le, b⟩ => [(y, b)]
-| ⟨y, .eq, b⟩ => [(y, b), (-y, -b)]
-| ⟨y, .ge, b⟩ => [(-y, -b)]
+| le y b => [(y, b)]
+| eq y b => [(y, b), (-y, -b)]
+| ge y b => [(-y, -b)]
 
-@[simp] lemma le_toExtendedRows : toExtendedRows ⟨y, .le, b⟩ = [(y, b)] := rfl
-@[simp] lemma eq_toExtendedRows : toExtendedRows ⟨y, .eq, b⟩ = [(y, b), (-y, -b)] := rfl
-@[simp] lemma ge_toExtendedRows : toExtendedRows ⟨y, .ge, b⟩ = [(-y, -b)] := rfl
+@[simp] lemma le_toExtendedRows : toExtendedRows (le y b) = [(y, b)] := rfl
+@[simp] lemma eq_toExtendedRows : toExtendedRows (eq y b) = [(y, b), (-y, -b)] := rfl
+@[simp] lemma ge_toExtendedRows : toExtendedRows (ge y b) = [(-y, -b)] := rfl
+
+def Comparator.valid : Comparator → 𝔽 → 𝔽 → Prop
+| le => (· ≤ ·) | eq => (· = ·) | ge => (· ≥ ·)
 
 /-- Whether a linear constraint is valid for a given vector. -/
 def valid : LinearConstraint 𝔽 n → (Fin n → 𝔽) → Prop
-| ⟨y, cmp, b⟩, x =>
-  let p := y ⬝ᵥ x
-  match cmp with | .le => p ≤ b | .eq => p = b | .ge => p ≥ b
+| ⟨y, cmp, b⟩, x => cmp.valid (y ⬝ᵥ x) b
 
-@[simp] lemma le_valid : valid ⟨y, Comparator.le, b⟩ x = (y ⬝ᵥ x ≤ b) := rfl
-@[simp] lemma eq_valid : valid ⟨y, Comparator.eq, b⟩ x = (y ⬝ᵥ x = b) := rfl
-@[simp] lemma ge_valid : valid ⟨y, Comparator.ge, b⟩ x = (y ⬝ᵥ x ≥ b) := rfl
+@[simp] lemma le_valid : (le y b).valid x = (y ⬝ᵥ x ≤ b) := rfl
+@[simp] lemma eq_valid : (eq y b).valid x = (y ⬝ᵥ x = b) := rfl
+@[simp] lemma ge_valid : (ge y b).valid x = (y ⬝ᵥ x ≥ b) := rfl
 
-lemma eq_valid_iff
-  : valid ⟨y, Comparator.eq, b⟩ x
-    ↔ valid ⟨y, Comparator.le, b⟩ x ∧ valid ⟨y, Comparator.ge, b⟩ x := by simp [le_antisymm_iff]
+lemma eq_valid_iff : (eq y b).valid x ↔ (le y b).valid x ∧ (ge y b).valid x := by
+  simp [le_antisymm_iff]
 
 end LinearConstraint
 
 namespace LinearSystem
 
 open LinearConstraint
 
-/-- Constructs a polyhedron description from a list of linear constraints. -/
+/-- Constructs a linear system from a list of linear constraints. -/
 def ofConstraints (cs : List (LinearConstraint 𝔽 n)) : LinearSystem 𝔽 n :=
   let rows := cs.bind toExtendedRows
   ⟨rows.length, Matrix.of (Prod.fst ∘ rows.get), Prod.snd ∘ rows.get⟩
@@ -70,31 +98,31 @@ lemma ofConstraints_vec_apply : (ofConstraints cs).vec i = (cs.bind toExtendedRo
   simp only [ofConstraints_mat_apply, ofConstraints_vec_apply]
   apply Prod.mk.inj_iff.symm
 
-macro "constraint_lemma_tac" h:ident : tactic =>
+macro "linear_constraint_lemma_tac" h:ident : tactic =>
   `(tactic|
     simp_rw [ofConstraints_apply_eq_lemma]
     <;> exact List.mem_iff_get.mp $ List.mem_bind.mpr ⟨_, $h, by simp [toExtendedRows]⟩)
 
 private lemma le_lemma (h : ⟨y, Comparator.le, b⟩ ∈ cs)
   : let s := ofConstraints cs; ∃ i, s.mat i = y ∧ s.vec i = b := by
-  constraint_lemma_tac h
+  linear_constraint_lemma_tac h
 
 private lemma ge_lemma (h : ⟨y, Comparator.ge, b⟩ ∈ cs)
   : let s := ofConstraints cs; ∃ i, -(s.mat i) = y ∧ -(s.vec i) = b := by
   simp_rw [neg_eq_iff_eq_neg]
-  constraint_lemma_tac h
+  linear_constraint_lemma_tac h
 
 private lemma eq_lemma (h : ⟨y, Comparator.eq, b⟩ ∈ cs)
   : let s := ofConstraints cs;
     (∃ i, s.mat i = y ∧ s.vec i = b) ∧ (∃ i, -(s.mat i) = y ∧ -(s.vec i) = b) := by
   simp_rw [neg_eq_iff_eq_neg]
-  constructor <;> constraint_lemma_tac h
+  constructor <;> linear_constraint_lemma_tac h
 
-theorem mem_toSet_ofConstraints (x : Fin n → 𝔽)
-  : x ∈ (ofConstraints cs).toSet ↔ ∀ c ∈ cs, c.valid x := by
+@[simp] theorem mem_solutions_ofConstraints (x : Fin n → 𝔽)
+  : x ∈ (ofConstraints cs).solutions ↔ ∀ c ∈ cs, c.valid x := by
   let rows := cs.bind toExtendedRows
   constructor
-  . show x ∈ (ofConstraints cs).toSet → ∀ c ∈ cs, c.valid _
+  . show x ∈ (ofConstraints cs).solutions → ∀ c ∈ cs, c.valid _
     intro h ⟨y, cmp, b⟩ mem_cs
     cases cmp
     case' le => have ⟨_, hy, hb⟩ := le_lemma mem_cs
@@ -108,22 +136,30 @@ theorem mem_toSet_ofConstraints (x : Fin n → 𝔽)
     case le | eq.left =>
       apply h
     case ge | eq.right =>
-      simp_rw [valid, neg_dotProduct, neg_le_neg_iff]
+      simp_rw [ge_valid, neg_dotProduct, neg_le_neg_iff]
       apply h
   . show (∀ c ∈ cs, c.valid x) → ∀ (i : Fin rows.length), rows[i].1 ⬝ᵥ _ ≤ rows[i].2
     intro h i
-    have : rows[i] ∈ rows := by apply List.get_mem
+    have : rows[i] ∈ rows := List.get_mem rows i i.prop
     have ⟨⟨y, cmp, b⟩, mem_cs, h'⟩ := List.mem_bind.mp this
-    have := h _ mem_cs
-    cases cmp <;> (
-      simp_all only [toExtendedRows, valid, List.mem_singleton, List.mem_pair]
-      try cases h'
-      all_goals simp_all only [neg_dotProduct, neg_le_neg_iff, le_refl]
-    )
-
-theorem toSet_ofConstraints
-  : (ofConstraints cs).toSet = { x : Fin n → 𝔽 | ∀ c ∈ cs, c.valid x } :=
-  Set.ext_iff.mpr mem_toSet_ofConstraints
+    have c_valid := h _ mem_cs
+    cases cmp
+    case' eq =>
+      rw [eq_valid_iff] at c_valid
+      rw [toExtendedRows, List.mem_pair] at h'
+      cases h'
+    case le | eq.inl =>
+      rw [le_valid] at c_valid
+      simp_all only [toExtendedRows, List.mem_singleton]
+    case ge | eq.inr =>
+      rw [ge_valid] at c_valid
+      simp_all only [toExtendedRows, List.mem_singleton, neg_dotProduct, neg_le_neg_iff]
+
+/-- The set of solutions of a linear system of constraints is the set of all points that satisfy
+  all constraints. -/
+@[simp] theorem solutions_ofConstraints
+  : (ofConstraints cs).solutions = { x : Fin n → 𝔽 | ∀ c ∈ cs, c.valid x } :=
+  Set.ext_iff.mpr mem_solutions_ofConstraints
 
 end toSet_ofConstraints