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?)
asbool is a function from
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
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