1
$\begingroup$

There is a theorem which says that there exists two irrationals $x, y$ such that $x^y$ is rational.

An interesting proof in classical logic is the following:

Consider $u = \sqrt{2}^{\sqrt{2}}$.
If $u$ is rational then we use $(x,y) = (\sqrt{2},\sqrt{2})$.
Otherwise, we notice that $u^\sqrt{2} = 2$ and use $(x,y) = (u,\sqrt{2})$.

I'd like to implement that proof in Lean (3) (the irrationality of $\sqrt{2}$ is already proven in mathlib).

I managed to write a signature of my theorem (execute):

import data.real.irrational
import analysis.special_functions.pow.real

open classical

theorem classical_logic_existence : ∃ x y : ℝ, irrational x ∧ irrational y ∧ ¬ (irrational (x.rpow y)) :=
sorry

My questions are:

  • How can I use x^y instead of (x.rpow y)? (just replacing it produces an error)
  • How would I implement my proof in Lean? I have no idea how to write the case disjunction and so on...
$\endgroup$
11
  • $\begingroup$ First of all I strongly suggest you to move to Lean4 (for this kind of question the answer is essentially the same, and Lean3 is end of life). The ^ is just notation introduced somewhere, try to import a less basic file and you should get it. Concerning the real question, have you read TPIL or any other basic reference? $\endgroup$
    – Ricky
    Sep 24, 2023 at 10:57
  • $\begingroup$ @Ricky the default online interpreter on Lean's website is running on Lean 3. Do they also provide one on Lean 4? $\endgroup$
    – Weier
    Sep 24, 2023 at 11:27
  • $\begingroup$ Here $\endgroup$
    – Trebor
    Sep 24, 2023 at 11:58
  • $\begingroup$ A fine exercise in Lean, but a poor demonstration of excluded middle: $(\sqrt{2})^{\log_2 9} = \sqrt{2^{\log_2 9}} = \sqrt{9} = 3$. $\endgroup$ Sep 24, 2023 at 13:14
  • 1
    $\begingroup$ Just use pow_mul and pow_two, (both backwards), then simp can probably do it. I don't see why simp should do it automatically, it's easy, but there is no reason to have pow_two as a simp lemma. $\endgroup$
    – Ricky
    Sep 24, 2023 at 18:29

1 Answer 1

1
$\begingroup$

I eventually managed to write a proof (execute here).

What I was looking for was essentially the tactic by_cases for cases disjunction.

It is also longer than I expected because I couldn't fully automate proving things like ((sqrt 2)^(sqrt 2))^(sqrt 2) = 2 or ¬(irrational 2).

Note that, as pointed out in a comment, this proof is in Lean 3 and it is preferable to use Lean 4 as of today.

import data.real.irrational
import data.rat.sqrt
import analysis.special_functions.pow.real

open real

lemma simple_lemma: ((sqrt 2)^(sqrt 2))^(sqrt 2) = 2 :=
begin
  rw <-rpow_mul,
  rw <-pow_two,
  by simp,
  simp [sqrt_nonneg],
end

theorem existence_theorem:
  ∃ x y : ℝ, (irrational x) ∧ (irrational y) ∧ ¬(irrational (x^y)) :=
begin
  -- Technicality: we need to prove that 2 (as a real) is not irrational
  have not_irrat_2 : ¬(irrational 2),
  {
    convert rat.not_irrational 2,
    norm_cast,
  },
  by_cases h : irrational ((sqrt 2)^(sqrt 2)),
  -- h : irrational (sqrt 2 ^ sqrt 2)
  {
    existsi [(sqrt 2)^(sqrt 2), sqrt 2],
    simp [h, simple_lemma, irrational_sqrt_two, not_irrat_2],
  },
  -- h : ¬irrational (sqrt 2 ^ sqrt 2)
  {
    existsi [sqrt 2, sqrt 2],
    simp [h, irrational_sqrt_two],
  },
end
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.