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.

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

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.

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`

.

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 ;-)

@Enrico Tassi the error is with Coq's rewrite

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.
rewrite mulSn add0n IHn'.
reflexivity.
Qed.
```

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

```
Proof.
elim => [//|n' IHn'].
by rewrite mulSn add0n IHn'.
Qed.
```

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?

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. rewrite mulSn add0n IHn'. reflexivity. Qed.`

Ah, now I understand. I need to keep this in mind. Thanks!

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.

Last updated: Jul 25 2024 at 16:02 UTC