Stream: math-comp users

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


view this post on Zulip 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.

view this post on Zulip Pierre Castéran (Jul 21 2022 at 19:23):

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

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 ;-)

view this post on Zulip Paolo Giarrusso (Jul 21 2022 at 23:37):

@Enrico Tassi the error is with Coq's rewrite

view this post on Zulip 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.
  rewrite mulSn add0n IHn'.
  reflexivity.
Qed.

view this post on Zulip 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'].
  by rewrite mulSn add0n IHn'.
Qed.

view this post on Zulip 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?

view this post on Zulip 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.
  rewrite mulSn add0n IHn'.
  reflexivity.
Qed.

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

view this post on Zulip 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.


Last updated: Feb 08 2023 at 04:04 UTC