7.1.1. Injectivity🔗

We can prove the injectivity of Nat.succ by using the Nat.pred function:

This technique for proving injectivity can be generalized to any constructor by writing the equivalent of Nat.pred — i.e., writing a function that "undoes" one application of the constructor.

As a more convenient alternative, Lean provides a tactic called injection that allows us to directly exploit the injectivity of any constructor. Here is an alternate proof of the above theorem using injection:

Writing injection h directs Lean to generate all equations that follow from h using the injectivity of constructors, adding them to the context. In the present example, Lean can infer that n = m from n + 1 = m + 1.

When a generated equation matches the goal, as is the case here, injection automatically closes the goal.

When the generated equations do not immediately close the goal, the equations are added to the context instead; adding with allows us to explicitly name the equations (otherwise Lean generates names for us).

There is also a related tactic, injections, that applies the injection tactic to all hypotheses, repeatedly. Using it simplifies the proof of the above example.

Note that both injection and injections will simplify a hypothesis before applying injectivity. Thus we could also use them to solve the following example, which requires simplifying the ++ and List.reverse expressions:

7.1.2. Disjointness🔗

So much for injectivity of constructors. What about disjointness?

The principle of disjointness says that two terms beginning with different constructors (like 0 and Nat.succ, or true and false) can never be equal. Therefore, any time we find ourselves in a context where we've assumed that two such terms are equal, we are justified in concluding anything we want, since the assumption is nonsensical.

The contradiction tactic embodies this principle. If the context contains a contradictory hypothesis, such as false = true, contradiction solves the current goal immediately. Some examples:

These examples are instances of a logical principle known as the principle of explosion, which asserts that a contradictory hypothesis entails anything — even manifestly false things!

In the above example, n + 1 is shorthand for a constructor application Nat.succ n so contradiction applies to it directly.

Sometimes you need to do a little work to expose a contradictory hypothesis involving constructors.

For example, recall that Nat.add recurses on its second argument, so deriving a contradiction from 1 + n = 0 is not direct.

To fix it, rewriting with Nat.one_add changes the hypothesis from 1 + n = 0 to n.succ = 0. Then Lean can immediately recognize this as impossible.

If you find the principle of explosion confusing, remember that these proofs are not simply showing that the conclusion of the statement holds. Rather, they are showing that, if the nonsensical situation described by the premise did somehow hold, then the nonsensical conclusion would hold too (because we'd be living in an inconsistent universe where every statement is true).

We'll explore the principle of explosion in more detail in the next chapter.

7.1.3. Quizzes🔗

Recall our RGB and Color types:

x : RGB
y : RGB
h : .primary x = .primary y
------------------------------
⊢ y = x

x : Bool
y : Bool
h : !x = !y
--------------
⊢ y = x

Tactic `injection` failed: equality of constructor applications expected

x y:Boolh:(!decide (x = !y)) = true⊢ y = x

x : Nat
y : Nat
h : x + 1 = y + 1
-------------------
⊢ y = x

x : Nat
y : Nat
h : 1 + x = 1 + y
-------------------
⊢ y = x

Tactic `injection` failed: equality of constructor applications expected

x y:Nath:1 + x = 1 + y⊢ y = x

7.1.4. Tactic congr🔗

The injectivity of constructors allows us to reason that ∀ (n m : Nat), n + 1 = m + 1 → n = m. The converse of this implication also holds:

This is an instance of a more general fact about both constructors and functions:

There is a tactic named congr that can prove such goals directly. Given a goal of the form f a₁ ... aₙ = g b₁ ... bₙ, writing congr will produce subgoals of the form f = g, a₁ = b₁, ..., aₙ = bₙ. If any of these subgoals that are simple enough to be discharged automatically (e.g., immediately provable by rfl), they will disappear.

The congr tactic accepts an optional numerical argument, which tells Lean how deeply to decompose the goal. So, given a goal like ((a, b), (c, d)) = ((e, f), (g, h)), congr 1 only applies congr just once to the goal to produce two subgoals: (a, b) = (e, f) and (c, d) = (g, h), while congr 2 would apply congr again to both these subgoals and produce four subgoals: a = e, b = f, c = g and d = h. Using congr without an argument decomposes the goal as deeply as possible.

Why might we want this level of control? Because, depending on what we are trying to prove, deeper applications of congr may sometimes make our goal unprovable. Consider:

We now have two goals: a = b and c = d, but these are not provable from our hypotheses! congr has gone too deep.

unsolved goals
e_fst.e_aa b c d:Nath1:a = b + 1h2:d = c + 1⊢ a = b

e_fst.e_aa b c d:Nath1:a = b + 1h2:d = c + 1⊢ c = d

7.2.1. Destructing Tuples🔗

The cases tactic is useful when we are dealing with values that can be one of a list of things (a Bool is either a false or a true, a Nat is either 0 or succ n, etc.). When we want more information about a value that is a tuple of multiple things, we instead want a way to extract the pieces of that value.

If we have a value v : α × β in our context, we can extract the first and second components of v and give them names using this tactic:

let ⟨a, b⟩ := v

7.2.2. Splitting with Equations🔗

When using cases, we can specify to Lean that it should remember an equality between a compound expression and what we are decomposing it into, using cases h : ... syntax. This step is sometimes critical: if we leave it out, we might lack information we need to complete a proof.

For example, suppose we define a function keepIf like this:

Now suppose that we want to prove that, if keepIf returns a result of the form some y, then x = y. If we start the proof like this (with no h : ⋯ on the cases)...

unsolved goals
falseα:Typetest:α → Boolx y:αh:(bif test x then some x else none) = some y⊢ x = y

trueα:Typetest:α → Boolx y:αh:(bif test x then some x else none) = some y⊢ x = y

... then we are stuck because the context does not contain enough information to prove the goal. Because test x appears in the hypothesis rather than the goal, cases (test x) does not automatically replace the expression with false or true like it did during the proof of chooseIf. We want to add an equation to the context that records which case we are in. This is precisely what the h : ⋯ qualifier does.