Library mathcomp.ssreflect.choice
- -
-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
- Distributed under the terms of CeCILL-B. *)
- -
-
-
-- Distributed under the terms of CeCILL-B. *)
- -
-
- 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.
- -
-
-
--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).
- -
-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.
-
-
--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).
- -
-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.
- -
- -
-
-
--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.
- -
-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.
- -
-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}.
- -
-Structure type := Pack {sort; _ : class_of sort}.
-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.
-Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of xT).
- -
-Definition pack m :=
- fun b bT & phant_id (Equality.class bT) b ⇒ Pack (@Class T b m).
- -
-
-
--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}.
- -
-Structure type := Pack {sort; _ : class_of sort}.
-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.
-Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of xT).
- -
-Definition pack m :=
- fun b bT & phant_id (Equality.class bT) b ⇒ Pack (@Class T b m).
- -
-
- Inheritance
-
-
-Definition eqType := @Equality.Pack cT xclass.
- -
-End ClassDef.
- -
-Module Import Exports.
-Coercion base : class_of >-> Equality.class_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 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.
- -
-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 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 }.
- -
-Structure type : Type := Pack {sort : Type; _ : class_of sort}.
-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.
-Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of xT).
- -
-Definition pack m :=
- fun bT b & phant_id (Choice.class bT) b ⇒ Pack (@Class T b m).
- -
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
- -
-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).
- -
-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.
- -
- -
-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.
- -
-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 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 }.
- -
-Structure type : Type := Pack {sort : Type; _ : class_of sort}.
-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.
-Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of xT).
- -
-Definition pack m :=
- fun bT b & phant_id (Choice.class bT) b ⇒ Pack (@Class T b m).
- -
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
- -
-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).
- -
-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.
- -
- -
-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 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 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.
-