Module mathcomp.experimental_reals.discrete
From Corelib Require Setoid.
From HB Require Import structures.
From mathcomp Require Import boot order algebra.
From mathcomp.classical Require Import boolp.
From mathcomp Require Import xfinmap reals.
Unset SsrOldRewriteGoalsOrder.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import GRing.Theory Num.Theory.
Local Open Scope ring_scope.
Local Open Scope real_scope.
Section ProofIrrelevantChoice.
Context { : choiceType}.
Lemma
existsTPUsed by
Source code
( : T -> Prop) : { : T | P x } + (forall , ~ P x).- mathcomp.experimental_reals.realsum
Source code
Proof.
End ProofIrrelevantChoice.
Section PredSubtype.
Section Def.
Variable : Type.
Variable : pred T.
Record
pred_subSource code
: Type :=PSubSub {
rsvalSource code
:> T; rsvalPSource code
: rsval \in E }..
instanceSource code
DefinitionSource code
[isSubSource code
for rsval].End Def.
.
instanceSource code
DefinitionSource code
( eqTypeSource code
) (E : pred T) :=[Equality of pred_sub E by <:].
.
instanceSource code
DefinitionSource code
( choiceTypeSource code
) (E : pred T) :=[Choice of pred_sub E by <:].
.
instanceSource code
DefinitionSource code
( countTypeSource code
) (E : pred T) :=[Countable of pred_sub E by <:].
End PredSubtype.
Notation
"[ 'psub' E ]"Source code
:= (@pred_sub _ E)(format "[ 'psub' E ]").
Section PIncl.
Variables ( : Type) ( : pred T) ( : {subset E <= F}).
Definition
pincl
Source code
( : [psub E]) : [psub F] :=Source code
PSubSub (le (valP x)).
End PIncl.
Section Countable.
Variable ( : Type) ( : pred T).
Variant
countableUsed by
Source code
: Type :=- mathcomp.experimental_reals.realsum
Source code
CountableSource code
(
rpickleSource code
: [psub E] -> nat)(
runpickleSource code
: nat -> option [psub E])of pcancel rpickle runpickle.
Definition
rpickle
Source code
( : countable) :=Source code
let: Countable p _ _ := c in p.
Definition
runpickle
Source code
( : countable) :=pincl : forall [T : Type] [E F : pred T], {subset E <= F} -> [psub E] -> [psub F] pincl is not universe polymorphic Arguments pincl [T]%_type_scope [E F] le x pincl is transparent Expands to: Constant mathcomp.experimental_reals.discrete.pincl Declared in library mathcomp.experimental_reals.discrete, line 66, characters 11-16
Source code
let: Countable _ p _ := c in p.
Lemma
rpickleKSource code
: pcancel (rpickle c) (runpickle c).Proof.
by case: c. Qed.
Section CountableTheory.
Lemma
countable_countableSource code
( : countType) ( : pred T) : countable E.Section CanCountable.
Variables ( : Type) ( : countType) ( : pred T).
Variables ( : [psub E] -> U) ( : U -> [psub E]).
Lemma
can_countableSource code
: cancel f g -> countable E.Proof.
Section CountType.
Variables ( : eqType) ( : pred T) ( : countable E).
Definition
countable_countMixin
Source code
:= Countable.copy [psub E]rpickle : forall [T : Type] [E : pred T], countable (T:=T) E -> [psub E] -> nat rpickle is not universe polymorphic Arguments rpickle [T]%_type_scope [E] c _ rpickle is transparent Expands to: Constant mathcomp.experimental_reals.discrete.rpickle Declared in library mathcomp.experimental_reals.discrete, line 80, characters 11-18
Source code
(pcan_type (rpickleK c)).
Definition
countable_choiceMixin
Source code
:= Choice.copy [psub E]runpickle : forall [T : Type] [E : pred T], countable (T:=T) E -> nat -> option [psub E] runpickle is not universe polymorphic Arguments runpickle [T]%_type_scope [E] c _%_nat_scope runpickle is transparent Expands to: Constant mathcomp.experimental_reals.discrete.runpickle Declared in library mathcomp.experimental_reals.discrete, line 83, characters 11-20
Source code
(pcan_type (rpickleK c)).
End CountType.
End CountableTheory.
Section Finite.
Variables ( : eqType).
CoInductive
finiteSource code
( : pred T) : Type :=|
FiniteSource code
of uniq s & {subset E <= s}.End Finite.
Section FiniteTheory.
Context { : choiceType}.
Lemma
finitePUsed by
Source code
( : pred T) : (exists : seq T, {subset E <= s}) -> finite E.- mathcomp.experimental_reals.realsum
Source code
Proof.
case/cid=> s sEs; exists (undup s); first by rewrite undup_uniq.
by move=> x; rewrite mem_undup; exact: sEs.
Qed.
by move=> x; rewrite mem_undup; exact: sEs.
Qed.
Lemma
finiteNPUsed by
Source code
( : pred T): (forall : seq T, ~ {subset E <= s}) ->- mathcomp.experimental_reals.realsum
Source code
forall , exists : seq T, [/\ size s = n, uniq s & {subset s <= E}].
Proof.
move=> finN; elim=> [|n [s] [<- uq_s sE]]; first by exists [::].
have [x sxN xE]: exists2 , x \notin s & x \in E.
apply: contra_notP (finN (filter (mem E) s)) => /forall2NP finE x Ex.
move/or_asboolP: (finE x).
by rewrite !asbool_neg !asboolb negbK Ex mem_filter orbF [(mem E) x]Ex.
exists (x :: s) => /=; rewrite sxN; split=> // y.
by rewrite in_cons => /orP[/eqP->//|/sE].
Qed.
have [x sxN xE]: exists2 , x \notin s & x \in E.
apply: contra_notP (finN (filter (mem E) s)) => /forall2NP finE x Ex.
move/or_asboolP: (finE x).
by rewrite !asbool_neg !asboolb negbK Ex mem_filter orbF [(mem E) x]Ex.
exists (x :: s) => /=; rewrite sxN; split=> // y.
by rewrite in_cons => /orP[/eqP->//|/sE].
Qed.
End FiniteTheory.
Section FiniteCountable.
Variables ( : eqType) ( : pred T).
Lemma
finite_countableUsed by
Source code
: finite E -> countable E.- mathcomp.experimental_reals.realsum
Source code
Proof.
case=> s uqs Es; pose t := pmap (fun => (insub x : option [psub E])) s.
pose f := index x t; pose g := nth None [seq Some x | <- t] i.
apply (@Countable _ E f g) => x; rewrite {}/f {}/g /=.
have x_in_t: x \in t; first case: x => x h.
by rewrite {}/t mem_pmap_sub /= Es.
by rewrite (nth_map x) ?index_mem ?nth_index.
Qed.
pose f := index x t; pose g := nth None [seq Some x | <- t] i.
apply (@Countable _ E f g) => x; rewrite {}/f {}/g /=.
have x_in_t: x \in t; first case: x => x h.
by rewrite {}/t mem_pmap_sub /= Es.
by rewrite (nth_map x) ?index_mem ?nth_index.
Qed.
Section CountSub.
Variables ( : eqType) ( : pred T).
Lemma
countable_subUsed by
Source code
: {subset E <= F} -> countable F -> countable E.- mathcomp.experimental_reals.realsum
Source code
Proof.
Section CountableUnion.
Variables ( : eqType) ( : nat -> pred T).
Hypothesis : forall , countable (E i).
Lemma
cunion_countableUsed by
Source code
: countable [pred | `[< exists , x \in E i >]].- mathcomp.experimental_reals.realsum
Source code
Proof.
pose Ci : countType := HB.pack [psub (E i)] (countable_countMixin (cE i)).
pose S := { : nat & Ci i }; set F := [pred | _].
have H: forall ( : [psub F]), exists : nat, val x \in E i.
by case=> x /= /asboolP[i] Eix; exists i.
have G: forall ( : S), val (tagged x) \in F.
by case=> i [x /= Eix]; apply/asboolP; exists i.
pose f ( : [psub F]) : S := Tagged (fun => [psub E i])
(PSubSub (xchooseP (H x))).
pose g ( : S) := PSubSub (G x).
by have /can_countable: cancel f g by case=> x hx; apply/val_inj.
Qed.
pose S := { : nat & Ci i }; set F := [pred | _].
have H: forall ( : [psub F]), exists : nat, val x \in E i.
by case=> x /= /asboolP[i] Eix; exists i.
have G: forall ( : S), val (tagged x) \in F.
by case=> i [x /= Eix]; apply/asboolP; exists i.
pose f ( : [psub F]) : S := Tagged (fun => [psub E i])
(PSubSub (xchooseP (H x))).
pose g ( : S) := PSubSub (G x).
by have /can_countable: cancel f g by case=> x hx; apply/val_inj.
Qed.