Evert Geerling (Jul 21 2022 at 18:31): 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 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).
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.
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' * 0to becomen' * 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. rewrite mulSn add0n IHn'. reflexivity. Qed.
Ah, now I understand. I need to keep this in mind. Thanks!
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