vanilla way to do contradiction (simple example)

Stream: new members

[rzeta0]

After completing MoP's chapter 4 which concludes with contradiction ... I'm trying to create vanilla Lean examples that don't use. the MoP special tactics.

Here is a simple example - note the final 2 lines:

import Mathlib.Tactic

example {n : ℕ} (h: n = 5) : ¬ n = 1 := by
  intro hn
  have g :=
    calc
      5 = n := by rw [h]
      _ = 1 := by rw [hn]
  -- contradiction --<-- also works to my surprise
  linarith

The goal state just after calc is

n : ℕ
h : n = 5
hn : n = 1
g : 5 = 1
⊢ False

So in MoP we learned that:

• tactic numbers at hip can be used to complete a proof by contradiction by pointing it at a numerically false hypothesis.
• tactic contradiction which can conclude a proof by contradiction if it sees a hypothesis of the form h1: P and another h2: ¬P

In vanilla Lean we don't have numbers. I tried linarith as in the above example, and it seems to work.

I also tried contradiction and that worked to my surprise because here it identifies a numerically false hypothesis but in MoP it only looks for lexically opposing hypotheses.

Question 1: What is the correct way to do contradiction, at least for the above example?

Question 2: I'd welcome commentary, history, about whether linearity works but shouldn't be used like this, and whether lean's own contradiction tactic only recently did numerically false hypotheses (motivating the need for MoP to have its own).

[rzeta0]

---

further experimenting shows even the following works:

import Mathlib.Tactic

example {n : ℕ} (h: n = 5) : ¬ n = 1 := by
  intro hn
  linarith

Again, I'm surprised.

[Matt Diamond]

linarith handles equalities as well as inequalities

[rzeta0]

Thanks Matt.

Back to my original question, I'm trying to get a sense of when one should use contradiction over linarith when both appear to work.

[Kyle Miller]

It makes sense that contradiction works here, because 5 = 1 is the sort of contradiction it can handle. The reasoning is that 5 = 1 is the same as Nat.succ 4 = Nat.succ 0, which reduces to 4 = 0, and this is the same as Nat.succ 3 = Nat.zero, but Nat.succ of something can't ever be Nat.succ. The keywords are "injectivity of constructors for inductive types."

There's a whole list of things that contradiction tries.

[Kyle Miller]

The docstrings to both docs#Lean.MVarId.contradiction and docs#Lean.Parser.Tactic.contradiction give a list of the things that the tactic considers.