Stream: Coq devs & plugin devs

Topic: Rewrite *


view this post on Zulip Pierre-Marie Pédrot (Sep 07 2020 at 12:23):

Is that me or the rewrite * and autorewrite * variants are not documented?

view this post on Zulip Pierre-Marie Pédrot (Sep 07 2020 at 12:24):

I'm not even sure what these variants do actually.

view this post on Zulip Pierre-Marie Pédrot (Sep 07 2020 at 12:25):

The commit that introduces them is not that helpful either: https://github.com/coq/coq/commit/fa7e44d

view this post on Zulip Jason Gross (Sep 08 2020 at 01:24):

Oh, neat! I didn't realize this existed. I think this solves a problem that I've worked around in the past (in fact, I think the * behavior should be the default (perhaps guarded by a compatibility flag)). Here's an example where it matters:

Axiom foo : forall x, x = 1 -> 2 * x = 2.

Goal forall x y, x = 1 -> 2 * y = 2 * x.
  intros.
  Fail rewrite foo by assumption. (* The command has indeed failed with message: No such assumption. *)
  Fail rewrite !foo by assumption. (* The command has indeed failed with message: No such assumption. *)
  Fail progress rewrite ?foo by assumption. (* The command has indeed failed with message: Failed to progress. *)
  rewrite *foo by assumption. (* success *)

view this post on Zulip Jason Gross (Sep 08 2020 at 01:25):

In fact, I reported this as https://github.com/coq/coq/issues/4976, Sam reported a related issue at https://github.com/coq/coq/issues/7672 explicitly mentioning rewrite *, and perhaps the commit was originally a fix for https://github.com/coq/coq/issues/1933 ?


Last updated: Oct 16 2021 at 09:07 UTC