zohaze (Nov 17 2022 at 16:31): 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).)
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.
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?)
Julien Puydt (Nov 17 2022 at 16:52):In boolp.v, asbool is a function from Prop to bool which can do your conversion.
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?
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.
zohaze (Jan 21 2023 at 04:28):1) In predicate (In n l) whose output is proposition may be converted into bool ?
like {In nl+~In nl} ?
2) When i Check ltb_reflect theorem ,i get message "The reference ltb_reflect was not found in the current environment" (reference given by you) .
3) What about a function which is inductively defined and its output is proposition ? I want to convert below one
Inductive beautiful : nat -> Prop :=
b_0 : beautiful 0
| b_3 : beautiful 3
| b_5 : beautiful 5
| b_sum : forall n m, beautiful n -> beautiful m -> beautiful (n+m)
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.
zohaze (Jan 21 2023 at 14:38):i have to describe function in boolean form ,against each and every constructor separately?
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.
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?
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?
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: Oct 13 2024 at 01:02 UTC