Cannot rewrite subterm in Coq

Question

I have a proof in Coq where one of the hypothesis is:

H : m = pred q * n + (r + n)

And I have a proven lemma which states:

Lemma suma_conmutativa: forall m, forall n, m + n = n + m.

Where + is Notation for a function called suma that I defined:

Fixpoint suma (m:nat) (n:nat) : nat :=
match m with 
  | 0 => n
  | S k => S (suma k n)
end.
Notation "m + n" := (suma m n).

For some reason when I try to rewrite suma_conmutativa with r n in H I get the following error:

Error: Found no subterm matching "r + n" in H.

However, there clearly is a subterm matching r + n in H. Why can't Coq find it?

Thank you.

It seems to be a porblem with Notation because if H was m = pred q * n + (suma r n) then apparently it would be able to rewrite it. — Martin Copes
Yes, are you sure the + in your expression is your suma ? Trying Unset Printing Notations (or equivalent in your IDE) to be sure. — Vinz

eponier eponier · Accepted Answer · 2015-11-25T13:07:34

I am not an expert of notations in Coq, but here is how I understand your problem.

Coq replaces the first occurrence of + with suma. suma binds its arguments to scope nat_scope. Classic notation + is bound to nat_scope and is prefered for the second occurrence of +.

The solution I propose is to bound your notation to nat_scope to completely hide the original notation. This gives: Notation "m + n" := (suma m n) : nat_scope.

Cannot rewrite subterm in Coq

1 Answers