Stream: Coq users

Topic: Reliable names from inductive definitions?


view this post on Zulip Ralf Jung (Jun 24 2021 at 08:09):

Set Mangle Names is a great way to harden proofs against names shifting accidentally. However, it also reveals that Coq is poorly equipped to actually write proofs in this robust style once one works with large inductive types where intro patterns are infeasible.
Is there a way to tell destruct/induction to use exactly the names that the terms have been given in the Inductive definition, and error of those names are already used? (and some deterministic scheme for induction hypotheses) That would avoid the dreaded fresh and there would let us write proofs where we can rely on the names without enormous intro patterns or ad-hoc hacks.

view this post on Zulip Janno (Jun 24 2021 at 08:17):

I suspect you could write this in Ltac2 by extracting the inductive type from the type of the discriminee, then generating all its constructors unsafely (using the same universe instance as the type), typechecking the resulting term and extracting the names from these types (which can be converted to Coq strings if necessary). The last step is the one I am most worried about because I think it will generate fresh names since it is executed in the current context. So maybe the best approach would be doing all of this outside a proof (maybe after defining the inductive type) and saving the resulting strings in a canonical structure/typeclass instance which can then be queried at proof time.

view this post on Zulip Janno (Jun 24 2021 at 08:18):

I haven't worked much with Ltac2's Std module but I suspect you can assemble the intro patterns programatically. That would of course be necessary for all of this to work.

view this post on Zulip Janno (Jun 24 2021 at 08:23):

Okay, the docs tell me that this should be possible. It's a bit of implementation work but not too much, I think.

view this post on Zulip MackieLoeffel (Jun 24 2021 at 11:00):

You can also use the [^ ident] intro pattern from ssreflect, which I think was made for this purpose: https://coq.inria.fr/distrib/current/refman/proof-engine/ssreflect-proof-language.html#block-introduction

view this post on Zulip Ralf Jung (Jun 24 2021 at 11:06):

@MackieLoeffel is it possible to use that with induction/destruct?
I suppose we could try using the ssreflect versions of those tactcs...

view this post on Zulip Ralf Jung (Jun 24 2021 at 11:10):

hm, elim: Htyped=> [^ x]. does not work

Error: Syntax error: [ssripats_ne] expected after '=>' (in [ssrintros_ne]).

view this post on Zulip Ralf Jung (Jun 24 2021 at 11:15):

hm, maybe something is interfering with the syntax here, but more spaces just change the error message

elim: Htyped => [ ^ x ].

shows

Error: No assumption in (uPred_entails emp (  Unit : TUnit))

view this post on Zulip Ralf Jung (Jun 24 2021 at 11:16):

doesn't look to me like this pattern was made for that purpose...?

view this post on Zulip MackieLoeffel (Jun 24 2021 at 11:19):

Can you try elim: Htyped => -[ ^ x ].?

view this post on Zulip MackieLoeffel (Jun 24 2021 at 11:20):

I think something in stdpp is messing with the [^ notation, so you have to write [ ^. But elim: v => [ ^ v]. works for me. The only problem is that the induction hypothesis don't have usable names.

view this post on Zulip Ralf Jung (Jun 24 2021 at 11:59):

no it's something in iris, we have big-op notation that uses [^

view this post on Zulip Ralf Jung (Jun 24 2021 at 11:59):

https://gitlab.mpi-sws.org/iris/iris/-/issues/273

view this post on Zulip Ralf Jung (Jun 24 2021 at 12:00):

we might even use that syntax already longer than ssreflect does^^

view this post on Zulip Ralf Jung (Jun 24 2021 at 12:02):

MackieLoeffel said:

Can you try elim: Htyped => -[ ^ x ].?

that doesnt error but also doesnt seem to do anything useful

view this post on Zulip Ralf Jung (Jun 24 2021 at 12:02):

it doesnt even introduce anything, it just renames the topmost assumption on the goal to x

view this post on Zulip Ralf Jung (Jun 24 2021 at 12:02):

also the goal

  Σ : gFunctors
  H : irisGS stlc_lang Σ
  Γ : list type
  e : expr
  τ : type
  ============================
   (x : var) (τ0 : type), [] !! x = Some τ0   []  Var x : τ0

makes me wonder if I am using elim correctly. there are a bunch of unused variables here which the Coq induction does not have.

view this post on Zulip Janno (Jun 24 2021 at 13:37):

I got pretty far with the Ltac2 stuff but I am not sure if this is what you wanted. Still, maybe this is useful for further experiments: https://gist.github.com/Janno/60c93a2eb001a318426e57b79331a987

view this post on Zulip Ralf Jung (Jun 24 2021 at 13:41):

oO

view this post on Zulip Ralf Jung (Jun 24 2021 at 13:41):

why does it need Coq strings for anything...?

view this post on Zulip Janno (Jun 24 2021 at 13:58):

Because I am talking a bit of a detour through canonical structures to perform the extraction of names from constructor arguments in a (more or less) empty context. I think I could skip that by making a new goal and clearing all hypotheses.

view this post on Zulip Janno (Jun 24 2021 at 13:58):

Right now this thing is pretty useless because nobody wants to declare structures for all their types.

view this post on Zulip Janno (Jun 24 2021 at 13:59):

It's more of a proof of concept.. The question is whether the final two testcases have the desired behavior

view this post on Zulip Ralf Jung (Jun 24 2021 at 14:03):

can't Ltac2 directly access the Inductive definition, get the name as an Ltac2 string, turn that into an ident without freshening, and use that?

view this post on Zulip Ralf Jung (Jun 24 2021 at 14:04):

(Ident.of_string does the last step)

view this post on Zulip Janno (Jun 24 2021 at 14:06):

No, Ltac2 is still missing a lot of functions related to inductive types. I think right now there isn't even a way to get the number of constructors of an inductive type, which is why I am using a match term as a workaround.

view this post on Zulip Janno (Jun 24 2021 at 14:06):

This might be different in 8.14


Last updated: Jan 31 2023 at 13:02 UTC