Stream: math-comp users

Topic: ✔ Evaluating option values

Pierre Jouvelot (Jan 23 2022 at 12:04):

What is the motivation for this unexpected (for me) behavior regarding add and sub operations on options of nat?

From mathcomp Require Import all_ssreflect all_algebra all_fingroup.

Definition x := Some 3.
Eval compute in (x - 1, x, x + 1).

yielding (0, Some 3, 2) : nat * option nat * nat.

Emilio Jesús Gallego Arias (Jan 23 2022 at 12:27):

Hi Pierre, sub for nat is defined as 0 - x = 0 , that' standard, for the rest, the coercion will map None to 0, Some x to x, so that's also expected. It is quite convenient and I don't see any other option.

What are your expectations here ? [Other than making sub partial, but that's a hell usually, at least in a setting like Coq's)

Pierre Jouvelot (Jan 23 2022 at 12:50):

Emilio Jesús Gallego Arias said:

Hi Pierre, sub for nat is defined as 0 - x = 0 , that' standard, for the rest, the coercion will map None to 0, Some x to x, so that's also expected. It is quite convenient and I don't see any other option.

What are your expectations here ? [Other than making sub partial, but that's a hell usually, at least in a setting like Coq's)

Yes, that's what I was expecting; so why is x - 1 equal to 0 and not 2?

Kenji Maillard (Jan 23 2022 at 13:05):

Isn't there a coercion path through bool : isSome : option A -> bool and nat_of_bool : bool -> nat ?

Kenji Maillard (Jan 23 2022 at 13:06):

From mathcomp Require Import all_ssreflect all_algebra all_fingroup.

Definition x := Some 3.

Set Printing All.
Check (x : nat).
(* nat_of_bool (@isSome nat x) : nat *)
(*      : nat *)

Emilio Jesús Gallego Arias (Jan 23 2022 at 13:06):

Indeed, what @Kenji Maillard says, sorry Pierre I was careless

Emilio Jesús Gallego Arias (Jan 23 2022 at 13:07):

in both cases x is coerced to 1

Emilio Jesús Gallego Arias (Jan 23 2022 at 13:07):

what I said above is false, Some x is not coerced to x

Pierre Jouvelot (Jan 23 2022 at 13:13):

Emilio Jesús Gallego Arias said:

what I said above is false, Some x is not coerced to x

No problem. Thanks to @Kenji Maillard for his coercion path explanation.

Notification Bot (Jan 23 2022 at 13:15):

Pierre Jouvelot has marked this topic as resolved.

Last updated: Feb 08 2023 at 07:02 UTC