Skip to content

Commit

Permalink
Merge pull request #299 from math-comp/generalizations_20201209
Browse files Browse the repository at this point in the history
minor generalizations from realType
  • Loading branch information
CohenCyril authored Dec 9, 2020
2 parents 5dbb171 + 2fc3fff commit dfddc69
Show file tree
Hide file tree
Showing 2 changed files with 77 additions and 61 deletions.
8 changes: 5 additions & 3 deletions CHANGELOG_UNRELEASED.md
Original file line number Diff line number Diff line change
Expand Up @@ -68,11 +68,13 @@
+ notation `x > y` defined as `y < x` (only parsing) instead of `gte`
+ definition `mkset`
+ lemma `eq_set`

### Changed

- in `classical_sets.v`:
+ notation `[set x : T | P]` now use definition `mkset`
- in `reals.v`:
+ lemmas generalized from `realType` to `numDomainType`:
`setNK`, `memNE`, `lb_ubN`, `ub_lbN`, `nonemptyN`, `has_lb_ubN `
+ lemmas generalized from `realType` to `realDomainType`:
`has_ubPn`, `has_lbPn`

### Renamed

Expand Down
130 changes: 72 additions & 58 deletions theories/reals.v
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,78 @@ Delimit Scope real_scope with real.
Local Open Scope ring_scope.
Local Open Scope classical_set_scope.

Section subr_image.
Variable R : numDomainType.
Implicit Types E : set R.
Implicit Types x : R.

Lemma setNK : involutive (fun E => -%R @` E).
Proof.
move=> F; rewrite predeqE => y; split => [|Fy].
by case=> z -[u xu <-{z} <-{y}]; rewrite opprK.
by exists (- y); rewrite ?opprK //; exists y.
Qed.

Lemma memNE E x : E x = (-%R @` E) (- x).
Proof.
rewrite propeqE; split => [Ex|[y Ey]]; [by exists x|].
by move/eqP; rewrite eqr_opp => /eqP <-.
Qed.

Lemma lb_ubN E x : lbound E x <-> ubound (-%R @` E) (- x).
Proof.
split=> [/lbP xlbE|/ubP xlbE].
by apply/ubP=> y [z Ez <-{y}]; rewrite ler_oppr opprK; apply xlbE.
by apply/lbP => y Ey; rewrite -(opprK x) ler_oppl; apply xlbE; exists y.
Qed.

Lemma ub_lbN E x : ubound E x <-> lbound (-%R @` E) (- x).
Proof.
split=> [? | /lb_ubN].
by apply/lb_ubN; rewrite opprK setNK.
by rewrite opprK setNK.
Qed.

Lemma nonemptyN E : nonempty (-%R @` E) <-> nonempty E.
Proof.
split=> [[x ENx]|[x Ex]]; exists (- x); last by rewrite -memNE.
by rewrite memNE opprK.
Qed.

Lemma has_lb_ubN E : has_lbound E <-> has_ubound (-%R @` E).
Proof.
by split=> [[x /lb_ubN] | [x /ub_lbN]]; [|rewrite setNK]; exists (- x).
Qed.

End subr_image.

Section has_bound_lemmas.
Variable R : realDomainType.
Implicit Types E : set R.
Implicit Types x : R.

Lemma has_ubPn {E} : ~ has_ubound E <-> (forall x, exists2 y, E y & x < y).
Proof.
split; last first.
move=> h [x] /ubP hle; case/(_ x): h => y /hle.
by rewrite leNgt => /negbTE ->.
move/forallNP => h x; have {h} := h x.
move=> /ubP /existsNP => -[y /not_implyP[Ey /negP]].
by rewrite -ltNge => ltx; exists y.
Qed.

Lemma has_lbPn E : ~ has_lbound E <-> (forall x, exists2 y, E y & y < x).
Proof.
split=> [/has_lb_ubN /has_ubPn NEnub x|Enlb /has_lb_ubN].
have [y ENy ltxy] := NEnub (- x); exists (- y); rewrite 1?ltr_oppl //.
by case: ENy => z Ez <-; rewrite opprK.
apply/has_ubPn => x; have [y Ey ltyx] := Enlb (- x).
exists (- y); last by rewrite ltr_oppr.
by exists y => //; rewrite opprK.
Qed.

End has_bound_lemmas.

(* -------------------------------------------------------------------- *)
Module Real.
Section Mixin.
Expand Down Expand Up @@ -321,16 +393,6 @@ rewrite -(ler_add2r y) -Dz -mulr2n -[X in X<=_]mulr_natl.
by rewrite ler_pmul2l ?ltr0Sn.
Qed.

Lemma has_ubPn {E} : ~ has_ubound E <-> (forall x, exists2 y, E y & x < y).
Proof.
split; last first.
move=> h [x] /ubP hle; case/(_ x): h => y /hle.
by rewrite leNgt => /negbTE ->.
move/forallNP => h x; have {h} := h x.
move=> /ubP /existsNP => -[y /not_implyP[Ey /negP]].
by rewrite -ltNge => ltx; exists y.
Qed.

Lemma has_supPn {E} : E !=set0 ->
~ has_sup E <-> (forall x, exists2 y, E y & x < y).
Proof.
Expand All @@ -348,39 +410,6 @@ Variables (R : realType).
Implicit Types E : set R.
Implicit Types x : R.

Lemma setNK : involutive (fun E : set R => -%R @` E).
Proof.
move=> F; rewrite predeqE => y; split => [|Fy].
by case=> z -[u xu <-{z} <-{y}]; rewrite opprK.
by exists (- y); rewrite ?opprK //; exists y.
Qed.

Lemma memNE E x : E x = (-%R @` E) (- x).
Proof.
rewrite propeqE; split => [Ex|[y Ey]]; [by exists x|].
by move/eqP; rewrite eqr_opp => /eqP <-.
Qed.

Lemma lb_ubN E x : lbound E x <-> ubound (-%R @` E) (- x).
Proof.
split=> [/lbP xlbE|/ubP xlbE].
by apply/ubP=> y [z Ez <-{y}]; rewrite ler_oppr opprK; apply xlbE.
by apply/lbP => y Ey; rewrite -(opprK x) ler_oppl; apply xlbE; exists y.
Qed.

Lemma ub_lbN E x : ubound E x <-> lbound (-%R @` E) (- x).
Proof.
split=> [? | /lb_ubN].
by apply/lb_ubN; rewrite opprK setNK.
by rewrite opprK setNK.
Qed.

Lemma nonemptyN E : nonempty (-%R @` E) <-> nonempty E.
Proof.
split=> [[x ENx]|[x Ex]]; exists (- x); last by rewrite -memNE.
by rewrite memNE opprK.
Qed.

Lemma has_inf_supN E : has_inf E <-> has_sup (-%R @` E).
Proof.
split=> [ [En0 [x /lb_ubN xlbe]] | [NEn0 [x /ub_lbN xubE]] ].
Expand Down Expand Up @@ -408,11 +437,6 @@ move=> ninfE; rewrite -oppr0 -(@sup_out _ (-%R @` E)) => // supNE; apply: ninfE.
exact/has_inf_supN.
Qed.

Lemma has_lb_ubN E : has_lbound E <-> has_ubound (-%R @` E).
Proof.
by split=> [[x /lb_ubN] | [x /ub_lbN]]; [|rewrite setNK]; exists (- x).
Qed.

Lemma inf_lb E : has_lbound E -> (lbound E) (inf E).
Proof. by move/has_lb_ubN/sup_ub/ub_lbN; rewrite setNK. Qed.

Expand All @@ -421,16 +445,6 @@ Proof.
by move=> /(nonemptyN E) En0 /lb_ubN /(sup_le_ub En0); rewrite ler_oppr.
Qed.

Lemma has_lbPn E : ~ has_lbound E <-> (forall x, exists2 y, E y & y < x).
Proof.
split=> [/has_lb_ubN /has_ubPn NEnub x|Enlb /has_lb_ubN].
have [y ENy ltxy] := NEnub (- x); exists (- y); rewrite 1?ltr_oppl //.
by case: ENy => z Ez <-; rewrite opprK.
apply/has_ubPn => x; have [y Ey ltyx] := Enlb (- x).
exists (- y); last by rewrite ltr_oppr.
by exists y => //; rewrite opprK.
Qed.

Lemma has_infPn E : nonempty E ->
~ has_inf E <-> (forall x, exists2 y, E y & y < x).
Proof.
Expand Down

0 comments on commit dfddc69

Please sign in to comment.