Stream: Coq users

Topic: Behavior change of 'specialize' tactic in Coq 8.14


view this post on Zulip Ralf Jung (Nov 24 2021 at 01:35):

I noticed (by accident) that the behavior of the specialize tactic changed in Coq 8.14:

Lemma test (X : nat -> Prop) (H : forall n, X n) (H' : forall n, X n -> X (S n)) : True.
Proof.
  specialize (H 5) as J%H'.

In 8.13, this produces the following goal:

  X : nat -> Prop
  H' : forall n : nat, X n -> X (S n)
  J : X 6
  ============================
  True

In 8.14, it instead produces:

  X : nat -> Prop
  H : X 6
  H' : forall n : nat, X n -> X (S n)
  ============================
  True

Notice there is no J even though the as pattern says to call the result J.
Is this deliberate? the changelog does not seem to mention it (I did Ctrl-F 'specialize').

view this post on Zulip Ralf Jung (Nov 24 2021 at 01:36):

Arguably specialize ... as is weird, but just ignoring the name in the pattern seems like a bug to me -- in particular since without the %H', the name is still honored. (Cc @Hugo Herbelin because % patterns seem relevant.)

view this post on Zulip Ralf Jung (Nov 24 2021 at 17:18):

looks like it was not deliberate: https://github.com/coq/coq/issues/15244

view this post on Zulip Hugo Herbelin (Nov 24 2021 at 17:23):

It is a bug. Thanks for reporting. This is issue #15244, fixed by #15245.


Last updated: Feb 08 2023 at 23:03 UTC