Organization and cleaner proofs

PolyhedralCombinatorics/LinearSystem/LinearConstraints.lean

@@ -12,7 +12,7 @@ structure LinearConstraint where
   comparator : LinearConstraint.Comparator
   rhs : 𝔽
 
-variable {𝔽 n}
+variable {𝔽 n} {y : Fin n → 𝔽} {b : 𝔽}
 
 namespace LinearConstraint
 open Matrix
@@ -24,19 +24,23 @@ def toExtendedRows : LinearConstraint 𝔽 n → List ((Fin n → 𝔽) × 𝔽)
 | ⟨y, .eq, b⟩ => [(y, b), (-y, -b)]
 | ⟨y, .ge, b⟩ => [(-y, -b)]
 
-@[simp] lemma le_toExtendedRows : @toExtendedRows 𝔽 _ n ⟨y, .le, b⟩ = [(y, b)] := rfl
-@[simp] lemma eq_toExtendedRows : @toExtendedRows 𝔽 _ n ⟨y, .eq, b⟩ = [(y, b), (-y, -b)] := rfl
-@[simp] lemma ge_toExtendedRows : @toExtendedRows 𝔽 _ n ⟨y, .ge, b⟩ = [(-y, -b)] := rfl
+@[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
 
 /-- 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
 
-@[simp] lemma le_valid : @valid 𝔽 _ n ⟨y, Comparator.le, b⟩ x = (y ⬝ᵥ x ≤ b) := rfl
-@[simp] lemma eq_valid : @valid 𝔽 _ n ⟨y, Comparator.eq, b⟩ x = (y ⬝ᵥ x = b) := rfl
-@[simp] lemma ge_valid : @valid 𝔽 _ n ⟨y, Comparator.ge, b⟩ x = (y ⬝ᵥ x ≥ b) := rfl
+@[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
+
+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]
 
 end LinearConstraint
 
@@ -45,71 +49,81 @@ namespace LinearSystem
 open LinearConstraint
 
 /-- Constructs a polyhedron description from a list of linear constraints. -/
-def ofConstraints (constraints : List (LinearConstraint 𝔽 n)) : LinearSystem 𝔽 n :=
-  let rows := constraints.bind LinearConstraint.toExtendedRows
+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⟩
 
 section toSet_ofConstraints
-open LinearConstraint
-
--- FIXME: there must be a better way?
-private lemma prod_eq (p : α × β) : p.1 = a ∧ p.2 = b ↔ p = (a, b) := by
-  obtain ⟨fst, snd⟩ := p
-  simp_all only [Prod.mk.injEq]
-
-private lemma le_lemma
-  {constraints : List (LinearConstraint 𝔽 n)} {y : Fin n → 𝔽} {b : 𝔽}
-  : ⟨y, Comparator.le, b⟩ ∈ constraints →
-    ∃ i, (LinearSystem.ofConstraints constraints).mat i = y ∧ (LinearSystem.ofConstraints constraints).vec i = b := by
-  let rows := constraints.bind toExtendedRows
-  intro h
-  show ∃ i : Fin rows.length, rows[i].1 = y ∧ rows[i].2 = b
-  simp_rw [prod_eq]
-  apply List.mem_iff_get.mp
-  rw [List.mem_bind]
-  exact ⟨_, h, by simp [toExtendedRows]⟩
-
-private lemma ge_lemma
-  {constraints : List (LinearConstraint 𝔽 n)} {y : Fin n → 𝔽} {b : 𝔽}
-  : ⟨y, Comparator.ge, b⟩ ∈ constraints →
-    ∃ i, (LinearSystem.ofConstraints constraints).mat i = -y ∧ (LinearSystem.ofConstraints constraints).vec i = -b := by
-  let rows := constraints.bind toExtendedRows
-  intro h
-  show ∃ i : Fin rows.length, rows[i].1 = -y ∧ rows[i].2 = -b
-  simp_rw [prod_eq]
-  apply List.mem_iff_get.mp
-  rw [List.mem_bind]
-  exact ⟨_, h, by simp [toExtendedRows]⟩
-
-private lemma eq_lemma
-  {constraints : List (LinearConstraint 𝔽 n)} {y : Fin n → 𝔽} {b : 𝔽}
-  : ⟨y, Comparator.eq, b⟩ ∈ constraints →
-      (∃ i, (LinearSystem.ofConstraints constraints).mat i = y ∧ (LinearSystem.ofConstraints constraints).vec i = b)
-    ∧ (∃ i, (LinearSystem.ofConstraints constraints).mat i = -y ∧ (LinearSystem.ofConstraints constraints).vec i = -b) := by
-  let rows := constraints.bind toExtendedRows
-  intro h
-  show  (∃ i : Fin rows.length, rows[i].1 = y ∧ rows[i].2 = b)
-      ∧ (∃ i : Fin rows.length, rows[i].1 = -y ∧ rows[i].2 = -b)
-  simp_rw [prod_eq]
-  constructor <;> (
-    apply List.mem_iff_get.mp
-    rw [List.mem_bind]
-    exact ⟨_, h, by simp [toExtendedRows]⟩
-  )
+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 "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
+
+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
+
+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
+
+theorem mem_toSet_ofConstraints (x : Fin n → 𝔽)
+  : x ∈ (ofConstraints cs).toSet ↔ ∀ c ∈ cs, c.valid x := by
+  let rows := cs.bind toExtendedRows
+  constructor
+  . show x ∈ (ofConstraints cs).toSet → ∀ 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 [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 ⟨⟨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 constraints).toSet = { x : Fin n → 𝔽 | ∀ c ∈ constraints, c.valid x } := by
-  let rows := constraints.bind toExtendedRows
-  simp_rw [Set.ext_iff, ofConstraints, toSet, Set.mem_setOf]
-  intro x
-  conv =>
-    congr
-    . rw [Pi.le_def]
-      intro i
-      change (rows.get i).1 ⬝ᵥ x ≤ (rows.get i).2
-      rfl
-    . rfl
-  sorry
+  : (ofConstraints cs).toSet = { x : Fin n → 𝔽 | ∀ c ∈ cs, c.valid x } :=
+  Set.ext_iff.mpr mem_toSet_ofConstraints
 
 end toSet_ofConstraints
 

PolyhedralCombinatorics/Polyhedron/Basic.lean

@@ -39,132 +39,45 @@ theorem toSet_inj {p q : Polyhedron 𝔽 n} : p.toSet = q.toSet ↔ p = q := by
   . subst h
     rfl
 
-@[simp] theorem ofDescr_eq_ofDescr {d d'  : LinearSystem 𝔽 n}
+@[simp] theorem ofLinearSystem_eq_ofLinearSystem {d d'  : LinearSystem 𝔽 n}
   : ofLinearSystem d = ofLinearSystem d' ↔ d.toSet = d'.toSet := by
   simp_rw [←toSet_inj, ofLinearSystem, toSet, Quotient.lift_mk]
 
 /-- The set of points of a polyhedron is convex. -/
 theorem toSet_convex : Convex 𝔽 p.toSet :=
   Quot.recOn p
-    (fun P ↦ by
-      intro
-        x x_mem_P
-        y y_mem_P
-        α β α_nonneg β_nonneg αβ_affine
-      show P.mat *ᵥ (α • x + β • y) ≤ P.vec
+    (fun p x x_mem_P y y_mem_P α β α_nonneg β_nonneg αβ_affine ↦ by
       calc
-        P.mat *ᵥ (α • x + β • y) = α • P.mat *ᵥ x + β • P.mat *ᵥ y := by
+        p.mat *ᵥ (α • x + β • y) = α • p.mat *ᵥ x + β • p.mat *ᵥ y := by
           simp_rw [mulVec_add, mulVec_smul]
-        _ ≤ α • P.vec + β • P.vec :=
+        _ ≤ α • 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])
-    (fun _ _ ↦ by simp)
-
-section toSet_ofConstraints
-open LinearConstraint
-
--- FIXME: there must be a better way?
-private lemma prod_eq (p : α × β) : p.1 = a ∧ p.2 = b ↔ p = (a, b) := by
-  obtain ⟨fst, snd⟩ := p
-  simp_all only [Prod.mk.injEq]
-
-private lemma le_lemma
-  {constraints : List (LinearConstraint 𝔽 n)} {y : Fin n → 𝔽} {b : 𝔽}
-  : ⟨y, Comparator.le, b⟩ ∈ constraints →
-    ∃ i, (LinearSystem.ofConstraints constraints).mat i = y ∧ (LinearSystem.ofConstraints constraints).vec i = b := by
-  let rows := constraints.bind toExtendedRows
-  intro h
-  show ∃ i : Fin rows.length, rows[i].1 = y ∧ rows[i].2 = b
-  simp_rw [prod_eq]
-  apply List.mem_iff_get.mp
-  rw [List.mem_bind]
-  exact ⟨_, h, by simp [toExtendedRows]⟩
-
-private lemma ge_lemma
-  {constraints : List (LinearConstraint 𝔽 n)} {y : Fin n → 𝔽} {b : 𝔽}
-  : ⟨y, Comparator.ge, b⟩ ∈ constraints →
-    ∃ i, (LinearSystem.ofConstraints constraints).mat i = -y ∧ (LinearSystem.ofConstraints constraints).vec i = -b := by
-  let rows := constraints.bind toExtendedRows
-  intro h
-  show ∃ i : Fin rows.length, rows[i].1 = -y ∧ rows[i].2 = -b
-  simp_rw [prod_eq]
-  apply List.mem_iff_get.mp
-  rw [List.mem_bind]
-  exact ⟨_, h, by simp [toExtendedRows]⟩
-
-private lemma eq_lemma
-  {constraints : List (LinearConstraint 𝔽 n)} {y : Fin n → 𝔽} {b : 𝔽}
-  : ⟨y, Comparator.eq, b⟩ ∈ constraints →
-      (∃ i, (LinearSystem.ofConstraints constraints).mat i = y ∧ (LinearSystem.ofConstraints constraints).vec i = b)
-    ∧ (∃ i, (LinearSystem.ofConstraints constraints).mat i = -y ∧ (LinearSystem.ofConstraints constraints).vec i = -b) := by
-  let rows := constraints.bind toExtendedRows
-  intro h
-  show  (∃ i : Fin rows.length, rows[i].1 = y ∧ rows[i].2 = b)
-      ∧ (∃ i : Fin rows.length, rows[i].1 = -y ∧ rows[i].2 = -b)
-  simp_rw [prod_eq]
-  constructor <;> (
-    apply List.mem_iff_get.mp
-    rw [List.mem_bind]
-    exact ⟨_, h, by simp [toExtendedRows]⟩
-  )
-
-@[simp] theorem mem_ofConstraints (constraints : List (LinearConstraint 𝔽 n))
-  : ∀ x, x ∈ ofLinearSystem (ofConstraints constraints) ↔ ∀ c ∈ constraints, c.valid x := by
-  intro x
-  let rows := constraints.bind toExtendedRows
-  constructor <;> intro h
-  . show ∀ constr ∈ constraints, constr.valid _
-    intro ⟨y, cmp, b⟩ mem_constraints
-    cases cmp <;> simp only [valid]
-    case le =>
-      have ⟨i, hy, hb⟩ := le_lemma mem_constraints
-      subst hy hb
-      apply h
-    case ge =>
-      have ⟨i, hy, hb⟩ := ge_lemma mem_constraints
-      rw [←neg_eq_iff_eq_neg] at hy hb
-      subst hy hb
-      rw [neg_dotProduct, ge_iff_le, neg_le_neg_iff]
-      apply h
-    case eq =>
-      have ⟨⟨i₁, hy₁, hb₁⟩, ⟨i₂, hy₂, hb₂⟩⟩ := eq_lemma mem_constraints
-      apply le_antisymm
-      . subst hy₁ hb₁
-        apply h
-      . rw [←neg_eq_iff_eq_neg] at hy₂ hb₂
-        subst hy₂ hb₂
-        rw [neg_dotProduct, neg_le_neg_iff]
-        apply h
-  . show ∀ (i : Fin rows.length), rows[i].1 ⬝ᵥ _ ≤ rows[i].2
-    intro i
-    show rows[i].1 ⬝ᵥ _ ≤ rows[i].2
-    have : rows[i] ∈ rows := by apply List.get_mem
-    have ⟨⟨y, cmp, b⟩, mem_constraints, h'⟩ := List.mem_bind.mp this
-    have := h _ mem_constraints
-    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]
-    )
+        _ = p.vec := by rw [←add_smul, αβ_affine, one_smul])
+    (fun _ _ _ ↦ rfl)
+
+@[simp] theorem mem_ofConstraints {constraints : List (LinearConstraint 𝔽 n)}
+  : ∀ x, x ∈ ofLinearSystem (ofConstraints constraints) ↔ ∀ c ∈ constraints, c.valid x :=
+  LinearSystem.mem_toSet_ofConstraints
 
 /-- The set of points of a polyhedron defined by a given list of `constraints` is the set of
   points that satisfy those constraints. -/
-@[simp] theorem toSet_ofConstraints (constraints : List (LinearConstraint 𝔽 n))
+@[simp] theorem toSet_ofConstraints {constraints : List (LinearConstraint 𝔽 n)}
   : (ofConstraints constraints).toSet = { x | ∀ constr ∈ constraints, constr.valid x } :=
-  Set.ext_iff.mpr (mem_ofConstraints _)
+  LinearSystem.toSet_ofConstraints
 
-end toSet_ofConstraints
-
-instance : Inter (Polyhedron 𝔽 n) where
-  inter := Quotient.lift₂ (ofLinearSystem $ concat · ·) $ by
+/-- Intersection of polyhedra. -/
+def inter : Polyhedron 𝔽 n → Polyhedron 𝔽 n → Polyhedron 𝔽 n :=
+  Quotient.lift₂ (ofLinearSystem $ concat · ·) $ by
     intro a b a' b' ha hb
-    simp_rw [ofDescr_eq_ofDescr, toSet_concat]
+    simp_rw [ofLinearSystem_eq_ofLinearSystem, toSet_concat]
     change a.toSet = a'.toSet at ha
     change b.toSet = b'.toSet at hb
     simp_all only
 
+instance : Inter (Polyhedron 𝔽 n) := ⟨inter⟩
+
 @[simp] theorem toSet_inter (p q : Polyhedron 𝔽 n) : (p ∩ q).toSet = p.toSet ∩ q.toSet :=
   Quotient.inductionOn₂ p q LinearSystem.toSet_concat
 

PolyhedralCombinatorics/Polyhedron/Defs.lean

@@ -49,7 +49,9 @@ def empty : Polyhedron 𝔽 n :=
     | 1, _ => -1
   let b : Fin 2 → 𝔽 := ![-1, 0]
   of A b
+
 instance : EmptyCollection (Polyhedron 𝔽 n) := ⟨empty⟩
+
 instance : Bot (Polyhedron 𝔽 n) := ⟨empty⟩
 
 /-- The universe polyhedron (`𝔽^n`). -/