Ralf Jung (Aug 28 2020 at 07:47): 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.
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.
Enrico Tassi (Aug 28 2020 at 07:52):Why do you need to revert i? Can't you just run induction on it?
Ralf Jung (Aug 28 2020 at 07:52):This is an extremely simplified example
Enrico Tassi (Aug 28 2020 at 07:53):OK. To my understanding "names" below the bar are not stable by mangling.
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.
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.)
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.
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?
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.
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.
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.
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..)
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.
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:
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.
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.
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
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.
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.
Maxime Dénès (Aug 28 2020 at 08:31):you mean like in an assert?
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
names in bindings (forall, fun, ...) always get refreshed so mangle always mangles them
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 *)
It seems that stdlib++ is relying more on generated names than you thought ;)
Enrico Tassi (Aug 28 2020 at 08:33):This is because you should never call an hypothesis H ;-P
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.
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.
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 ;)
Maxime Dénès (Aug 28 2020 at 08:35):Yes, that's what I call Coq's paranoiac renaming.
Maxime Dénès (Aug 28 2020 at 08:36):There are examples where it even triggers more clashes than it would without renaming :)
Ralf Jung (Aug 28 2020 at 08:37):lol^^
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.
Ralf Jung (Aug 28 2020 at 08:37):this thing fails: https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/theories/lexico.v#L150
Maxime Dénès (Aug 28 2020 at 08:38):looks a bit strange at first glance
Ralf Jung (Aug 28 2020 at 08:40):it uses a local lambda in refine... but those names sure should still be usable?
Ralf Jung (Aug 28 2020 at 08:51):@Maxime Dénès looks like the problem is abstract
Ralf Jung (Aug 28 2020 at 08:51):apply (sig_eq_pi P). works but abstract (apply (sig_eq_pi P). fails.
Ralf Jung (Aug 28 2020 at 08:51):maybe P somehow gets mangles as part of being abstracted or so?
Ralf Jung (Aug 28 2020 at 08:52):minimal reproducer:
Lemma test: forall x: nat, nat.
Proof. intros x. abstract (exact x). Qed.
works without name mangling but breaks with it.
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.
Ralf Jung (Aug 28 2020 at 08:54):https://github.com/coq/coq/issues/12928
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.
Ralf Jung (Aug 28 2020 at 09:35):Cc @robbert
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.
Ralf Jung (Aug 28 2020 at 14:01):okay :) so when I see more of these I'll just intros or use numbers
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.
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.
Ralf Jung (Aug 28 2020 at 14:54):@Jasper Hugunin we already reduced that to an abstract problem
Ralf Jung (Aug 28 2020 at 14:54):reported at https://github.com/coq/coq/issues/12928
Jasper Hugunin (Aug 28 2020 at 14:55):Ah! I was overlooking the P inside abstract. Alright then.
Last updated: Oct 13 2024 at 01:02 UTC