2
$\begingroup$

I am playing the Natural Number Game found here and am trying to prove a theorem in Lean4. The theorem states that if a natural number x is less than or equal to 0, then x must be 0. The formal statement is ∀ (x : ℕ), x ≤ 0 → x = 0.

Here's my current code:

theorem le_zero (x : ℕ) (hx : x ≤ 0) : x = 0 := by {
  apply le_trans x 0 x at hx,
  cases x with d,
  rfl,
  symm,
  -- Now I have a goal of `succ d = 0`
  apply zero_le at hx,
  -- Stuck here, it says 'oops'
}

I applied le_trans and then used cases to handle the base case x = 0 and the successor case x = succ d. The base case is easily solved with rfl, but I'm stuck on the successor case.

$\endgroup$
1
  • $\begingroup$ Hint 1: Note that in the natural numbers, succ d can never be 0. So your mistake has to be before you got to the goal succ d = 0. Hint 2: Have you tried it on paper? $\endgroup$
    – Jason Rute
    Oct 30, 2023 at 1:32

1 Answer 1

3
$\begingroup$

this is my proof that uses the rules of the game

cases hx
contrapose! h
symm
intro t
apply eq_zero_of_add_right_eq_zero at t
apply h at t
exact t

Not sure if cases is allowed at the beginning without a with but it seems to be accepted, Game will accept this proof.


Edit: Someone posted another shorter proof, but I don't see their proof anymore, so here it goes

cases hx with a ha
exact eq_zero_of_add_right_eq_zero _ _ ha.symm
$\endgroup$
0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.