performance of reduce with ℚ

Stream: general

[Matthew Pocock]

I had some very simple calculations that I was performing in ℕ and displaying with #reduce that were for all practical purposes instant. I have the identical code, except in ℚ, and I'm melting my CPU and getting a full screen of timeout errors:

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

Here's a mwe:

import Mathlib.Tactic

inductive ColS where
| zero : ColS
| up : ColS → ColS

structure LinEq (α : Type) :=
  (m : α)
  (c : α)

def LinEq.eval {α} [Semiring α] (le : LinEq α) (n : α) : α := le.m * n + le.c

def ColS.to_lf (cs: ColS) : LinEq ℚ := match cs with
| ColS.zero => ⟨1, 0⟩
| ColS.up ds =>
  let ⟨m, c⟩ := ds.to_lf
  ⟨3 * m, 3 * c + 1⟩


#reduce (ColS.up $ ColS.zero).to_lf -- works
#reduce (ColS.up $ ColS.zero).to_lf.eval 1 -- times out

[Henrik Böving]

The answer to perf issues with reduce is basically always dont use reduce use eval, reduce is not optimized well at all.

[Matthew Pocock]

Henrik Böving said:

The answer to perf issues with reduce is basically always dont use reduce use eval, reduce is not optimized well at all.

Eval does, indeed, work. Thanks. Sprinkling through some deriving Repr seems to also get the other things that only worked with #reduce working with #eval.