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

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.

Module CodeSeq.

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 jj < 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 xIH_leaf x
| Node n f0
let fix iter_pair f : foldr (fun tprod (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 xIH_leaf x
| Node n f0
let fix iter_conj f : foldr (fun tand (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 finl _ 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)
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 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.
#[deprecated(since="mathcomp 2.0.0", note="Use Choice.copy with can_type or CanHasChoice.")]
Notation CanChoiceMixin := CanHasChoice.
#[deprecated(since="mathcomp 2.0.0", note="Use Choice.copy with pcan_type or PCanHasChoice.")]
Notation PcanChoiceMixin := PCanHasChoice.

#[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.
#[deprecated(since="mathcomp 2.0.0", note="Use [Choice of _ by <:] instead.")]
Notation "[ 'choiceMixin' 'of' T 'by' <: ]" := [Choice of T%type by <:]
(at level 0, format "[ 'choiceMixin' '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 }.

Notation "[ 'isCountable' 'of' T ]" := (Countable.on T%type : Choice_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.

Arguments isCountable.axioms_ T%type_scope.

Section CountableTheory.

Variable T : countType.

Definition pickle_inv n :=
obind (fun x : Tif 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.
#[deprecated(since="mathcomp 2.0.0", note="Use Countable.copy with can_type or CanIsCountable.")]
Notation CanCountMixin := CanIsCountable.
#[deprecated(since="mathcomp 2.0.0", note="Use Countable.copy with pcan_type or PCanIsCountable")]
Notation PcanCountMixin := PCanIsCountable.

Notation "[ 'Countable' 'of' T 'by' <: ]" :=
(Countable.copy T%type (sub_type T%type))
(at level 0, format "[ 'Countable' 'of' T 'by' <: ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use [Countable of _ by <:] instead.")]
Notation "[ 'countMixin' 'of' T 'by' <: ]" := [Countable of T%type by <:]
(at level 0, format "[ 'countMixin' '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.
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 iomap (@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.