Stream: Coq devs & plugin devs

Topic: Scheme duplicate variable names in 8.15

Karl Palmskog (Jan 12 2022 at 23:59):

I have the following example which works fine in 8.14 and below:

``````Inductive
even    : nat->Prop :=
evenO : even  O |
evenS : forall n, odd n -> even (S n)
with
odd    : nat->Prop :=
oddS : forall n, even n -> odd (S n).

Scheme Even_induction := Minimality for even Sort Prop
with   Odd_induction  := Minimality for odd  Sort Prop.

Theorem even_plus_four : forall n:nat, even n -> even (4+n).
Proof.
intros n H.
elim H using Even_induction with (P0 := fun n => odd (4+n));
simpl;repeat constructor;assumption.
Qed.
``````

However, in 8.15+rc1, the `elim H using ...` fails with the following strange message:

``````Error: No such bound variable P0 (possible names are: P, P and n).
``````

Karl Palmskog (Jan 13 2022 at 00:00):

If I do `Check Even_induction`, the `P0` variable is shown just fine:

``````Even_induction
: forall P P0 : nat -> Prop,
P 0 ->
(forall n : nat, odd n -> P0 n -> P (S n)) ->
(forall n : nat, even n -> P n -> P0 (S n)) ->
forall n : nat, even n -> P n
``````

Karl Palmskog (Jan 13 2022 at 00:00):

can report this as issue if you want, but would like to confirm it's worth doing...

Paolo Giarrusso (Jan 13 2022 at 00:43):

I think I know: Check is lying, About Even_induction won't.

Karl Palmskog (Jan 13 2022 at 00:44):

``````About Even_induction.

Even_induction :
forall P P0 : nat -> Prop,
P 0 ->
(forall n : nat, odd n -> P0 n -> P (S n)) ->
(forall n : nat, even n -> P n -> P0 (S n)) -> forall n : nat, even n -> P n

Even_induction is not universe polymorphic
Arguments Even_induction (P P)%function_scope f (f f)%function_scope
n%nat_scope e
Even_induction is transparent
Expands to: Constant min.Even_induction
``````

Paolo Giarrusso (Jan 13 2022 at 00:44):

Is this also with 8.15?

Karl Palmskog (Jan 13 2022 at 00:45):

it's 8.15+rc1, `v8.15`, `master`

Paolo Giarrusso (Jan 13 2022 at 00:45):

Oh, right, can you paste the full output?

Paolo Giarrusso (Jan 13 2022 at 00:45):

When I ran into this, the problem was that all arguments are actually named P.

Paolo Giarrusso (Jan 13 2022 at 00:46):

and induction (and elim apparently) stopped renaming them for you.

Paolo Giarrusso (Jan 13 2022 at 00:46):

As a workaround, I ended up applying the induction principle explicitly to its argument.

Paolo Giarrusso (Jan 13 2022 at 00:47):

The Arguments line is correct, while the type is also correct but unhelpful, since it must rename some P's to print the type.

Karl Palmskog (Jan 13 2022 at 00:48):

"thanks for all the Ps"

(possible names are: P, P and n).

Paolo Giarrusso (Jan 13 2022 at 00:49):

issue: https://github.com/coq/coq/issues/15420. @Gaëtan Gilbert already saw this and removed it from the 8.15.0 milestone.

Paolo Giarrusso (Jan 13 2022 at 00:50):

how annoying do you think is the workaround?

Karl Palmskog (Jan 13 2022 at 00:51):

thanks. I think this is a pretty serious breakage... workaround means one has to completely rewrite the above proof

Paolo Giarrusso (Jan 13 2022 at 00:51):

(not that the UX is very good, of course)

Paolo Giarrusso (Jan 13 2022 at 00:52):

hm, how bad would `induction H using (Even_induction _ (fun n => odd (4 + n)))` or `apply (Even_induction _ (fun n => odd (4 + n)))` be?

Karl Palmskog (Jan 13 2022 at 00:53):

the first one doesn't work at all, neither does:

``````elim H using (@Even_induction _ (fun n => odd (4+n))).
``````

Karl Palmskog (Jan 13 2022 at 00:53):

if we have to rewrite all this stuff using `apply`, why do we even have induction tactics?

Paolo Giarrusso (Jan 13 2022 at 00:56):

yeah, I see that `induction` is broken here.

Paolo Giarrusso (Jan 13 2022 at 00:58):

I just never found this pattern useful, because the `Combined Scheme` is the more useful one for me, and those aren’t supported by `induction`

Karl Palmskog (Jan 13 2022 at 01:01):

the following seems to be the only thing that works, and means we have to completely drop `induction`:

``````Theorem even_plus_four : forall n:nat, even n -> even (4+n).
Proof.
apply (Even_induction _ (fun n => odd (4 + n)));
simpl;repeat constructor;assumption.
Qed.
``````

Paolo Giarrusso (Jan 13 2022 at 01:01):

yep, and you’re even lucky — I expected you’d need an explicit `pattern`

Paolo Giarrusso (Jan 13 2022 at 01:04):

FWIW you might want to add some code like this in CI since mutual inductives get very little testing, this isn’t the first mutual-only regression that I’m the first to notice. Not sure why CompCert doesn’t catch them, probably it’s too heavy for CI?

Karl Palmskog (Jan 13 2022 at 01:05):

this code is from https://github.com/coq-community/coq-art - I guess we could add that project into Coq's CI if devs are OK with this...

Karl Palmskog (Jan 13 2022 at 01:08):

well, this also breaks my trust in `Check` quite a bit, but `About` is so incredibly verbose

Paolo Giarrusso (Jan 13 2022 at 01:09):

just to be sure, `Check` isn’t at fault, `Scheme` is IMHO

Paolo Giarrusso (Jan 13 2022 at 01:10):

if `Check`’s output started with `forall P P : nat -> Prop`, how would the rest look like?

Karl Palmskog (Jan 13 2022 at 01:10):

but as you said, `Check` does surface-level conversion of names, so from now on I won't trust it to give me actual names (I guess I have to use SerAPI or something to get those)

Karl Palmskog (Jan 13 2022 at 01:11):

it could annotate the names with numbers in a syntactically disallowed way or whatever, instead of just inventing stuff out of thin air

Karl Palmskog (Jan 13 2022 at 01:12):

e.g., `forall P\0 P\1 : nat -> Prop`

Paolo Giarrusso (Jan 13 2022 at 01:12):

yes, but instead of inventing a notation, it’d be simpler if top-level terms were guaranteed to avoid shadowing

Karl Palmskog (Jan 13 2022 at 01:13):

sure, that's also a solution, but are we going to get that invariant anytime soon?

Paolo Giarrusso (Jan 13 2022 at 01:14):

ah, you mean that’s not just a bug in Scheme… I was assuming this shadowing at least cannot be produced in normal Gallina?

Karl Palmskog (Jan 13 2022 at 01:14):

I mean, ideally you won't even allow plugins to generate terms which have shadowing?

agreed

Karl Palmskog (Jan 13 2022 at 01:15):

but I will probably not be able to sell that to type theorists

Paolo Giarrusso (Jan 13 2022 at 01:15):

I _thought_ it was just a matter of fixing `Scheme`

hmm

Paolo Giarrusso (Jan 13 2022 at 01:16):

I think this only matters for the names of arguments of top-level symbols, does `apply …. with` support anything else?

Karl Palmskog (Jan 13 2022 at 01:17):

yeah, I guess it's a top-level thing. Not sure about the support.

Paolo Giarrusso (Jan 13 2022 at 01:18):

BTW there’s also `Set Apply With Renaming` as a compat option to get the old behavior, if it helps.

Karl Palmskog (Jan 13 2022 at 01:20):

sigh, it seemingly isn't mentioned in the changelog for 8.15

OK, looks like it was mentioned in changelog after all. But the connection to `induction`/`elim`, etc., is far from obvious (I didn't know they were `apply` under the hood)

Paolo Giarrusso (Jan 13 2022 at 01:24):

Patch welcome. And https://github.com/coq/coq/pull/12756 seems more gung-ho about repeated argument, so your proposed output sounds more compelling

Karl Palmskog (Jan 13 2022 at 01:28):

well, I respectfully disagree strongly with Maxime's claim:

I think it's ok to tolerate duplicated names, like OCaml does for labels.

Karl Palmskog (Jan 13 2022 at 01:29):

not least because it makes `Check` unreliable...

Guillaume Melquiond (Jan 13 2022 at 06:23):

Paolo Giarrusso said:

yes, but instead of inventing a notation, it’d be simpler if top-level terms were guaranteed to avoid shadowing

That is impossible. It would mean forbidding any kind of reduction. For example, Coq would fail on the following script.

``````Definition f := (fun y (x : nat) => y) (fun x : nat => x).
Definition g := Eval compute in f. (* should this really fail? *)
``````

Paolo Giarrusso (Jan 13 2022 at 08:45):

Why would that have to fail, rather than freshen names when defining g?

Paolo Giarrusso (Jan 13 2022 at 08:49):

My intuition is that terms are deBruijn and top-level terms add a (mutable) list of unique names, usable in apply....with.

Guillaume Melquiond (Jan 13 2022 at 09:01):

But, then we are back to Coq having to invent names on the fly, which has been a source of pain for users.

Guillaume Melquiond (Jan 13 2022 at 09:02):

As for the actual representation, bound variables are de Bruijn, while binders (whether toplevel or not) are potentially named.

Gaëtan Gilbert (Jan 13 2022 at 10:41):

using generated names is not a good idea, even the first P is generated and can produce strange things
eg pre 8.15

``````Section S.
Variable P : nat.
Inductive foo : P = P -> Prop :=
with bar := X (_:foo eq_refl).

Scheme find := Minimality for foo Sort Prop
with bind := Minimality for bar Sort Prop.

Lemma bli : bar -> False.
Proof.
induction 1 using bind with (P0:=fun _ : P=P => False).
assumption.
Qed.
``````

Karl Palmskog (Jan 13 2022 at 11:22):

so is this a WONTFIX for the `Scheme` behavior? In this case, at least make sure `Check` doesn't rename duplicates...

Karl Palmskog (Jan 23 2022 at 20:05):

sigh, the following code is hitting the bug in https://github.com/coq/coq/issues/15420 hard, does anyone know an easy way to convert `elim t using ntree_ind2 ...` to plain `apply`?

``````Require Import ZArith.

Inductive ntree (A:Type) : Type :=
nnode : A -> nforest A -> ntree A
with nforest (A:Type) : Type :=
nnil : nforest A | ncons : ntree A -> nforest A -> nforest A.

Fixpoint count (A:Type)(t:ntree A){struct t} : Z :=
match t with
| nnode _ a l => 1 + count_list A l
end
with count_list (A:Type)(l:nforest A){struct l} : Z :=
match l with
| nnil _ => 0
| ncons _ t tl => count A t + count_list A tl
end.

Scheme ntree_ind2 :=
Induction for ntree Sort Prop
with nforest_ind2 :=
Induction for nforest Sort Prop.

Inductive occurs (A:Type)(a:A) : ntree A -> Prop :=
| occurs_root : forall l, occurs A a (nnode A a l)
| occurs_branches :
forall b l, occurs_forest A a l -> occurs A a (nnode A b l)
with occurs_forest (A:Type)(a:A) : nforest A -> Prop :=
forall t tl, occurs A a t -> occurs_forest A a (ncons A t tl)
| occurs_tail :
forall t tl,
occurs_forest A a tl -> occurs_forest A a (ncons A t tl).

Fixpoint n_sum_values (t:ntree Z) : Z :=
match t with
| nnode _ z l => z + n_sum_values_l l
end
with n_sum_values_l (l:nforest Z) : Z :=
match l with
| nnil _ => 0
| ncons _ t tl => n_sum_values t + n_sum_values_l tl
end.

#[local] Hint Resolve occurs_branches occurs_root Zplus_le_compat : core.

Open Scope Z_scope.

Theorem greater_values_sum :
forall t:ntree Z,
(forall x:Z, occurs Z x t -> 1 <= x)-> count Z t <= n_sum_values t.
Proof.
intros t; elim t using ntree_ind2 with
(P0 := fun l:nforest Z =>
(forall x:Z, occurs_forest Z x l -> 1 <= x)->
count_list Z l <= n_sum_values_l l).
-  intros z l Hl Hocc. lazy beta iota delta -[Zplus Z.le];
fold count_list n_sum_values_l;   auto with *.

-  auto with zarith.
-  intros t1 Hrec1 tl Hrec2 Hocc; lazy beta iota delta -[Zplus Z.le];
fold count count_list n_sum_values n_sum_values_l.
apply Zplus_le_compat.
apply Hrec1; intros; apply Hocc; apply occurs_head; auto.
apply Hrec2; intros; apply Hocc; apply occurs_tail; auto.
Qed.
``````

Karl Palmskog (Jan 23 2022 at 20:06):

it works fine in 8.14 and below... and to be clear, this is from a coq-community project, so not just a theoretical exercise.

Gaëtan Gilbert (Jan 23 2022 at 20:11):

simplest fix is probably to use `Arguments : rename` on your scheme

Karl Palmskog (Jan 23 2022 at 20:22):

thanks, that seems to work reasonably well

Gaëtan Gilbert (Jan 24 2022 at 14:50):

Karl Palmskog said:

the first one doesn't work at all, neither does:

``````elim H using (@Even_induction _ (fun n => odd (4+n))).
``````

`elim H using (fun P => Even_induction P (fun n => odd (4+n))).` should work if you don't want to use Arguments

``````elim t using (fun P => ntree_ind2 _ P
(fun l:nforest Z =>
(forall x:Z, occurs_forest Z x l -> 1 <= x)->
count_list Z l <= n_sum_values_l l)).
``````

for the latest code block

Karl Palmskog (Jan 24 2022 at 14:52):

I tried that one (`elim t using (fun ...)`), didn't seem to give the same goals as before, but maybe it actually does.

Paolo Giarrusso (Jan 24 2022 at 14:55):

FTR, on gitlab Matthieu agreed Scheme should be fixed...

Karl Palmskog (Jan 24 2022 at 14:55):

I still think the argument renaming approach is the way to go though, since it's both backward and forward compatible, and doesn't require changing anything else

Paolo Giarrusso (Jan 24 2022 at 14:57):

AFAICT, @Gaëtan Gilbert 's objection would suggest shadowing the P from the section. I don't get why, but that seems acceptable...

Paolo Giarrusso (Jan 24 2022 at 14:57):

Nobody should be writing that code anyway (EDIT: at least arguably)

Karl Palmskog (Feb 02 2022 at 12:36):

when is the nice fix by Hugo going to be rolled out to the masses? It won't be until 8.16.0, right? https://github.com/coq/coq/pull/15537

Gaëtan Gilbert (Feb 02 2022 at 12:39):

we can do a 8.15.1

Théo Zimmermann (Feb 02 2022 at 13:39):

Note that this means a few Coq Platform projects will need to be updated to be marked as compatible with < 8.15.1 and new package releases will be needed for the 2022.03.0 Platform (cc @Michael Soegtrop).

Michael Soegtrop (Feb 02 2022 at 15:55):

I must admit I don't fully understand the discussion here (hadn't time to dig into it) but from what @Théo Zimmermann said I guess that putting this into 8.15.1 would introduce a significant incompatibility between 8.15.0 and 8.15.1. I would try to avoid this, since in the end it would mean that it would be impossible to to a Coq Platform patch release for 8.15.1.

Did I interpret @Théo Zimmermann 's comment right?

Hugo Herbelin (Feb 02 2022 at 16:00):

Answering in passing: I would say that the significant incompatibilities are more about 8.15.0. That is, 8.15.1 will be more compatible with 8.14 than 8.15.0 is.

Michael Soegtrop (Feb 02 2022 at 16:04):

OK, so one would declare this as bug introduced in 8.15.0 and fixed in 8.15.1?

Karl Palmskog (Feb 02 2022 at 16:07):

Michael Soegtrop said:

OK, so one would declare this as bug introduced in 8.15.0 and fixed in 8.15.1?

this is my understanding, and what I have seen in the projects I help maintain (i.e., they broke on 8.15.0, but are fixed by Hugo's fix)

Théo Zimmermann (Feb 02 2022 at 16:25):

That's also my understanding and is in line with the fact that 8.15 was only in a platform preview pick so far.

Théo Zimmermann (Feb 02 2022 at 16:26):

The reason why I mentioned this is because there are three packages in the platform that had to get a (backward-compatible) fix and thus will need a new release to be compatible with 8.15.1.

Gaëtan Gilbert (Feb 02 2022 at 16:30):

if the fix was backward compatible isn't it forward compatible too?

Karl Palmskog (Feb 02 2022 at 16:32):

it's not obvious to me there would need to be new package releases because of the fix.

Karl Palmskog (Feb 02 2022 at 16:33):

for example, all workarounds discussed in this topic work fine even after Hugo's fix

Théo Zimmermann (Feb 02 2022 at 21:34):

But there were overlays in the PR, why were they needed then?

Gaëtan Gilbert (Feb 02 2022 at 21:53):

because something else broke x_x

Gaëtan Gilbert (Feb 02 2022 at 21:54):

dunno what to do about it

Gaëtan Gilbert (Feb 03 2022 at 10:26):

I guess we should wait for the other regression fixes https://github.com/coq/coq/pull/15594 and https://github.com/coq/coq/pull/15577 before doing 8.15.1

Paolo Giarrusso (Feb 03 2022 at 11:13):

I'm not sure about the relevant etiquette, but I noticed you didn't mention https://github.com/coq/coq/issues/15567

Gaëtan Gilbert (Feb 03 2022 at 11:26):

that's an issue not a fix

Janno (Feb 03 2022 at 12:20):

@Gaëtan Gilbert do you expect the fix for 15567 to be very complicated? It's a blocker for us upgrading to 8.15 so it would be good to know if this is going to take a long time. We are still hoping a fix could go into 8.15.1.

Gaëtan Gilbert (Feb 10 2022 at 10:33):

fix for 15567 is looking ok https://github.com/coq/coq/pull/15653
I don't want to backport the scheme name fix though due to the incompatibilities it has
maybe we can go for a stupider fix that only renames for `P` binders, that would avoid the incompatibility
cc @Hugo Herbelin

Hugo Herbelin (Feb 10 2022 at 10:44):

Sorry, I'm missing context. I don't get the relation between #15653 and the `P` names in schemes.

Gaëtan Gilbert (Feb 10 2022 at 10:45):

there is no relation except that they are both being considered for 8.15.1

Hugo Herbelin (Feb 10 2022 at 10:48):

Ah, ok I see, you'd like a variant of #15420 which does not fix the `eq` bug name.

Hugo Herbelin (Feb 10 2022 at 10:52):

Maybe removing 138bae9f in the backport would be enough? Can you try or do you want me to try to submit a specific 8.15 PR?

Gaëtan Gilbert (Feb 10 2022 at 10:55):

I'll try

Last updated: Feb 05 2023 at 23:30 UTC