Stream: Coq users

Topic: Trying to de-rust on Coq matching


view this post on Zulip Eli Dupree (Jan 23 2024 at 16:26):

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

view this post on Zulip Karl Palmskog (Jan 23 2024 at 23:08):

standard advice for handling provenance inside matches is to use something like Equations

view this post on Zulip Eli Dupree (Jan 23 2024 at 23:09):

interesting, I'll take a look!

view this post on Zulip Eli Dupree (Jan 23 2024 at 23:12):

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

view this post on Zulip Karl Palmskog (Jan 23 2024 at 23:13):

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

view this post on Zulip Karl Palmskog (Jan 23 2024 at 23:15):

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

view this post on Zulip Eli Dupree (Jan 23 2024 at 23:17):

thanks, that helps me out a bit!

view this post on Zulip Karl Palmskog (Jan 23 2024 at 23:18):

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

view this post on Zulip Karl Palmskog (Jan 23 2024 at 23:20):

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.

view this post on Zulip Paolo Giarrusso (Jan 24 2024 at 10:08):

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.

view this post on Zulip Eli Dupree (Jan 24 2024 at 11:46):

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

view this post on Zulip Paolo Giarrusso (Jan 25 2024 at 04:57):

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