Why is this simple proof with real numbers not proven by auto (or even sledgehammer)

What am I doing wrong/ forgetting that this can't be automatically proven by isabelle:

lemma "sqrt 5 = (1 + sqrt 5) / 2 - (1 - sqrt 5) / 2"
  apply auto
  sorry

This is what I actually want to prove:

fun fib :: "nat ⇒ nat" where
  "fib (Suc 0) = Suc 0" 
| "fib (Suc (Suc 0)) = Suc 0"
| "fib (Suc n)  = (fib (n - 1)) + (fib (n - 2))"

lemma "(n::nat) > 0 ⟹ fib n = (1 / sqrt 5) * (
      (((1 + sqrt 5) / 2)^n) - 
      (((1 - sqrt 5) / 2)^n)
      )"
proof(induction n)
  case 0
  then show ?case 
    by auto
next
  case (Suc n)
  then show ?case 
  proof(induction n)
    case 0
    then show ?case 
      apply(auto)
      sorry          
  next
    case (Suc n)
    then show ?case 
      apply auto
      sorry
  qed
qed

Solution

Sledgehammer usually isn't good at doing heavy arithmetic rewriting, which is required here. Proof methods that use the simplifier, like auto and simp, are good at this. But you have to give them the right rules.

There are a number of theorem collections for this:

algebra_simps, which normalises a term w.r.t. associativity, commutativity, and distributivity (essentially sorting everything in ascending order and multiplying out)
field_simps, which additionally cross-multiplies fractions. But caution: the denominator must be provably non-zero. If the simplifier cannot show that, it will not cross-multiply. If the denominator is a product of several factors, it may multiply out the product first and then the denominator is so ugly that it cannot show non-zeroness anymore.
divide_simps is like field_simps except that it does not use distributivity, and it always cross-multiplies by introducing a case distinction for the case that the denominator is zero. (In Isabelle/HOL, x / 0 = 0 holds by definition.)

Another rule you will need here is power2_eq_square to rewrite the square into a multiplication. Then you get:

lemma "sqrt 5 = (1 + sqrt 5) / 2 - ((1 - sqrt 5) / 2)^2"
apply (auto simp: field_simps power2_eq_square)

proof (prove)
goal (1 subgoal):
 1. False

So something is not quite right here. As NieDzejkob pointed out in the comment, the left-hand side should be sqrt 5 - 1. With that, the proof goes through.

By the way, in case you're not aware, Fibonacci numbers are in the Isabelle/HOL standard library: https://isabelle.in.tum.de/library/HOL/HOL-Number_Theory/Fib.html