## Stream: math-comp users

### Topic: sumbool_of_bool in math-comp?

#### Ana de Almeida Borges (Oct 18 2020 at 15:22):

I have some definitions similar to the following one:

``````From mathcomp Require Import ssrnat fintype.

Definition example (T : Type) (j k : nat) (f : 'I_k -> T) (d : T) : T :=
match Sumbool.sumbool_of_bool (j < k) with
| left ltjk => f (Ordinal ltjk)
| right _ => d
end.
``````

This doesn't feel like the math-comp way. Is there a function I can use other than `Sumbool.sumbool_of_bool`? This one is annoying because when `example` is part of a goal, rewriting with a hypothesis `ltjk : j < k = true` doesn't work. I have to destruct the whole expression being matched and then prove that one of the branches reaches a contradiction.

I've thought of using `inord j`, but here I can't be sure that `k > 0`, or adding that as an extra case doesn't really improve my current situation.

#### Reynald Affeldt (Oct 18 2020 at 23:56):

if k is some k'.+1 then you can write `if j <= k' then f (inord j) else d.`

#### Kazuhiko Sakaguchi (Oct 19 2020 at 05:52):

Case analysis on `ltnP` (or `boolP`) is useful in this case. (See https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/fintype.v#L2172)

``````Definition example (T : Type) (j k : nat) (f : 'I_k -> T) (d : T) : T :=
match ltnP j k with
| LtnNotGeq ltjk => f (Ordinal ltjk)
| _ => d
end.
``````

#### Christian Doczkal (Oct 19 2020 at 11:24):

@Ana de Almeida Borges I would use the following definition of `example`:

``````Definition example (T : Type) (j k : nat) (f : 'I_k -> T) (d : T) : T :=
if insub j is Some j' then f j' else d.
``````

The rationale is that casing on `ltnP` (or `idP` or `boolP`) requires taking care of the dependency. Moreover for `insub` there are the rewrite lemmas `insubT` and `insubF` that avoid a case analysis if `j < k` (or `k <= j`) follows from the context. Fun exercise: prove that my definition is equivalent to the definition given by @Kazuhiko Sakaguchi

#### Ana de Almeida Borges (Oct 19 2020 at 12:55):

Thank you! These suggestions are indeed much nicer than my solution. :)

#### Cyril Cohen (Oct 19 2020 at 13:50):

Isn't it `oapp f (insub j) d`?

#### Christian Doczkal (Oct 19 2020 at 14:27):

@Cyril Cohen , ah `oapp` was the one I was looking for :smile:

#### Christian Doczkal (Oct 19 2020 at 14:35):

Here is another related question. While toying around with the definition of @Kazuhiko Sakaguchi , I found myself unable to do the case analysis on `ltnP j k`. If one replaces `ltnP j k` with `@idP (j < k)` one can use idiom `case: {-}_ / idP` to do the case analysis. For `ltnP` I didn't manage to come up with the right invocation of `case:`. However, `destruct (ltnP j k)` did work. :thinking:
(This is mostly out of curiosity, given that the lack of anything corresponding to `insubT` and `insubF` is, at least to me, enough to prefer `insub` whenever possible.)

#### Enrico Tassi (Oct 19 2020 at 14:56):

Use `case: {-}_ {-}_ / (ltnP j k).` (there are two index occurrence to skip here, one per branch)

#### Enrico Tassi (Oct 19 2020 at 14:57):

`destruct` tries all possibilities, in this case it is nicer.

#### Enrico Tassi (Oct 19 2020 at 14:58):

the two occurrences are hidden in the types of the lambdas in the branches of the match. They should not even be there, and they are not printed. We all love dependent elimination :-)

#### Ana de Almeida Borges (Oct 19 2020 at 15:24):

Cyril Cohen said:

Isn't it `oapp f (insub j) d`?

the order of the arguments is `oapp f d (insub j)`, and yes, this works very well!

#### Christian Doczkal (Oct 19 2020 at 15:46):

Enrico Tassi said:

Use `case: {-}_ {-}_ / (ltnP j k).` (there are two index occurrence to skip here, one per branch)

That was enlightening, thanks!

#### Enrico Tassi (Oct 19 2020 at 16:14):

Clearly this approach does not scale, `ltnP` has 6 indexes, if one had to skip them all....

#### Christian Doczkal (Oct 19 2020 at 16:35):

Yes, if `insub` doesn't to the trick, I would advocate for using either `boolP` or `idP`, depending on whether one wants a boolean negation or a propositional one in the second branch. In this example, either one is fine.

Last updated: Feb 08 2023 at 07:02 UTC