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?

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).

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