## Stream: new members

#### Kauê Campos (Feb 15 2023 at 04:34):

Hello,
I'm new to Lean and pretty much just started messing with it, I've been experimenting with proving basic arithmetic from scratch and just started porting most of my experiments to Lean 4, I however can't seem to understand why the contradiction tactic can't seem to find a contradiction inside the context in this scenario.

theorem zero_iff_eq_zero (a b : mynat) : a+b = 0 → a = 0 ∧ b = 0 := by
intro h1
apply And.intro
· cases a with
| zero => rw [zero_eq_zero]
| succ a => have h2 := succ_ne_zero a ; contradiction
· cases b with
| zero => rw [zero_eq_zero]
| succ b => have h2 := succ_ne_zero b ; contradiction -- it errors out here


image.png

#### Bulhwi Cha (Feb 15 2023 at 06:19):

I hope this helps:

import Std.Data.Nat.Lemmas

-- theorem Nat.eq_zero_of_add_eq_zero in Std.Data.Nat.Lemmas
theorem zero_iff_eq_zero (a b : Nat) : a+b = 0 → a = 0 ∧ b = 0 := by
intro h1
apply And.intro
· cases a with
| zero => rfl
· cases b with
| zero => rfl



#### Mauricio Collares (Feb 15 2023 at 07:29):

In the screenshot, what is the contradiction you expected Lean to find? Lean needs your help in finding a contradiction from h1 because of the way addition is defined (I'm assuming that your definition of mynat addition includes the case succ a + b = succ (a+b), so the statement a + succ b = succ (a+b) is not true by definition and must be proved by induction), so spelling it out might help.

#### Kevin Buzzard (Feb 15 2023 at 13:57):

The contradiction tactic does not work hard to find a complicated argument which leads to a contradiction from your hypothesis. Doesn't it only work when there are two hypotheses, one of which is literally not the other one?

#### Alex J. Best (Feb 15 2023 at 14:54):

It does a few other things too it seems https://github.com/leanprover-community/lean/blob/855e5b74e3a52a40552e8f067169d747d48743fd/library/init/meta/contradiction_tactic.lean#L73 but all are somewhat basic, false as a hypothesis, not x ~ x for reflexive ~, no confusion for constructors of inductive types.

Last updated: Dec 20 2023 at 11:08 UTC