Rephrasing Matrix operation for more convenient proving

Stream: mathlib4

[Bernardo Borges]

Hello everyone, I am starting to prove my Addition rule for Matrices that represent PseudoBoolean restrictions:

import Mathlib.Data.Fin.Tuple.Reflection
import Mathlib.Data.Matrix.Notation
open FinVec BigOperators

def PBSum (cs : Matrix (Fin n) (Fin 2) ℕ) (xs : Fin n → Fin 2) :=
  ∑ i, ((cs i) 0 * xs i + (cs i) 1 * (1 - xs i))

def PBIneq {n : ℕ} (cs : Matrix (Fin n) (Fin 2) ℕ) (xs : Fin n → Fin 2) (const : ℕ) :=
  PBSum cs xs ≥ const

-- Addition
-- ∑i (a i * l i) ≥ A
-- ∑i (b i * l i) ≥ B
-- ⊢
-- ∑i ((a i + b i) * l i) ≥ A + B
theorem Addition
  {xs : Fin n → Fin 2}
  {as : Matrix (Fin n) (Fin 2) ℕ} {A : ℕ} (ha : PBIneq as xs A)
  {bs : Matrix (Fin n) (Fin 2) ℕ} {B : ℕ} (hb : PBIneq bs xs B)
  : PBIneq (tighten $ as + bs) xs (A + B) := by
  rw [PBIneq,PBSum,tighten] at *
  sorry

Now, this tighten function below is meant to cancel out terms, since each row of the matrix represents the coefficient of variables $x$ and $\overline x$, with the relationship $\overline x = 1 - x$ and $x \in \{0,1\}$. This is what I came up with:

import Mathlib.Data.Fin.Tuple.Reflection
import Mathlib.Data.Matrix.Notation

open BigOperators FinVec

/--
 For each row, I want to have the elements cancel out, so one of them will always be zero
 Ex: row [1,0] -> [1,0]
     row [2,1] -> [1,0]
     row [1,5] -> [0,4]
-/
def tighten (as : Matrix (Fin n) (Fin 2) ℕ) : Matrix (Fin n) (Fin 2) ℕ :=
  (as.map Int.ofNat) * !![1,-1;-1,1] |>.map Int.toNat
-- Proving with this matrix multiplication may get challenging
#eval tighten !![1,0;1,0] = !![1,0;1,0]
#eval tighten !![1,1;1,0] = !![0,0;1,0]
#eval tighten !![1,0;1,2] = !![1,0;0,1]

Where this matrix just want to subtract one column from another and leave 0 if it should be negative. Firstly I ask, will this complicate my Addition proof? I have a guess that it will be harder to unwrap and verify, that's why I'm asking if there is a more convenient way to write this, something like:

def tighten' (as : Matrix (Fin n) (Fin 2) ℕ) : Matrix (Fin n) (Fin 2) ℕ :=
  sorry
  -- as.rows ![a,b] -> ![a-b,b-a]
  -- as.rows ![a,b] -> if a > b then ![a-b,0] else ![0,b-a]

Any suggestions are welcome!

[Bernardo Borges]

It got some more complicated, since I also need the number of positions that were tightened, with the matrix I get this:

def tighten (as : Matrix (Fin n) (Fin 2) ℕ) : Matrix (Fin n) (Fin 2) ℕ × ℕ :=
  (t, ∑i, (as - t) i 0)
  where
  M := !![1,-1;-1,1]
  t := as.map Int.ofNat * M |>.map Int.toNat

theorem Addition
  {xs : Fin n → Fin 2}
  {as : Matrix (Fin n) (Fin 2) ℕ} {A : ℕ} (ha : PBIneq as xs A)
  {bs : Matrix (Fin n) (Fin 2) ℕ} {B : ℕ} (hb : PBIneq bs xs B)
  : PBIneq (tighten (as + bs) |>.1) xs ((A + B) - (tighten (as+bs)).2) := by
  sorry

[Bernardo Borges]

Then the description of the tighten function should be:

Given a N by 2 Matrix as, return a tuple, where
1. Is another matrix, where each row follows
def eq : ℕ × ℕ → ℕ × ℕ
| (a,b) => if a > b then (a-b,0) else (0,b-a)
Agains each row of as.

2. A natural number, the sum of all removed lines, where for a single row it is
def rem : ℕ × ℕ → ℕ
| (a,b) => min a b

[Bernardo Borges]

To be yet more specific, I would like to use a notation like this:

def tighten' (as : Matrix (Fin n) (Fin 2) ℤ) := -- : Matrix (Fin n) (Fin 2) ℕ × ℕ :=
  ∑i:Fin n,
    ![if as i 0 > as i 1 then as i 0 - as i 1 else as i 1 - as i 0,
      min (as i 0) (as i 1)]

But I don't want the \sum operator, because I need the matrix back, I just need to access the rows and transform them somehow.

[Bernardo Borges]

And also an alias to as i 0 and as i 1 would make it more readable.

[Bernardo Borges]

Matrix.map will apply to each element, which is not what I need.

[Bernardo Borges]

Matrix.updateRow Looks promissing but i need to gather the rows of A first

[Bernardo Borges]

Apparently we can just use a function as a matrix definition:

def tighten'' (as : Matrix (Fin n) (Fin 2) ℕ) : Matrix (Fin n) (Fin 2) ℕ :=
  λ i : Fin n =>
    let x := as i 0
    let y := as i 1
    if x > y then
      ![x - y,0]
    else
      ![0,y - x]

[Damiano Testa]

Everything in Lean is a function.

[Eric Wieser]

You shouldn't do that without prepending Matrix.of

[Bernardo Borges]

Care to explain why, please?

[Bernardo Borges]

For all I know the type assertion of the def will take care of instances, won't it?

[Johan Commelin]

simp will thank you :wink:

[Bernardo Borges]

Ok! It's looking more promising. Last thing, is there such a thing as a pattern match for finvec, like a list does? It'd be interesting to get elements like:

def tighten (as : Matrix (Fin n) (Fin 2) ℕ) : Matrix (Fin n) (Fin 2) ℕ :=
  Matrix.of λ i : Fin n =>
    let ![x,y] := as i
    if x > y then
      ![x - y,0]
    else
      ![0,y - x]

[Brendan Seamas Murphy]

Sort of. You can use Fin.consInduction and Fin.consCases to mimick this, but it won't look like pattern matching unless you do induction as i using Fin.consInduction with or cases as i using Fin.consInduction with inside tactic mode

[Brendan Seamas Murphy]

Short answer no

[Eric Wieser]

What you have looks optimal

[Eric Wieser]

Are you later doing multiplication with these matrices?

[Eric Wieser]

If not, then maybe you should be working with Fin n -> ℕ \times ℕinstead

[Bernardo Borges]

Eric Wieser said:

If not, then maybe you should be working with Fin n -> ℕ \times ℕinstead

I will multiply with a scalar among other operations. Why is it better to use a tuple?

[Eric Wieser]

If you never do matrix multiplication, then Matrix is probably getting in your way. Scalar multiplication works fine on tuples.

[Eric Wieser]

Why is it better to use a tuple?

For one, the (x, y) pattern-matching syntax will work

[Bernardo Borges]

So, if I use a tuple how can this operation be done:

def ceildiv (c : ℕ) (a : ℕ) := (a+c-1) / c

def ApplyCeildiv
  (M : Matrix (Fin n) (Fin 2) ℕ)
  (c : ℕ)
  : Matrix (Fin n) (Fin 2) ℕ :=
  M.map (ceildiv c)

[Bernardo Borges]

I'll need to map over matrix and tuple, right?