Files

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 {TSource code : choiceType}.

Lemma existsTPUsed by
  • mathcomp.experimental_reals.realsum
Source code (PSource code : T -> Prop) : { xSource code : T | P x } + (forall xSource code, ~ P x).
Proof.
case: (boolP `[<exists xSource code : T, P x>]) => [/exists_asboolP | /asboolPn] h.
  by case/cid: h => w Pw; left; exists w; apply/asboolP.
by right=> x Px; apply/h; exists x.
Qed.

End ProofIrrelevantChoice.

Section PredSubtype.
Section Def.
Variable TSource code : Type.
Variable ESource code : pred T.

Record pred_subSource code : Type :=
  PSubSub { rsvalSource code :> T; rsvalPSource code : rsval \in E }.

HBSource code.instanceSource code DefinitionSource code _Source code :=Source code [isSubSource code for rsval].
End Def.

HBSource code.instanceSource code DefinitionSource code _Source code (TSource code :Source code eqTypeSource code) (E : pred T) :=
  [Equality of pred_sub E by <:].

HBSource code.instanceSource code DefinitionSource code _Source code (TSource code :Source code choiceTypeSource code) (E : pred T) :=
  [Choice of pred_sub E by <:].

HBSource code.instanceSource code DefinitionSource code _Source code (TSource code :Source 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 (TSource code : Type) (ESource code FSource code : pred T) (leSource code : {subset E <= F}).

Definition pincl
Source code (xSource code : [psub E]) : [psub F] :=
  PSubSub (le (valP x)).
End PIncl.

Section Countable.
Variable (TSource code : Type) (ESource code : pred T).

Variant countableUsed by
  • mathcomp.experimental_reals.realsum
Source code : Type :=
  CountableSource code
    (rpickleSource code : [psub E] -> nat)
    (runpickleSource code : nat -> option [psub E])
    of pcancel rpickle runpickle.

Definition rpickle
Source code (cSource code : countable) :=
  let: Countable p _ _ := c in p.

Definition runpickle
Source code (cSource code : countable) :=
  let: Countable _ p _ := c in p.

Lemma rpickleKSource code cSource code: pcancel (rpickle c) (runpickle c).
Proof.
by case: c. Qed.
End Countable.

Section CountableTheory.
Lemma countable_countableSource code (TSource code : countType) (ESource code : pred T) : countable E.
Proof.
by exists choice.pickle choice.unpickle; apply/choice.pickleK. Qed.

Section CanCountable.
Variables (TSource code : Type) (USource code : countType) (ESource code : pred T).
Variables (fSource code : [psub E] -> U) (gSource code : U -> [psub E]).

Lemma can_countableSource code : cancel f g -> countable E.
Proof.
pose p := choice.pickle \o f; pose u nSource code := omap g (choice.unpickle n).
move=> can_fg; apply (@Countable _ E p u) => x.
by rewrite {}/u {}/p /= choice.pickleK /= can_fg.
Qed.
End CanCountable.

Section CountType.
Variables (TSource code : eqType) (ESource code : pred T) (cSource code : countable E).

Definition countable_countMixin

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  := Countable.copy [psub E]
  (pcan_type (rpickleK c)).
Definition countable_choiceMixin

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 := Choice.copy [psub E]
  (pcan_type (rpickleK c)).
End CountType.
End CountableTheory.

Section Finite.
Variables (TSource code : eqType).

CoInductive finiteSource code (ESource code : pred T) : Type :=
| FiniteSource code sSource code of uniq s & {subset E <= s}.
End Finite.

Section FiniteTheory.
Context {TSource code : choiceType}.


Lemma finitePUsed by
  • mathcomp.experimental_reals.realsum
Source code (ESource code : pred T) : (exists sSource code : seq T, {subset E <= s}) -> finite E.
Proof.
case/cid=> s sEs; exists (undup s); first by rewrite undup_uniq.
by move=> x; rewrite mem_undup; exact: sEs.
Qed.


Lemma finiteNPUsed by
  • mathcomp.experimental_reals.realsum
Source code (ESource code : pred T): (forall sSource code : seq T, ~ {subset E <= s}) ->
  forall nSource code, exists sSource code : 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 xSource code, 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 (TSource code : eqType) (ESource code : pred T).

Lemma finite_countableUsed by
  • mathcomp.experimental_reals.realsum
Source code : finite E -> countable E.
Proof.
case=> s uqs Es; pose t := pmap (fun xSource code => (insub x : option [psub E])) s.
pose f xSource code := index x t; pose g iSource code := nth None [seq Some x | xSource code <- 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.
End FiniteCountable.

Section CountSub.
Variables (TSource code : eqType) (ESource code FSource code : pred T).

Lemma countable_subUsed by
  • mathcomp.experimental_reals.realsum
Source code: {subset E <= F} -> countable F -> countable E.
Proof.
move=> le_EF [f g fgK]; pose f' (xSource code : [psub E]) := f (pincl le_EF x).
pose g' xSource code := obind (insub (sT := [psub E])) (omap val (g x)).
by exists f' g' => x; rewrite /f' /g' fgK /= valK.
Qed.
End CountSub.

Section CountableUnion.
Variables (TSource code : eqType) (ESource code : nat -> pred T).

Hypothesis cESource code : forall iSource code, countable (E i).

Lemma cunion_countableUsed by
  • mathcomp.experimental_reals.realsum
Source code : countable [pred xSource code | `[< exists iSource code, x \in E i >]].
Proof.
pose Ci iSource code : countType := HB.pack [psub (E i)] (countable_countMixin (cE i)).
pose S := { iSource code : nat & Ci i }; set F := [pred xSource code | _].
have H: forall (xSource code : [psub F]), exists iSource code : nat, val x \in E i.
  by case=> x /= /asboolP[i] Eix; exists i.
have G: forall (xSource code : S), val (tagged x) \in F.
  by case=> i [x /= Eix]; apply/asboolP; exists i.
pose f (xSource code : [psub F]) : S := Tagged (fun iSource code => [psub E i])
  (PSubSub (xchooseP (H x))).
pose g (xSource code : S) := PSubSub (G x).
by have /can_countable: cancel f g by case=> x hx; apply/val_inj.
Qed.
End CountableUnion.
Generated by rocqnavi
Source
Uses
Used By