What is the best way to infer Decidable propositions?

Stream: general

[l1mey]

I have defined iN.poisonPreconditions taking in a function isPoison that returns a decidable proposition. Is there a way to make working with iN.poisonPreconditions nicer, instead of having to write out an instance declaration every time?

image.png

A solution to this would be to accept a function that returns a boolean, but I believe this wouldn't actually show that the isPoison function is decidable at all. Since I control all the code for these functions, every possible isPoison function I write will be decidable.

Is there a common pattern for writing functions that return a bool/decidable proposition?

[Aaron Liu]

just take a function returning a boolean

[Matt Diamond]

I believe this wouldn't actually show that the isPoison function is decidable

why is this a problem, though? you don't need decidability if you're working with a boolean function

[Matt Diamond]

btw, you can do bif ... then ... else and it's optimized for booleans (see docs#cond)

[Matt Diamond]

to expand on this a little more: if you were to use a boolean value x in an if ... then ... else statement, Lean would just convert the condition to x = true (since if works with propositions, not booleans), and this would already be decidable because boolean equality is decidable in Lean (via docs#Bool.decEq)

however, as I said, you might as well just use bif ... then ... else / cond if you're using a boolean condition