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.
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.
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.
Okay, the docs tell me that this should be possible. It's a bit of implementation work but not too much, I think.
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
@MackieLoeffel is it possible to use that with
I suppose we could try using the ssreflect versions of those tactcs...
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 ].
Error: No assumption in (uPred_entails emp (xΓ ⊨ Unit : TUnit))
doesn't look to me like this pattern was made for that purpose...?
Can you try
elim: Htyped => -[ ^ x ].?
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.
no it's something in iris, we have big-op notation that uses
we might even use that syntax already longer than ssreflect does^^
Can you try
elim: Htyped => -[ ^ x ].?
that doesnt error but also doesnt seem to do anything useful
it doesnt even introduce anything, it just renames the topmost assumption on the goal to
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.
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
why does it need Coq strings for anything...?
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.
Right now this thing is pretty useless because nobody wants to declare structures for all their types.
It's more of a proof of concept.. The question is whether the final two testcases have the desired behavior
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?
Ident.of_string does the last step)
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.
This might be different in 8.14
Last updated: Jan 31 2023 at 13:02 UTC