I am trying to prove a goal of the form $a = b$. I can do "apply my_thm" which works but not "rewrite my_thm." I vaguely recall that there are different unification algorithms at play here but I can't remember the details and I found this very frustrating.

Can somebody remind me why this doesn't work?

Here I am using the `stdpp`

library.

```
n : nat
i : Fin.t (S n)
j : Fin.t (S (S n))
ineq : lt (@fin_to_nat (S n) i) (@fin_to_nat (S (S n)) j)
p : Fin.t n
z : lt (S (@fin_to_nat n p)) (S n)
x := @fin_to_nat (S n) (@Fin.of_nat_lt (S (@fin_to_nat n p)) (S n) z)
: nat
============================
@eq nat x (S (@fin_to_nat n p))
```

And the theorem I want to use is `fin_to_nat_to_fin`

. I can `apply`

it but not `rewrite`

with it.

(This is Ltac2 rewrite, which I assume is the same as Ltac1. I commonly use the SSReflect rewrite tactic but i'm trying to use Ltac2 in this project and I don't think those are super easy to make compatible.)

Tangential but I think the function `fin_to_nat_to_fin`

is misnamed? Seems like it should be called `nat_to_fin_to_nat`

. are there any stdpp maintainers who could comment on that?

Does `rewrite`

work after `unfold x`

?

Re `Lemma fin_to_nat_to_fin n m (H : n < m) : fin_to_nat (nat_to_fin H) = n.`

, I think I agree

I think `rewrite`

isn't expected to unfold `x`

when looking for the term to rewrite

although rewrite's unification may unfold stuff when matching terms without unification variables (in this case the term from the lemma is `fin_to_nat (nat_to_fin ?X)`

so this doesn't happen)

Ok. I am a little rusty, does rewrite work inside definitions, like `x := t a b c`

, can I `rewrite H in x`

using some `H : a = a'`

? It looks like the answer is no, which I can understand.

It would be rebinding the local definition, so maybe you can only get away with `change _ with _ in x`

Like if you do

```
Goal forall (i j :nat) (H : i=j), i+1=j+1)
intros i j H
set x := i+1
rewrite H in x
```

it'll throw `Error: found no subterm matching i in x`

.

Is this the intended behavior? is there a way I can get around this

I haven't used the rewrite tactic in a long time sorry.

Here you could revert x, rewrite, then introduce it again

In principle I thought one could do `rewrite H in (value x)`

cf https://coq.inria.fr/refman/proof-engine/tactics.html#grammar-token-hypident but I never used it, and it does not seem to work. Indeed

```
Goal forall (i j : nat) (H : i = j), i + 1 = j + 1.
intros i j H.
set (x := i + 1).
rewrite H in (value of x).
```

fails with error message: `Error: Found no subterm matching "i" in x.`

@Paolo Giarrusso's answer would work but might also rewrite occurences of `i`

in the goal, which might be undesirable (otherwise, why would you abstract `x`

in the first place), but if not, that's the way to go!

The SSReflect solution to this problem is usually to protect the goal before discharging, but in this case it will not work because the goal depends on `x`

. If necessary, I can expand on that.

Back to the orginal question, the reason why `apply`

works and `rewrite`

does not is that `apply`

knows what unification to try (unify the conclusion of the lemma to apply with the goal), while `rewrite`

needs first to select a subterm of the goal to rewrite, if not even the head symbol of the right hand side of the equation you want to rewrite with appears in the goal, it's very risky and potentially very costly to try and expand everything with the hope to find it, so it's better if`rewrite`

fails.

Last updated: Jun 13 2024 at 19:02 UTC