Proving false is equivalent to false

Stream: new members

[Barinder S Banwait]

I'm at a point in a proof where my goal is to prove that, for $n$ a nonzero natural number, the statement "$2^n$ is odd" is equivalent to "$7$ is even'". Each statement is obviously false so the two are indeed equivalent, but I'm having trouble formalizing this in Lean:

example (n : ℕ) (h : n ≠ 0) : Odd ((2 : ℤ) ^ n) ↔ Even (7 : ℤ) := by
  sorry

(Type casting to ℤ arises from a previous part of the proof.)

Can anyone help get me unstuck?

[Markus Himmel]

Which part are you stuck on? Showing that the statements are individually false or concluding the claim from that? Once you have that the statements are individually false, simp is usually really good at finishing off the goal. Here's a proof:

import Mathlib

theorem not_even_seven : ¬Even (7 : ℤ) := by decide

theorem not_odd_two_pow (n : ℕ) : n ≠ 0 → ¬Odd ((2 : ℤ) ^ n) := by
  cases n <;> simp [pow_succ]

example (n : ℕ) (h : n ≠ 0) : Odd ((2 : ℤ) ^ n) ↔ Even (7 : ℤ) := by
  simp [not_even_seven, not_odd_two_pow _ h]

[Yaël Dillies]

or use docs#iff_of_false

[Barinder S Banwait]

Markus Himmel said:

Which part are you stuck on? Showing that the statements are individually false or concluding the claim from that? Once you have that the statements are individually false, simp is usually really good at finishing off the goal. Here's a proof:

import Mathlib

theorem not_even_seven : ¬Even (7 : ℤ) := by decide

theorem not_odd_two_pow (n : ℕ) : n ≠ 0 → ¬Odd ((2 : ℤ) ^ n) := by
  cases n <;> simp [pow_succ]

example (n : ℕ) (h : n ≠ 0) : Odd ((2 : ℤ) ^ n) ↔ Even (7 : ℤ) := by
  simp [not_even_seven, not_odd_two_pow _ h]

Thanks for your response Markus; I was trying to split the ↔ and attempt to prove each direction, but I couldn't get that to work. I've not seen <;> before, is that like repeat?

[Barinder S Banwait]

but from Yaël's response, it seems I was looking for apply iff_of_false :sweat_smile:

[Markus Himmel]

You can hover over the <;> in VS Code to get a description. It says

tac <;> tac' runs tac on the main goal and tac' on each produced goal, concatenating all goals produced by tac'.

[Barinder S Banwait]

Here's the solution inspired by both Markus and Yaël:

example (n : ℕ) (h : n ≠ 0) : Odd ((2 : ℤ) ^ n) ↔ Even (7 : ℤ) := by
  apply iff_of_false
  · exact not_odd_two_pow n h
  · decide