Addition is only declared as `Commutative` in iris
Just learned that addition on naturals is not "commutative" for stdpp, but only in Iris. Take the following proof:
Require Import iris.algebra.base iris.algebra.cmra.
Lemma foo i j: i + j = j + i. Proof. rewrite {1}[_ + _]comm //. Qed.
That works, but the instance found for Commutative
is @cmra_comm natR
.
But if we load the whole stdpp (and algebra.base to get ssreflect), no instance is found. After:
Require Import iris.algebra.base stdpp.prelude.
Lemma foo i j: i + j = j + i. Proof. Fail rewrite {1}[_ + _]comm //. Qed.
we get:
The command has indeed failed with message:
Ltac call to "rewrite (ssrrwargs) (ssrclauses)" failed.
pattern (i + j) does not match LHS of comm
I'm creating an issue because this instance might have been omitted on purpose, and code might be relying on its absence accidentally. But I expect this isn't for performance reasons — or the instance we currently get would already be a problem.
Instance @cmra_assoc natR
might cause similar concerns, but I haven't checked; other instances might as well, but it's less clear how.
I also wonder whether something more should be Typeclasses Opaque
(say, nat_op
?), to avoid this instance triggering accidentally, tho I'm not sure that's possible.