Using the contrapositive in lean 4

Question

I'm trying to learn lean (version 4) by proving some basic facts about the natural numbers. Please feel free to critique my code if you see have general comments, but I also have a specific question involving a proof below. Here is my nat type:

-- Axiom 2.1. 0 is a natural number.
-- Axiom 2.2. If n is a natural number, then n++ is also a natural number.
inductive nat : Type | zero : nat | succ : nat → nat

I also have this axiom:

-- Axiom 2.4. Different natural numbers must have 
-- different successors; i.e., if n, m are natural 
-- numbers and n ≠ m, then n++ ≠ m++. Equivalently, 
-- if n++ = m++, then we must have n = m.
axiom succ_inj : ∀ n : nat, ∀ m : nat, n ≠ m → succ n ≠ succ m

I am using classical mode:

open Classical

I would like to use the contrapositive of axiom 2.4 (or a proof by contradiction) to prove the inductive step of this proposition

-- Proposition 2.2.6 (Cancellation law). Let a,b,c be natural 
-- numbers such that a+b=a+c. Then we have b=c.
theorem cancellation_law (a b c : nat) : (a + b) = (a + c) → b = c := by
  intro h
  induction a with
  | zero =>
    have h1 : b = zero + b := by rfl
    have h2 : c = zero + c := by rfl
    rw [h1, h2]
    exact h
  | succ a ih =>
    have h1 : succ a + b = succ (a + b) := by rfl
    have h2 : succ a + c = succ (a + c) := by rfl
    rw [h1,h2] at h

So now my lean state looks like this:

> case succ
bca: nat
ih: a + b = a + c → b = c
h: succ (a + b) = succ (a + c)
h1: succ a + b = succ (a + b)
h2: succ a + c = succ (a + c)
⊢ b = c

So now I would like to use the fact that

succ (a + b) = succ (a + c) -> a + b = a + c

which follows from axiom 2.4, and then apply the induction hypothesis. But I can't seem to figure out how to do a proof by contradiction. I continue the proof of proposition 2.2.6 with something like

have h3: a + b = a + c := by
...
...
contradiction

The theorem proving in lean 4 book says the contradiction tactic looks for a contradiction in the hypotheses introduced, but how do I introduce an assumption for the purpose of contradiction? What is a good/canonical way to write this proof?

Here is a MWE:

open Classical

-- Section 2.1 The Peano axioms

-- Axiom 2.1. 0 is a natural number.
-- Axiom 2.2. If n is a natural number, then n++ is also a natural number.
inductive nat : Type | zero : nat | succ : nat → nat

namespace nat

-- Axiom 2.3. 0 is not the successor of any natural number; i.e.,
-- we have n++ ̸= 0 for every natural number n.
axiom zero_not_succ : ∀ n : nat, zero ≠ succ n

-- Axiom 2.4. Different natural numbers must have 
-- different successors; i.e., if n, m are natural 
-- numbers and n ≠ m, then n++ ≠ m++. Equivalently, 
-- if n++ = m++, then we must have n = m.
axiom succ_inj : ∀ n : nat, ∀ m : nat, n ≠ m → succ n ≠ succ m

-- Section 2.2 Addition
def add : nat → nat → nat
| zero, m => m
| succ n, m => succ (add n m)

-- Get to use the plus operator
instance : Add nat where add := add

-- Proposition 2.2.6 (Cancellation law). Let a,b,c be natural 
-- numbers such that a+b=a+c. Then we have b=c.
theorem cancellation_law (a b c : nat) : (a + b) = (a + c) → b = c := by
  intro h
  induction a with
  | zero =>
    have h1 : b = zero + b := by rfl
    have h2 : c = zero + c := by rfl
    rw [h1, h2]
    exact h
  | succ a ih =>
    have h1 : succ a + b = succ (a + b) := by rfl
    have h2 : succ a + c = succ (a + c) := by rfl
    rw [h1,h2] at h
/-
    > case succ
    bca: nat
    ih: a + b = a + c → b = c
    h: succ (a + b) = succ (a + c)
    h1: succ a + b = succ (a + b)
    h2: succ a + c = succ (a + c)
    ⊢ b = c
-/

end nat

Answer 1

First, to answer your direct question, you can complete your proof with the following.

    apply ih
    contrapose h
    apply succ_inj
    exact h

After apply ih the goal is:

...
h: succ (a + b) = succ (a + c)
...
⊢ a + b = a + c

What contrapose h does is:

• Move the assumption h into the goal to get succ (a + b) = succ (a + c) -> a + b = a + c
• Swap the goal with its contrapositive.
• intro h to put the new assumption ¬ a + b = a + c back into the assumption list.

To use contrapose you have to import it from mathlib with import Mathlib.Tactic.Contrapose.

Now you can apply your succ_inj axiom.

---

Having said that, here are two points about succ_inj:

• It is almost always best to express injectivity as the contrapositive from the beginning. So succ_inj would be ∀ n : nat, ∀ m : nat, succ n = succ m → n = m. This is much cleaner to work with.
• Injectivity follows directly from Lean's inductive types and is automatically created in this case as nat.succ.inj (using the version I just wrote in the bullet above). See here for how this works in Lean 3. For Lean 4, it is a bit trickier to find the list of these automatically generated theorems since they aren't generated until you use them which can be done by calling them directly by name or invoking them with simp.

Now your proof doesn't have to rely on classical reasoning. While your proof with have statements above works fine, I think this is a nice opportunity to use the calc tactic (which has the same syntax as the calc command).

theorem cancellation_law' (a b c : nat) : a + b = a + c → b = c := by
  intro h
  induction a with
  | zero =>
    calc
      b = zero + b := rfl
      _ = zero + c := h
      _ = c        := rfl
  | succ a ih =>
    apply ih
    apply nat.succ.inj
    calc
      succ (a + b) = (succ a) + b := rfl
      _            = (succ a) + c := h
      _            = succ (a + c) := rfl

---

Finally, while my calc proof is clean and easy to read, the book-ends of both calc were just rfl proofs. Lean is actually smart enough to realize at that point that the goal and assumption h are definitionally equal, so we could just do this:

theorem cancellation_law'' (a b c : nat) : a + b = a + c → b = c := by
  intro h
  induction a with
  | zero =>
    exact h
  | succ a ih =>
    apply ih
    apply nat.succ.inj
    exact h