Stream: Coq users

Topic: conversion


view this post on Zulip zohaze (Nov 17 2022 at 16:31):

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

view this post on Zulip Julien Puydt (Nov 17 2022 at 16:49):

That's in general not possible, since bool is basically for computable while Prop is for logical.

view this post on Zulip Julien Puydt (Nov 17 2022 at 16:50):

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

view this post on Zulip Julien Puydt (Nov 17 2022 at 16:52):

In boolp.v, asbool is a function from Prop to bool which can do your conversion.

view this post on Zulip zohaze (Jan 20 2023 at 17:23):

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?

view this post on Zulip Michael Soegtrop (Jan 20 2023 at 18:24):

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

view this post on Zulip zohaze (Jan 21 2023 at 04:28):

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

view this post on Zulip Michael Soegtrop (Jan 21 2023 at 09:16):

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.

view this post on Zulip zohaze (Jan 21 2023 at 14:38):

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

view this post on Zulip Huỳnh Trần Khanh (Jan 21 2023 at 14:40):

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.

view this post on Zulip Huỳnh Trần Khanh (Jan 21 2023 at 14:49):

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?

view this post on Zulip Huỳnh Trần Khanh (Jan 21 2023 at 14:51):

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?

view this post on Zulip zohaze (Jan 21 2023 at 15:11):

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