heartbeat "golf"

Stream: Is there code for X?

[Chris Birkbeck]

I'm trying to make some PR code run fast (i.e. less heartbeats), so I'm trying to remove some expensive tactics like linarith. What fastest proof of the following:

example (k : ℤ) (hk : 3 ≤ k) : k - 1 ≠ 0 := by

linarith does this in 886. I can't something to do it super quickly, the best I have (from using apply? several times) is

Ne.symm (Int.ne_of_lt (Int.le_sub_left_of_add_le (Int.le_of_lt hk)))

which is 80, quite ugly, but much faster. I bet that there is just some lemma I'm not finding (or maybe this is basically as good as it gets). Is there a faster way to do this?

[Joachim Breitner]

This looks pretty fast already. I would try instantiating the implicit parameters of these lemmas, but elaborating them might actually be slower than inferring.

[Richard Copley]

Fast, but doesn't work :) Unless I misunderstood what you meant, or something changed in Lean or Mathlib between your version and mine to break it.
I would have guessed it would be hard to beat by omega.

import Mathlib.Tactic

count_heartbeats in -- 59
example (k : ℤ) (hk : 3 ≤ k - 1) : k - 1 ≠ 0 :=
  Ne.symm (Int.ne_of_lt  (Int.le_sub_left_of_add_le (Int.le_of_lt hk)))
-- application type mismatch
--   Int.le_of_lt hk
-- argument
--   hk
-- has type
--   3 ≤ k - 1 : Prop
-- but is expected to have type
--   1 + (0 + 1) < k : Prop

count_heartbeats in -- 170
example (k : ℤ) (hk : 3 ≤ k - 1) : k - 1 ≠ 0 :=
  fun h => ((Int.negSucc_not_nonneg 2).mp (hk.trans h.le))

count_heartbeats in -- 125
example (k : ℤ) (hk : 3 ≤ k - 1) : k - 1 ≠ 0 := by omega

[Chris Birkbeck]

hmm yes omega does it in 102 (on mine), which is good enough for me, so thats probably what I'll use.

[Chris Birkbeck]

Richard Copley said:

Fast, but doesn't work :) Unless I misunderstood what you meant, or something changed in Lean or Mathlib between your version and mine to break it.
I would have guessed it would be hard to beat by omega.

import Mathlib.Tactic

count_heartbeats in -- 59
example (k : ℤ) (hk : 3 ≤ k - 1) : k - 1 ≠ 0 :=
  Ne.symm (Int.ne_of_lt  (Int.le_sub_left_of_add_le (Int.le_of_lt hk)))
-- application type mismatch
--   Int.le_of_lt hk
-- argument
--   hk
-- has type
--   3 ≤ k - 1 : Prop
-- but is expected to have type
--   1 + (0 + 1) < k : Prop

count_heartbeats in -- 170
example (k : ℤ) (hk : 3 ≤ k - 1) : k - 1 ≠ 0 :=
  fun h => ((Int.negSucc_not_nonneg 2).mp (hk.trans h.le))

count_heartbeats in -- 125
example (k : ℤ) (hk : 3 ≤ k - 1) : k - 1 ≠ 0 := by omega

oh also, I had a typo in my original post, (hk : 3 ≤ k), which is why it doesnt work for you!

[Chris Birkbeck]

I thought I'd fixed fast enough, but you were faster :P

[Kim Morrison]

For those playing heartbeat golf, notice that master now supports count_heartbeats in my_tactic.

[Kim Morrison]

(i.e. you can count heartbeats in a single proof step, rather than the whole declaration)

[Kim Morrison]

And remember that the relevant scale for heartbeats is 200000. Whether a step takes 80 or 800 is basically irrelevant.

[Michael Stoll]

The difference can accumulate, though...