## Stream: math-comp users

### Topic: S n' not the same as n' .+1?

#### Evert Geerling (Jul 21 2022 at 18:31):

The following code works in the Logical Foundations context, but fails in mat-comp.
Message: "Found no subterm matching "n' * 0" in the current goal." at rewrite -> IHn'.
Goals are S n' * 0 = 0 versus n'.+1 * 0 = 0 .
How should I treat the differences in these contexts?
Theorem mult_0_r : forall n:nat,
n * 0 = 0.
Proof.
intros n. induction n as [|n' IHn'].
simpl. reflexivity.
simpl. rewrite -> IHn'.
reflexivity.
Qed.

#### Pierre Castéran (Jul 21 2022 at 19:23):

Looks like the issue comes from the definition of `muln` in ssreflect/mathcomp (with a `nosimpl`flag).

``````Print muln.

muln = nosimpl muln_rec
: nat -> nat -> nat
``````

Your proof works if you start it by unfolding `muln` (by `unfold muln`, or, better `rewrite /muln` if you use the SSreflect style).

#### Evert Geerling (Jul 21 2022 at 20:16):

Thank you.
I do see that unfolding works, but I can't imagine that math-comp definitions should often be unfolded for standard code to keep working.
This example could hardly be simpler.
Seems like I am missing something else.

#### Enrico Tassi (Jul 21 2022 at 20:34):

in SSR rewrite looks for a head symbol `*` and then compare arguments `(S n')` and `n'` are not the same.
At the same time, if you apply the induction hypothesis things are fine, since `S n' * 0` is convertible to `0 + n' * 0` which is convertible to `n' * 0`. This is how it is proved in ssrnat, see https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/ssrnat.v for `muln0`.

#### Enrico Tassi (Jul 21 2022 at 20:37):

Coq's rewrite looks more blindly for any term which unifies. In this case it looks smart, but it may also be surprising. I mean, if you rewrite wth the commutativity of addition, do you expect `S n' * 0` to become `n' * 0 + 0`? I don't ;-)

#### Paolo Giarrusso (Jul 21 2022 at 23:37):

@Enrico Tassi the error is with Coq's rewrite

#### Paolo Giarrusso (Jul 21 2022 at 23:42):

but I can't imagine that math-comp definitions should often be unfolded for standard code to keep working.

Loading `From mathcomp Require Import ssrnat.` changes what `*` and `+` mean, and I don't think there's any compatibility guarantee, and neither simplifies. I'm not sure the right fix is unfolding, but appropriate lemmas are available:

``````Theorem mult_0_r' : forall n:nat,
n * 0 = 0.
Proof.
intros n. induction n as [|n' IHn'].
reflexivity.
reflexivity.
Qed.
``````

#### Paolo Giarrusso (Jul 21 2022 at 23:44):

FWIW, an idiomatic proof is shorter nonetheless, even if this isn't a very meaningful benchmark:

``````Proof.
elim => [//|n' IHn'].
Qed.
``````

#### Evert Geerling (Jul 22 2022 at 07:59):

Enrico Tassi said:

Coq's rewrite looks more blindly for any term which unifies. In this case it looks smart, but it may also be surprising. I mean, if you rewrite wth the commutativity of addition, do you expect `S n' * 0` to become `n' * 0 + 0`? I don't ;-)

Clearly no. But when I read in your document (which by the way is great, thank you for the diligent work),
that "if x is a value of type nat, x.+1 is another way to write (S x).", I do expect n'.+1 * 0 = 0 and S n' * 0 = 0 to have the same result at simpl, whereas now the results are n'.+1 * 0 = 0 and n' * 0 = 0. It seems they are not equal.
Is this the result of nosimpl?

#### Evert Geerling (Jul 22 2022 at 08:04):

Paolo Giarrusso said:

but I can't imagine that math-comp definitions should often be unfolded for standard code to keep working.

Loading `From mathcomp Require Import ssrnat.` changes what `*` and `+` mean, and I don't think there's any compatibility guarantee, and neither simplifies. I'm not sure the right fix is unfolding, but appropriate lemmas are available:

``````Theorem mult_0_r' : forall n:nat,
n * 0 = 0.
Proof.
intros n. induction n as [|n' IHn'].
reflexivity.
#### Pierre Roux (Jul 22 2022 at 08:21):
Yes, the difference is not in `n.+1` versus `S n` (since `.+1` is just a notation for `S`, those are exactly the same thing) but in the definition of `+` and `*`. You can use `Locate "_ + _". ` and `Print` the result in each case to see that.