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

I'm a little confused by your example, can you elaborate?

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

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.

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.

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: Jun 22 2024 at 23:01 UTC