applying theorems with mismatched types

Stream: new members

[Kamila Szewczyk]

I wish to prove this:

example (a : ℕ) (b : ℝ) (h : a > 1) : b ^ a / b ^ (a - 1) = b := by
  sorry

However, using the many pow_sub rules fails, as the type of the exponent is N, but the type of the base is R. Can I somehow add a cast around a without modifying the premise? Is there a variant of pow_sub that can deal with these mixed types?

[Kevin Buzzard]

Are you absolutely sure you want to prove things about (a : Nat) (ha : 1 < a)? Can you make do instead with b : Nat and let a be b+2 in your application? Whenever I see a natural subtraction (especially an x-1) my first thought is not to fight it like you're suggesting but to renormalise and remove it.

[Kevin Buzzard]

The way I'd deal with your goal would be precisely to do this at this point in the proof, ie do cases on a, get a contradiction with a=0, and in the a=succ b case now change all the succ b's to b+1's, use lemmas to get b+1-1 back to b, and then go on from there. But the sooner one does this the better.

[Kamila Szewczyk]

Kevin Buzzard said:

Are you absolutely sure you want to prove things about (a : Nat) (ha : 1 < a)? Can you make do instead with b : Nat and let a be b+2 in your application? Whenever I see a natural subtraction (especially an x-1) my first thought is not to fight it like you're suggesting but to renormalise and remove it.

Yes. The original problem comes from a actually being Nat.Prime, while b must be R.

[Kamila Szewczyk]

Thanks to your hint I managed to solve it:

example (a : ℕ) (b : ℝ) (h : a > 1) (h' : b ≠ 0) : b ^ a / b ^ (a - 1) = b := by
  cases a with
  | zero => linarith
  | succ a =>
    rw [Nat.succ_eq_add_one, pow_add, Nat.add_sub_cancel]
    rw [mul_div_right_comm, pow_one]
    rw [div_self]
    rw [one_mul]
    apply pow_ne_zero
    assumption

[Kevin Buzzard]

(sorry I confusingly introduced a second b in my answer, that was supposed to be an independent new variable)

[Kamila Szewczyk]

When it comes to the greater picture though, I am stuck (on the "sorry"). Any help would be very appreciated. I know that this proof can be alternatively conducted in a group-theoretic way, but I do not have an in-depth understanding of it.

-- Prove that fib(p) * 2^(p-1) = sum k=0 to (p-1)/2 of 5^k*C(p,2k+1)
-- Then we prove that this is equal to 5^(p-1)/2 mod p,
-- which is (5/p) mod p (legendre symbol).
-- Then by fermat's little theorem 2^(p-1) = 1 mod p, so we get that
-- fib(p) = (5/p) mod p, which is the desired final result.
-- Easier said than done, though.
example (p : ℕ) (hp : Nat.Prime p) : (Nat.fib p : ℝ) * 2 ^ (p - 1) = ∑ k in Finset.range ((p - 1) / 2 + 1), 5 ^ k * Nat.choose p (2 * k + 1) := by
  rw [coe_fib_eq]
  norm_num
  rw [add_pow, sub_eq_add_neg 1, add_pow]
  simp
  rw [div_sub_div_same]
  rw [div_div, div_mul, mul_div_right_comm]
  have h₀ (a : ℕ) (b : ℝ) (h : a > 1) (h' : b ≠ 0) : b ^ a / b ^ (a - 1) = b := by
    cases a with
    | zero => linarith
    | succ a =>
      rw [Nat.succ_eq_add_one, pow_add, Nat.add_sub_cancel]
      rw [mul_div_right_comm, pow_one]
      rw [div_self]
      rw [one_mul]
      apply pow_ne_zero
      assumption
  rw [h₀]
  · rw [← Finset.sum_sub_distrib]
    sorry
  · exact Nat.Prime.one_lt hp
  · linarith

[Kevin Buzzard]

Yikes, that goal has both natural subtraction and division! Is it true for p=2?

[Kevin Buzzard]

Instead of launching into a proof of this I would tidy up first. You can get rid of one of the natural subtractions by multiplying both sides of the equation by 2, and the other one by simplifying (p-1)/2+1 to (p+1)/2, which is probably the form I'd start with. You can then deduce the result you claimed from that, although again I would say: do you really want to? Natural subtraction isn't mathematical subtraction, it's a pathological function.

[Kamila Szewczyk]

My ultimate goal is proving that Nat.Fib (p) = (p / 5) mod p and this was the easiest (on paper!) way I could think of. Do you have other suggestions?

[Kevin Buzzard]

I would be very surprised if the goal you stated above is a theorem about prime numbers. I suspect that it is a theorem about odd numbers. I would suggesf that first you check this, and if I'm right then then replace p by 2 * q + 1 with q : Nat and then go through the entire goal, removing all natural subtractions and divisions, and prove that instead. The more general statement will be easier to prove.

[Kevin Buzzard]

My guess is that this is true:

import Mathlib.Tactic

open BigOperators

example (e : ℕ) : Nat.fib e * 2 ^ e =
    2 * ∑ k in Finset.range ((e + 1) / 2), 5 ^ k * Nat.choose e (2 * k + 1) := by
  induction e using Nat.twoStepInduction with
  | H1 => rfl
  | H2 => rfl
  | H3 n h1 h2 =>
    rw [Nat.succ_eq_add_one] at *
    rw [Nat.fib_add_two, pow_add, pow_one, add_mul, ← mul_assoc (Nat.fib (n + 1)), h2]
    clear h2
    rw [pow_add, pow_one, ← mul_assoc (Nat.fib n), ←mul_assoc (Nat.fib n), h1]
    sorry
    done

but I've run out of Lean time for today unfortunately.

[Kamila Szewczyk]

Kevin Buzzard said:

My guess is that this is true:

import Mathlib.Tactic

open BigOperators

example (e : ℕ) : Nat.fib e * 2 ^ e =
    2 * ∑ k in Finset.range ((e + 1) / 2), 5 ^ k * Nat.choose e (2 * k + 1) := by
  induction e using Nat.twoStepInduction with
  | H1 => rfl
  | H2 => rfl
  | H3 n h1 h2 =>
    rw [Nat.succ_eq_add_one] at *
    rw [Nat.fib_add_two, pow_add, pow_one, add_mul, ← mul_assoc (Nat.fib (n + 1)), h2]
    clear h2
    rw [pow_add, pow_one, ← mul_assoc (Nat.fib n), ←mul_assoc (Nat.fib n), h1]
    sorry
    done

but I've run out of Lean time for today unfortunately.

yes, the sums on the left converge to some rational expressions involving golden ratios that ultimately equal to what we have on the right.

[Kamila Szewczyk]

If I have:

example (e : ℕ) : ((Nat.fib (e + 1)) : ℝ) * 2 ^ e =
    ∑ k in Finset.range (e + 1), 5 ^ k * Nat.choose (e + 1) (2 * k + 1) := by
  rw [coe_fib_eq]
  norm_num
  rw [div_sub_div_same]
  rw [@div_div]
  rw [@div_mul_eq_div_div_swap]
  rw [@div_mul]
  rw [← rpow_sub]

then rpow_sub fails due to mismatched types. Why? how do I fix it?

[Alex J. Best]

Can you give a full #mwe so we can see the error for ourselves more easily? Or paste the actual state and error message (but an #mwe is better)

[Alex J. Best]

I would guess that maybe you don't have any rpows here, just normal pows, but I have no idea really without more info

[Kamila Szewczyk]

The expression is of type:

e: ℕ
⊢ ((1 + sqrt 5) ^ (e + 1) - (1 - sqrt 5) ^ (e + 1)) / sqrt 5 / (2 ^ (e + 1) / 2 ^ e) =
  ∑ x in Finset.range (e + 1), 5 ^ x * ↑(Nat.choose (e + 1) (2 * x + 1))

The expected type is:

e: ℕ
⊢ ∀ {x : ℝ}, 0 < x → ∀ (y z : ℝ), x ^ (y - z) = x ^ y / x ^ z

The error is:

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  ?m.135009 ^ ?y / ?m.135009 ^ ?z
e: ℕ
⊢ ((1 + sqrt 5) ^ (e + 1) - (1 - sqrt 5) ^ (e + 1)) / sqrt 5 / (2 ^ (e + 1) / 2 ^ e) =
  ∑ x in Finset.range (e + 1), 5 ^ x * ↑(Nat.choose (e + 1) (2 * x + 1))

Relevant type of the expression: @HDiv.hDiv ℝ ℝ ℝ instHDiv (2 ^ (e + 1)) (2 ^ e) : ℝ

[Kevin Buzzard]

the mew is

import Mathlib

open BigOperators Real

example (e : ℕ) : ((Nat.fib (e + 1)) : ℝ) * 2 ^ e =
    ∑ k in Finset.range (e + 1), 5 ^ k * Nat.choose (e + 1) (2 * k + 1) := by
  rw [coe_fib_eq]
  norm_num
  rw [div_sub_div_same]
  rw [@div_div]
  rw [@div_mul_eq_div_div_swap]
  rw [@div_mul]
  rw [← rpow_sub]

[Kevin Buzzard]

The error is because rpow_sub expects the exponents to also be real.

[Kamila Szewczyk]

i have tried rpow_sub_nat too, and it didn't work either

[Alex J. Best]

import Mathlib

open BigOperators Real

example (e : ℕ) : ((Nat.fib (e + 1)) : ℝ) * 2 ^ e =
    ∑ k in Finset.range (e + 1), 5 ^ k * Nat.choose (e + 1) (2 * k + 1) := by
  rw [coe_fib_eq]
  norm_num
  rw [div_sub_div_same]
  rw [@div_div]
  rw [@div_mul_eq_div_div_swap]
  rw [@div_mul]
  rw [← rpow_nat_cast]
  rw [← rpow_nat_cast]
  rw [← rpow_nat_cast]
  rw [← rpow_nat_cast]
  rw [← rpow_sub]

is one solution then

[Kevin Buzzard]

Kamila Szewczyk said:

i have tried rpow_sub_nat too, and it didn't work either

That's because that lemma expects precisely one of the exponents to be real.