@Maxime Dénès `-mangle-names`

has found the first issues in std++. :) The remaining failures are getting more... interesting.

One is this:

```
Global Set Mangle Names.
Lemma test (i: nat): i = 0.
Proof. revert i. induction i.
```

Previously that would work, but now it does not any more. I am not sure if that is intended behavior or not.

Also, it looks like applying a lemma such as `(forall x, P x) -> Q`

to a goal no longer preserves the name `x`

. I am not sure if that is deliberate. It means name mangling affects our output tests, which could become a challenge when adding this to CI.

Why do you need to revert i? Can't you just run induction on it?

This is an extremely simplified example

OK. To my understanding "names" below the bar are not stable by mangling.

and while it might be possible to work around in this particular case, I am asking about the general case -- currently `revert`

forgets the name with mangling enabled. That seems odd.

(I am trying to get Robbert to join here so he can raise his opinion on whether he thinks this proof script is reasonable or not.)

The name is kept, but as a "pretty printing" hint. Or at least, this is my mental model. Coq is "locally nameless" in some sense.

Enrico Tassi said:

OK. To my understanding "names" below the bar are not stable by mangling.

yes that's what currently happens. I am wondering why though -- AFAIK there is no case where the name would change when being reverted without mangling?

the point of name mangling is to detect proof scripts that rely on auto-generated names and as such could break when the context changes a bit. but AFAIK the proof script above dos not rely on auto-generated names in any way, ergo I would expect it to still work.

Try your first example but add a section variable i. I would not be surprised to see a forall i0 after the revert. Then it may still work, but kind of odd.

Hum, no I guess the section variable thing cannot trick it here.. but for another reason. Anyway, I guess @Jasper Hugunin can explain how it works better than me.

I thought being able to do induction in names in the goal was considered to be unreliable anyway? (I thought it had something to do with section variables but maybe not..)

I didn't even know one can do induction on names in the goal, so I wouldn't know^^ but that was just to demonstrate. I am more wondering why `revert`

forgets the name in the first place.

For revert, I'm not sure. For lemmas like `(forall x, Px) -> Q`

, it looks clear that it relies on auto-generated names:

```
Lemma foo : (forall H : nat, H = H) -> True.
Proof.
trivial.
Qed.
Goal True -> True.
Proof.
intros.
apply foo. (* goal is now forall H0 : nat, H0 = H0 *)
Abort.
```

This is a bit verbose, but shows that `induction i`

(where the `i`

is in the goal) can be tricked by adding an `i`

in the context.

```
Coq < Lemma test j i : i = j + 1.
1 subgoal
j, i : nat
============================
i = j + 1
test < revert j i.
1 subgoal
============================
forall j i : nat, i = j + 1
test < induction i.
2 subgoals
j : nat
============================
0 = j + 1
subgoal 2 is:
S i = j + 1
test < Undo.
1 subgoal
============================
forall j i : nat, i = j + 1
test < intro i.
1 subgoal
i : nat
============================
forall i0 : nat, i0 = i + 1
test < induction i.
2 subgoals
============================
forall i : nat, i = 0 + 1
subgoal 2 is:
forall i0 : nat, i0 = S i + 1
```

My guess is that `i`

is also in the goal (as a pretty printing hint), but in order to point to that `i`

you have to say `induction i0`

because the pretty printer said so.

it looks clear that it relies on auto-generated names:

that is surprising, I wouldn't have expected coq to rename things here

This is a bit verbose, but shows that induction i (where the i is in the goal) can be tricked by adding an i in the context.

that's a good argument against induction with names in the goal. however, mangle-names doesnt prevent that -- it affects revert, not induction.

oh, hm, okay looks like name mangling also changes the name when explicitly stating the goal as `forall x, P x`

. interesting.

you mean like in an `assert`

?

This shows that taking a lemma and copy pasting it into a different section triggers the pretty printer rage, and this in turn breaks `induction i`

```
Coq < Section A. Variable i : nat. Lemma test : forall i, i = 0.
i is declared
1 subgoal
i : nat
============================
forall i0 : nat, i0 = 0
```

names in bindings (forall, fun, ...) always get refreshed so mangle always mangles them

@Ralf Jung I think the behiavor of mangle names is expected given the one of renaming:

```
Goal True -> True.
intros.
assert (forall H : nat, H = H). (* gives forall H0 : nat, H0 = H0 *)
```

It seems that stdlib++ is relying more on generated names than you thought ;)

This is because you should never call an hypothesis `H`

;-P

@Gaëtan Gilbert I guess the question is why do we refresh. Doesn't seem immediately obvious to me.

Maxime Dénès said:

you mean like in an

`assert`

?

I meant like in `Lemma test: forall x:nat, x=0.`

Maxime Dénès said:

It seems that stdlib++ is relying more on generated names than you thought ;)

it seems that coq is changing user-given names more than I thought ;)

Yes, that's what I call Coq's paranoiac renaming.

There are examples where it even triggers more clashes than it would without renaming :)

lol^^

anyway this `induction`

case should be easy to fix here, I can just not revert. we have another failure but that's a proof script that I do not understand, we will have to wait for robbert for that.

this thing fails: https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/theories/lexico.v#L150

looks a bit strange at first glance

it uses a local lambda in `refine`

... but those names sure should still be usable?

@Maxime Dénès looks like the problem is `abstract`

`apply (sig_eq_pi P).`

works but `abstract (apply (sig_eq_pi P).`

fails.

maybe `P`

somehow gets mangles as part of being abstracted or so?

minimal reproducer:

```
Lemma test: forall x: nat, nat.
Proof. intros x. abstract (exact x). Qed.
```

works without name mangling but breaks with it.

I'll open an issue for this, this definitely feels like a bug to me -- and there's no work-around that I can see other than not using `abstract`

.

https://github.com/coq/coq/issues/12928

Yup, I imagine abstract reverts the whole proof context, and then uses that goal to start a new proof.

Cc @robbert

(I am trying to get Robbert to join here so he can raise his opinion on whether he thinks this proof script is reasonable or not.)

I don't think this proof script is reasonable. The fact that `induction x`

works when `x`

is a forall in the goal is a kludge, IMHO.

I agree with Enrico's argument for why it's weird:

Try your first example but add a section variable i. I would not be surprised to see a forall i0 after the revert. Then it may still work, but kind of odd.

okay :) so when I see more of these I'll just intros or use numbers

okay :) so when I see more of these I'll just intros or use numbers

Number only work for non-dependent ∀s, I think, which are generally not named in the first place.

Looks like you've worked things out without me. I'll take a closer look at `lexico.v#L150`

, but might be a bit; I'll probably have to clone and compile stdpp.

@Jasper Hugunin we already reduced that to an `abstract`

problem

reported at https://github.com/coq/coq/issues/12928

Ah! I was overlooking the `P`

inside `abstract`

. Alright then.

Last updated: Jun 20 2024 at 11:02 UTC