adding a `Decidable` instance to a definition

Stream: mathlib4

[Jireh Loreaux]

I have a definition which I would like to define in terms of dite, but the if condition is something which will rarely (but potentially could in certain circumstances) have an existing Decidable instance. Moreover the condition is a bit messy, so requiring [Decidable messy_condition] everywhere just in order to write the function in a theorem statement is undesirable. To put icing on the cake, in practice the then term will (almost?) always be noncomputable.

So, my desire would be to use Classical.decidable in the definition, but I realize that this is bad practice. I'm soliciting recommendations.

[Emilie (Shad Amethyst)]

You do have the classical tactic for making proofs which you know won't be needed for computation easier to work with

[Jireh Loreaux]

yes, but that doesn't help me with statements

[Yakov Pechersky]

import Mathlib

def foo : ℕ → Prop := fun n => Nat.Prime n

#synth DecidablePred foo -- failed, as expected

def bar (n : ℕ) : ℕ  :=
  if h : foo n then 0 else 1 -- failed to synthesize instance Decidable (foo n)

noncomputable def baz (n : ℕ) : ℕ  := by
  classical exact if h : foo n then 0 else 1 -- this is fine

[Sébastien Gouëzel]

You can definitely use Classical.decidable in the definition (possibly with an irreducible_def to make sure that unfolding will only happen on purpose), and then register a lemma with [Decidable messy_condition] unfolding the definition but using this decidability condition instead of the Classical.decidable one.

[Sébastien Gouëzel]

Then most lemmas just using the statement wouldn't need any decidability condition, and you can start a proof with classical if you need to unfold the definition inside the proof, and moreover if sometimes you have the [Decidable messy_condition] in the context you can unfold the definition using the lemma I just alluded to, and avoid diamonds like that.