## 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: Jul 23 2024 at 21:01 UTC