zvezdin (Aug 07 2020 at 09:00): zvezdin (Aug 07 2020 at 09:00):Is it possible in Galina to branch within a function based on the ability for me to construct a specific type or not. (e.g. assume that a function takes two nat's and does something different if they are equal).
Cody Roux (Aug 07 2020 at 13:19):I'm a little confused by your example, can you elaborate?
Paolo Giarrusso (Aug 08 2020 at 03:19):You can at least branch on booleans or use pattern matching on inductives. In that specific case, IIRC you can use if (Nat.eqb n1 n2) then ... else...
More in general, it sounds like you might want a way to branch on whether a proposition P (like n1 = n2) holds. Usually, that's only possible if P is decidable (or if you postulate that it is); for instance, equality of two naturals is decidable, equality of two functions from naturals to booleans is not. There are multiple libraries with ways to deal with decidable propositions (e.g. stdpp has a Decision typeclass).
k32 (Aug 08 2020 at 11:39):If you manage to prove that your proposition is decidable, then you can branch on it (sort of):
Definition foo (P : Prop) (P_decidable : {P} + {not P}) :=
if P_decidable then
something
else
something_else.
Thank you for all this clarification! You correctly guessed my question. I was missing the fact that I can construct a bool and then case analyse that. This works. However for the sake of it, is it possible for me to check, inside of a function, if it is legal for me to construct something or not? I.e. given a, b: nat, can my function safely check if it can construct a proof of "a = b" through "eq_refl a" ? Or is the only way to check via bool constructions.
zvezdin (Aug 08 2020 at 12:46):Thank you for all this clarification! You correctly guessed my question. I was missing the fact that I can construct a bool and then case analyse that. This works. However for the sake of it, is it possible for me to check, inside of a function, if it is legal for me to construct something or not? I.e. given a, b: nat, can my function safely check if it can construct a proof of "a = b" through "eq_refl a" ? Or is the only way to check via bool constructions.
Jasper Hugunin (Aug 08 2020 at 14:49):If you want to branch on whether or not types or terms are well-formed, like you suggest here, you have to be working on the meta-level, which in Coq is primarily done by writing tactics in Ltac or Ltac2.
Last updated: Oct 13 2024 at 01:02 UTC