Skip to content

Adapting to new Order.max #218

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
CohenCyril merged 1 commit into from
Jun 11, 2020
Merged

Adapting to new Order.max #218

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .github/workflows/nix.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,5 +16,5 @@ jobs:
name: math-comp
# Authentication token for Cachix, needed only for private cache access
signingKey: '${{ secrets.CACHIX_SIGNING_KEY }}'
- run: nix-build https://github.com/math-comp/math-comp-nix/archive/master.tar.gz --arg config '{mathcomp = "1.11.0+beta1"; mathcomp-analysis = "${{ steps.branch-short-name.outputs.branch }}";}' --argstr package mathcomp-analysis
- run: nix-build https://github.com/math-comp/math-comp-nix/archive/master.tar.gz --arg config '{mathcomp = "mathcomp-1.11.0"; mathcomp-analysis = "${{ steps.branch-short-name.outputs.branch }}";}' --argstr package mathcomp-analysis
# - run: export CACHIX_SIGNING_KEY=${{ secrets.CACHIX_SIGNING_KEY }} cachix push math-comp result
4 changes: 2 additions & 2 deletions .travis.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,8 +21,8 @@ install:
- docker pull ${DOCKERIMAGE}
- docker tag ${DOCKERIMAGE} ci:current
- docker run --env=OPAMYES --init -id --name=CI -v ${TRAVIS_BUILD_DIR}:/home/coq/${CONTRIB} -w /home/coq/${CONTRIB} ci:current
- docker exec CI /bin/bash --login -c "cd ..; curl -LO https://github.com/math-comp/finmap/archive/1.5.0.tar.gz; tar -xvzf 1.5.0.tar.gz; cd finmap-1.5.0/; opam pin add -y -n coq-mathcomp-finmap.1.5.0 .; opam install coq-mathcomp-finmap.1.5.0; cd /home/coq/${CONTRIB}"
- docker exec CI /bin/bash --login -c "opam pin add -y -n coq-mathcomp-${CONTRIB} ."
- docker exec CI /bin/bash --login -c "opam update -y"
- docker exec CI /bin/bash --login -c "opam pin add -n -y -k path coq-mathcomp-${CONTRIB}.dev ."
- docker exec CI /bin/bash --login -c "opam install --deps-only coq-mathcomp-${CONTRIB}"

script:
Expand Down
4 changes: 2 additions & 2 deletions config.nix
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
{
coq = "8.10";
mathcomp = "1.11.0+beta1";
mathcomp-real-closed = "1.1.0";
mathcomp = "mathcomp-1.11.0";
mathcomp-real-closed = "1.1.1";
}
8 changes: 4 additions & 4 deletions theories/Rbar.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -525,8 +525,8 @@ move=> [:wlog]; case: a b => [a||] [b||] //= ltax ltxb.
- move: a b ltax ltxb; abstract: wlog. (*BUG*)
move=> {a b} a b ltxa ltxb.
have m_gt0 : Num.min ((x - a) / 2) ((b - x) / 2) > 0.
by rewrite ltxI !divr_gt0 ?subr_gt0.
exists (PosNum m_gt0) => y //=; rewrite ltxI !ltr_distl.
by rewrite lt_minr !divr_gt0 ?subr_gt0.
exists (PosNum m_gt0) => y //=; rewrite lt_minr !ltr_distl.
move=> /andP[/andP[ay _] /andP[_ yb]].
rewrite (lt_trans _ ay) ?(lt_trans yb) //=.
by rewrite -subr_gt0 opprD addrA {1}[b - x]splitr addrK divr_gt0 ?subr_gt0.
Expand All @@ -539,10 +539,10 @@ move=> [:wlog]; case: a b => [a||] [b||] //= ltax ltxb.
Qed.

Lemma Rbar_min_comm (x y : Rbar) : Rbar_min x y = Rbar_min y x.
Proof. by case: x y => [x||] [y||] //=; rewrite meetC. Qed.
Proof. by case: x y => [x||] [y||] //=; rewrite minC. Qed.

Lemma Rbar_min_r (x y : Rbar) : Rbar_le (Rbar_min x y) y.
Proof. by case: x y => [x||] [y||] //=; rewrite leIx lexx orbT. Qed.
Proof. by case: x y => [x||] [y||] //=; rewrite le_minl lexx orbT. Qed.

Lemma Rbar_min_l (x y : Rbar) : Rbar_le (Rbar_min x y) x.
Proof. by rewrite Rbar_min_comm Rbar_min_r. Qed.
Expand Down
26 changes: 13 additions & 13 deletions theories/Rstruct.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -482,15 +482,15 @@ Proof. by elim: n => [ | n In] //=; rewrite exprS In RmultE. Qed.

Lemma RmaxE x y : Rmax x y = Num.max x y.
Proof.
case: (lerP x y) => H; first by rewrite join_r // Rmax_right //; apply: RlebP.
by rewrite join_l ?ltW // Rmax_left //; apply/RlebP; move/ltW : H.
case: (lerP x y) => H; first by rewrite Rmax_right //; apply: RlebP.
by rewrite ?ltW // Rmax_left //; apply/RlebP; move/ltW : H.
Qed.

(* useful? *)
Lemma RminE x y : Rmin x y = Num.min x y.
Proof.
case: (lerP x y) => H; first by rewrite meet_l // Rmin_left //; apply: RlebP.
by rewrite meet_r ?ltW // Rmin_right //; apply/RlebP; move/ltW : H.
case: (lerP x y) => H; first by rewrite Rmin_left //; apply: RlebP.
by rewrite ?ltW // Rmin_right //; apply/RlebP; move/ltW : H.
Qed.

Section bigmaxr.
Expand All @@ -503,23 +503,23 @@ Lemma bigmaxr_nil (x0 : R) : bigmaxr x0 [::] = x0.
Proof. by rewrite /bigmaxr /= big_nil. Qed.

Lemma bigmaxr_un (x0 x : R) : bigmaxr x0 [:: x] = x.
Proof. by rewrite /bigmaxr /= big_cons big_nil joinxx. Qed.
Proof. by rewrite /bigmaxr /= big_cons big_nil maxxx. Qed.

(* previous definition *)
Lemma bigmaxrE (r : R) s : bigmaxr r s = foldr Num.max (head r s) (behead s).
Proof.
rewrite (_ : bigmaxr _ _ = if s isn't h :: t then r else \big[Num.max/h]_(i <- s) i).
case: s => // ? t; rewrite big_cons /bigmaxr.
by elim: t => //= [|? ? <-]; [rewrite big_nil joinxx | rewrite big_cons joinCA].
by elim: t => //= [|? ? <-]; [rewrite big_nil maxxx | rewrite big_cons maxCA].
by case: s => //=; rewrite /bigmaxr big_nil.
Qed.

Lemma bigrmax_dflt (x y : R) s : Num.max x (\big[Num.max/x]_(j <- y :: s) j) =
Num.max x (\big[Num.max/y]_(i <- y :: s) i).
Proof.
elim: s => /= [|h t IH] in x y *.
by rewrite !big_cons !big_nil joinxx joinCA joinxx joinC.
by rewrite big_cons joinCA IH joinCA [in RHS]big_cons IH.
by rewrite !big_cons !big_nil maxxx maxCA maxxx maxC.
by rewrite big_cons maxCA IH maxCA [in RHS]big_cons IH.
Qed.

Lemma bigmaxr_cons (x0 x y : R) lr :
Expand All @@ -530,9 +530,9 @@ Lemma bigmaxr_ler (x0 : R) s i :
(i < size s)%N -> (nth x0 s i) <= (bigmaxr x0 s).
Proof.
rewrite /bigmaxr; elim: s i => // h t IH [_|i] /=.
by rewrite big_cons /= lexU lexx.
by rewrite big_cons /= le_maxr lexx.
rewrite ltnS => ti; case: t => [|h' t] // in IH ti *.
by rewrite big_cons bigrmax_dflt lexU orbC IH.
by rewrite big_cons bigrmax_dflt le_maxr orbC IH.
Qed.

(* Compatibilité avec l'addition *)
Expand All @@ -547,10 +547,10 @@ Qed.
Lemma bigmaxr_mem (x0 : R) lr : (0 < size lr)%N -> bigmaxr x0 lr \in lr.
Proof.
rewrite /bigmaxr; case: lr => // h t _.
elim: t => //= [|h' t IH] in h *; first by rewrite big_cons big_nil inE joinxx.
elim: t => //= [|h' t IH] in h *; first by rewrite big_cons big_nil inE maxxx.
rewrite big_cons bigrmax_dflt inE eq_le; case: lerP => /=.
- by rewrite lexU lexx.
- by rewrite ltxU ltxx => ?; rewrite join_r ?IH // ltW.
- by rewrite le_maxr lexx.
- by rewrite lt_maxr ltxx => ?; rewrite max_r ?IH // ltW.
Qed.

(* TODO: bigmaxr_morph? *)
Expand Down
15 changes: 6 additions & 9 deletions theories/altreals/distr.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -79,18 +79,15 @@ Definition clamp (x : R) :=
Num.max (Num.min x 1) 0.

Lemma ge0_clamp x : 0 <= clamp x.
Proof. by rewrite lexU lexx orbT. Qed.
Proof. by rewrite le_maxr lexx orbT. Qed.

Lemma le1_clamp x : clamp x <= 1.
Proof. by rewrite leUx leIx lexx ler01 orbT. Qed.
Proof. by rewrite le_maxl le_minl lexx ler01 orbT. Qed.

Definition cp01_clamp := (ge0_clamp, le1_clamp).

Lemma clamp_in01 x : 0 <= x <= 1 -> clamp x = x.
Proof.
case/andP=> ge0_x le1_x; rewrite /clamp (elimT join_idPr).
by rewrite lexI ge0_x ler01. by rewrite (elimT meet_idPl).
Qed.
Proof. by case/andP=> ge0_x le1_x; rewrite /clamp min_l ?max_l. Qed.

Lemma clamp_id x : clamp (clamp x) = clamp x.
Proof. by rewrite clamp_in01 // !cp01_clamp. Qed.
Expand Down Expand Up @@ -1144,14 +1141,14 @@ Lemma has_esp_bounded f mu :
(exists M, forall x, `|f x| < M) -> \E?_[mu] f.
Proof. (* TO BE REMOVED *)
case=> M ltM; rewrite /has_esp; apply/summable_seqP.
exists (Num.max M 0); first by rewrite lexU lexx orbT.
exists (Num.max M 0); first by rewrite le_maxr lexx orbT.
move=> J uqJ; apply/(@le_trans _ _ (\sum_(j <- J) M * mu j)).
apply/ler_sum=> j _; rewrite normrM [X in _*X]ger0_norm //.
by apply/ler_wpmul2r=> //; apply/ltW.
case: (ltrP M 0) => [lt0_M|ge0_M].
rewrite (elimT join_idPl) ?(ltW lt0_M) // -mulr_sumr.
rewrite ?(ltW lt0_M) // -mulr_sumr.
by rewrite nmulr_rle0 //; apply/sumr_ge0.
by rewrite (elimT join_idPr) // -mulr_sumr ler_pimulr // -pr_mem ?le1_pr.
by rewrite -mulr_sumr ler_pimulr // -pr_mem ?le1_pr.
Qed.

Lemma bounded_has_exp mu F :
Expand Down
10 changes: 5 additions & 5 deletions theories/altreals/realseq.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -215,20 +215,20 @@ Lemma ncvg_nbounded u x : ncvg u x%:E -> nbounded u.
Proof. (* FIXME: factor out `sup` of a finite set *)
case/(_ (B x 1)) => K cu; pose S := [seq `|u n| | n <- iota 0 K].
pose M : R := sup [set x : R | x \in S]; pose e := Num.max (`|x| + 1) (M + 1).
apply/asboolP/nboundedP; exists e => [|n]; first by rewrite ltxU ltr_paddl.
apply/asboolP/nboundedP; exists e => [|n]; first by rewrite lt_maxr ltr_paddl.
case: (ltnP n K); last first.
move/cu; rewrite inE eclamp_id ?ltr01 // => ltunBx1.
rewrite ltxU; apply/orP; left; rewrite -[u n](addrK x) addrAC.
rewrite lt_maxr; apply/orP; left; rewrite -[u n](addrK x) addrAC.
by apply/(le_lt_trans (ler_norm_add _ _)); rewrite addrC ltr_add2l.
move=> lt_nK; have: `|u n| \in S; first by apply/map_f; rewrite mem_iota.
move=> un_S; rewrite ltxU; apply/orP; right.
move=> un_S; rewrite lt_maxr; apply/orP; right.
case E: {+}K lt_nK => [|k] // lt_nSk; apply/ltr_spaddr; first apply/ltr01.
suff : has_sup (fun x : R => x \in S) by move/sup_upper_bound/ubP => ->.
split; first by exists `|u 0%N|; rewrite /S E inE eqxx.
elim: {+}S => [|v s [ux /ubP hux]]; first by exists 0; apply/ubP.
exists (Num.max v ux); apply/ubP=> y; rewrite inE => /orP[/eqP->|].
by rewrite lexU lexx.
by move/hux=> le_yux; rewrite lexU le_yux orbT.
by rewrite le_maxr lexx.
by move/hux=> le_yux; rewrite le_maxr le_yux orbT.
Qed.

Lemma nboundedC c : nbounded c%:S.
Expand Down
22 changes: 11 additions & 11 deletions theories/altreals/realsum.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,10 +54,10 @@ Lemma eq_fneg f g : f =1 g -> fneg f =1 fneg g.
Proof. by move=> eq_fg x; rewrite /fneg eq_fg. Qed.

Lemma fpos0 x : fpos (fun _ : T => 0) x = 0 :> R.
Proof. by rewrite /fpos joinxx normr0. Qed.
Proof. by rewrite /fpos maxxx normr0. Qed.

Lemma fneg0 x : fneg (fun _ : T => 0) x = 0 :> R.
Proof. by rewrite /fneg meetxx normr0. Qed.
Proof. by rewrite /fneg minxx normr0. Qed.

Lemma fnegN f : fneg (\- f) =1 fpos f.
Proof. by move=> x; rewrite /fpos /fneg -{1}oppr0 -oppr_max normrN. Qed.
Expand Down Expand Up @@ -92,10 +92,10 @@ by apply/eq_fpos=> y; rewrite mulrN.
Qed.

Lemma fneg_ge0 f x : (forall x, 0 <= f x) -> fneg f x = 0.
Proof. by move=> ?; rewrite /fneg (elimT meet_idPl) ?normr0. Qed.
Proof. by move=> ?; rewrite /fneg min_l ?normr0. Qed.

Lemma fpos_ge0 f x : (forall x, 0 <= f x ) -> fpos f x = f x.
Proof. by move=> ?; rewrite /fpos (elimT join_idPl) ?ger0_norm. Qed.
Proof. by move=> ?; rewrite /fpos max_r ?ger0_norm. Qed.

Lemma ge0_fpos f x : 0 <= fpos f x.
Proof. by apply/normr_ge0. Qed.
Expand All @@ -105,19 +105,19 @@ Proof. by apply/normr_ge0. Qed.

Lemma le_fpos_norm f x : fpos f x <= `|f x|.
Proof.
rewrite /fpos ger0_norm ?(lexU, lexx) //.
by rewrite leUx normr_ge0 ler_norm.
rewrite /fpos ger0_norm ?(le_maxr, lexx) //.
by rewrite le_maxl normr_ge0 ler_norm.
Qed.

Lemma le_fpos f1 f2 : f1 <=1 f2 -> fpos f1 <=1 fpos f2.
Proof.
move=> le_f x; rewrite /fpos !ger0_norm ?lexU ?lexx //.
by rewrite leUx lexx /=; case: ltP => //=; rewrite le_f.
move=> le_f x; rewrite /fpos !ger0_norm ?le_maxr ?lexx //.
by rewrite le_maxl lexx /=; case: ltP => //=; rewrite le_f.
Qed.

Lemma fposBfneg f x : fpos f x - fneg f x = f x.
Proof.
rewrite /fpos /fneg joinC.
rewrite /fpos /fneg maxC.
case: (leP (f x) 0); rewrite normr0 (subr0, sub0r) => ?.
by rewrite ler0_norm ?opprK.
by rewrite gtr0_norm.
Expand Down Expand Up @@ -1177,10 +1177,10 @@ Proof.
move=> eqr domS; rewrite /sum !(psum_finseq eqr).
+ move=> x; rewrite !inE => xPS; apply/domS; rewrite !inE.
move: xPS; rewrite /fpos normr_eq0.
by apply: contra => /eqP ->; rewrite joinxx.
by apply: contra => /eqP ->; rewrite maxxx.
+ move=> x; rewrite !inE => xPS; apply/domS; rewrite !inE.
move: xPS; rewrite /fneg normr_eq0.
by apply: contra => /eqP ->; rewrite meetxx.
by apply: contra => /eqP ->; rewrite minxx.
rewrite -sumrB; apply/eq_bigr=> i _.
by rewrite !ger0_norm ?(ge0_fpos, ge0_fneg) ?fposBfneg.
Qed.
Expand Down
12 changes: 4 additions & 8 deletions theories/derive.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -768,21 +768,17 @@ have -> : (ku^-1 *: u, kv^-1 *: v) =
rewrite mulrC -[_ *: u]scalerA [X in X *: v]mulrC -[_ *: v]scalerA.
by rewrite invf_div.
rewrite normmZ ger0_norm // -mulrA gtr_pmulr // ltr_pdivr_mull // mulr1.
rewrite prod_normE /= (_ : _%:nng = 1%:nng); last first.
by apply/val_inj => /=; rewrite normmZ normrV ?unitfE ?gt_eqF // normr_id mulVf ?gt_eqF.
rewrite (_ : _%:nng = 1%:nng); last first.
by apply/val_inj => /=; rewrite normmZ normrV ?unitfE ?gt_eqF // normr_id mulVf ?gt_eqF.
by rewrite joinxx /= ltr1n.
by rewrite prod_normE/= !normmZ !normfV !normr_id !mulVf ?gt_eqF// maxxx ltr1n.
Qed.

Lemma bilinear_eqo (U V' W' : normedModType R) (f : {bilinear U -> V' -> W'}) :
continuous (fun p => f p.1 p.2) -> (fun p => f p.1 p.2) =o_ (0 : U * V') id.
Proof.
move=> fc; have [_ /posnumP[k] fschwarz] := bilinear_schwarz fc.
apply/eqoP=> _ /posnumP[e]; near=> x; rewrite (le_trans (fschwarz _ _))//.
rewrite ler_pmul ?pmulr_rge0 //; last by rewrite nng_lexU /= lexx orbT.
rewrite ler_pmul ?pmulr_rge0 //; last by rewrite nng_le_maxr /= lexx orbT.
rewrite -ler_pdivl_mull //.
suff : `|x| <= k%:num ^-1 * e%:num by apply: le_trans; rewrite nng_lexU /= lexx.
suff : `|x| <= k%:num ^-1 * e%:num by apply: le_trans; rewrite nng_le_maxr /= lexx.
near: x; rewrite !near_simpl; apply/locally_le_locally_norm.
by exists (k%:num ^-1 * e%:num) => // ? /=; rewrite distrC subr0 => /ltW.
Grab Existential Variables. all: end_near. Qed.
Expand Down Expand Up @@ -846,7 +842,7 @@ Lemma eqo_pair (U V' W' : normedModType R) (F : filter_on U)
(f : U -> V') (g : U -> W') :
(fun t => ([o_F id of f] t, [o_F id of g] t)) =o_F id.
Proof.
apply/eqoP => _/posnumP[e]; near=> x; rewrite nng_leUx /=.
apply/eqoP => _/posnumP[e]; near=> x; rewrite nng_le_maxl /=.
by apply/andP; split; near: x; apply: littleoP.
Grab Existential Variables. all: end_near. Qed.

Expand Down
71 changes: 10 additions & 61 deletions theories/ereal.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -156,6 +156,9 @@ Definition ereal_porderMixin :=
Canonical ereal_porderType :=
POrderType ereal_display {ereal R} ereal_porderMixin.

Lemma leEereal x y : (x <= y)%O = le_ereal x y. Proof. by []. Qed.
Lemma ltEereal x y : (x < y)%O = lt_ereal x y. Proof. by []. Qed.

End ERealOrder.

Notation lee := (@Order.le ereal_display _) (only parsing).
Expand All @@ -179,16 +182,16 @@ Proof. by []. Qed.
Lemma lte_fin (R : numDomainType) (x y : R) : (x%:E < y%:E)%E = (x < y)%O.
Proof. by []. Qed.

Lemma lte_pinfty (R : realDomainType) (x : R) : (x%:E < +oo).
Lemma lte_pinfty (R : realDomainType) (x : R) : x%:E < +oo.
Proof. exact: num_real. Qed.

Lemma lee_pinfty (R : realDomainType) (x : {ereal R}) : (x <= +oo).
Lemma lee_pinfty (R : realDomainType) (x : {ereal R}) : x <= +oo.
Proof. case: x => //= r; exact: num_real. Qed.

Lemma lte_ninfty (R : realDomainType) (x : R) : (-oo < x%:E).
Proof. exact: num_real. Qed.

Lemma lee_ninfty (R : realDomainType) (x : {ereal R}) : (-oo <= x).
Lemma lee_ninfty (R : realDomainType) (x : {ereal R}) : -oo <= x.
Proof. case: x => //= r; exact: num_real. Qed.

Lemma lee_ninfty_eq (R : numDomainType) (x : {ereal R}) : (x <= -oo)%E = (x == -oo%E).
Expand All @@ -201,67 +204,13 @@ Section ERealOrder_realDomainType.
Context {R : realDomainType}.
Implicit Types (x y : {ereal R}).

Definition min_ereal x1 x2 :=
match x1, x2 with
| -oo, _ | _, -oo => -oo
| +oo, x | x, +oo => x

| x1%:E, x2%:E => (Num.Def.minr x1 x2)%:E
end.

Definition max_ereal x1 x2 :=
match x1, x2 with
| -oo, x | x, -oo => x
| +oo, _ | _, +oo => +oo

| x1%:E, x2%:E => (Num.Def.maxr x1 x2)%:E
end.

Lemma min_erealC : commutative min_ereal.
Proof. by case=> [?||][?||] //=; rewrite meetC. Qed.

Lemma max_erealC : commutative max_ereal.
Proof. by case=> [?||][?||] //=; rewrite joinC. Qed.

Lemma min_erealA : associative min_ereal.
Proof. by case=> [?||][?||][?||] //=; rewrite meetA. Qed.

Lemma max_erealA : associative max_ereal.
Proof. by case=> [?||][?||][?||] //=; rewrite joinA. Qed.

Lemma joinKI_ereal y x : min_ereal x (max_ereal x y) = x.
Proof. by case: x y => [?||][?||] //=; rewrite (joinKI, meetxx). Qed.

Lemma meetKU_ereal y x : max_ereal x (min_ereal x y) = x.
Proof. by case: x y => [?||][?||] //=; rewrite (meetKU, joinxx). Qed.

Lemma leEmeet_ereal x y : (x <= y)%E = (min_ereal x y == x).
Proof.
case: x y => [x||][y||] //=; rewrite ?eqxx ?lee_pinfty ?lee_ninfty //.
exact: leEmeet.
Qed.

Lemma meetUl_ereal : left_distributive min_ereal max_ereal.
Lemma le_total_ereal : totalPOrderMixin [porderType of {ereal R}].
Proof.
by case=> [?||][?||][?||] //=; rewrite ?(meetUl, meetUK, meetKUC, joinxx).
by move=> [?||][?||]//=; rewrite (ltEereal, leEereal)/= ?num_real ?le_total.
Qed.

Lemma minE_ereal x y : min_ereal x y = if le_ereal x y then x else y.
Proof. by case: x y => [?||][?||] //=; rewrite ?num_real //; case: leP. Qed.

Lemma maxE_ereal x y : max_ereal x y = if le_ereal y x then x else y.
Proof. by case: x y => [?||][?||] //=; rewrite ?num_real //; case: ltP. Qed.

Lemma le_total_ereal : total (@le_ereal R).
Proof. by case=> [?||][?||] //=; rewrite ?num_real //; exact: le_total. Qed.

Definition ereal_latticeMixin :=
LatticeMixin min_erealC max_erealC min_erealA max_erealA
joinKI_ereal meetKU_ereal leEmeet_ereal.
Canonical ereal_latticeType := LatticeType {ereal R} ereal_latticeMixin.
Definition ereal_distrLatticeMixin := DistrLatticeMixin meetUl_ereal.
Canonical ereal_distrLatticeType :=
DistrLatticeType {ereal R} ereal_distrLatticeMixin.
Canonical ereal_latticeType := LatticeType {ereal R} le_total_ereal.
Canonical ereal_distrLatticeType := DistrLatticeType {ereal R} le_total_ereal.
Canonical ereal_orderType := OrderType {ereal R} le_total_ereal.

End ERealOrder_realDomainType.
Expand Down
Loading