Stream: math-comp users

Topic: Meaning of `ChoiceType`

view this post on Zulip Julin Shaji (Oct 03 2023 at 17:04):

What is the need and use for a ChoiceType?

I'm totally new to mathcomp and came across it in Chapter 8 of the mathcomp book (didn't read what came before it, that's the reason :grimacing:)

Had a look at
But still wasn't sure.

view this post on Zulip Karl Palmskog (Oct 03 2023 at 17:07):

the most obvious (computer science) application of choiceType is arguably for key-value mappings where the key type is not necessarily finite, like in finmap. Even more basic is that you can make sets with finitely many members from a type that has infinitely many members.

view this post on Zulip Julin Shaji (Oct 03 2023 at 17:25):

Well, I was trying out the example from the book like:

From mathcomp Require Import all_ssreflect all_algebra.

(* Example from Chapter 8 of mathcomp book *)

Inductive dir: predArgType :=
| South | North | East | West.

(* dir to an existing ordinal ?? *)
Definition d2o (d: dir): 'I_4 :=
  match d with
  | South => inord 0
  | North => inord 1
  | East => inord 2
  | West => inord 3

Definition o2d (o: 'I_4): option dir :=
  match val o with
  | 0 => Some South
  | 1 => Some North
  | 2 => Some East
  | 3 => Some West
  | _ => None

(* d2o and o2d cancel out *)
Lemma pcan_do4: pcancel d2o o2d.
  by case; rewrite /o2d /= inordK.

Compute (North \in dir).
(* = true : bool *)

Fail Check (North != South).  (* needs EqType *)
Fail Check (#| dir | == 4).   (* needs FinType *)

(* Give structure of ordinals to [dir] *)
Definition dir_eqMixin := PcanEqMixin pcan_do4.
Canonical dir_eqType := EqType dir dir_eqMixin.
Check (North != South).
(* North != South : bool *)

(* [CountType] implies [ChoiceType] by the way.
   Here it's explicitly given though *)
Definition dir_choiceMixin := PcanChoiceMixin pcan_do4.
Canonical dir_choiceType := ChoiceType dir dir_choiceMixin.

Definition dir_countMixin := PcanCountMixin pcan_do4.
Canonical dir_countType := CountType dir dir_countMixin.

Definition dir_finMixin := PcanFinMixin pcan_do4.
Canonical dir_finType := FinType dir dir_finMixin.
Check (#| dir | == 4).
(* #|dir| == 4 : bool *)

Check (North != South) && (North \in dir) && (#| dir | == 4).

I was looking for examples to illustrate what having the choice and count mixins add to the dir type.
What could be such examples?

As in, we can do boolean equality checks after adding the EqType mixin and find cardinality (that's it, right) after adding mixin for FinType.
Something similar.

view this post on Zulip Paolo Giarrusso (Oct 03 2023 at 17:59):

"Countable" means your type is isomorphic with a subset of the naturals

view this post on Zulip Julin Shaji (Oct 03 2023 at 18:04):

Does that entail having a function like ord North giving 0: nat in this case?

view this post on Zulip Pierre Roux (Oct 03 2023 at 18:13):

More precisely that there exist an injection into N (finite sets are countable for instance)

view this post on Zulip Emilio Jesús Gallego Arias (Oct 03 2023 at 18:21):

Indeed a motivation for having both choiceType and countable is to allow to have an instance of choiceType for the reals, which are not in bijection with N.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 03 2023 at 18:21):

most CS applications would only care about countable

Last updated: Jul 15 2024 at 20:02 UTC