help formalizing a simple proof from definition

Stream: new members

[tzlil]

import Mathlib

inductive Disk where
  | White : Disk
  | Black : Disk
deriving DecidableEq, Fintype

def Disk.flip : Disk → Disk
  | .White => .Black
  | .Black => .White

def Board (n : ℕ) := Matrix (Fin n) (Fin n) Disk deriving DecidableEq, Fintype

structure Move {n : ℕ} (b : Board n) where
  x : Fin n
  y : Fin n
  -- dimensions must be nonzero and no bigger than x
  -- if our rectangle starts at x=1, y=1
  -- then width is how far left it extends
  width : Finset.Icc 1 (x.val+1)
  height : Finset.Icc 1 (y.val+1)
  p₁ : IsSquare width.val
  p₂ : IsTriangular height.val
  p₃ : b x y = Disk.White

-- a move flips the rectangle whose upper right corner is m.x,m.y
def Move.Apply (b : Board n) (m : Move b) : Board n := fun x y => if (
  x ≤ m.x.val ∧ x ≥ (1+m.x.val-m.width) ∧ y ≤ m.y.val ∧ y ≥ (1+m.y.val-m.height)
) then Disk.flip (b x y) else (b x y)

def A059474 : ℕ → ℕ → ℕ := by
  intros i j
  use 1 + ?_
  use ∑ (p : Fin (i+1) × Fin (j+1)) with p ≠ ⟨⟨i, by simp⟩,⟨j, by simp⟩⟩, ?_
  use @A059474 p.1 p.2
  -- use if p = ⟨⟨i, by simp⟩,⟨j, by simp⟩⟩ then 1 else @A059474 p.1.val p.2.val
  termination_by i j => i + j
  decreasing_by
  · {
      -- need to use the fact that p.1,p.2 ≠ a,a
      -- but i dont have this here, why?
      sorry
    }

def Move.Measure {n : ℕ} (b : Board n) : ℕ :=
  ∑ (p : Fin n × Fin n), if b p.1 p.2 = Disk.White then A059474 p.1 p.2 else 0


lemma Move.Measure.decreasing_with_respect_to_apply (b : Board n) (m : Move b) :
  Move.Measure (Move.Apply b m) < Move.Measure b := by
  unfold Move.Measure
  simp [Finset.sum_ite]
  suffices : Apply b m m.x m.y = Disk.Black
  {
    -- Move.Apply could only flip stuff below and to the left of ⟨m.x, m.y⟩
    -- and by the definition of A059474 that disk is more valuable than
    -- the biggest rectangle that we could pick for it
    -- and since that disk is black in `Move.Apply b m`
    -- and is white in `b`
    -- the measure of `b` is bigger
    sorry
  }
  {
    -- the top right corner of the rectangle is inside the rectangle
    -- therefore it is flipped, and by p₃ it was white previously
    -- so it is black now
    unfold Move.Apply
    have := Finset.mem_Icc.mp m.width.property
    have := Finset.mem_Icc.mp m.height.property
    rw [m.p₃]
    refine if_pos ?_
    constructor <;> grind
  }

my problem is with the first block of Move.Measure.decreasing_with_respect_to_apply, i'm having a really hard time proving it even though the measure is defined exactly in a way to make it work
is there some better phrasing of measure that im not seeing that makes it much easier to work with?

[vxctyxeha]

may be i can help you

[Matt Diamond]

FYI your code has an error in the web editor, IsTriangular is not defined

[tzlil]

@Matt Diamond sorry about that,

def IsTriangular [Preorder α] [LocallyFiniteOrderBot α] [AddCommMonoid α] (a : α)
  : Prop := ∃ r, a = ∑ i ∈ Finset.Iio r, i

either way only proposition 3 is required for this proof