diff --git a/PolyhedralCombinatorics/LinearSystem/LinearConstraints.lean b/PolyhedralCombinatorics/LinearSystem/LinearConstraints.lean index fa7dbe1..0540339 100644 --- a/PolyhedralCombinatorics/LinearSystem/LinearConstraints.lean +++ b/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,9 +24,9 @@ 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 @@ -34,9 +34,13 @@ def valid : LinearConstraint 𝔽 n → (Fin n → 𝔽) → Prop 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 diff --git a/PolyhedralCombinatorics/Polyhedron/Basic.lean b/PolyhedralCombinatorics/Polyhedron/Basic.lean index 23e32a4..7ae96f3 100644 --- a/PolyhedralCombinatorics/Polyhedron/Basic.lean +++ b/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 diff --git a/PolyhedralCombinatorics/Polyhedron/Defs.lean b/PolyhedralCombinatorics/Polyhedron/Defs.lean index 4ace3e3..96b556d 100644 --- a/PolyhedralCombinatorics/Polyhedron/Defs.lean +++ b/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`). -/ diff --git a/PolyhedralCombinatorics/Polyhedron/Notation.lean b/PolyhedralCombinatorics/Polyhedron/Notation.lean index 9eb7e66..2e932eb 100644 --- a/PolyhedralCombinatorics/Polyhedron/Notation.lean +++ b/PolyhedralCombinatorics/Polyhedron/Notation.lean @@ -5,8 +5,7 @@ open Matrix LinearSystem variable {𝔽} [LinearOrderedField 𝔽] {n : ℕ} -open Lean.Parser -open Lean.Elab.Term +open Lean.Parser Lean.Elab.Term LinearConstraint.Comparator @[inherit_doc ofLinearSystem] scoped notation:max (name := matVecPolyhedron) "P(" A " , " b ")" => ofLinearSystem $ of A b @@ -23,15 +22,16 @@ syntax:60 term:61 " = " term : linConstraint syntax:60 term:61 " ≥ " term : linConstraint /-- Syntax for declaring polyhedra as systems of linear constraints. -/ -syntax:100 (name := systemPolyhedron) +syntax:max (name := systemPolyhedron) "P" ("[" term:90 "^" term "]")? "{" linConstraint,*,? "}" : term + 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, LinearConstraint.Comparator.le, $y⟩) - | `(linConstraint| $x:term = $y:term) => `(⟨$x, LinearConstraint.Comparator.eq, $y⟩) - | `(linConstraint| $x:term ≥ $y:term) => `(⟨$x, LinearConstraint.Comparator.ge, $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⟩) | _ => Lean.Macro.throwUnsupported) `(ofLinearSystem $ ofConstraints [$constraints,*])