How to use rewrite on a subexpression of the current goal

Question

In coq, is it somehow possible to apply a lemma or hypothesis to a subexpression of the current goal? For example I would like to apply the fact that plus is commutative in order to swap 3 and 4 in this example.

Require Import Coq.Arith.Plus.

Inductive foobar : nat -> Prop :=
 | foob : forall n:nat, foobar n.

Goal foob (3 + 4) = foob (4 + 3).
Proof.
apply plus_comm. (* or maybe rewrite plus_comm *)

gives:

Error: Impossible to unify "?199 + ?200 = ?200 + ?199" with
"foob (3 + 4) = foob (4 + 3)".

How can I tell coq where exactly in this goal to apply plus_comm?

score 5 · Accepted Answer · 2012-11-30T14:05:58.467

5

Using the tactic simpl works, but don't ask me why rewrite plus_comm or rewrite (plus_comm 3 4) doesn't work. apply is for implications, not equations.

edited Nov 30 '12 at 14:05

answered Nov 30 '12 at 13:57

It works when I do the following, which is what I actually wanted to prove in the first place. Goal foobar (3 + 4) = foobar (4 + 3). Proof. rewrite plus_comm. reflexivity. Qed. I guess rewrite doesn't work on values, only on types. – Markus Klinik Nov 30 '12 at 13:59
1

`rewrite` works on both (actually types are terms in Coq ;-). The main issue here is that `foob (3+4)` has type `foobar (3+4)` and `foob(4+3)` has type `foobar (4+3)`. Coq can check that both are equal (hence the equality is well-typed), but `rewrite` uses an intermediate form where it is not the case, hence the cryptic error message you get with `rewrite (plus_comm 3 4)`. – Virgile Nov 30 '12 at 15:29
1

Normally, you should be able to use `pattern` (http://coq.inria.fr/refman/Reference-Manual011.html#pattern) for local actions somewhere inside the term. However, this fails for the same reason @Virgile mentioned. If that's possible, you can also move to a 'more complete' equality type temporarily (e.g. `JMeq`), do stuff there and then move back. (I like to think of it as the 'complex number'-analogue of equality.) – nobody Dec 03 '12 at 03:07

Max Heiber · Answer 2 · 2020-01-14T20:56:58.507

In this particular case, rewrite will work if you define the inductive type using a constructor parameter instead of an index:

Inductive foobar : Type :=
    | foob (n : nat).

Since there is only one constructor for this type, my understanding (from this answer) is that using an index does not provide any benefit but makes it harder for Coq to pattern-match.

In general, either of the following techniques can achieve the effect of a targeted rewrite:

assert

assert (H: 3 + 4 = 4 + 3). { rewrite <- plus_comm. reflexivity. }

rewrite

(* introduce a new sub-goal where you can prove that the replacement is OK *)
replace (3 + 4) with (4 + 3).
(* Coq orders the new goal last. I think it's clearer to tackle it first *)
Focus 2.
(* do the rewrite *)
rewrite <- plus_comm. reflexivity.

How to use rewrite on a subexpression of the current goal

2 Answers2