It's been a while since I've done sophisticated Coq programming, and I'm forgetting how to approach this situation.

So, in my code, I have a bunch of functions that are parameterized with a symbol type, and some Symbols may represent variables, but not all of them do. So I have things like:

```
Lemma some_lemma
[Symbol]
IsVar : Symbol -> Prop
VarMeaning : ∀s:Symbol, IsVar s -> Meaning
...
: ...
```

This is working fine. But in other places, I need it reified, where you can match on whether a particular symbol is a variable or not. So I've written

```
Definition some_function
[Symbol]
is_var : Symbol -> bool
var_meaning : ∀s:Symbol, eq_true (is_var s) -> Meaning
...
: ...
match is_var s with
| true => var_meaning s _
| false => ...
end
```

But now I have a problem: How do I fill the hole in `var_meaning s _`

? In the `match`

, coq "forgets" the fact `is_var s = true`

that would allow me to produce the `eq_true`

instance. I know I've done this before, but I'm blanking on it.

I also wonder if there's a cleaner way to represent this in Coq in the first place

standard advice for handling provenance inside `match`

es is to use something like Equations

interesting, I'll take a look!

I do want to understand the underlying way it's done rather than _just_ having it be generated for me, so that I won't have trouble understanding how to prove things about the resulting definition

Equations uses a quite different approach from what you would use manually

but here is a manual example of what Equations will give you "for free": https://github.com/palmskog/fitch/blob/master/coq/fitch_decidable.v#L767-L778

thanks, that helps me out a bit!

as do nearly all definitional packages for proof assistants, Equations ultimately works at implementation language API level

so to me there's not all that much to be gained by knowing what goes on under the hood there. But there are ways to do a lot of things Equations does using regular Gallina code, sure.

~~Let me rephrase that:~~ with Equations, you're never supposed to care about the generated definitions. You treat it as abstract, and the equations you write become lemmas used for simplification.

oh! that makes sense to me now. Kind of like how inductive type definitions relate to the raw Calculus of Constructions.

Roughly yes. (Your example makes sense, even if Coq doesn't use the raw Calculus of Constructions, but the Calculus of Inductive Constructions, where inductives are primitives).

Last updated: Jun 13 2024 at 19:02 UTC