Stream: Coq users

Topic: Nat.mul_succ_l

Pierre Rousselin (Oct 02 2023 at 10:39):

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
``````

Laurent Théry (Oct 02 2023 at 10:43):

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

Pierre Rousselin (Oct 02 2023 at 10:55):

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.

Paolo Giarrusso (Oct 02 2023 at 11:04):

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

Paolo Giarrusso (Oct 02 2023 at 11:07):

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.

Paolo Giarrusso (Oct 02 2023 at 11:12):

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

Pierre Rousselin (Oct 02 2023 at 11:33):

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

Pierre Rousselin (Oct 02 2023 at 11:34):

and deprecate poor `pow_succ_r`.

Last updated: Jun 23 2024 at 03:02 UTC