Looking for existing structure for Cutting Planes

Stream: Is there code for X?

[Bernardo Borges]

Hello Everyone! I am starting to model and develop proofs for cutting planes and pseudo boolean equations in lean. The notation looks like this:
image.png
Where I am looking for a nice notation to model the Sum over ai*li and express the following rules:
image.png
Of which I will prove the correctness of each using Lean as well.
Now I have approached modelling with List Int, where I keep the as and ls separate and unite them with the predicate:

-- Σᵢ(aᵢ*lᵢ)
def pbSum (as : List Int) (ls : List Int) : Int := (as.zipWith (·*·) ls).foldl (·+·) 0

And then the rules look like this:

-- Σᵢ aᵢlᵢ ≥ A   Σᵢ bᵢlᵢ ≥ B
-- => Σ(aᵢ+bᵢ)lᵢ ≥ A + B
theorem addition : ∀ {A B : Int} {as ls bs : List Int},
                      (pbSum as ls) ≥ A →
                      (pbSum bs ls) ≥ B →
                      (pbSum (as.zipWith (·+·) bs) ls) ≥ (A + B) := sorry

As a attempt, but i start to struggle when I want to represent the addition rule and the terms li are not the same. I have looked at Finite Sets because the implement the ∑ but it's not the same semantics.

Is there a structure (in mathlib4) that can better express these rules like adition of the pbSums and scalar multiplication? Any help and pointers is greatly appreciated!

[Martin Dvořák]

I would rather use something like this:

import Mathlib.Algebra.BigOperators.Basic

open BigOperators

abbrev pbSum {n : ℕ} (as ls : Fin n → ℤ) : Int := ∑ i, as i * ls i

You will get more support from Mathlib when you want to prove properties about pbSum.

[Martin Dvořák]

Your theorem, translated to my notation, can then be proved as follows:

import Mathlib.Tactic

open BigOperators

@[simp]
abbrev pbSum {n : ℕ} (a b : Fin n → ℤ) : ℤ := ∑ i, a i * b i

theorem pbSum_addition {n : ℕ} {A B : ℤ} {x y z : Fin n → ℤ}
    (hx : pbSum x z ≥ A) (hy : pbSum y z ≥ B) :
    pbSum (x + y) z ≥ A + B := by
  suffices : pbSum (x + y) z = pbSum x z + pbSum y z
  · linarith
  simp [←Finset.sum_add_distrib, add_mul]

[Martin Dvořák]

Also see our recent discussion about whether using docs#Matrix.dotProduct is a good idea:
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/ERat.20as.20Semiring

[Martin Dvořák]

If you decide to use it, it will look as follows:

import Mathlib.Tactic

open scoped Matrix

theorem pbSum_addition {n : ℕ} {A B : ℤ} {x y z : Fin n → ℤ}
    (hx : x ⬝ᵥ z ≥ A) (hy : y ⬝ᵥ z ≥ B) :
    (x + y) ⬝ᵥ z ≥ A + B := by
  suffices : (x + y) ⬝ᵥ z = x ⬝ᵥ z + y ⬝ᵥ z
  · linarith
  simp

[Martin Dvořák]

Or even shorter proof (but slightly harder to find):

import Mathlib.Tactic

open scoped Matrix

theorem pbSum_addition {n : ℕ} {A B : ℤ} {x y z : Fin n → ℤ}
    (hx : x ⬝ᵥ z ≥ A) (hy : y ⬝ᵥ z ≥ B) :
    (x + y) ⬝ᵥ z ≥ A + B := by
  rw [Matrix.add_dotProduct]
  exact Int.add_le_add hx hy

[Martin Dvořák]

Bernardo Borges said:

∑ but it's not the same semantics.

Why don't you want to use it? Is it because as could have a different length from ls but you still want pbSum as ls to make sense?

[Bernardo Borges]

Martin Dvořák said:

Bernardo Borges said:

∑ but it's not the same semantics.

Why don't you want to use it? Is it because as could have a different length from ls but you still want pbSum as ls to make sense?

I didn't think it was a good idea initially, because I saw its implementation of FinSet, but this data structure would not work as it enforces unique values.

Also, another thing I'm trying to wrap my head around is how I will represent the negated coefficient, as in x + !x = 1, I might have a 3*!x in my expressions, and it won't fit neatly into the FinVec

[Martin Dvořák]

Bernardo Borges said:

I didn't think it was a good idea initially, because I saw its implementation of FinSet, but this data structure would not work as it enforces unique values.

The indices have to be unique. Values at those indices don't have to be unique.

[Martin Dvořák]

docs#FinVec

[Martin Dvořák]

Bernardo Borges said:

Also, another thing I'm trying to wrap my head around is how I will represent the negated coefficient, as in x + !x = 1, I might have a 3*!x in my expressions, and it won't fit neatly into the FinVec

Can you elaborate?

[Martin Dvořák]

Oh! If I understand the slides, you actually want this:

import Mathlib.Algebra.BigOperators.Basic

open BigOperators

@[simp]
abbrev pbSum {n : ℕ} (a : Fin n → ℤ) (s x : Fin n → Bool) : ℤ :=
  ∑ i, a i * (if s i = x i then 1 else 0)

You have a vector a of weights, a vector s of signs, and a vector x representing a boolean solution.
Am I right?

[Bernardo Borges]

Seems right, but I think I didnt get how it will be applied in the end. If I want to represent the proof in this image, do I write this?

open BigOperators

@[simp]
abbrev pbSum {n : ℕ} (a : Fin n → ℤ) (s x : Fin n → Bool) : ℤ :=
  ∑ i, a i * (if s i = x i then 1 else 0)

open scoped Matrix

theorem pbSum_addition := sorry


-- t1 = 2w + 4x + 2y ≥ 4
def t1 := (pbSum ![2,4,2,0]) ≥ 2

-- t2 = w + 2x + 4y + 2z ≥ 5
def t2 := (pbSum ![1,2,4,2]) ≥ 5

-- t3 = 3w + 6x + 6y + 2z ≥ 9
def t3 := pbSum_addition t1 t2

image.png

[Martin Dvořák]

No negations in your example?

[Bernardo Borges]

Truly, If this is the intended interface, then when I add negations, I need to supply another vector of the signs, right

[Bernardo Borges]

image.png

[Martin Dvořák]

It seems that pbSum_addition will have to be a significantly different theorem than what it looked like originally. Can you state what you want to prove?

[Bernardo Borges]

-- 3w + 6x + 6y + 2z ≥ 9
def t3 := pbSum ![3,6,6,2] ![false,false,false,false] ≥ 9

-- 2!z ≥ 0
def t4 := pbSum ![0,0,0,2] ![false,false,false,true] ≥ 0

-- 3w + 6x + 6y ≥ 7
def t5 := pbSum_addition t3 t4

[Bernardo Borges]

Martin Dvořák said:

It seems that pbSum_addition will have to be a significantly different theorem than what it looked like originally. Can you state what you want to prove?

I agree that the slides are taking high level steps that should be broken down. Firstly, I need to address the possiblity of both 2z and 2!z appear in the expression. And then I can add another step that will equilibrate this, in this case the z term vanishes completely, but not without the effect of a constant 2 appearing in the lhs, which is also compensated to the rhs, by subtracting 2

[Martin Dvořák]

It seems to me that you mixed up operations on data with theorems about those operations. However, I think I now understand what you want. Let me formalize it.

[Martin Dvořák]

Unpolished sketch:

import Mathlib.Algebra.BigOperators.Basic

open BigOperators

def pbSum {n : ℕ} (a : Fin n → ℤ) (s x : Fin n → Bool) : ℤ :=
  ∑ i, a i * (if s i = x i then 1 else 0)

structure Condition (n : ℕ) where
  weights : Fin n → ℤ
  rhs : ℤ

def Condition.eval {n : ℕ} (C : Condition n) (x : Fin n → Bool) : ℤ :=
  ∑ i, if x i then C.weights i else 0

def Condition.isSatisfied {n : ℕ} (C : Condition n) (x : Fin n → Bool) : Bool :=
  C.eval x ≥ C.rhs

def condition_of_signs {n : ℕ} (w : Fin n → ℤ) (s : Fin n → Bool) (r : ℤ) : Condition n :=
  Condition.mk (fun i => if s i then w i else -(w i)) (r - ∑ i, if s i then 0 else w i)

lemma condition_of_signs_eval_eq_pbSum_minus {n : ℕ}
    (w : Fin n → ℤ) (s : Fin n → Bool) (r : ℤ) (x : Fin n → Bool) :
    (condition_of_signs w s r).eval x = pbSum w s x - ∑ i, if s i then 0 else w i := by
  unfold condition_of_signs
  unfold Condition.eval
  unfold pbSum
  apply eq_sub_of_add_eq
  apply eq_of_sub_eq_zero
  rw [←Finset.sum_add_distrib]
  rw [←Finset.sum_sub_distrib]
  apply Finset.sum_eq_zero
  intro i _
  cases x i <;> cases hsi : s i <;> simp [hsi]

theorem condition_of_signs_isSatisfied_iff_pbSum_ge {n : ℕ}
    (w : Fin n → ℤ) (s : Fin n → Bool) (r : ℤ) (x : Fin n → Bool) :
    (condition_of_signs w s r).isSatisfied x ↔ pbSum w s x ≥ r := by
  unfold Condition.isSatisfied
  rw [condition_of_signs_eval_eq_pbSum_minus]
  unfold condition_of_signs
  simp

def addConditions {n : ℕ} (a b : Condition n) : Condition n :=
  Condition.mk (a.weights + b.weights) (a.rhs + b.rhs)

theorem addConditions_isSatisfied {n : ℕ} {a b : Condition n} {x : Fin n → Bool}
    (ha : a.isSatisfied x) (hb : b.isSatisfied x) :
    (addConditions a b).isSatisfied x := by
  unfold addConditions
  simp [Condition.isSatisfied, Condition.eval] at *
  convert add_le_add ha hb
  rw [←Finset.sum_add_distrib]
  congr
  ext i
  cases x i <;> simp

• The original formula (which works with weights and signs) is represented by pbSum.
• I convert the weights-and-signs representation to a structure Condition that has no negations.
• Condition.eval evaluates the LHS of given condition for given vector x.
• Condition.isSatisfied determines whether the vector x satisfies the condition.
• Theorem condition_of_signs_isSatisfied_iff_pbSum_ge provides an equivalence between Condition.isSatisfied and the original pbSum formulation.
• When we have conditions represented by the negation-free structure Condition, it is very easy to add two conditions together, which addConditions defines. Note that (a.weights + b.weights) is element-wise addition.
• Theorem addConditions_isSatisfied says that, if both conditions are satisfied by given vector x, their sum is also satisfied by x.

[Bernardo Borges]

I am getting that the negation structure is conceptually irrelevant, and also we can map any of these negated values to another valid GE inequality without loss of information. So in 2!z >= 0, we want to transform it into a Condition that will not have such negation, and this will represent:

2 !z >= 0            <- rw !z = 1 - z
2 (1-z) >= 0
2 - 2z >= 0
-2z >= -2

[Martin Dvořák]

This is what I did above.

[Bernardo Borges]

And then without negations the proofs follow smoothly, much like vector addition etc.
(I'm just typing this to wrap my head around it)

[Bernardo Borges]

So then you followed proving that this conversion generates equivalent proof

[Martin Dvořák]

Yes. I proved the equivalence between these two formulations above, so that you can trust me the much simpler definition of adding two condition together.

[Bernardo Borges]

Bravo! It looks much simpler indeed after the inconvenience of !z's is gone

[Bernardo Borges]

Thank you for the clarification!
I will read this calmly and try to better grasp the steps now!

[Martin Dvořák]

I don't know if the original formulation is useful later. Either way, the code above will need a lot of polishing. Also note that the definitions all use (x : Fin n → Bool) and so they are useless if you wanted to do e.g. linear relaxations of the problem.

[Martin Dvořák]

Please, note the distinction between my definition addConditions (which says what adding two conditions together means) and my theorem addConditions_isSatisfied (which formalizes the "obvious" property of this operation).