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`

.

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)

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?

Isn't there a coercion path through bool : `isSome : option A -> bool`

and `nat_of_bool : bool -> nat`

?

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

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

in both cases x is coerced to 1

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

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.

Pierre Jouvelot has marked this topic as resolved.

Last updated: Jul 23 2024 at 21:01 UTC