Library mathcomp.ssreflect.choice
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
This file contains the definitions of:
choiceType == interface for types with a choice operator.
countType == interface for countable types (implies choiceType).
subCountType == interface for types that are both subType and countType.
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.
choiceMixin T == type of choice mixins; the exact contents is
documented below in the Choice submodule.
ChoiceType T m == the packed choiceType class for T and mixin m.
[choiceType of T for cT] == clone for T of the choiceType cT.
[choiceType of T] == clone for T of the choiceType inferred for T.
CountType T m == the packed countType class for T and mixin m.
[countType of T for cT] == clone for T of the countType cT.
[count Type of T] == clone for T of the countType inferred for T.
[choiceMixin of T by <: ] == Choice mixin for T when T has a subType p
structure with p : pred cT and cT has a Choice
structure; the corresponding structure is Canonical.
[countMixin of T by <: ] == Count mixin for a subType T of a countType.
PcanChoiceMixin fK == Choice mixin for T, given f : T -> cT where cT has
a Choice structure, a left inverse partial function
g and fK : pcancel f g.
CanChoiceMixin fK == Choice mixin for T, given f : T -> cT, g and
fK : cancel f g.
PcanCountMixin fK == Count mixin for T, given f : T -> cT where cT has
a Countable structure, a left inverse partial
function g and fK : pcancel f g.
CanCountMixin fK == Count mixin 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 canonical eqType, choiceType, and countType
instances, and so simple datatypes can be similarly
equipped by encoding into GenTree.tree and using
the mixins 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 a Canonical choiceType and countType instances for
all basic datatypes (e.g., nat, bool, subTypes, pairs, sums, etc.).
Set Implicit Arguments.
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
Definition code := foldr (fun n m ⇒ 2 ^ n × m.*2.+1) 0.
Fixpoint decode_rec (v q r : nat) {struct q} :=
match q, r with
| 0, _ ⇒ [:: v]
| q'.+1, 0 ⇒ v :: [rec 0, q', q']
| q'.+1, 1 ⇒ [rec v.+1, q', q']
| q'.+1, r'.+2 ⇒ [rec v, q', r']
end where "[ 'rec' v , q , r ]" := (decode_rec v q r).
Arguments decode_rec : simpl nomatch.
Definition decode n := if n is 0 then [::] else [rec 0, n.-1, n.-1].
Lemma decodeK : cancel decode code.
Lemma codeK : cancel code decode.
Lemma ltn_code s : all (fun j ⇒ j < code s) s.
Lemma gtn_decode n : all (ltn^~ n) (decode n).
End CodeSeq.
Section OtherEncodings.
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.
Variables T T1 T2 : Type.
Definition seq_of_opt := @oapp T _ (nseq 1) [::].
Lemma seq_of_optK : cancel seq_of_opt ohead.
Definition tag_of_pair (p : T1 × T2) := @Tagged T1 p.1 (fun _ ⇒ T2) p.2.
Definition pair_of_tag (u : {i : T1 & T2}) := (tag u, tagged u).
Lemma tag_of_pairK : cancel tag_of_pair pair_of_tag.
Lemma pair_of_tagK : cancel pair_of_tag tag_of_pair.
Definition opair_of_sum (s : T1 + T2) :=
match s with inl x ⇒ (Some x, None) | inr y ⇒ (None, Some y) end.
Definition sum_of_opair p :=
oapp (some \o @inr T1 T2) (omap (@inl _ T2) p.1) p.2.
Lemma opair_of_sumK : pcancel opair_of_sum sum_of_opair.
Lemma bool_of_unitK : cancel (fun _ ⇒ true) (fun _ ⇒ tt).
End OtherEncodings.
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.
Module GenTree.
Section Def.
Variable T : Type.
Inductive tree := Leaf of T | Node of nat & seq tree.
Definition tree_rect K IH_leaf IH_node :=
fix loop t : K t := match t with
| Leaf x ⇒ IH_leaf x
| Node n f0 ⇒
let fix iter_pair f : foldr (fun t ⇒ prod (K t)) unit f :=
if f is t :: f' then (loop t, iter_pair f') else tt in
IH_node n f0 (iter_pair f0)
end.
Definition tree_rec (K : tree → Set) := @tree_rect K.
Definition tree_ind K IH_leaf IH_node :=
fix loop t : K t : Prop := match t with
| Leaf x ⇒ IH_leaf x
| Node n f0 ⇒
let fix iter_conj f : foldr (fun t ⇒ and (K t)) True f :=
if f is t :: f' then conj (loop t) (iter_conj f') else Logic.I
in IH_node n f0 (iter_conj f0)
end.
Fixpoint encode t : seq (nat + T) :=
match t with
| Leaf x ⇒ [:: inr _ x]
| Node n f ⇒ inl _ n.+1 :: rcons (flatten (map encode f)) (inl _ 0)
end.
Definition decode_step c fs :=
match c with
| inr x ⇒ (Leaf x :: fs.1, fs.2)
| inl 0 ⇒ ([::], fs.1 :: fs.2)
| inl n.+1 ⇒ (Node n fs.1 :: head [::] fs.2, behead fs.2)
end.
Definition decode c := ohead (foldr decode_step ([::], [::]) c).1.
Lemma codeK : pcancel encode decode.
End Def.
End GenTree.
Arguments GenTree.codeK : clear implicits.
Definition tree_eqMixin (T : eqType) := PcanEqMixin (GenTree.codeK T).
Canonical tree_eqType (T : eqType) := EqType (GenTree.tree T) (tree_eqMixin T).
Section Def.
Variable T : Type.
Inductive tree := Leaf of T | Node of nat & seq tree.
Definition tree_rect K IH_leaf IH_node :=
fix loop t : K t := match t with
| Leaf x ⇒ IH_leaf x
| Node n f0 ⇒
let fix iter_pair f : foldr (fun t ⇒ prod (K t)) unit f :=
if f is t :: f' then (loop t, iter_pair f') else tt in
IH_node n f0 (iter_pair f0)
end.
Definition tree_rec (K : tree → Set) := @tree_rect K.
Definition tree_ind K IH_leaf IH_node :=
fix loop t : K t : Prop := match t with
| Leaf x ⇒ IH_leaf x
| Node n f0 ⇒
let fix iter_conj f : foldr (fun t ⇒ and (K t)) True f :=
if f is t :: f' then conj (loop t) (iter_conj f') else Logic.I
in IH_node n f0 (iter_conj f0)
end.
Fixpoint encode t : seq (nat + T) :=
match t with
| Leaf x ⇒ [:: inr _ x]
| Node n f ⇒ inl _ n.+1 :: rcons (flatten (map encode f)) (inl _ 0)
end.
Definition decode_step c fs :=
match c with
| inr x ⇒ (Leaf x :: fs.1, fs.2)
| inl 0 ⇒ ([::], fs.1 :: fs.2)
| inl n.+1 ⇒ (Node n fs.1 :: head [::] fs.2, behead fs.2)
end.
Definition decode c := ohead (foldr decode_step ([::], [::]) c).1.
Lemma codeK : pcancel encode decode.
End Def.
End GenTree.
Arguments GenTree.codeK : clear implicits.
Definition tree_eqMixin (T : eqType) := PcanEqMixin (GenTree.codeK T).
Canonical tree_eqType (T : eqType) := EqType (GenTree.tree T) (tree_eqMixin T).
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).
Module Choice.
Section ClassDef.
Record mixin_of T := Mixin {
find : pred T → nat → option T;
_ : ∀ P n x, find P n = Some x → P x;
_ : ∀ P : pred T, (∃ x, P x) → ∃ n, find P n;
_ : ∀ P Q : pred T, P =1 Q → find P =1 find Q
}.
Record class_of T := Class {base : Equality.class_of T; mixin : mixin_of T}.
Local Coercion base : class_of >-> Equality.class_of.
Structure type := Pack {sort; _ : class_of sort}.
Local Coercion sort : type >-> Sortclass.
Variables (T : Type) (cT : type).
Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack T c.
Definition pack m :=
fun b bT & phant_id (Equality.class bT) b ⇒ Pack (@Class T b m).
Inheritance
Definition eqType := @Equality.Pack cT class.
End ClassDef.
Module Import Exports.
Coercion base : class_of >-> Equality.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Notation choiceType := type.
Notation choiceMixin := mixin_of.
Notation ChoiceType T m := (@pack T m _ _ id).
Notation "[ 'choiceType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
(at level 0, format "[ 'choiceType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'choiceType' 'of' T ]" := (@clone T _ _ id)
(at level 0, format "[ 'choiceType' 'of' T ]") : form_scope.
End Exports.
Module InternalTheory.
Section InternalTheory.
End ClassDef.
Module Import Exports.
Coercion base : class_of >-> Equality.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Notation choiceType := type.
Notation choiceMixin := mixin_of.
Notation ChoiceType T m := (@pack T m _ _ id).
Notation "[ 'choiceType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
(at level 0, format "[ 'choiceType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'choiceType' 'of' T ]" := (@clone T _ _ id)
(at level 0, format "[ 'choiceType' 'of' T ]") : form_scope.
End Exports.
Module InternalTheory.
Section InternalTheory.
Inner choice function.
Definition find T := find (mixin (class T)).
Variable T : choiceType.
Implicit Types P Q : pred T.
Lemma correct P n x : find P n = Some x → P x.
Lemma complete P : (∃ x, P x) → (∃ n, find P n).
Lemma extensional P Q : P =1 Q → find P =1 find Q.
Fact xchoose_subproof P exP : {x | find P (ex_minn (@complete P exP)) = Some x}.
End InternalTheory.
End InternalTheory.
End Choice.
Export Choice.Exports.
Section ChoiceTheory.
Implicit Type T : choiceType.
Import Choice.InternalTheory CodeSeq.
Local Notation dc := decode.
Section OneType.
Variable T : choiceType.
Implicit Types P Q : pred T.
Definition xchoose P exP := sval (@xchoose_subproof T P exP).
Lemma xchooseP P exP : P (@xchoose P exP).
Lemma eq_xchoose P Q exP exQ : P =1 Q → @xchoose P exP = @xchoose Q exQ.
Lemma sigW P : (∃ x, P x) → {x | P x}.
Lemma sig2W P Q : (exists2 x, P x & Q x) → {x | P x & Q x}.
Lemma sig_eqW (vT : eqType) (lhs rhs : T → vT) :
(∃ x, lhs x = rhs x) → {x | lhs x = rhs x}.
Lemma sig2_eqW (vT : eqType) (P : pred T) (lhs rhs : T → vT) :
(exists2 x, P x & lhs x = rhs x) → {x | P x & lhs x = rhs x}.
Definition choose P x0 :=
if insub x0 : {? x | P x} is Some (exist x Px) then
xchoose (ex_intro [eta P] x Px)
else x0.
Lemma chooseP P x0 : P x0 → P (choose P x0).
Lemma choose_id P x0 y0 : P x0 → P y0 → choose P x0 = choose P y0.
Lemma eq_choose P Q : P =1 Q → choose P =1 choose Q.
Section CanChoice.
Variables (sT : Type) (f : sT → T).
Lemma PcanChoiceMixin f' : pcancel f f' → choiceMixin sT.
Definition CanChoiceMixin f' (fK : cancel f f') :=
PcanChoiceMixin (can_pcan fK).
End CanChoice.
Section SubChoice.
Variables (P : pred T) (sT : subType P).
Definition sub_choiceMixin := PcanChoiceMixin (@valK T P sT).
Definition sub_choiceClass := @Choice.Class sT (sub_eqMixin sT) sub_choiceMixin.
Canonical sub_choiceType := Choice.Pack sub_choiceClass.
End SubChoice.
Fact seq_choiceMixin : choiceMixin (seq T).
Canonical seq_choiceType := Eval hnf in ChoiceType (seq T) seq_choiceMixin.
End OneType.
Section TagChoice.
Variables (I : choiceType) (T_ : I → choiceType).
Fact tagged_choiceMixin : choiceMixin {i : I & T_ i}.
Canonical tagged_choiceType :=
Eval hnf in ChoiceType {i : I & T_ i} tagged_choiceMixin.
End TagChoice.
Fact nat_choiceMixin : choiceMixin nat.
Canonical nat_choiceType := Eval hnf in ChoiceType nat nat_choiceMixin.
Definition bool_choiceMixin := CanChoiceMixin oddb.
Canonical bool_choiceType := Eval hnf in ChoiceType bool bool_choiceMixin.
Canonical bitseq_choiceType := Eval hnf in [choiceType of bitseq].
Definition unit_choiceMixin := CanChoiceMixin bool_of_unitK.
Canonical unit_choiceType := Eval hnf in ChoiceType unit unit_choiceMixin.
Definition void_choiceMixin := PcanChoiceMixin (of_voidK unit).
Canonical void_choiceType := Eval hnf in ChoiceType void void_choiceMixin.
Definition option_choiceMixin T := CanChoiceMixin (@seq_of_optK T).
Canonical option_choiceType T :=
Eval hnf in ChoiceType (option T) (option_choiceMixin T).
Definition sig_choiceMixin T (P : pred T) : choiceMixin {x | P x} :=
sub_choiceMixin _.
Canonical sig_choiceType T (P : pred T) :=
Eval hnf in ChoiceType {x | P x} (sig_choiceMixin P).
Definition prod_choiceMixin T1 T2 := CanChoiceMixin (@tag_of_pairK T1 T2).
Canonical prod_choiceType T1 T2 :=
Eval hnf in ChoiceType (T1 × T2) (prod_choiceMixin T1 T2).
Definition sum_choiceMixin T1 T2 := PcanChoiceMixin (@opair_of_sumK T1 T2).
Canonical sum_choiceType T1 T2 :=
Eval hnf in ChoiceType (T1 + T2) (sum_choiceMixin T1 T2).
Definition tree_choiceMixin T := PcanChoiceMixin (GenTree.codeK T).
Canonical tree_choiceType T := ChoiceType (GenTree.tree T) (tree_choiceMixin T).
End ChoiceTheory.
Notation "[ 'choiceMixin' 'of' T 'by' <: ]" :=
(sub_choiceMixin _ : choiceMixin T)
(at level 0, format "[ 'choiceMixin' 'of' T 'by' <: ]") : form_scope.
Module Countable.
Record mixin_of (T : Type) : Type := Mixin {
pickle : T → nat;
unpickle : nat → option T;
pickleK : pcancel pickle unpickle
}.
Definition EqMixin T m := PcanEqMixin (@pickleK T m).
Definition ChoiceMixin T m := PcanChoiceMixin (@pickleK T m).
Section ClassDef.
Record class_of T := Class { base : Choice.class_of T; mixin : mixin_of T }.
Local Coercion base : class_of >-> Choice.class_of.
Structure type : Type := Pack {sort : Type; _ : class_of sort}.
Local Coercion sort : type >-> Sortclass.
Variables (T : Type) (cT : type).
Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack T c.
Definition pack m :=
fun bT b & phant_id (Choice.class bT) b ⇒ Pack (@Class T b m).
Definition eqType := @Equality.Pack cT class.
Definition choiceType := @Choice.Pack cT class.
End ClassDef.
Module Exports.
Coercion base : class_of >-> Choice.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Notation countType := type.
Notation CountType T m := (@pack T m _ _ id).
Notation CountMixin := Mixin.
Notation CountChoiceMixin := ChoiceMixin.
Notation "[ 'countType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
(at level 0, format "[ 'countType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'countType' 'of' T ]" := (@clone T _ _ id)
(at level 0, format "[ 'countType' 'of' T ]") : form_scope.
End Exports.
End Countable.
Export Countable.Exports.
Definition unpickle T := Countable.unpickle (Countable.class T).
Definition pickle T := Countable.pickle (Countable.class T).
Arguments unpickle {T} n.
Arguments pickle {T} x.
Section CountableTheory.
Variable T : countType.
Lemma pickleK : @pcancel nat T pickle unpickle.
Definition pickle_inv n :=
obind (fun x : T ⇒ if pickle x == n then Some x else None) (unpickle n).
Lemma pickle_invK : ocancel pickle_inv pickle.
Lemma pickleK_inv : pcancel pickle pickle_inv.
Lemma pcan_pickleK sT f f' :
@pcancel T sT f f' → pcancel (pickle \o f) (pcomp f' unpickle).
Definition PcanCountMixin sT f f' (fK : pcancel f f') :=
@CountMixin sT _ _ (pcan_pickleK fK).
Definition CanCountMixin sT f f' (fK : cancel f f') :=
@PcanCountMixin sT _ _ (can_pcan fK).
Definition sub_countMixin P sT := PcanCountMixin (@valK T P sT).
Definition pickle_seq s := CodeSeq.code (map (@pickle T) s).
Definition unpickle_seq n := Some (pmap (@unpickle T) (CodeSeq.decode n)).
Lemma pickle_seqK : pcancel pickle_seq unpickle_seq.
Definition seq_countMixin := CountMixin pickle_seqK.
Canonical seq_countType := Eval hnf in CountType (seq T) seq_countMixin.
End CountableTheory.
Notation "[ 'countMixin' 'of' T 'by' <: ]" :=
(sub_countMixin _ : Countable.mixin_of T)
(at level 0, format "[ 'countMixin' 'of' T 'by' <: ]") : form_scope.
Arguments pickle_inv {T} n.
Arguments pickleK {T} x.
Arguments pickleK_inv {T} x.
Arguments pickle_invK {T} n : rename.
Section SubCountType.
Variables (T : choiceType) (P : pred T).
Import Countable.
Structure subCountType : Type :=
SubCountType {subCount_sort :> subType P; _ : mixin_of subCount_sort}.
Coercion sub_countType (sT : subCountType) :=
Eval hnf in pack (let: SubCountType _ m := sT return mixin_of sT in m) id.
Canonical sub_countType.
Definition pack_subCountType U :=
fun sT cT & sub_sort sT × sort cT → U × U ⇒
fun b m & phant_id (Class b m) (class cT) ⇒ @SubCountType sT m.
End SubCountType.
Variable T : choiceType.
Implicit Types P Q : pred T.
Lemma correct P n x : find P n = Some x → P x.
Lemma complete P : (∃ x, P x) → (∃ n, find P n).
Lemma extensional P Q : P =1 Q → find P =1 find Q.
Fact xchoose_subproof P exP : {x | find P (ex_minn (@complete P exP)) = Some x}.
End InternalTheory.
End InternalTheory.
End Choice.
Export Choice.Exports.
Section ChoiceTheory.
Implicit Type T : choiceType.
Import Choice.InternalTheory CodeSeq.
Local Notation dc := decode.
Section OneType.
Variable T : choiceType.
Implicit Types P Q : pred T.
Definition xchoose P exP := sval (@xchoose_subproof T P exP).
Lemma xchooseP P exP : P (@xchoose P exP).
Lemma eq_xchoose P Q exP exQ : P =1 Q → @xchoose P exP = @xchoose Q exQ.
Lemma sigW P : (∃ x, P x) → {x | P x}.
Lemma sig2W P Q : (exists2 x, P x & Q x) → {x | P x & Q x}.
Lemma sig_eqW (vT : eqType) (lhs rhs : T → vT) :
(∃ x, lhs x = rhs x) → {x | lhs x = rhs x}.
Lemma sig2_eqW (vT : eqType) (P : pred T) (lhs rhs : T → vT) :
(exists2 x, P x & lhs x = rhs x) → {x | P x & lhs x = rhs x}.
Definition choose P x0 :=
if insub x0 : {? x | P x} is Some (exist x Px) then
xchoose (ex_intro [eta P] x Px)
else x0.
Lemma chooseP P x0 : P x0 → P (choose P x0).
Lemma choose_id P x0 y0 : P x0 → P y0 → choose P x0 = choose P y0.
Lemma eq_choose P Q : P =1 Q → choose P =1 choose Q.
Section CanChoice.
Variables (sT : Type) (f : sT → T).
Lemma PcanChoiceMixin f' : pcancel f f' → choiceMixin sT.
Definition CanChoiceMixin f' (fK : cancel f f') :=
PcanChoiceMixin (can_pcan fK).
End CanChoice.
Section SubChoice.
Variables (P : pred T) (sT : subType P).
Definition sub_choiceMixin := PcanChoiceMixin (@valK T P sT).
Definition sub_choiceClass := @Choice.Class sT (sub_eqMixin sT) sub_choiceMixin.
Canonical sub_choiceType := Choice.Pack sub_choiceClass.
End SubChoice.
Fact seq_choiceMixin : choiceMixin (seq T).
Canonical seq_choiceType := Eval hnf in ChoiceType (seq T) seq_choiceMixin.
End OneType.
Section TagChoice.
Variables (I : choiceType) (T_ : I → choiceType).
Fact tagged_choiceMixin : choiceMixin {i : I & T_ i}.
Canonical tagged_choiceType :=
Eval hnf in ChoiceType {i : I & T_ i} tagged_choiceMixin.
End TagChoice.
Fact nat_choiceMixin : choiceMixin nat.
Canonical nat_choiceType := Eval hnf in ChoiceType nat nat_choiceMixin.
Definition bool_choiceMixin := CanChoiceMixin oddb.
Canonical bool_choiceType := Eval hnf in ChoiceType bool bool_choiceMixin.
Canonical bitseq_choiceType := Eval hnf in [choiceType of bitseq].
Definition unit_choiceMixin := CanChoiceMixin bool_of_unitK.
Canonical unit_choiceType := Eval hnf in ChoiceType unit unit_choiceMixin.
Definition void_choiceMixin := PcanChoiceMixin (of_voidK unit).
Canonical void_choiceType := Eval hnf in ChoiceType void void_choiceMixin.
Definition option_choiceMixin T := CanChoiceMixin (@seq_of_optK T).
Canonical option_choiceType T :=
Eval hnf in ChoiceType (option T) (option_choiceMixin T).
Definition sig_choiceMixin T (P : pred T) : choiceMixin {x | P x} :=
sub_choiceMixin _.
Canonical sig_choiceType T (P : pred T) :=
Eval hnf in ChoiceType {x | P x} (sig_choiceMixin P).
Definition prod_choiceMixin T1 T2 := CanChoiceMixin (@tag_of_pairK T1 T2).
Canonical prod_choiceType T1 T2 :=
Eval hnf in ChoiceType (T1 × T2) (prod_choiceMixin T1 T2).
Definition sum_choiceMixin T1 T2 := PcanChoiceMixin (@opair_of_sumK T1 T2).
Canonical sum_choiceType T1 T2 :=
Eval hnf in ChoiceType (T1 + T2) (sum_choiceMixin T1 T2).
Definition tree_choiceMixin T := PcanChoiceMixin (GenTree.codeK T).
Canonical tree_choiceType T := ChoiceType (GenTree.tree T) (tree_choiceMixin T).
End ChoiceTheory.
Notation "[ 'choiceMixin' 'of' T 'by' <: ]" :=
(sub_choiceMixin _ : choiceMixin T)
(at level 0, format "[ 'choiceMixin' 'of' T 'by' <: ]") : form_scope.
Module Countable.
Record mixin_of (T : Type) : Type := Mixin {
pickle : T → nat;
unpickle : nat → option T;
pickleK : pcancel pickle unpickle
}.
Definition EqMixin T m := PcanEqMixin (@pickleK T m).
Definition ChoiceMixin T m := PcanChoiceMixin (@pickleK T m).
Section ClassDef.
Record class_of T := Class { base : Choice.class_of T; mixin : mixin_of T }.
Local Coercion base : class_of >-> Choice.class_of.
Structure type : Type := Pack {sort : Type; _ : class_of sort}.
Local Coercion sort : type >-> Sortclass.
Variables (T : Type) (cT : type).
Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack T c.
Definition pack m :=
fun bT b & phant_id (Choice.class bT) b ⇒ Pack (@Class T b m).
Definition eqType := @Equality.Pack cT class.
Definition choiceType := @Choice.Pack cT class.
End ClassDef.
Module Exports.
Coercion base : class_of >-> Choice.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Notation countType := type.
Notation CountType T m := (@pack T m _ _ id).
Notation CountMixin := Mixin.
Notation CountChoiceMixin := ChoiceMixin.
Notation "[ 'countType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
(at level 0, format "[ 'countType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'countType' 'of' T ]" := (@clone T _ _ id)
(at level 0, format "[ 'countType' 'of' T ]") : form_scope.
End Exports.
End Countable.
Export Countable.Exports.
Definition unpickle T := Countable.unpickle (Countable.class T).
Definition pickle T := Countable.pickle (Countable.class T).
Arguments unpickle {T} n.
Arguments pickle {T} x.
Section CountableTheory.
Variable T : countType.
Lemma pickleK : @pcancel nat T pickle unpickle.
Definition pickle_inv n :=
obind (fun x : T ⇒ if pickle x == n then Some x else None) (unpickle n).
Lemma pickle_invK : ocancel pickle_inv pickle.
Lemma pickleK_inv : pcancel pickle pickle_inv.
Lemma pcan_pickleK sT f f' :
@pcancel T sT f f' → pcancel (pickle \o f) (pcomp f' unpickle).
Definition PcanCountMixin sT f f' (fK : pcancel f f') :=
@CountMixin sT _ _ (pcan_pickleK fK).
Definition CanCountMixin sT f f' (fK : cancel f f') :=
@PcanCountMixin sT _ _ (can_pcan fK).
Definition sub_countMixin P sT := PcanCountMixin (@valK T P sT).
Definition pickle_seq s := CodeSeq.code (map (@pickle T) s).
Definition unpickle_seq n := Some (pmap (@unpickle T) (CodeSeq.decode n)).
Lemma pickle_seqK : pcancel pickle_seq unpickle_seq.
Definition seq_countMixin := CountMixin pickle_seqK.
Canonical seq_countType := Eval hnf in CountType (seq T) seq_countMixin.
End CountableTheory.
Notation "[ 'countMixin' 'of' T 'by' <: ]" :=
(sub_countMixin _ : Countable.mixin_of T)
(at level 0, format "[ 'countMixin' 'of' T 'by' <: ]") : form_scope.
Arguments pickle_inv {T} n.
Arguments pickleK {T} x.
Arguments pickleK_inv {T} x.
Arguments pickle_invK {T} n : rename.
Section SubCountType.
Variables (T : choiceType) (P : pred T).
Import Countable.
Structure subCountType : Type :=
SubCountType {subCount_sort :> subType P; _ : mixin_of subCount_sort}.
Coercion sub_countType (sT : subCountType) :=
Eval hnf in pack (let: SubCountType _ m := sT return mixin_of sT in m) id.
Canonical sub_countType.
Definition pack_subCountType U :=
fun sT cT & sub_sort sT × sort cT → U × U ⇒
fun b m & phant_id (Class b m) (class cT) ⇒ @SubCountType sT m.
End SubCountType.
This assumes that T has both countType and subType structures.
Notation "[ 'subCountType' 'of' T ]" :=
(@pack_subCountType _ _ T _ _ id _ _ id)
(at level 0, format "[ 'subCountType' 'of' T ]") : form_scope.
Section TagCountType.
Variables (I : countType) (T_ : I → countType).
Definition pickle_tagged (u : {i : I & T_ i}) :=
CodeSeq.code [:: pickle (tag u); pickle (tagged u)].
Definition unpickle_tagged s :=
if CodeSeq.decode s is [:: ni; nx] then
obind (fun i ⇒ omap (@Tagged I i T_) (unpickle nx)) (unpickle ni)
else None.
Lemma pickle_taggedK : pcancel pickle_tagged unpickle_tagged.
Definition tag_countMixin := CountMixin pickle_taggedK.
Canonical tag_countType := Eval hnf in CountType {i : I & T_ i} tag_countMixin.
End TagCountType.
(@pack_subCountType _ _ T _ _ id _ _ id)
(at level 0, format "[ 'subCountType' 'of' T ]") : form_scope.
Section TagCountType.
Variables (I : countType) (T_ : I → countType).
Definition pickle_tagged (u : {i : I & T_ i}) :=
CodeSeq.code [:: pickle (tag u); pickle (tagged u)].
Definition unpickle_tagged s :=
if CodeSeq.decode s is [:: ni; nx] then
obind (fun i ⇒ omap (@Tagged I i T_) (unpickle nx)) (unpickle ni)
else None.
Lemma pickle_taggedK : pcancel pickle_tagged unpickle_tagged.
Definition tag_countMixin := CountMixin pickle_taggedK.
Canonical tag_countType := Eval hnf in CountType {i : I & T_ i} tag_countMixin.
End TagCountType.
The remaining Canonicals for standard datatypes.
Section CountableDataTypes.
Implicit Type T : countType.
Lemma nat_pickleK : pcancel id (@Some nat).
Definition nat_countMixin := CountMixin nat_pickleK.
Canonical nat_countType := Eval hnf in CountType nat nat_countMixin.
Definition bool_countMixin := CanCountMixin oddb.
Canonical bool_countType := Eval hnf in CountType bool bool_countMixin.
Canonical bitseq_countType := Eval hnf in [countType of bitseq].
Definition unit_countMixin := CanCountMixin bool_of_unitK.
Canonical unit_countType := Eval hnf in CountType unit unit_countMixin.
Definition void_countMixin := PcanCountMixin (of_voidK unit).
Canonical void_countType := Eval hnf in CountType void void_countMixin.
Definition option_countMixin T := CanCountMixin (@seq_of_optK T).
Canonical option_countType T :=
Eval hnf in CountType (option T) (option_countMixin T).
Definition sig_countMixin T (P : pred T) := [countMixin of {x | P x} by <:].
Canonical sig_countType T (P : pred T) :=
Eval hnf in CountType {x | P x} (sig_countMixin P).
Canonical sig_subCountType T (P : pred T) :=
Eval hnf in [subCountType of {x | P x}].
Definition prod_countMixin T1 T2 := CanCountMixin (@tag_of_pairK T1 T2).
Canonical prod_countType T1 T2 :=
Eval hnf in CountType (T1 × T2) (prod_countMixin T1 T2).
Definition sum_countMixin T1 T2 := PcanCountMixin (@opair_of_sumK T1 T2).
Canonical sum_countType T1 T2 :=
Eval hnf in CountType (T1 + T2) (sum_countMixin T1 T2).
Definition tree_countMixin T := PcanCountMixin (GenTree.codeK T).
Canonical tree_countType T := CountType (GenTree.tree T) (tree_countMixin T).
End CountableDataTypes.
Implicit Type T : countType.
Lemma nat_pickleK : pcancel id (@Some nat).
Definition nat_countMixin := CountMixin nat_pickleK.
Canonical nat_countType := Eval hnf in CountType nat nat_countMixin.
Definition bool_countMixin := CanCountMixin oddb.
Canonical bool_countType := Eval hnf in CountType bool bool_countMixin.
Canonical bitseq_countType := Eval hnf in [countType of bitseq].
Definition unit_countMixin := CanCountMixin bool_of_unitK.
Canonical unit_countType := Eval hnf in CountType unit unit_countMixin.
Definition void_countMixin := PcanCountMixin (of_voidK unit).
Canonical void_countType := Eval hnf in CountType void void_countMixin.
Definition option_countMixin T := CanCountMixin (@seq_of_optK T).
Canonical option_countType T :=
Eval hnf in CountType (option T) (option_countMixin T).
Definition sig_countMixin T (P : pred T) := [countMixin of {x | P x} by <:].
Canonical sig_countType T (P : pred T) :=
Eval hnf in CountType {x | P x} (sig_countMixin P).
Canonical sig_subCountType T (P : pred T) :=
Eval hnf in [subCountType of {x | P x}].
Definition prod_countMixin T1 T2 := CanCountMixin (@tag_of_pairK T1 T2).
Canonical prod_countType T1 T2 :=
Eval hnf in CountType (T1 × T2) (prod_countMixin T1 T2).
Definition sum_countMixin T1 T2 := PcanCountMixin (@opair_of_sumK T1 T2).
Canonical sum_countType T1 T2 :=
Eval hnf in CountType (T1 + T2) (sum_countMixin T1 T2).
Definition tree_countMixin T := PcanCountMixin (GenTree.codeK T).
Canonical tree_countType T := CountType (GenTree.tree T) (tree_countMixin T).
End CountableDataTypes.