Odd and even numbers without witness

Stream: new members

[Tyler Josephson ⚛️]

Mechanics of Proof introduces odd and even numbers with examples like this:

import Mathlib.Tactic
example : Odd (7 : ℤ) := by
  dsimp [Odd]
  use 3
  norm_num

How would one prove this without providing the witness (3)? It would be nice to prove things like this without needing to anticipate what number is needed to solve it.

[Asei Inoue]

Your MWE does not work on Lean 4 playground. How about this?

def Odd (n : Int) : Prop := ∃ k : Int, n = 2 * k + 1

example : Odd (7 : Int) := by
  dsimp [Odd]
  exists 3

[Tyler Josephson ⚛️]

Thanks - edited to avoid the tactics specific to the textbook.

My aim is to not use "3" at all. That means that I need to do extra work to find the witness - is there a way to ask Lean to find it for me?

[Eric Wieser]

decide, with the right imports?

[Asei Inoue]

decide fails.

import Mathlib

namespace Hidden

def Odd (n : Int) : Prop := ∃ k : Int, n = 2 * k + 1

example : Odd (7 : Int) := by
  dsimp [Odd]
  /-
  failed to synthesize
    Decidable (∃ k, 7 = 2 * k + 1)
  use `set_option diagnostics true` to get diagnostic information
  -/
  decide

[Asei Inoue]

Is there a tactic that transforms 7 = 2 * k + 1 into k = 3? If that can be done, it would not be an exaggeration to say that Lean has found k.

[Bjørn Kjos-Hanssen]

You can do this (for naturals, a more elaborate version would work for Ints):

import Mathlib

instance (n : Nat) : Decidable (Odd n) := decidable_of_iff (∃ k : Fin n, n = 2 * k.1 +1) (by
  unfold Odd;constructor;intro ⟨k,hk⟩;exists k.1;intro ⟨k,hk⟩;
  exists ⟨k,by linarith⟩
)

example : Odd 57 := by decide

[Kyle Miller]

@Asei Inoue The decide tactic definitely works:

import Mathlib

example : Odd (7 : Int) := by
  decide

[Kyle Miller]

Another approach (and likely what decide effectively does) is

example : Odd (7 : Int) := by
  rw [Int.odd_iff]
  rfl

which turns it into a simple modular arithmetic problem and then uses rfl to tell Lean to just calculate it.

[Bjørn Kjos-Hanssen]

Kyle Miller said:

Asei Inoue The decide tactic definitely works:

import Mathlib

example : Odd (7 : Int) := by
  decide

Unless you make your own definition of Odd right before trying that. :man_shrugging:

[Asei Inoue]

Oh nice!! @Kyle Miller @Bjørn Kjos-Hanssen Thank you!!

@Tyler Josephson ⚛️ Thank you for nice question!

I find this also works without Mathlib

def Odd (n : Int) : Prop := ∃ t : Int, n = 2 * t + 1

instance (n : Int) : Decidable (Odd n) := by
  refine decidable_of_iff (n % 2 = 1) ?_
  dsimp [Odd]
  constructor <;> intro h
  · exists (n / 2)
    omega
  · obtain ⟨t, th⟩ := h
    rw [th]
    omega

example : Odd (7 : Int) := by
  decide

[Mitchell Lee]

(deleted)

[Eric Wieser]

Yes, if you make your own definitions of things then you won't get any of the tools about them that mathlib already knows!