Stream: Coq devs & plugin devs

Topic: Scheme duplicate variable names in 8.15


view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip Paolo Giarrusso (Jan 13 2022 at 00:43):

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

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Jan 13 2022 at 00:44):

Is this also with 8.15?

view this post on Zulip Karl Palmskog (Jan 13 2022 at 00:45):

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

view this post on Zulip Paolo Giarrusso (Jan 13 2022 at 00:45):

Oh, right, can you paste the full output?

view this post on Zulip Paolo Giarrusso (Jan 13 2022 at 00:45):

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

view this post on Zulip Paolo Giarrusso (Jan 13 2022 at 00:46):

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

view this post on Zulip Paolo Giarrusso (Jan 13 2022 at 00:46):

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

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Jan 13 2022 at 00:48):

"thanks for all the Ps"

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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Jan 13 2022 at 00:50):

how annoying do you think is the workaround?

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Jan 13 2022 at 00:51):

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

view this post on Zulip 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?

view this post on Zulip 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))).

view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Jan 13 2022 at 00:56):

yeah, I see that induction is broken here.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Jan 13 2022 at 01:01):

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

view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Jan 13 2022 at 01:09):

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

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Jan 13 2022 at 01:12):

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

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Jan 13 2022 at 01:13):

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

view this post on Zulip 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?

view this post on Zulip Karl Palmskog (Jan 13 2022 at 01:14):

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

view this post on Zulip Paolo Giarrusso (Jan 13 2022 at 01:14):

agreed

view this post on Zulip Karl Palmskog (Jan 13 2022 at 01:15):

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

view this post on Zulip Paolo Giarrusso (Jan 13 2022 at 01:15):

I _thought_ it was just a matter of fixing Scheme

view this post on Zulip Paolo Giarrusso (Jan 13 2022 at 01:15):

hmm

view this post on Zulip 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?

view this post on Zulip Karl Palmskog (Jan 13 2022 at 01:17):

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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Jan 13 2022 at 01:29):

not least because it makes Check unreliable...

view this post on Zulip 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? *)

view this post on Zulip Paolo Giarrusso (Jan 13 2022 at 08:45):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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 :=
  occurs_head :
   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.

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Jan 23 2022 at 20:11):

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

view this post on Zulip Karl Palmskog (Jan 23 2022 at 20:22):

thanks, that seems to work reasonably well

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Jan 24 2022 at 14:55):

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

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip Paolo Giarrusso (Jan 24 2022 at 14:57):

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

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Feb 02 2022 at 12:39):

we can do a 8.15.1

view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Feb 02 2022 at 16:30):

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

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Feb 02 2022 at 16:33):

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

view this post on Zulip Théo Zimmermann (Feb 02 2022 at 21:34):

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

view this post on Zulip Gaëtan Gilbert (Feb 02 2022 at 21:53):

because something else broke x_x

view this post on Zulip Gaëtan Gilbert (Feb 02 2022 at 21:54):

dunno what to do about it

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Feb 03 2022 at 11:26):

that's an issue not a fix

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Feb 10 2022 at 10:45):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Feb 10 2022 at 10:55):

I'll try


Last updated: Feb 05 2023 at 23:30 UTC