Library mathcomp.analysis.altreals.discrete
(* --------------------------------------------------------------------
Copyright (c) - 2015--2016 - IMDEA Software Institute
Copyright (c) - 2015--2018 - Inria
Copyright (c) - 2016--2018 - Polytechnique *)
Copyright (c) - 2015--2016 - IMDEA Software Institute
Copyright (c) - 2015--2018 - Inria
Copyright (c) - 2016--2018 - Polytechnique *)
Set Implicit Arguments.
Import GRing.Theory Num.Theory.
Local Open Scope ring_scope.
Local Open Scope real_scope.
Section ProofIrrelevantChoice.
Context {T : choiceType}.
Lemma existsTP (P : T → Prop) : { x : T | P x } + (∀ x, ¬ P x).
End ProofIrrelevantChoice.
Import GRing.Theory Num.Theory.
Local Open Scope ring_scope.
Local Open Scope real_scope.
Section ProofIrrelevantChoice.
Context {T : choiceType}.
Lemma existsTP (P : T → Prop) : { x : T | P x } + (∀ x, ¬ P x).
End ProofIrrelevantChoice.
Section PredSubtype.
Section Def.
Variable T : Type.
Variable E : pred T.
Record pred_sub : Type :=
PSubSub { rsval : T; rsvalP : rsval \in E }.
Coercion rsval : pred_sub >-> T.
Canonical pred_sub_subType := Eval hnf in [subType for rsval].
End Def.
Definition pred_sub_eqMixin (T : eqType) (E : pred T) :=
Eval hnf in [eqMixin of pred_sub E by <:].
Canonical pred_sub_eqType (T : eqType) (E : pred T) :=
Eval hnf in EqType (@pred_sub T E) (pred_sub_eqMixin E).
Definition pred_sub_choiceMixin (T : choiceType) (E : pred T) :=
Eval hnf in [choiceMixin of pred_sub E by <:].
Canonical pred_sub_choiceType (T : choiceType) (E : pred T) :=
Eval hnf in ChoiceType (@pred_sub T E) (pred_sub_choiceMixin E).
Definition pred_sub_countMixin (T : countType) (E : pred T) :=
Eval hnf in [countMixin of pred_sub E by <:].
Canonical pred_sub_countType (T : countType) (E : pred T) :=
Eval hnf in CountType (@pred_sub T E) (pred_sub_countMixin E).
End PredSubtype.
Notation "[ 'psub' E ]" := (@pred_sub _ E)
(format "[ 'psub' E ]").
Section Def.
Variable T : Type.
Variable E : pred T.
Record pred_sub : Type :=
PSubSub { rsval : T; rsvalP : rsval \in E }.
Coercion rsval : pred_sub >-> T.
Canonical pred_sub_subType := Eval hnf in [subType for rsval].
End Def.
Definition pred_sub_eqMixin (T : eqType) (E : pred T) :=
Eval hnf in [eqMixin of pred_sub E by <:].
Canonical pred_sub_eqType (T : eqType) (E : pred T) :=
Eval hnf in EqType (@pred_sub T E) (pred_sub_eqMixin E).
Definition pred_sub_choiceMixin (T : choiceType) (E : pred T) :=
Eval hnf in [choiceMixin of pred_sub E by <:].
Canonical pred_sub_choiceType (T : choiceType) (E : pred T) :=
Eval hnf in ChoiceType (@pred_sub T E) (pred_sub_choiceMixin E).
Definition pred_sub_countMixin (T : countType) (E : pred T) :=
Eval hnf in [countMixin of pred_sub E by <:].
Canonical pred_sub_countType (T : countType) (E : pred T) :=
Eval hnf in CountType (@pred_sub T E) (pred_sub_countMixin E).
End PredSubtype.
Notation "[ 'psub' E ]" := (@pred_sub _ E)
(format "[ 'psub' E ]").
Section PIncl.
Variables (T : Type) (E F : pred T) (le : {subset E ≤ F}).
Definition pincl (x : [psub E]) : [psub F] :=
PSubSub (le (valP x)).
End PIncl.
Variables (T : Type) (E F : pred T) (le : {subset E ≤ F}).
Definition pincl (x : [psub E]) : [psub F] :=
PSubSub (le (valP x)).
End PIncl.
Section Countable.
Variable (T : Type) (E : pred T).
CoInductive countable : Type :=
Countable
(rpickle : [psub E] → nat)
(runpickle : nat → option [psub E])
of pcancel rpickle runpickle.
Definition rpickle (c : countable) :=
let: Countable p _ _ := c in p.
Definition runpickle (c : countable) :=
let: Countable _ p _ := c in p.
Lemma rpickleK c: pcancel (rpickle c) (runpickle c).
End Countable.
Variable (T : Type) (E : pred T).
CoInductive countable : Type :=
Countable
(rpickle : [psub E] → nat)
(runpickle : nat → option [psub E])
of pcancel rpickle runpickle.
Definition rpickle (c : countable) :=
let: Countable p _ _ := c in p.
Definition runpickle (c : countable) :=
let: Countable _ p _ := c in p.
Lemma rpickleK c: pcancel (rpickle c) (runpickle c).
End Countable.
Section CountableTheory.
Lemma countable_countable (T : countType) (E : pred T) : countable E.
Section CanCountable.
Variables (T : Type) (U : countType) (E : pred T).
Variables (f : [psub E] → U) (g : U → [psub E]).
Lemma can_countable : cancel f g → countable E.
End CanCountable.
Section CountType.
Variables (T : eqType) (E : pred T) (c : countable E).
Definition countable_countMixin := CountMixin (rpickleK c).
Definition countable_choiceMixin := CountChoiceMixin countable_countMixin.
Definition countable_choiceType :=
ChoiceType [psub E] countable_choiceMixin.
Definition countable_countType :=
CountType countable_choiceType countable_countMixin.
End CountType.
End CountableTheory.
Notation "[ 'countable' 'of' c ]" := (countable_countType c)
(format "[ 'countable' 'of' c ]").
Lemma countable_countable (T : countType) (E : pred T) : countable E.
Section CanCountable.
Variables (T : Type) (U : countType) (E : pred T).
Variables (f : [psub E] → U) (g : U → [psub E]).
Lemma can_countable : cancel f g → countable E.
End CanCountable.
Section CountType.
Variables (T : eqType) (E : pred T) (c : countable E).
Definition countable_countMixin := CountMixin (rpickleK c).
Definition countable_choiceMixin := CountChoiceMixin countable_countMixin.
Definition countable_choiceType :=
ChoiceType [psub E] countable_choiceMixin.
Definition countable_countType :=
CountType countable_choiceType countable_countMixin.
End CountType.
End CountableTheory.
Notation "[ 'countable' 'of' c ]" := (countable_countType c)
(format "[ 'countable' 'of' c ]").
Section Finite.
Variables (T : eqType).
CoInductive finite (E : pred T) : Type :=
| Finite s of uniq s & {subset E ≤ s}.
End Finite.
Variables (T : eqType).
CoInductive finite (E : pred T) : Type :=
| Finite s of uniq s & {subset E ≤ s}.
End Finite.
Section FiniteTheory.
Context {T : choiceType}.
Lemma finiteP (E : pred T) : (∃ s : seq T, {subset E ≤ s}) → finite E.
Lemma finiteNP (E : pred T): (∀ s : seq T, ¬ {subset E ≤ s}) →
∀ n, ∃ s : seq T, [/\ size s = n, uniq s & {subset s ≤ E}].
End FiniteTheory.
Context {T : choiceType}.
Lemma finiteP (E : pred T) : (∃ s : seq T, {subset E ≤ s}) → finite E.
Lemma finiteNP (E : pred T): (∀ s : seq T, ¬ {subset E ≤ s}) →
∀ n, ∃ s : seq T, [/\ size s = n, uniq s & {subset s ≤ E}].
End FiniteTheory.
Section FiniteCountable.
Variables (T : eqType) (E : pred T).
Lemma finite_countable : finite E → countable E.
End FiniteCountable.
Variables (T : eqType) (E : pred T).
Lemma finite_countable : finite E → countable E.
End FiniteCountable.
Section CountSub.
Variables (T : eqType) (E F : pred T).
Lemma countable_sub: {subset E ≤ F} → countable F → countable E.
End CountSub.
Variables (T : eqType) (E F : pred T).
Lemma countable_sub: {subset E ≤ F} → countable F → countable E.
End CountSub.