feat(data/real/ereal): add `ereal` := [-oo,oo] #1703

kbuzzard · 2019-11-17T18:49:00Z

TO CONTRIBUTORS:

Make sure you have:

reviewed and applied the coding style: coding, naming
reviewed and applied the documentation requirements
for tactics:
- added or adapted documentation in tactics.md
- write an example of use of the new feature in tactics.lean
make sure definitions and lemmas are put in the right files
make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

src/data/real/ereal.lean

PatrickMassot · 2019-11-17T20:21:05Z

src/data/real/ereal.lean

+/-- A set of ereals has a Sup in ereal -/
+theorem Sup_exists (X : set ereal) : has_Sup X :=
+  let Xoc : set (with_top ℝ) := λ x, X (↑x : with_bot _) in
+dite (Xoc = ∅) (λ h, ⟨⊥, ⟨


Is there a reason to use dite instead of its sugared version?

I needed a dependent if/then/else. What's the sugared way to do this?

if h : Xoc = ∅ then _ else _

Done in ac2ac59

src/data/real/ereal.lean

fpvandoorn · 2019-11-18T21:03:39Z

I did some cleanup in this PR. I hope that is fine.

kbuzzard · 2019-12-13T08:50:39Z

Note to self: https://isabelle.in.tum.de/dist/library/HOL/HOL-Library/Extended_Real.html

kbuzzard · 2019-12-22T00:15:29Z

OK so the situation with this PR was that I needed ereal and the proof that it was a complete lattice, which was initially a more substantial piece of work. It was then suggested that I prove a more general theorem about adding top and bot to a conditionally complete lattice gives a complete lattice, and this all happened in #1725 . The result is that this PR is essentially basic facts about unary neg on ereal and nothing else. I don't really know if this is worthy for mathlib any more so if people just want to close it then this is fine, but if people think it's better as a stub then here it is. I am unlikely to go any further with this now; in my opinion things like addition are unnatural on ereal, we have addition on the reals anyway.

sgouezel · 2019-12-22T09:47:45Z

src/data/real/ereal.lean

+
+/-- ereal : The type $$[-\infty,+\infty]$$ or `[-∞, ∞]` -/
+@[derive [linear_order, lattice.order_bot, lattice.order_top,
+  lattice.has_Sup, lattice.complete_lattice]]


Why do you derive has_Sup but not has_Inf?

sgouezel · 2019-12-22T09:48:03Z

src/data/real/ereal.lean

+
+-/
+
+/-- ereal : The type $$[-\infty,+\infty]$$ or `[-∞, ∞]` -/


Suggested change

/-- ereal : The type $$[-\infty,+\infty]$$ or `[-∞, ∞]` -/

/-- ereal : The type `[-∞, ∞]` -/

sgouezel · 2019-12-22T09:48:37Z

src/order/bounded_lattice.lean

@@ -26,6 +26,8 @@ class has_bot (α : Type u) := (bot : α)
 notation `⊤` := has_top.top _
 notation `⊥` := has_bot.bot _

+attribute [pattern] lattice.has_bot.bot lattice.has_top.top


What does this do?

It allows us to write ⊤ and ⊥ in the equation compiler, like this:

protected def neg : ereal → ereal | ⊥ := ⊤ | ⊤ := ⊥ | (x : ℝ) := (-x : ℝ)

sgouezel · 2019-12-22T09:51:06Z

Don't with_top and with_bot constructions automatically extend addition and/or multiplication? If so, this means that your ereal already has some of these operations. It might be worth checking which operations are already defined, and mentioning it in the docstring. Other than this, having a stub like this one is definitely better than nothing.

kbuzzard · 2020-01-03T13:49:20Z

(sorry, I will get to this at some point, I have a bunch of references to write before I leave for the US this weekend)

kbuzzard · 2020-01-05T14:58:17Z

OK so so the answer to the with_top and with_bot question of @sgouezel is that ereal will inherit an addition if I @derive it on line 38, but because apply_instance does not unfold ereal the addition is not inherited otherwise. So there are two choices: either I leave things as they are, or I derive addition and then prove some simp and refl lemmas about it (n.b. bot + top = top, for what it's worth).

I guess that given that a mathematician would say that addition is partially defined on ereal, I should derive addition and prove the simp lemmas, right? The only possible issue I can see with this is if someone wants bot + top to be bot for some reason (which it probably would have been if I'd defined ereal to be with_bot (with_top real).

Going further with this, I could define sub and mul and div (and even pow??), just giving them junk values at places where I would consider them undefined. What should I do here? Sorry this has all taken so long; I will finish up this PR within the next day or two now Christmas is over.

sgouezel · 2020-01-08T20:00:47Z

I would say that you can just derive addition, but don't bother proving its properties: if someone needs them, then he will come back to it. Maybe add a comment in the file docstring though?

kbuzzard · 2020-01-21T23:52:55Z

OK I derived addition. I am still a bit conflicted by all this; I guess my instinct is to leave things as they are until someone actually needs some arithmetic on ereal. I only need inf and sup, and I have these now.

…1703) * feat(data/real/ereal): add `ereal` := [-oo,oo] * some updates * some cleanup in ereal * move pattern attribute * works * more docstring * don't understand why this file was broken * more tidyup * deducing complete lattice from type class inference * another neg theorem * adding some module doc * tinkering * deriving addition Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com> Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

feat(data/real/ereal): add ereal := [-oo,oo]

8110667

ChrisHughes24 reviewed Nov 17, 2019

View reviewed changes

src/data/real/ereal.lean Outdated Show resolved Hide resolved

PatrickMassot reviewed Nov 17, 2019

View reviewed changes

kbuzzard and others added 5 commits November 17, 2019 20:37

Merge branch 'master' into ereal

2ed666c

some updates

da8baf4

Merge remote-tracking branch 'blessed/lean-3.4.2' into ereal

9c04f51

some cleanup in ereal

ac2ac59

move pattern attribute

8f6448e

fpvandoorn added the awaiting-author A reviewer has asked the author a question or requested changes label Nov 19, 2019

works

f96b4d0

kbuzzard mentioned this pull request Nov 22, 2019

feat(order/conditionally_complete_lattice): with_top (with_bot L) ins… #1725

Merged

3 tasks

robertylewis assigned fpvandoorn Dec 2, 2019

kbuzzard added 2 commits December 4, 2019 16:06

Merge branch 'master' into ereal

49dfcd1

fixing conflicts

1ffc605

kbuzzard added 7 commits December 20, 2019 19:02

Merge branch 'master' into ereal

c564539

more docstring

4234ab6

don't understand why this file was broken

25d9078

more tidyup

164c7ba

deducing complete lattice from type class inference

32813dd

another neg theorem

a7377df

adding some module doc

f65a547

sgouezel reviewed Dec 22, 2019

View reviewed changes

sgouezel mentioned this pull request Jan 1, 2020

feat(analysis/calculus/mean_value): add generalized "fencing" inequality #1838

Merged

4 tasks

tinkering

884b54c

deriving addition

37da1dd

sgouezel added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jan 25, 2020

sgouezel approved these changes Jan 25, 2020

View reviewed changes

ChrisHughes24 and others added 2 commits January 25, 2020 20:49

Merge remote-tracking branch 'origin/master' into HEAD

fa4f49a

Merge branch 'master' into ereal

b77db94

mergify bot merged commit d3e5621 into master Jan 25, 2020

mergify bot deleted the ereal branch January 25, 2020 23:46

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(data/real/ereal): add `ereal` := [-oo,oo] #1703

feat(data/real/ereal): add `ereal` := [-oo,oo] #1703

kbuzzard commented Nov 17, 2019

PatrickMassot Nov 17, 2019

kbuzzard Nov 17, 2019

ChrisHughes24 Nov 17, 2019

fpvandoorn Nov 18, 2019

fpvandoorn commented Nov 18, 2019

kbuzzard commented Dec 13, 2019

kbuzzard commented Dec 22, 2019

sgouezel Dec 22, 2019

sgouezel Dec 22, 2019

sgouezel Dec 22, 2019

fpvandoorn Jan 3, 2020

sgouezel commented Dec 22, 2019

kbuzzard commented Jan 3, 2020

kbuzzard commented Jan 5, 2020

sgouezel commented Jan 8, 2020

kbuzzard commented Jan 21, 2020


		-/

		/-- ereal : The type $$[-\infty,+\infty]$$ or `[-∞, ∞]` -/

	/-- ereal : The type $$[-\infty,+\infty]$$ or `[-∞, ∞]` -/
	/-- ereal : The type `[-∞, ∞]` -/

feat(data/real/ereal): add ereal := [-oo,oo] #1703

feat(data/real/ereal): add ereal := [-oo,oo] #1703

Conversation

kbuzzard commented Nov 17, 2019

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

fpvandoorn commented Nov 18, 2019

kbuzzard commented Dec 13, 2019

kbuzzard commented Dec 22, 2019

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

sgouezel commented Dec 22, 2019

kbuzzard commented Jan 3, 2020

kbuzzard commented Jan 5, 2020

sgouezel commented Jan 8, 2020

kbuzzard commented Jan 21, 2020

feat(data/real/ereal): add `ereal` := [-oo,oo] #1703

feat(data/real/ereal): add `ereal` := [-oo,oo] #1703