Stuck on a proof requiring coercion

Stream: new members

[Kevin Cheung]

I am stuck on the following proof.

import Mathlib.Data.Real.Sqrt

def A : ℕ → ℤ
  | 0 => 2
  | 1 => 2
  | n + 2 => 2 * A (n + 1) + A n

theorem An_closed (n : ℕ) :
  A n = (1 + Real.sqrt 2)^n + (1 - Real.sqrt 2)^n := by
  match n with
  | 0 => rw [A]
         rw [pow_zero, pow_zero]
         exact one_add_one_eq_two.symm
  | 1 => rw [A]
         rw [pow_one, pow_one]
         simp
         exact one_add_one_eq_two.symm
  | k + 2 =>
    have IH1 := An_closed k
    have IH2 := An_closed (k+1)
    calc A (k+2) = 2 * A (k+1) + A k := by rw [A]
     _ = (1+Real.sqrt 2)^(k+1)+(1-Real.sqrt 2)^(k+1)
         +(1+Real.sqrt 2)^k + (1-Real.sqrt 2)^k := sorry

It complains about

invalid 'calc' step, left-hand-side is
  ↑?m.16940 : ℝ
previous right-hand-side is
  2 * A (k + 1) + A k : ℤ

I guess I need some sort of coercion here but I am at lost as to what to do. Hints greatly appreciated.

[Richard Copley]

import Mathlib.Data.Real.Sqrt

def A : ℕ → ℤ
  | 0 => 2
  | 1 => 2
  | n + 2 => 2 * A (n + 1) + A n

theorem An_closed (n : ℕ) :
  A n = (1 + Real.sqrt 2)^n + (1 - Real.sqrt 2)^n := by
  match n with
  | 0 => rw [A]
         rw [pow_zero, pow_zero]
         exact one_add_one_eq_two.symm
  | 1 => rw [A]
         rw [pow_one, pow_one]
         simp
         exact one_add_one_eq_two.symm
  | k + 2 =>
    have IH1 := An_closed k
    have IH2 := An_closed (k+1)
    calc (A (k + 2) : ℝ)
     _ = ↑((2 * A (k + 1) + A k : ℤ)) := rfl
     _ = 2 * ↑(A (k + 1)) + ↑(A k) := by norm_cast
     _ = 2 * ((1 + Real.sqrt 2) ^ (k + 1) + (1 - Real.sqrt 2) ^ (k + 1)) +
             ((1 + Real.sqrt 2) ^ k + (1 - Real.sqrt 2) ^ k) := by rw [IH1, IH2]
     _ = _ := sorry

The line you proved with "by rw [A]" is true by definition, and it can be proved from rfl, or even omitted.

The left hand side of the equality in the theorem statement is "↑(A k)" or "((A k : ℤ) : ℝ)", so in order for an expression to be rewritten using that equality, the expression must have a subexpression that matches "↑(A k)".

[Kevin Cheung]

Oh. So the theorem has the coercion but the first line of calc doesn't. Is that what Lean is complaining about?

[Ruben Van de Velde]

Basically, yes. It ends up thinking that you're writing a calc about natural numbers and then use it to prove a goal about reals

[Kevin Cheung]

Thank you all. I managed to complete the proof as follows. But I find it quite ugly, especially with using simp a couple of times. Is the use of simp reasonable (for a beginner) here? Critiques welcome.

theorem An_closed (n : ℕ) :
  A n = (1 + Real.sqrt 2)^n + (1 - Real.sqrt 2)^n := by
  match n with
  | 0 => rw [A]
         rw [pow_zero, pow_zero]
         exact one_add_one_eq_two.symm
  | 1 => rw [A]
         rw [pow_one, pow_one]
         simp
         exact one_add_one_eq_two.symm
  | k + 2 =>
    have IH1 := An_closed k
    have IH2 := An_closed (k+1)
    calc
      --↑ (A (k+2)) = ↑ (2 * A (k+1) + A k)  := by
      --  rw [A]
      _ = 2*((1+Real.sqrt 2)^(k+1)+(1-Real.sqrt 2)^(k+1))
          + ((1+Real.sqrt 2)^k+(1-Real.sqrt 2)^k) := by
        rw [A]
        simp [IH1, IH2]
      _ = ((1+Real.sqrt 2)+(1 - Real.sqrt 2))
          * ((1+Real.sqrt 2)^(k+1)+(1-Real.sqrt 2)^(k+1))
          + ((1+Real.sqrt 2)^k+(1-Real.sqrt 2)^k) := by
          simp [one_add_one_eq_two]
      _ = (1+Real.sqrt 2)^(k+2) + (1-Real.sqrt 2)^(k+2) := by
          simp [one_add_one_eq_two]

[Ruben Van de Velde]

That looks fine, in my opinion

[Kevin Cheung]

Thank you. Surprisingly, after copying this proof to another project, the last simp couldn't solve all goals. It looks like this proof is not portable. Is this even possible?

[Kevin Buzzard]

Do you have different imports? Does the output of simp? change?

[Kevin Cheung]

Interesting. I went back to the old copy and indeed the proof didn't work. Looks like I haven't completed the proof yet.

[Kevin Cheung]

I must have missed some warnings.

[Kevin Buzzard]

It's a good idea to end proofs with done; sometimes the error if you're not done can occur a long way from the cursor (e.g. on the by 25 lines up), but with done the error is on done.

[Kevin Cheung]

Thanks for the tip.