Stream: Coq users

Topic: Rewrite with a condition

view this post on Zulip Nicolas Rinaudo (Sep 18 2023 at 12:24):

I've been using rewrite with equalities so far: foo = bar allows me to replace foo with bar, or bar with foo.

Recently however, I've seen a proof that rewrote something of the shape foo = bar -> baz = bad and while I can sort of understand what the result is, I'm not at all convinced I fully understand the semantics. Is there a (beginner-readable) description of what it does?

view this post on Zulip Pierre Rousselin (Sep 18 2023 at 12:33):

Well, the refman says:

Replaces subterms with other subterms that have been proven to be equal. The type of one_term must have the form:
forall open_binders ,? EQ term1 term2
where EQ is the Leibniz equality eq or a registered setoid equality. Note that eq term1 term2 is typically written with the infix notation term1 = > term2. You must Require Setoid to use the tactic with a setoid equality or with setoid rewriting.

rewrite one_term finds subterms matching term1 in the goal, and replaces them with term2 (or the reverse if <- is given). Some of the variables xi are solved by unification, and some of the types A1, …, An may become new subgoals.

Which could be clearer (in particular it does not state what the Ai's are).

view this post on Zulip Pierre Rousselin (Sep 18 2023 at 12:36):

More simply, if you have something like
H: A -> baz = bad and some occurrence of baz in the goal then rewrite H will replace baz with bad but then ask that you prove that A holds (that is, it will add a new subgoal).

Last updated: Jun 22 2024 at 16:02 UTC