Robert Shlyakhtenko (Oct 06 2025 at 18:05): Robert Shlyakhtenko (Oct 06 2025 at 18:05):I am working towards a formal proof that every automorphism of the real numbers is trivial. The proof relies on the fact that all automorphisms of the rationals are trivial, that automorphisms of R must preserve order, and and that every real number is an equivalence class of Cauchy sequences of rational numbers.
I am stuck on the last part. Given a real number x, I can use the data in HOL-Real to obtain a Cauchy sequence which represents x with the following code snippet:
fix x :: real
obtain seq_x :: "nat ⇒ rat"
where "seq_x = rep_real x ∧ Real.cauchy seq_x"
(* here seq_x is a Cauchy sequence of rats *)
by (metis Domainp_pcr_real Quotient_real Quotient_rel_rep real.domain_eq)
However, I would like to obtain not just any Cauchy sequence representing x, but also impose some restrictions on the sequence. In particular, I need to obtain an increasing Cauchy sequence representing x and a decreasing Cauchy sequence doing the same.
I haven't found anything in HOL-Real that would enable me to do this, and just running sledgehammer doesn't give a proof. I'm wondering if there is another library that would have basic facts like this about Cauchy sequences. If not, is there a particularly easy way to set up a proof of this in Isabelle?
Thanks!
Manuel Eberl (Oct 07 2025 at 18:47):I would really not recommend using Cauchy sequences for this, especially not pulling apart the definition of real numbers in Isabelle to get to them.
In any complete vector space, "Cauchy sequence" is the same as "convergent sequence", so I'd just work with a convergent increasing sequence.
Manuel Eberl (Oct 07 2025 at 18:47):It's kind of considered bad style to look under the hood of the definitions of the real numbers. One should rather use their derived properties.
Manuel Eberl (Oct 07 2025 at 19:15):One lemma from the standard library that is pretty close to what you want is approx_from_above_dense_linorder:
lemma approx_from_above_dense_linorder:
fixes x::"'a::{dense_linorder, linorder_topology, first_countable_topology}"
assumes "x < y"
shows "∃u. (∀n. u n > x) ∧ (u ⇢ x)"
However, this doesn't give you the strict monotonicity. The most straightforward way to get this without using a more general topological argument that I'm too lazy to come up with is to just use the axiom of dependent choice together with the density of the rationals in the reals.
Basically: given a fixed real number , we can always pick as the -th number in the sequence a number that is less than (to ensure approach from below), greater than everything we picked so far (to ensure monotonicity), and also greater than (to ensure convergence to ).
The variant where we approach from above instead follows by just plugging in to the below version and then flipping the sign of the resulting sequence.
lemma approx_from_below_real_strict_mono:
fixes x :: real
obtains f where "strict_mono f" "⋀n. of_rat (f n) < x" "(λn. of_rat (f n)) ⇢ x"
proof -
have "∃f. ∀n. (of_rat (f n) < x ∧ of_rat (f n) > x - 1 / (real n + 1)) ∧ f n < f (Suc n)"
proof (rule dependent_nat_choice)
show "∃y. of_rat y < x ∧ x - 1 / (real 0 + 1) < of_rat y"
using of_rat_dense[of "x - 1" x] by auto
next
show "∃y. (of_rat y < x ∧ of_rat y > x - 1 / (real (Suc n) + 1)) ∧ y > z"
if "of_rat z < x ∧ of_rat z > x - 1 / (real n + 1)" for z n
using of_rat_dense[of "max (of_rat z) (x - 1 / (real (Suc n) + 1))" x] that
by (auto simp: of_rat_less)
qed
then obtain f where f: "⋀n. of_rat (f n) ∈ {x - 1 / (real n + 1)<..<x} ∧ f n < f (Suc n)"
by auto
show ?thesis
proof
show "strict_mono f"
using f by (simp add: strict_mono_Suc_iff)
next
show "(λn. of_rat (f n)) ⇢ x"
proof (rule tendsto_sandwich)
have "of_rat (f n) ≤ x" for n
using f[of n] by auto
thus "eventually (λn. of_rat (f n) ≤ x) at_top"
by (auto intro!: always_eventually)
next
have "of_rat (f n) ≥ x - 1 / (real n + 1)" for n
using f[of n] by auto
thus "eventually (λn. of_rat (f n) ≥ x - 1 / (real n + 1)) at_top"
by (auto intro!: always_eventually)
next
have "(λn. x - 1 / (real n + 1)) ⇢ x - 0"
by (intro tendsto_intros) (use LIMSEQ_inverse_real_of_nat in ‹auto simp: field_simps›)
thus "(λn. x - 1 / (real n + 1)) ⇢ x"
by simp
qed auto
qed (use f in auto)
qed
lemma approx_from_above_real_strict_mono:
fixes x :: real
obtains f where "strict_antimono_on UNIV f" "⋀n. of_rat (f n) > x" "(λn. of_rat (f n)) ⇢ x"
proof -
obtain g where g: "strict_mono g" "⋀n. of_rat (g n) < -x" "(λn. of_rat (g n)) ⇢ -x"
using approx_from_below_real_strict_mono[of "-x"] by blast
show ?thesis
proof
show "strict_antimono_on UNIV (λn. -g n)"
using g(1) by (auto simp: monotone_def)
next
show "of_rat (-g n) > x" for n
using g(2)[of n] by (simp add: of_rat_minus)
next
have "(λn. -real_of_rat (g n)) ⇢ -(-x)"
by (intro tendsto_intros g(3))
thus "(λn. real_of_rat (-g n)) ⇢ x"
by (simp add: of_rat_minus)
qed
qed
If you have any questions about the proof, feel free to ask!
Manuel Eberl (Oct 07 2025 at 19:20):Oh and just in case you really are interested in Cauchy sequences, there is the lemma Cauchy_convergent_iff which says that for any complete real vector space (in particular for the real numbers themselves), Cauchy convergence is equivalent to normal convergence. Where "normal" convergence is just "has some limit", and since the above lemmas show that the limit is , it would be easy to show that they are Cauchy sequences.
Manuel Eberl (Oct 07 2025 at 19:22):All this Real.cauchy stuff you dug up is just some internal leftovers from the construction of the reals. It is not intended to be used by an "end user" such as you. The standard concept is Cauchy. The reason why these two are different is probably because Cauchy depends on the real numbers, so you need to bootstrap them somehow. But once you have them, you might as well forget about all the material used for bootstrapping.
Robert Shlyakhtenko (Oct 08 2025 at 18:27):Thanks a lot! This was really helpful. I was able to prove what I needed, and it's a good lesson for me to avoid looking too deep into the internal definitions.
Last updated: Oct 12 2025 at 20:20 UTC