Could someone please explain me why `Nat.mul_succ_l`

is:

```
mul_succ_l
: forall n m : nat, S n * m = n * m + m
```

while `mul`

is defined by:

```
mul =
fix mul (n m : nat) {struct n} : nat :=
match n with
| 0 => 0
| S p => m + mul p m
end
: nat -> nat -> nat
```

I guess it is to get the simplication that is not directly provable by evaluation (that's the meaning of l)

I thought these kind of lemmas were here to offer some better control than `simpl`

for evaluation. That's how `pow_succ_r'`

(and`pow_succ_r`

, though it has a strange useless condition), and `add_succ_l`

work.

These statements are reused across `Nat`

, `N`

and `Z`

through the number hierarchy in `theories/Numbers/NatInt/NZAxioms.v`

:

```
Axiom add_succ_l : forall n m, (S n) + m == S (n + m).
Axiom mul_succ_l : forall n m, S n * m == n * m + m.
```

and for `N`

and `Z`

, the intention isn't to expose the internals of a definition on binary numbers, but to show that binary numbers follow the same laws as unary/Peano ones.

it wouldn't be wrong it they matched for `Nat`

, but I'm not even sure what statement is more natural, and if the surprise is worth the breakage. At least, `mul_succ_l`

encodes accurately that this matches on `(S ?m) * ?n`

.

Thanks for your answers. After playing around with some `mul_succ_l'`

mimicking the definition, I agree that one is not more natural than the other. It was surprising, though. There might be some room for a `mul_succ_l'`

and `mul_succ_r'`

(or better names if someone has a better idea) to offer finer control, imho (mathcomp has both).

and deprecate poor `pow_succ_r`

.

Last updated: Jun 23 2024 at 03:02 UTC