Stream: Coq users

Topic: Nat.mul_succ_l


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

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

view this post on Zulip 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' (andpow_succ_r, though it has a strange useless condition), and add_succ_l work.

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

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

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

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

view this post on Zulip Pierre Rousselin (Oct 02 2023 at 11:34):

and deprecate poor pow_succ_r.


Last updated: Jun 23 2024 at 03:02 UTC