Statement runs into "(deterministic) timeout at 'whnf'"

Stream: mathlib4

[Bernardo Borges]

I am currently defining the statements for theorems I will be proving the next weeks, Addition, Multiplication, Division for Pseudo Booleans:

open FinVec

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

-- Division
-- ∑i (a i * l i) ≥ A
-- c : ℕ
-- c > 0
-- ⊢
-- ∑i (ceil(a i / c) * l i) ≥ ceil(A / c)
theorem Division {as : Fin n → ℤ} {A : ℤ} (c : ℕ) (hc0 : c > 0)
  (ha : PBProp as A)
  : PBProp (map (ceildiv c) as) (ceildiv c A) := sorry

Note the ceildiv that I defined for the division and ceiling.
The problem is when declaring this example:

example (ha : PBProp ![3,4] 3)
  : PBProp ![2,2] 2 := by
  let h2z : 2 > 0 := Nat.zero_lt_succ 1
  exact Division 2 h2z ha
  done

That should work, but i am getting the error in the exact line:

(deterministic) timeout at 'whnf', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)

What is probably causing it? How can I avoid it? Appreciate any pointers :)

[Bernardo Borges]

By the way, the definition of PBProp is:

open FinVec BigOperators

def PBInequality {n : ℕ} (cs : Fin n → ℤ) (xs : Fin n → Fin 2) (const : Int) :=
  ∑ i, (cs i * xs i) ≥ const

def PBProp (cs : Fin n → ℤ) (const : Int) := ∃xs, PBInequality cs xs const

[Bernardo Borges]

Apparently the implicit FinVec is causing the timeout. Is there a long search happening to infer that as := ![2,2] from ha : PBProp ![2,2] 2? How can I aid it?

[Floris van Doorn]

Next time, please ask your question using a single #mwe. This works:

import Mathlib.Data.Fin.Tuple.Reflection
import Mathlib.Algebra.BigOperators.Basic
open FinVec BigOperators

def PBInequality {n : ℕ} (cs : Fin n → ℤ) (xs : Fin n → Fin 2) (const : Int) :=
  ∑ i, (cs i * xs i) ≥ const

def PBProp (cs : Fin n → ℤ) (const : Int) := ∃xs, PBInequality cs xs const

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

theorem Division {as : Fin n → ℤ} {A : ℤ} (c : ℕ) (hc0 : c > 0)
  (ha : PBProp as A)
  : PBProp (map (ceildiv c) as) (ceildiv c A) := sorry

example (ha : PBProp ![3,4] 3)
  : PBProp ![2,2] 2 := by
  let h2z : 2 > 0 := Nat.zero_lt_succ 1
  convert Division 2 h2z ha
  done

Another fix is to replace def PBProp by irreducible_def PBProp.
Not quite sure why the exact is timing out while the convert is succeeding. Presumably it doesn't see that map (ceildiv 2) ![3, 4] is the same as ![2,2] and then starts unfolding PBProp and reducing PBInequality with variable xs...

[Bernardo Borges]

It definetly is helping! Thanks a lot!
Do I lose anything by using irreducible_def tho? I'll replace it whenever it's possible.

[Bernardo Borges]

Apparently I did lose something:

import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Data.Fin.Tuple.Reflection
import Mathlib.Data.Fin.VecNotation

open FinVec BigOperators

def PBInequality {n : ℕ} (cs : Fin n → ℤ) (xs : Fin n → Fin 2) (const : ℤ) :=
  ∑ i, (cs i * xs i) ≥ const

irreducible_def PBProp (cs : Fin n → ℤ) (const : ℤ) := ∃xs, PBInequality cs xs const

example : PBProp ![3,4] 2 :=
  let xs := ![0,1]
  let proof : PBInequality ![3,4] xs 2 := by
    reduce
    exact Int.NonNeg.mk 2
    done
  ⟨xs,proof⟩
  /-
  invalid constructor ⟨...⟩, expected type must be an inductive type
  PBProp ![3, 4]
  -/