`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 `induction`

/`destruct`

?

I suppose we could try using the ssreflect versions of those tactcs...

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...?

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 `[^`

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

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

MackieLoeffel said:

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 `x`

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

oO

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: Jun 23 2024 at 01:02 UTC