Making a proposition decidable

Stream: new members

[fkefjlwejlfk]

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]

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]

@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]

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]

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]

Then what you want is to fill in

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

[Patrick Johnson]

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]

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

[Reid Barton]

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]

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]

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]

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]

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).