cases syntax

Stream: new members

[David Gold]

hi all! very new to lean, but had a blast working thru the natural number game. now trying to replicate the even/odd proofs in https://www.youtube.com/watch?v=QI-fEXSX1BA, but struggling with the syntax of cases. the video has this:

lemma succ_even_odd (n : ℕ) : (even n) → (odd (n + 1)) := by
  intro h
  unfold even at h
  cases h with d hd
  unfold odd
  use d

what actually works in my environment (and what the tactics cheat sheet recommends) is

lemma succ_even_odd (n : ℕ) : (even n) → (odd (n + 1)) := by
  intro h
  unfold even at h
  cases h with | intro d hd => {
    rw [hd]
    unfold odd
    use d }

im assuming this is just a lean3/lean4 compatibility issue, but is there something else going on? is there a better/easier way to do this? sorry if this question is in the wrong place/too simple, but thanks in advance :)

[Alex J. Best]

Yes this is a lean3 / 4 issue, you can use cases' (which is defined in mathlib4) to get the old style behaviour. But using the new syntax is also fine, and it looks like you worked it out ok!

[David Gold]

aha got it! much appreciated!!

[Joachim Breitner]

If there is only one case to match against, the constructor name might be more a distraction than helpful, and you can write

cases h with | _ d hd =>

You also don't need { here, I believe, since you are indenting. And since there is only one case, it’s a bit unnatural to even indent, so you could just keep going in the same column here.

[Kevin Buzzard]

On the tube home I was working on adding EvenOdd World to NNG4. Here's a Zulip-only exclusive of some of the levels in EvenOdd world:

import Mathlib.Tactic

def IsEven (n : ℕ) := ∃ (t : ℕ), t + t = n

theorem isEven_def (n : ℕ) : IsEven n ↔ ∃ t, t + t = n := Iff.rfl

theorem isEven_zero : IsEven 0 := by
  sorry

theorem isEven_two : IsEven 2 := by
  sorry

theorem not_isEven_one : ¬ IsEven 1 := by
  sorry

theorem isEven_add_isEven (a b : ℕ) (ha : IsEven a) (hb : IsEven b) : IsEven (a + b) := by
  sorry

def IsOdd (n : ℕ) : Prop := ∃ t : ℕ, t + t + 1 = n

theorem isOdd_def (n : ℕ) : IsOdd n ↔ ∃ t : ℕ, t + t + 1 = n := Iff.rfl

theorem isOdd_one : IsOdd 1 := by
  sorry

theorem not_isOdd_zero : ¬ IsOdd 0 := by
  sorry

open Nat

@[simp] theorem isOdd_succ_iff (a : ℕ) : IsOdd (succ a) ↔ IsEven a := by
  sorry

@[simp] theorem isEven_succ_iff (a : ℕ) : IsEven (succ a) ↔ IsOdd a := by
  sorry

theorem isEven_or_isOdd (n : ℕ) : IsEven n ∨ IsOdd n := by
  sorry

theorem not_isEven_and_isOdd (n : ℕ) : ¬ (IsEven n ∧ IsOdd n) := by
  sorry

theorem isOdd_add_isOdd {a b : ℕ} (ha : IsOdd a) (hb : IsOdd b) : IsEven (a + b) := by
  sorry

theorem IsEven_add_IsOdd( a b : ℕ ) (ha : IsEven a) (hb : IsOdd b) : IsOdd (a + b) := by
  sorry

theorem IsOdd_add_IsEven( a b : ℕ ) (ha : IsOdd a) (hb : IsEven b) : IsOdd (a + b) := by
  sorry

[Kevin Buzzard]

@David Gold