Stream: math-comp users

Topic: Meaning of `ChoiceType`

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 https://math-comp.github.io/htmldoc/mathcomp.ssreflect.choice.html
But still wasn't sure.

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.

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

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


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

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.

Paolo Giarrusso (Oct 03 2023 at 17:59):

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

Julin Shaji (Oct 03 2023 at 18:04):

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

Pierre Roux (Oct 03 2023 at 18:13):

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

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.

Emilio Jesús Gallego Arias (Oct 03 2023 at 18:21):

most CS applications would only care about countable

Last updated: Oct 13 2024 at 01:02 UTC