Karl Palmskog (Jan 12 2022 at 23:59): 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).
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
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
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))).
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.
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?
Paolo Giarrusso (Jan 13 2022 at 01:14):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
Paolo Giarrusso (Jan 13 2022 at 01:15):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? *)
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.
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 :=
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.
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: Jun 09 2023 at 08:01 UTC