Stream: Beginner Questions

Topic: How exactly am I supposed to think of LEAST?

Ant S. (Aug 24 2026 at 10:47):

TL;DR: When should I be using/"unfolding" LEAST and how can I use it to prove a supremum property using Real.thy

So I thought it'd be a good idea to try to learn some (rigorous!) analysis by formalizing it in HOL, using Abbott's Understanding Analysis as a place to start

definition rsup where
  "rsup (X :: real set) z ≡  (∀x ∈ X. x ≤ z) ∧ (∀w. ((∀x ∈ X. x ≤ w) ⟶ z ≤ w))"

theorem lubp:
  fixes X :: "real set"
  assumes "bdd_above X"
  shows "∃z. rsup X z"
proof (unfold rsup_def)
oops

The reason I defined rsup was because I wanted to define a least-upper-bound property as it would usually be defined in a textbook, not using the LEAST operator (more on this below). If I were to use the latter, it would be something on the lines of ∃z. z = Sup X where Sup ?X = (LEAST z. ∀x∈?X. x ≤ z). I doubt that this is the right way of saying "a least upper bound exists". If so, what should I be using?

From what I understand from reading the manual, LEAST is guaranteed to exist, but if there is more than one, we can't "unfold" LEAST, if that makes sense.
From logics.pdf (in the documentation):

so Least is always meaningful, but may yield nothing useful in case there is not a unique least element satisfying P.

I presume then I must show the uniqueness of the least upper bound (which is trivial given antisymmetry and that the reals satisfy the poset typeclass if I recall)

How exactly am I supposed to use (and when should I use) LEAST? via auto, I can easily prove bdd_above (X :: real set) ==> \exists z. z = Sup X. It's a bit too easy, to be honest, so I'm probably not proving the right statement. Suprisingly, the converse doesn't hold? I'm able to nitpick \exists z. z = Sup X ==> bdd_above (X :: real set). Why is this the case?

If I want to use the least-upper-bound property as I would doing pen-and-paper real analysis, is rsup the right way to go?

Yong Kiam (Aug 25 2026 at 02:40):

others may be able to give a deeper explanation but here I think are the main points I can see:

1) every type is inhabited in Isabelle, and with choice, you can pick an element from any type.

2) as you suspect, the statements you've proved are "trivial" in that \exists z. z = Sup X is trivially witnessed by z = Sup X.

3) Sup X is always "meaningful" in the sense that Sup is a total function and will always return some element of the type, in this case the reals.

However, it may not be "useful" in that it may not have the expected properties you are looking for in the supremum (in case the supremum doesn't exist).

Ant S. (Aug 25 2026 at 04:41):

Yeah, that confirms my suspicions. How do I encode the notion that a supremum may not exist

Ant S. (Aug 25 2026 at 20:54):

Follow up question: how would I write out a statement such as "this set of reals has no supremum" in a logic of total functions?

Like, how would I say that "Sup X" returns no useful value?

Ant S. (Aug 25 2026 at 20:55):

if Sup is assumed to be total

Asterix Gallier (Aug 25 2026 at 21:39):

You can't use Sup to write statements about the existence of suprema, because Sup is total, like any function in Isabelle.
Your function rsup is perfect for this. With it, you can write ¬ rsup UNIV z to express that the set of reals (UNIV) has no supremum.

Like, how would I say that "Sup X" returns no useful value?

For this, you need to formalize what you mean by "useful". Presumably, you mean that Sup X actually fulfils the properties of a supremum. You can express this via rsup X (Sup X), because rsup already captures the properties of a supremum.
You could go on to prove rsup X (Sup X) ⟷ bdd_above X. You could also prove the uniqueness of the supremum as rsup X z ⟹ rsup X w ⟹ z = w.

Ant S. (Aug 26 2026 at 06:44):

Asterix Gallier said:

Your function rsup is perfect for this. With it, you can write ¬ rsup UNIV z to express that the set of reals (UNIV) has no supremum.

oh wait so UNIV is a set that contains an entire domain of discourse?

abbreviation UNIV :: "'a set"
  where "UNIV ≡ top"

where I presume it is ordered by set inclusion.

Also, since people have been formalizing analysis in isabelle for at least 25 years, how come this idea of "there is no supremum" isn't there? Surely someone's done something on these lines.

Asterix Gallier (Aug 26 2026 at 09:22):

Yes, UNIV :: 'a set contains all values of type 'a.
If you're interested, look up the theorem complete_real in Real.thy. It contains most of the work for proving that a supremum of a bounded-above set of reals always exists. Below it, there is an instantiation real :: linear_continuum, which uses this result to prove more properties. In particular, linear_continuum is a subclass of conditionally_complete_lattice, which contains the supremum properties you'd expect for the reals.
As for "there is no supremum", there is a (technically) stronger statement which has been proven: The set of reals isn't bounded. In Real.thy, real is proven to be a linordered_field (another type class), which in Fields.thy is shown to be a subclass of unbounded_dense_linorder, which in turn is a subclass of no_top, which assumes no_top.gt_ex: "∃y. x < y".
If you want to find these things, you can use Ctrl+F and select "Search in: Directory" with the HOL directory of your Isabelle installation. Then, you can type something like instantiation real :: to see what type classes real is part of. Additionally, you can use the "Query" panel at the bottom to semantically search for theorems (you can use underscores as placeholders, i.e. you could search for "∃_. _ < _" and get some results. For me, Query doesn't work when I'm looking at files outside of my project, for some reason.

Ant S. (Aug 26 2026 at 12:30):

Thanks! :sweat_smile: I must confess I did look at linear_continuumbut I think i missed unbounded_dense_linorder, that one's on me

Ant S. (Aug 27 2026 at 18:49):

I was skimming Kaliczyk and Urban's Quotients Revisites for Isabelle/HOL

And I wanted to ask if that's an implementation that's currently being used.

If so, I want to break down the implementation details here:

(* This seems clear to me *)
 definition vanishes :: "(nat ⇒ rat) ⇒ bool"
  where "vanishes X ⟷ (∀r>0. ∃k. ∀n≥k. ¦X n¦ < r)"

(* This is standard for anyone who has seen a Cauchy sequence before *)
definition cauchy :: "(nat ⇒ rat) ⇒ bool"
  where "cauchy X ⟷ (∀r>0. ∃k. ∀m≥k. ∀n≥k. ¦X m - X n¦ < r)"


(* this is a bit new to me, I can convince myself this is true but I'd like to know where this comes from *)
definition realrel :: "(nat ⇒ rat) ⇒ (nat ⇒ rat) ⇒ bool"
  where "realrel = (λX Y. cauchy X ∧ cauchy Y ∧ vanishes (λn. X n - Y n))"


quotient_type real = "nat ⇒ rat" / partial: realrel
  morphisms rep_real Real
  by (rule part_equivp_realrel)

It seems like there's a lot to break down here.
Why is realrel marked as partial?
What are the morphisms rep_real and Real? Are those the abstraction and representation papers mentioned in Kaliczyk's paper? One takes you to the abstract representation, and the other the concrete.

Why do we need rule part_equivp_realrel

Part_equivp is documented in Relations.thy as a "John Harrison style characterization"

Ok I found this paper that defines what a partial equivalence relation is
https://link.springer.com/content/pdf/10.1007/BFb0028401.pdf

Is the equivalence partial because we, in some sense, "don't care" that about sequences that are not Cauchy? Or is it that we cannot define equivalence for such sequences.

Apparently this is what's called a "higher-order" quotient? Is it higher order because we're quotienting over functions (the functions themselves are first order) and not, e.g. sum or product types?

Ant S. (Aug 27 2026 at 18:49):

Let me know if I should move this to #General

Ant S. (Aug 28 2026 at 15:23):

Or better yet, should I send an email to the mailing list

Last updated: Sep 08 2026 at 08:41 UTC