Refactor Linear system ofConstraints with recursive definition

PolyhedralCombinatorics/LinearSystem/Basic.lean

@@ -47,6 +47,16 @@ variable {𝔽 m n} (p q : LinearSystem 𝔽 n)
   vector `b`. -/
 abbrev of (A : Matrix (Fin m) (Fin n) 𝔽) (b : Fin m → 𝔽) : LinearSystem 𝔽 n := ⟨m, A, b⟩
 
+/-- Prepends a linear inequality `yᵀ x ≤ b` to a linear system `p`. -/
+def cons (y : Fin n → 𝔽) (b : 𝔽) (p : LinearSystem 𝔽 n) : LinearSystem 𝔽 n :=
+  of (vecCons y p.mat) (vecCons b p.vec)
+
+@[simp] lemma cons_m : (cons y b p : LinearSystem 𝔽 n).m = p.m + 1 := rfl
+
+@[simp] lemma cons_mat : (cons y b p : LinearSystem 𝔽 n).mat = vecCons y p.mat := rfl
+
+@[simp] lemma cons_vec : (cons y b p : LinearSystem 𝔽 n).vec = vecCons b p.vec := rfl
+
 /-- The concatenation of two linear systems. -/
 def concat : LinearSystem 𝔽 n :=
   {

PolyhedralCombinatorics/LinearSystem/LinearConstraints.lean

@@ -28,44 +28,22 @@ 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 → 𝔽
-  comparator : LinearConstraint.Comparator
-  rhs : 𝔽
+inductive LinearConstraint (𝔽 : Type*) (n : ℕ) where
+| le : (Fin n → 𝔽) → 𝔽 → LinearConstraint 𝔽 n
+| eq : (Fin n → 𝔽) → 𝔽 → LinearConstraint 𝔽 n
+| ge : (Fin n → 𝔽) → 𝔽 → LinearConstraint 𝔽 n
 
 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 → 𝔽) × 𝔽)
-| le y b => [(y, b)]
-| eq y b => [(y, b), (-y, -b)]
-| ge y b => [(-y, -b)]
-
-@[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 => cmp.valid (y ⬝ᵥ x) b
-
-@[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
+@[simp] def valid : LinearConstraint 𝔽 n → (Fin n → 𝔽) → Prop
+| le y b, x => y ⬝ᵥ x ≤ b
+| eq y b, x => y ⬝ᵥ x = b
+| ge y b, x => y ⬝ᵥ x ≥ b
 
 lemma eq_valid_iff : (eq y b).valid x ↔ (le y b).valid x ∧ (ge y b).valid x := by
   simp [le_antisymm_iff]
@@ -74,86 +52,73 @@ end LinearConstraint
 
 namespace LinearSystem
 
-open LinearConstraint
+open LinearConstraint Matrix
 
 /-- 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⟩
+def ofConstraints : List (LinearConstraint 𝔽 n) → LinearSystem 𝔽 n
+  | [] => of vecEmpty vecEmpty
+  | c :: cs =>
+    match c with
+    | le y b => cons y b $ ofConstraints cs
+    | ge y b => cons (-y) (-b) $ ofConstraints cs
+    | eq y b => cons y b $ cons (-y) (-b) $ ofConstraints cs
 
 section toSet_ofConstraints
 open Matrix LinearConstraint
 
 variable {cs : List (LinearConstraint 𝔽 n)} {y : Fin n → 𝔽} {b : 𝔽}
 
-@[simp]
-lemma ofConstraints_mat_apply : (ofConstraints cs).mat i = (cs.bind toExtendedRows)[i].1 := rfl
-
-@[simp]
-lemma ofConstraints_vec_apply : (ofConstraints cs).vec i = (cs.bind toExtendedRows)[i].2 := rfl
-
-@[simp] lemma ofConstraints_apply_eq_lemma
-  : let s := ofConstraints cs
-    s.mat i = y ∧ s.vec i = b ↔ (cs.bind toExtendedRows)[i] = (y, b) := by
-  simp only [ofConstraints_mat_apply, ofConstraints_vec_apply]
-  apply Prod.mk.inj_iff.symm
-
-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
-  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]
-  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 <;> linear_constraint_lemma_tac h
+@[simp] lemma ofConstraints_nil
+  : (@ofConstraints 𝔽 _ n  []) = of vecEmpty vecEmpty := rfl
+
+theorem mem_ofConstraints_nil_solutions : x ∈ (@ofConstraints 𝔽 _ n []).solutions := by simp
+
+@[simp] private lemma vecCons_mulVec
+  {m n : ℕ} (y : Fin n → 𝔽) (A : Matrix (Fin m) (Fin n) 𝔽) (x : Fin n → 𝔽)
+  : vecCons y A *ᵥ x = vecCons (y ⬝ᵥ x) (A *ᵥ x) := by
+  funext x
+  cases x using Fin.cases <;> rfl
+
+@[simp] private lemma vecCons_le_vecCons {n : ℕ} (a b : 𝔽) (x y : Fin n → 𝔽)
+  : vecCons a x ≤ vecCons b y ↔ a ≤ b ∧ x ≤ y := by
+  simp_rw [Pi.le_def]
+  constructor <;> intro h
+  . constructor
+    . exact h 0
+    . intro i
+      exact h i.succ
+  . intro i
+    cases i using Fin.cases
+    . simp only [cons_val_zero, h.1]
+    . simp only [cons_val_succ, h.2]
+
+@[simp] lemma mem_ofConstraints_cons_solutions
+  : x ∈ (@ofConstraints 𝔽 _ n $ c :: cs).solutions ↔
+    c.valid x ∧ x ∈ (ofConstraints cs).solutions := by
+  simp only [solutions, Set.mem_setOf_eq, valid, ge_iff_le]
+  rw [ofConstraints]
+  split <;> simp [le_antisymm_iff, and_assoc]
+
+@[simp] lemma ofConstraints_le_cons
+  : (ofConstraints $ le y b :: cs) = cons y b (ofConstraints cs) := by
+  rfl
+
+@[simp] lemma ofConstraints_ge_cons
+  : (ofConstraints $ ge y b :: cs) = cons (-y) (-b) (ofConstraints cs) := by
+  rfl
+
+@[simp] lemma ofConstraints_eq_cons
+  : (ofConstraints $ eq y b :: cs) =
+    cons y b (cons (-y) (-b) $ ofConstraints cs) := by
+  rfl
 
 @[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).solutions → ∀ c ∈ cs, c.valid _
-    intro h ⟨y, cmp, b⟩ mem_cs
-    cases cmp
-    case' le => have ⟨_, hy, hb⟩ := le_lemma mem_cs
-    case' ge => have ⟨_, hy, hb⟩ := ge_lemma mem_cs
-    case' eq =>
-      rw [eq_valid_iff]
-      constructor
-      case' left => have ⟨_, hy, hb⟩ := (eq_lemma mem_cs).1
-      case' right => have ⟨_, hy, hb⟩ := (eq_lemma mem_cs).2
-    all_goals subst hy hb
-    case le | eq.left =>
-      apply h
-    case ge | eq.right =>
-      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 := List.get_mem rows i i.prop
-    have ⟨⟨y, cmp, b⟩, mem_cs, h'⟩ := List.mem_bind.mp this
-    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]
+  induction cs
+  case nil =>
+    simp
+  case cons c cs ih =>
+    simp only [mem_ofConstraints_cons_solutions, List.forall_mem_cons, ih]
 
 /-- The set of solutions of a linear system of constraints is the set of all points that satisfy
   all constraints. -/

PolyhedralCombinatorics/Polyhedron/Notation.lean

@@ -5,7 +5,7 @@ open Matrix LinearSystem
 
 variable {𝔽} [LinearOrderedField 𝔽] {n : ℕ}
 
-open Lean.Parser Lean.Elab.Term LinearConstraint.Comparator
+open Lean.Parser Lean.Elab.Term
 
 @[inherit_doc ofLinearSystem]
 scoped notation:max (name := matVecPolyhedron) "P(" A " , " b ")" => ofLinearSystem $ of A b
@@ -31,11 +31,11 @@ macro_rules
   | `(!P[$t^$n]{$[$constraints],*}) => `((!P{$constraints,*} : Polyhedron $t $n))
   | `(!P{$[$constraints],*}) => do
     let constraints ← constraints.mapM (fun
-      | `(linConstraint| $x:term ≤ $y:term) => `(⟨$x, le, $y⟩)
-      | `(linConstraint| $x:term <= $y:term) => `(⟨$x, le, $y⟩)
-      | `(linConstraint| $x:term = $y:term) => `(⟨$x, eq, $y⟩)
-      | `(linConstraint| $x:term ≥ $y:term) => `(⟨$x, ge, $y⟩)
-      | `(linConstraint| $x:term >= $y:term) => `(⟨$x, ge, $y⟩)
+      | `(linConstraint| $x:term ≤ $y:term) => `(LinearConstraint.le $x $y)
+      | `(linConstraint| $x:term <= $y:term) => `(LinearConstraint.le $x $y)
+      | `(linConstraint| $x:term = $y:term) => `(LinearConstraint.eq $x $y)
+      | `(linConstraint| $x:term ≥ $y:term) => `(LinearConstraint.ge $x $y)
+      | `(linConstraint| $x:term >= $y:term) => `(LinearConstraint.ge $x $y)
       | _ => Lean.Macro.throwUnsupported)
     `(ofLinearSystem $ ofConstraints [$constraints,*])
 

PolyhedralCombinatorics/Polyhedron/Projection.lean

@@ -198,7 +198,7 @@ theorem mem_fourierMotzkin (p : Polyhedron 𝔽 n) (j : Fin n) :
   x ∈ p.fourierMotzkin j ↔ x j = 0 ∧ ∃ (α : 𝔽), x + Pi.single j α ∈ p := by
   simp_rw [
     fourierMotzkin, mem_projection, mem_ofConstraints,
-    List.mem_singleton, forall_eq, LinearConstraint.eq_valid,
+    List.mem_singleton, forall_eq, LinearConstraint.valid,
     single_dotProduct, one_mul, and_congr_right_iff,
     ←Pi.single_smul, smul_eq_mul, mul_one, implies_true
   ]