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 ( : T -> Prop) : { : T | P x } + (forall , ~ P x).

Proof.

case: (boolP `[<exists : 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 : Type.
Variable : pred T.

Record : Type :=
  PSubSub { :> T; : rsval \in E }.

. for rsval].
End Def.

. () (E : pred T) :=
  [Equality of pred_sub E by <:].

. () (E : pred T) :=
  [Choice of pred_sub E by <:].

. () (E : pred T) :=
  [Countable of pred_sub E by <:].
End PredSubtype.

Notation := (@pred_sub _ E)
  (format "[ 'psub' E ]").

Section PIncl.
Variables ( : Type) ( : pred T) ( : {subset E <= F}).

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

Section Countable.
Variable ( : Type) ( : pred T).

Variant : Type :=

    ( : [psub E] -> nat)
    ( : nat -> option [psub E])
    of pcancel rpickle runpickle.

Definition ( : countable) :=
  let: Countable p _ _ := c in p.

Definition ( : countable) :=
  let: Countable _ p _ := c in p.

Lemma : pcancel (rpickle c) (runpickle c).

Proof.

by case: c. Qed.

End Countable.

Section CountableTheory.
Lemma ( : countType) ( : pred T) : countable E.

Proof.

by exists choice.pickle choice.unpickle; apply/choice.pickleK. Qed.

Section CanCountable.
Variables ( : Type) ( : countType) ( : pred T).
Variables ( : [psub E] -> U) ( : U -> [psub E]).

Lemma : cancel f g -> countable E.

Proof.

pose p := choice.pickle \o f; pose u := 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 ( : eqType) ( : pred T) ( : countable E).

Definition := Countable.copy [psub E]
(pcan_type (rpickleK c)).
Definition := Choice.copy [psub E]
(pcan_type (rpickleK c)).
End CountType.
End CountableTheory.

Section Finite.
Variables ( : eqType).

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

Section FiniteTheory.
Context { : choiceType}.

Lemma ( : pred T) : (exists : 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 ( : pred T): (forall : seq T, ~ {subset E <= s}) ->
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.

End FiniteTheory.

Section FiniteCountable.
Variables ( : eqType) ( : pred T).

Lemma : finite E -> countable E.

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.

End FiniteCountable.

Section CountSub.
Variables ( : eqType) ( : pred T).

Lemma : {subset E <= F} -> countable F -> countable E.

Proof.

move=> le_EF [f g fgK]; pose f' ( : [psub E]) := f (pincl le_EF x).
pose g' := 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 ( : eqType) ( : nat -> pred T).

Hypothesis : forall , countable (E i).

Lemma : countable [pred | `[< exists , x \in E i >]].

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.

End CountableUnion.

Files

Module mathcomp.experimental_reals.discrete