Library mathcomp.ssreflect.choice
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
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.).
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.
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.
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).
#[short(type="choiceType")]
HB.structure Definition Choice := { T of hasChoice T & hasDecEq T}.
Module Export ChoiceNamespace.
Module Choice.
Module InternalTheory.
Notation find := find_subdef.
Notation correct := choice_correct_subdef.
Arguments correct {_ _ _ _}.
Notation complete := choice_complete_subdef.
Arguments complete {_ _}.
Notation extensional := choice_extensional_subdef.
Arguments extensional {_ _ _}.
Section InternalTheory.
Variable T : Choice.type.
Implicit Types P Q : pred T.
Fact xchoose_subproof P exP :
{x | find P (ex_minn (@choice_complete_subdef _ P exP)) = Some x}.
End InternalTheory.
End InternalTheory.
End Choice.
End ChoiceNamespace.
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 PCanHasChoice f' : pcancel f f' → hasChoice sT.
Definition CanHasChoice f' (fK : cancel f f') :=
PCanHasChoice (can_pcan fK).
End CanChoice.
Section SubChoice.
Variables (P : pred T) (sT : subType P).
#[hnf] HB.instance Definition _ := Choice.copy (sub_type sT) (pcan_type valK).
End SubChoice.
Fact seq_hasChoice : hasChoice (seq T).
End OneType.
Section TagChoice.
Variables (I : choiceType) (T_ : I → choiceType).
Fact tagged_hasChoice : hasChoice {i : I & T_ i}.
End TagChoice.
Fact nat_hasChoice : hasChoice nat.
End ChoiceTheory.
#[short(type="subChoiceType")]
HB.structure Definition SubChoice T (P : pred T) :=
{ sT of Choice sT & isSub T P sT }.
Notation "[ 'Choice' 'of' T 'by' <: ]" := (Choice.copy T%type (sub_type T%type))
(at level 0, format "[ 'Choice' 'of' T 'by' <: ]") : form_scope.
Arguments Choice_isCountable.axioms_ T%type_scope.
#[short(type="countType")]
HB.structure Definition Countable := { T of Choice T & Choice_isCountable T }.
Arguments isCountable.axioms_ T%type_scope.
Section CountableTheory.
Variable T : countType.
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 PCanIsCountable sT (f : sT → T) f' (fK : pcancel f f') :=
isCountable.Build sT (pcan_pickleK fK).
Definition CanIsCountable sT f f' (fK : cancel f f') :=
@PCanIsCountable sT _ _ (can_pcan fK).
#[hnf] HB.instance Definition _ (P : pred T) (sT : subType P) :=
Countable.copy (sub_type sT) (pcan_type valK).
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.
End CountableTheory.
Notation "[ 'Countable' 'of' T 'by' <: ]" :=
(Countable.copy T%type (sub_type T%type))
(at level 0, format "[ 'Countable' 'of' T 'by' <: ]") : form_scope.
Arguments pickle_inv {T} n.
Arguments pickleK {T} x : rename.
Arguments pickleK_inv {T} x.
Arguments pickle_invK {T} n : rename.
#[short(type="subCountType")]
HB.structure Definition SubCountable T (P : pred T) :=
{ sT of Countable sT & isSub T P sT}.
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.
End TagCountType.
The remaining instances for standard datatypes.
Section CountableDataTypes.
Implicit Type T : countType.
Lemma nat_pickleK : pcancel id (@Some nat).
End CountableDataTypes.
Implicit Type T : countType.
Lemma nat_pickleK : pcancel id (@Some nat).
End CountableDataTypes.