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.

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

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.
```

@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

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

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

?

@Cyril Cohen , ah `oapp`

was the one I was looking for :smile:

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.)

Use `case: {-}_ {-}_ / (ltnP j k).`

(there are two index occurrence to skip here, one per branch)

`destruct`

tries all possibilities, in this case it is nicer.

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 :-)

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!

Enrico Tassi said:

Use

`case: {-}_ {-}_ / (ltnP j k).`

(there are two index occurrence to skip here, one per branch)

That was enlightening, thanks!

Clearly this approach does not scale, `ltnP`

has 6 indexes, if one had to skip them all....

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: Jul 25 2024 at 16:02 UTC