Stream: Coq users

Topic: mangle-names


view this post on Zulip Ralf Jung (Aug 28 2020 at 07:47):

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

view this post on Zulip Ralf Jung (Aug 28 2020 at 07:52):

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.

view this post on Zulip Enrico Tassi (Aug 28 2020 at 07:52):

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

view this post on Zulip Ralf Jung (Aug 28 2020 at 07:52):

This is an extremely simplified example

view this post on Zulip Enrico Tassi (Aug 28 2020 at 07:53):

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

view this post on Zulip Ralf Jung (Aug 28 2020 at 07:53):

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.

view this post on Zulip Ralf Jung (Aug 28 2020 at 07:54):

(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.)

view this post on Zulip Enrico Tassi (Aug 28 2020 at 07:54):

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.

view this post on Zulip Ralf Jung (Aug 28 2020 at 07:54):

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?

view this post on Zulip Ralf Jung (Aug 28 2020 at 07:56):

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.

view this post on Zulip Enrico Tassi (Aug 28 2020 at 07:57):

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.

view this post on Zulip Enrico Tassi (Aug 28 2020 at 08:00):

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.

view this post on Zulip Janno (Aug 28 2020 at 08:16):

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

view this post on Zulip Ralf Jung (Aug 28 2020 at 08:19):

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.

view this post on Zulip Maxime Dénès (Aug 28 2020 at 08:19):

For revert, I'm not sure. For lemmas like (forall x, Px) -> Q, it looks clear that it relies on auto-generated names:

view this post on Zulip Maxime Dénès (Aug 28 2020 at 08:20):

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.

view this post on Zulip Enrico Tassi (Aug 28 2020 at 08:22):

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

view this post on Zulip Enrico Tassi (Aug 28 2020 at 08:24):

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.

view this post on Zulip Ralf Jung (Aug 28 2020 at 08:27):

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

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

view this post on Zulip Ralf Jung (Aug 28 2020 at 08:27):

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.

view this post on Zulip Ralf Jung (Aug 28 2020 at 08:28):

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

view this post on Zulip Maxime Dénès (Aug 28 2020 at 08:31):

you mean like in an assert?

view this post on Zulip Enrico Tassi (Aug 28 2020 at 08:31):

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

view this post on Zulip Gaëtan Gilbert (Aug 28 2020 at 08:32):

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

view this post on Zulip Maxime Dénès (Aug 28 2020 at 08:32):

@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 *)

view this post on Zulip Maxime Dénès (Aug 28 2020 at 08:33):

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

view this post on Zulip Enrico Tassi (Aug 28 2020 at 08:33):

This is because you should never call an hypothesis H ;-P

view this post on Zulip Maxime Dénès (Aug 28 2020 at 08:34):

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

view this post on Zulip Ralf Jung (Aug 28 2020 at 08:34):

Maxime Dénès said:

you mean like in an assert?

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

view this post on Zulip Ralf Jung (Aug 28 2020 at 08:35):

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 ;)

view this post on Zulip Maxime Dénès (Aug 28 2020 at 08:35):

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

view this post on Zulip Maxime Dénès (Aug 28 2020 at 08:36):

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

view this post on Zulip Ralf Jung (Aug 28 2020 at 08:37):

lol^^

view this post on Zulip Ralf Jung (Aug 28 2020 at 08:37):

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.

view this post on Zulip Ralf Jung (Aug 28 2020 at 08:37):

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

view this post on Zulip Maxime Dénès (Aug 28 2020 at 08:38):

looks a bit strange at first glance

view this post on Zulip Ralf Jung (Aug 28 2020 at 08:40):

it uses a local lambda in refine... but those names sure should still be usable?

view this post on Zulip Ralf Jung (Aug 28 2020 at 08:51):

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

view this post on Zulip Ralf Jung (Aug 28 2020 at 08:51):

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

view this post on Zulip Ralf Jung (Aug 28 2020 at 08:51):

maybe P somehow gets mangles as part of being abstracted or so?

view this post on Zulip Ralf Jung (Aug 28 2020 at 08:52):

minimal reproducer:

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

view this post on Zulip Ralf Jung (Aug 28 2020 at 08:52):

works without name mangling but breaks with it.

view this post on Zulip Ralf Jung (Aug 28 2020 at 08:53):

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.

view this post on Zulip Ralf Jung (Aug 28 2020 at 08:54):

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

view this post on Zulip Enrico Tassi (Aug 28 2020 at 08:55):

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

view this post on Zulip Ralf Jung (Aug 28 2020 at 09:35):

Cc @robbert

view this post on Zulip Robbert Krebbers (Aug 28 2020 at 13:56):

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

view this post on Zulip Ralf Jung (Aug 28 2020 at 14:01):

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

view this post on Zulip Robbert Krebbers (Aug 28 2020 at 14:03):

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.

view this post on Zulip Jasper Hugunin (Aug 28 2020 at 14:34):

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.

view this post on Zulip Ralf Jung (Aug 28 2020 at 14:54):

@Jasper Hugunin we already reduced that to an abstract problem

view this post on Zulip Ralf Jung (Aug 28 2020 at 14:54):

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

view this post on Zulip Jasper Hugunin (Aug 28 2020 at 14:55):

Ah! I was overlooking the P inside abstract. Alright then.


Last updated: Feb 01 2023 at 11:04 UTC