prevent contradiction from timing out

Stream: lean4

[Jakob von Raumer]

When I try this

import Mathlib.Data.ZMod.Basic

example
  (h₁ : 1 + 1 = 2)
  (h₂ : (123456789101112 : ZMod 340282366920938463463374607431768211456).val < 340282366920938463463374607431768211456)
  (h₃ : ¬ 1 + 1 = 2) : False := by
  contradiction

I get a timeout, probably because contradiction takes too long trying to match the type of h₂ with 1 + 1 = 2, how can I prevent this? Putting the big number in a definition doesn't help either...

[Alex J. Best]

I'm not sure it can be prevented without fixing contradiction to not do this. In the meantime I'd probably switch to spelling the contradiction out as exact h3 h1 or maybe just simp_all?

[Jakob von Raumer]

This is just an MWE pulled out of an aesop execution that stalls for the same reason, leaving goals with contradicting hypotheses

[Heather Macbeth]

contadiction tries decide by default, which may be why it is so slow. The MetaM version of contradiction includes a config option to disable this, and I've been thinking of requesting that this functionality be exposed to users of the tactic using set_option.

[Kevin Buzzard]

We just stopped simp from trying decide by default for this kind of reason, right?

[Ruben Van de Velde]

Can we override core tactics in mathlib or only extend them?

[Kevin Buzzard]

I am not an expert but my impression is that we can override them (my evidence: I overrode done so that it printed a tada emoji)

[Heather Macbeth]

I think this is an awkward case: you can override to make a tactic succeed in a different way, or succeed where it would have failed, but (AFAIK) you can't make it fail where it would have succeeded.

[Jakob von Raumer]

Ah thanks for the pointer, maybe this behaviour is actually not there anymore (I'm still using 4.3.0)

[Damiano Testa]

I also do not know if you can make a tactic fail "nicely" if it would have succeeded, but you can certainly cripple it:

import Lean.Elab.Tactic.Basic

open Lean Elab Tactic in
elab_rules : tactic
  | `(tactic| contradiction) => do
    logError "oh no!"
    setGoals []

example (h : False) : False := by
  contradiction