I have function f1 with two arguments of natural number and output a proposition . I want to convert the output(prop) into

bool (Definition converted (n1 n2 : nat) : bool :=(f1 n1 n2).)

That's in general not possible, since `bool`

is basically for computable while `Prop`

is for logical.

You can do something like this with more axioms, like what is in mathcomp-analysis' classical_sets.v (or is it boolp.v?)

In boolp.v, `asbool`

is a function from `Prop`

to `bool`

which can do your conversion.

Thank you. I want to implement

```
Variant reflect (P : Prop) : bool -> Type :=
| ReflectT : P -> reflect P true
| ReflectF : ~ P -> reflect P false.
```

in above function. Plz guide me how i can do it?

You might want to read the corresponding section in software foundations: https://softwarefoundations.cis.upenn.edu/vfa-current/Decide.html.

In predicate (In p l) whose output is proposition may be converted into bool by using above ?(From above lt,gt is possible)

There is no way to do an automatic conversion - in general this is not possible because Props might be undecidable while bools can simply be computed. If you would have a function which could convert a Prop to a bool automatically, you would have a function which can prove any theorem (since any theorem can be written as Prop).

If you have a function which is easily computable, it is a good idea to write it in bool right away.

Regarding the "beautiful" example from SF: I won't discuss the details here to not spoil the fun for others. I can say that an efficient algorithm which computes (as a bool) if a number is "beautiful" would look very different from the Prop based definition. It takes a little bit of thinking - you should have it in a few minutes.

i have to describe function in boolean form ,against each and every constructor separately?

No. To describe a function in boolean form, you have to provide an algorithm for the computer to check whether the number is beautiful or not. Then you can prove the algorithm is correct. In general, the algorithm can look entirely different from the inductive definition.

Now if you are creative enough, you will realize that `beautiful n`

is true if `n`

can be represented as `3 * i + 5 * j`

. So your algorithm can check every possible `i`

value (from 0 to `n`

is enough) and then check whether there's a corresponding `j`

value. Then you can prove that your algorithm is correct by doing some induction on `n`

?

Now in your correctness proof you will indeed need to use the constructors. I believe Software Foundations already has a cute example for the `ev`

predicate, maybe you can learn from it?

Thanks. Automatically conversion is not possible. Decidable In predicate can be converted to bool by using reflect.

Last updated: Jan 27 2023 at 00:03 UTC