tactic 'contradiction' failed

Stream: new members

[Kauê Campos]

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]

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]

See also Section Tactics for Inductive Types in #tpil4.

[Mauricio Collares]

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]

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]

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.