Stream: math-comp users

Topic: sumbool_of_bool in math-comp?


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Ana de Almeida Borges (Oct 19 2020 at 12:55):

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

view this post on Zulip Cyril Cohen (Oct 19 2020 at 13:50):

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

view this post on Zulip Christian Doczkal (Oct 19 2020 at 14:27):

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

view this post on Zulip 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.)

view this post on Zulip Enrico Tassi (Oct 19 2020 at 14:56):

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

view this post on Zulip Enrico Tassi (Oct 19 2020 at 14:57):

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

view this post on Zulip 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 :-)

view this post on Zulip 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!

view this post on Zulip 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!

view this post on Zulip 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....

view this post on Zulip 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: Oct 13 2024 at 01:02 UTC