## 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: Dec 07 2023 at 06:38 UTC