## Stream: new members

### Topic: Making a proposition decidable

#### fkefjlwejlfk (Jan 19 2023 at 20:02):

Hello guys,

I have a function that is a Prop. I need to make sure this function is decidable. For that I think I need to implement a function that returns tt if a Prop holds.
Is there any way to do this easily?

#### Kyle Miller (Jan 19 2023 at 20:06):

Could you give a #mwe with the Prop you're talking about? Deciding things depends a lot on the specifics.

It's true that one way to create decidable Props is to write boolean-valued functions, but that's not always the best way.

#### fkefjlwejlfk (Jan 19 2023 at 20:18):

@Kyle Miller basically I have a function that returns a Prop. the function takes an inductive type and recursively calls itself by "peeling" one of the constructors off until it has the "smallest" constructor, which it maps to a boolean value.

I guess a #mwe would be something like this (although its a bit random)

inductive lan : Type
| numb :  -> lan
| plus : lan -> lan -> lan

def foo (is_right_number :  -> bool) : lan -> Prop
| (lan.numb n) := is_right_number n
| (lan.plus f1 f2) := (foo f1)  (foo f2)

I now want to proof foo is decidable

#### Kyle Miller (Jan 19 2023 at 20:43):

Ok, in this case you're probably better off making it a bool-valued function (and change the conjuction into &&). Then whenever you use it as a Prop it will automatically be decidable.

#### fkefjlwejlfk (Jan 19 2023 at 21:04):

Kyle Miller said:

Ok, in this case you're probably better off making it a bool-valued function (and change the conjuction into &&). Then whenever you use it as a Prop it will automatically be decidable.

For reasons I am unable to explain outside of this #mwe, I am not albe to make it a bool-valued function sadly.

#### Yaël Dillies (Jan 19 2023 at 21:10):

Then what you want is to fill in

instance : foo (is_right_number :  -> bool) : decidable_pred (foo is_right_number) :=
sorry

#### Patrick Johnson (Jan 19 2023 at 21:16):

What exactly do you mean by making foo decidable? Classically, all propositions are decidable, but in order to be able to use it with dec_trivial, you have to construct a decidable instance explicitly:

instance {f x} : decidable (foo f x) :=
begin
induction x with n x y d₁ d₂; unfold foo,
{ apply_instance },
{ exact @and.decidable _ _ d₁ d₂ },
end

#### Eric Wieser (Jan 20 2023 at 01:14):

I would guess that you can use apply_instance in both branches after a resetI

#### Reid Barton (Jan 20 2023 at 07:37):

I would recommend dunfold foo instead of unfold foo just in case there is something fishy going on with the equational lemmas

#### Martin Dvořák (Jan 20 2023 at 07:47):

Reid Barton said:

I would recommend dunfold foo instead of unfold foo just in case there is something fishy going on with the equational lemmas

Is it something we should do always when dunfold foo works?

#### Patrick Johnson (Jan 20 2023 at 07:55):

According to the suggestions:

instance {f x} : decidable (foo f x) :=
by induction x; dunfold foo; resetI; apply_instance

or maybe even

instance {f} : decidable_pred (foo f) :=
λ x, by induction x; dunfold foo; resetI; apply_instance

#### Reid Barton (Jan 20 2023 at 07:56):

Well specifically when writing decidability instances (or other sorts of data that you want to reduce later), you don't want to be rewriting along non-definitional equalities

#### Kyle Miller (Jan 20 2023 at 09:12):

Kasper said:

For reasons I am unable to explain outside of this #mwe, I am not albe to make it a bool-valued function sadly.

Could explain more, hopefully with an #mwe that shows the obstruction? I'm concerned about this because writing a decidable instance is strictly more difficult than writing a bool-valued function. That's because decidable is essentially bool but with a proof of why the truth value is the correct one for the given proposition (and there's a function docs#decidable.to_bool to get a simple bool from a decidable proposition).

Last updated: Dec 20 2023 at 11:08 UTC