Ralf Jung (Jun 24 2021 at 08:09): 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.
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.
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.
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.
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
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...
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]).
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 (xΓ ⊨ Unit : TUnit))
doesn't look to me like this pattern was made for that purpose...?
MackieLoeffel (Jun 24 2021 at 11:19):Can you try elim: Htyped => -[ ^ x ].?
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.
Ralf Jung (Jun 24 2021 at 11:59):no it's something in iris, we have big-op notation that uses [^
Ralf Jung (Jun 24 2021 at 11:59):https://gitlab.mpi-sws.org/iris/iris/-/issues/273
Ralf Jung (Jun 24 2021 at 12:00):we might even use that syntax already longer than ssreflect does^^
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
Ralf Jung (Jun 24 2021 at 12:02):it doesnt even introduce anything, it just renames the topmost assumption on the goal to x
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.
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
Ralf Jung (Jun 24 2021 at 13:41):oO
Ralf Jung (Jun 24 2021 at 13:41):why does it need Coq strings for anything...?
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.
Janno (Jun 24 2021 at 13:58):Right now this thing is pretty useless because nobody wants to declare structures for all their types.
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
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?
Ralf Jung (Jun 24 2021 at 14:04):(Ident.of_string does the last step)
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.
Janno (Jun 24 2021 at 14:06):This might be different in 8.14
Last updated: Sep 23 2023 at 07:01 UTC