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...
I think I know: Check is lying, About Even_induction won't.
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?
it's 8.15+rc1, v8.15
, master
Oh, right, can you paste the full output?
When I ran into this, the problem was that all arguments are actually named P.
and induction (and elim apparently) stopped renaming them for you.
As a workaround, I ended up applying the induction principle explicitly to its argument.
The Arguments line is correct, while the type is also correct but unhelpful, since it must rename some P's to print the type.
"thanks for all the Ps"
(possible names are: P, P and n).
issue: https://github.com/coq/coq/issues/15420. @Gaëtan Gilbert already saw this and removed it from the 8.15.0 milestone.
how annoying do you think is the workaround?
thanks. I think this is a pretty serious breakage... workaround means one has to completely rewrite the above proof
(not that the UX is very good, of course)
hm, how bad would induction H using (Even_induction _ (fun n => odd (4 + n)))
or apply (Even_induction _ (fun n => odd (4 + n)))
be?
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?
yeah, I see that induction
is broken here.
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
…
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
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?
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...
well, this also breaks my trust in Check
quite a bit, but About
is so incredibly verbose
just to be sure, Check
isn’t at fault, Scheme
is IMHO
if Check
’s output started with forall P P : nat -> Prop
, how would the rest look like?
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)
it could annotate the names with numbers in a syntactically disallowed way or whatever, instead of just inventing stuff out of thin air
e.g., forall P\0 P\1 : nat -> Prop
yes, but instead of inventing a notation, it’d be simpler if top-level terms were guaranteed to avoid shadowing
sure, that's also a solution, but are we going to get that invariant anytime soon?
ah, you mean that’s not just a bug in Scheme… I was assuming this shadowing at least cannot be produced in normal Gallina?
I mean, ideally you won't even allow plugins to generate terms which have shadowing?
agreed
but I will probably not be able to sell that to type theorists
I _thought_ it was just a matter of fixing Scheme
hmm
I think this only matters for the names of arguments of top-level symbols, does apply …. with
support anything else?
yeah, I guess it's a top-level thing. Not sure about the support.
BTW there’s also Set Apply With Renaming
as a compat option to get the old behavior, if it helps.
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)
Patch welcome. And https://github.com/coq/coq/pull/12756 seems more gung-ho about repeated argument, so your proposed output sounds more compelling
well, I respectfully disagree strongly with Maxime's claim:
I think it's ok to tolerate duplicated names, like OCaml does for labels.
not least because it makes Check
unreliable...
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?
My intuition is that terms are deBruijn and top-level terms add a (mutable) list of unique names, usable in apply....with.
But, then we are back to Coq having to invent names on the fly, which has been a source of pain for users.
As for the actual representation, bound variables are de Bruijn, while binders (whether toplevel or not) are potentially named.
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...
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.
simplest fix is probably to use Arguments : rename
on your scheme
thanks, that seems to work reasonably well
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
I tried that one (elim t using (fun ...)
), didn't seem to give the same goals as before, but maybe it actually does.
FTR, on gitlab Matthieu agreed Scheme should be fixed...
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
AFAICT, @Gaëtan Gilbert 's objection would suggest shadowing the P from the section. I don't get why, but that seems acceptable...
Nobody should be writing that code anyway (EDIT: at least arguably)
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
we can do a 8.15.1
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).
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?
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.
OK, so one would declare this as bug introduced in 8.15.0 and fixed in 8.15.1?
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)
That's also my understanding and is in line with the fact that 8.15 was only in a platform preview pick so far.
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.
if the fix was backward compatible isn't it forward compatible too?
it's not obvious to me there would need to be new package releases because of the fix.
for example, all workarounds discussed in this topic work fine even after Hugo's fix
But there were overlays in the PR, why were they needed then?
because something else broke x_x
dunno what to do about it
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
I'm not sure about the relevant etiquette, but I noticed you didn't mention https://github.com/coq/coq/issues/15567
that's an issue not a fix
@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.
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
Sorry, I'm missing context. I don't get the relation between #15653 and the P
names in schemes.
there is no relation except that they are both being considered for 8.15.1
Ah, ok I see, you'd like a variant of #15420 which does not fix the eq
bug name.
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?
I'll try
Last updated: Jun 09 2023 at 08:01 UTC