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.
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.
hasChoice 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.
[hasChoice 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.
[isCountable 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.
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.
Notation "[ 'hasChoice' 'of' T ]" := (Choice.on _ : hasChoice T%type)
(at level 0, format "[ 'hasChoice' 'of' T ]") : form_scope.
Notation "[ 'choiceType' 'of' T 'for' C ]" := (Choice.clone T%type C)
(at level 0, format "[ 'choiceType' 'of' T 'for' C ]") : form_scope.
Notation "[ 'choiceType' 'of' T ]" := (Choice.clone T%type _)
(at level 0, format "[ 'choiceType' 'of' T ]") : form_scope.
Section ChoiceTheory.
Implicit Type T : choiceType.
Import Choice.InternalTheory CodeSeq.
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' → hasChoice 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_hasChoice := PcanChoiceMixin (@valK T P sT).
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 subChoiceType := SubChoice.type.
Notation "[ 'Choice' 'of' T 'by' <: ]" := (Choice.copy T%type (sub_type T))
(at level 0, format "[ 'Choice' 'of' T 'by' <: ]") : form_scope.
Notation "[ 'hasChoice' 'of' T 'by' <: ]" :=
(sub_hasChoice _ : hasChoice T)
(at level 0, format "[ 'hasChoice' 'of' T 'by' <: ]") : form_scope.
Arguments isCountable.axioms_ T%type_scope.
#[short(type="countType")]
HB.structure Definition Countable := { T of Choice T & isCountable T }.
Notation "[ 'isCountable' 'of' T ]" := (Countable.on T%type : isCountable T%type)
(at level 0, format "[ 'isCountable' 'of' T ]") : form_scope.
Notation "[ 'countType' 'of' T 'for' cT ]" := (Countable.clone T%type cT)
(at level 0, format "[ 'countType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'countType' 'of' T ]" := (Countable.clone T%type _)
(at level 0, format "[ 'countType' 'of' T ]") : form_scope.
count_type cntT is a canonical count type generated by
cntT : isCountable T
Definition count_type T of isCountable T := T.
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 PcanCountMixin sT (f : sT → T) f' (fK : pcancel f f') :=
isCountable.Build sT (pcan_pickleK fK).
Definition CanCountMixin sT f f' (fK : cancel f f') :=
@PcanCountMixin sT _ _ (can_pcan fK).
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))
(at level 0, format "[ 'Countable' 'of' T 'by' <: ]") : form_scope.
Notation "[ 'isCountable' 'of' T 'by' <: ]" := [Countable of T by <:]
(at level 0, format "[ 'isCountable' '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 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 PcanCountMixin sT (f : sT → T) f' (fK : pcancel f f') :=
isCountable.Build sT (pcan_pickleK fK).
Definition CanCountMixin sT f f' (fK : cancel f f') :=
@PcanCountMixin sT _ _ (can_pcan fK).
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))
(at level 0, format "[ 'Countable' 'of' T 'by' <: ]") : form_scope.
Notation "[ 'isCountable' 'of' T 'by' <: ]" := [Countable of T by <:]
(at level 0, format "[ 'isCountable' '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}.
This assumes that T has both countType and subType structures.
TODO: replace with trivial pack
Notation "[ 'subCountType' 'of' T ]" := (SubCountable.clone _ _ T%type _)
(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.
End TagCountType.
(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.
End TagCountType.
The remaining Canonicals 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.