Stream: Coq users

Topic: Rewrite confusion

view this post on Zulip Andrej Dudenhefner (Jul 30 2021 at 11:09):

I ran into trouble with rewrite (ssreflect's rewrite works though). Here are minimal examples (Coq 8.13.2 as well as master):

Definition f (n : nat) : nat := S n.

Lemma f_spec (n : nat) : f n = S n.
Proof. reflexivity. Qed.

Lemma test_f (n : nat) : S n = f n.
Proof.
  Fail rewrite f_spec. (* Tactic generated a subgoal identical to the original goal. *)
Abort.

view this post on Zulip Andrej Dudenhefner (Jul 30 2021 at 11:11):

Ah, possibly this is exactly #14132. Currently, @Ali Caglayan possibly the issue is mislabeled as kind: performance. This looks like a critical rewriting issue.

view this post on Zulip Ali Caglayan (Jul 30 2021 at 15:33):

Sorry for mislabelling, I've marked it as a bug now.

Last updated: Oct 01 2023 at 18:01 UTC