Library mathcomp.ssreflect.choice

Types with a choice operator NB: See CONTRIBUTING.md for an introduction to HB concepts and commands. This file contains the definitions of: choiceType == interface for types with a choice operator The HB class is Choice. The exact contents is documented below just before hasChoice. subChoiceType == interface for types that are both subType and choiceType The HB class is SubChoice. countType == interface for countable types (implies choiceType) The HB class is Countable. subCountType == interface for types that are both subType and countType The HB class is SubCountable. xchoose exP == a standard x such that P x, given exP : exists x : T, P x when T is a choiceType The choice depends only on the extent of P (in particular, it is independent of exP). choose P x0 == if P x0, a standard x such that P x pickle x == a nat encoding the value x : T, where T is a countType unpickle n == a partial inverse to pickle: unpickle (pickle x) = Some x pickle_inv n == a sharp partial inverse to pickle pickle_inv n = Some x if and only if pickle x = n PCanIsCountable ff' == builds an instance of the isCountable interface given ff' : pcancel f f' where the codomain of f is a countType CanIsCountable ff' == builds an instance of the isCountable interface given ff' : cancel f f' where the codomain of f is a countType [Choice of T by <: ], [Countable of T by <: ] == Choice/Countable interface for T when T has a subType p structure with p : pred cT and cT has a Choice/Countable interface The corresponding structure is Canonical. This notation is in form_scope. List of Choice/Countable factories with a dedicated alias: pcan_type fK == Choice/Countable for T, given f : T -> cT where cT has a Choice/Countable structure, a left inverse partial function g and fK : pcancel f g can_type fK == Choice/Countable for T, given f : T -> cT, g and fK : cancel f g GenTree.tree T == generic n-ary tree type with nat-labeled nodes and T-labeled leaves, for example GenTree.Leaf (x : T), GenTree.Node 5 [:: t; t' ] GenTree.tree is equipped with eqType, choiceType, and countType instances, and so simple datatypes can be similarly equipped by encoding into GenTree.tree and using the interfaces above. CodeSeq.code == bijection from seq nat to nat CodeSeq.decode == bijection inverse to CodeSeq.code In addition to the lemmas relevant to these definitions, this file also contains definitions of choiceType and countType instances for all basic basic datatypes (e.g., nat, bool, subTypes, pairs, sums, etc.).

Technical definitions about coding and decoding of nat sequences, which are used below to define various Canonical instances of the choice and countable interfaces.

Goedel-style one-to-one encoding of seq nat into nat. The code for [:: n1; ...; nk] has binary representation 1 0 ... 0 1 ... 1 0 ... 0 1 0 ... 0 <-----> <-----> <-----> nk 0s n2 0s n1 0s

Miscellaneous encodings: option T -c-> seq T, T1 * T2 -c-> {i : T1 & T2} T1 + T2 -c-> option T1 * option T2, unit -c-> bool; bool -c-> nat is already covered in ssrnat by the nat_of_bool coercion, the odd predicate, and their "cancellation" lemma oddb. We use these encodings to propagate canonical structures through these type constructors so that ultimately all Choice and Countable instanced derive from nat and the seq and sigT constructors.

Generic variable-arity tree type, providing an encoding target for miscellaneous user datatypes. The GenTree.tree type can be combined with a sigT type to model multi-sorted concrete datatypes.

Structures for Types with a choice function, and for Types with countably many elements. The two concepts are closely linked: we indeed make Countable a subclass of Choice, as countable choice is valid in CiC. This apparent redundancy is needed to ensure the consistency of the Canonical inference, as the canonical Choice for a given type may differ from the countable choice for its canonical Countable structure, e.g., for options. The Choice interface exposes two choice functions; for T : choiceType and P : pred T, we provide: xchoose : (exists x, P x) -> T choose : pred T -> T -> T While P (xchoose exP) will always hold, P (choose P x0) will be true if and only if P x0 holds. Both xchoose and choose are extensional in P and do not depend on the witness exP or x0 (provided P x0 holds). Note that xchoose is slightly more powerful, but less convenient to use. However, neither choose nor xchoose are composable: it would not be be possible to extend the Choice structure to arbitrary pairs using only these functions, for instance. Internally, the interfaces provides a subtly stronger operation, Choice.InternalTheory.find, which performs a limited search using an integer parameter only rather than a full value as [x]choose does. This is not a restriction in a constructive theory, where all types are concrete and hence countable. In the case of an axiomatic theory, such as that of the Coq reals library, postulating a suitable axiom of choice suppresses the need for guidance. Nevertheless this operation is just what is needed to make the Choice interface compose. The Countable interface provides three functions; for T : countType we get pickle : T -> nat, and unpickle, pickle_inv : nat -> option T. The functions provide an effective embedding of T in nat: unpickle is a left inverse to pickle, which satisfies pcancel pickle unpickle, i.e., unpickle \o pickle =1 some; pickle_inv is a more precise inverse for which we also have ocancel pickle_inv pickle. Both unpickle and pickle need to be partial functions to allow for possibly empty types such as {x | P x}. The names of these functions underline the correspondence with the notion of "Serializable" types in programming languages. Finally, we need to provide a join class to let type inference unify subType and countType class constraints, e.g., for a countable subType of an uncountable choiceType (the issue does not arise earlier with eqType or choiceType because in practice the base type of an Equality/Choice subType is always an Equality/Choice Type).

This assumes that T has both countType and subType structures.

The remaining instances for standard datatypes.