# Zulip Chat Archive

## Stream: new members

### Topic: tactic 'contradiction' failed

#### 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
```

#### 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
| succ a => rw [Nat.succ_add] at h1; contradiction
· cases b with
| zero => rfl
| succ b => rw [Nat.add_succ] at h1; contradiction
#print Nat.eq_zero_of_add_eq_zero
```

#### Bulhwi Cha (Feb 15 2023 at 07:08):

See also Section Tactics for Inductive Types in #tpil4.

#### 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