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: Oct 13 2024 at 01:02 UTC