Stream: Coq users

Topic: Apply vs rewrite


view this post on Zulip Patrick Nicodemus (Sep 04 2023 at 04:03):

I am trying to prove a goal of the form a=ba = 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.

view this post on Zulip Patrick Nicodemus (Sep 04 2023 at 04:04):

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

view this post on Zulip Patrick Nicodemus (Sep 04 2023 at 04:06):

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?

view this post on Zulip Paolo Giarrusso (Sep 04 2023 at 10:49):

Does rewrite work after unfold x?

view this post on Zulip Paolo Giarrusso (Sep 04 2023 at 10:53):

Re Lemma fin_to_nat_to_fin n m (H : n < m) : fin_to_nat (nat_to_fin H) = n., I think I agree

view this post on Zulip Gaëtan Gilbert (Sep 04 2023 at 14:40):

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)

view this post on Zulip Patrick Nicodemus (Sep 04 2023 at 22:29):

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.

view this post on Zulip Patrick Nicodemus (Sep 04 2023 at 22:30):

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

view this post on Zulip Patrick Nicodemus (Sep 04 2023 at 22:49):

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

view this post on Zulip Patrick Nicodemus (Sep 04 2023 at 22:50):

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

view this post on Zulip Paolo Giarrusso (Sep 05 2023 at 04:45):

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

view this post on Zulip Cyril Cohen (Sep 05 2023 at 07:14):

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 ifrewrite fails.


Last updated: Jun 13 2024 at 19:02 UTC