7.1.1. Injectivity🔗

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

As a convenience, the injection tactic allows us to exploit injectivity of any constructor (not just Nat.succ).

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🔗

Two terms beginning with different constructors (like 0 and Nat.succ, or true and false) can never be equal.

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!

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

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.

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:

Lean also provides congr as a tactic.

We can specify the recursion-depth with congr n.

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.

Adding the h : ⋯ qualifier saves this information so we can use it.

7.3.1. Supplying arguments to apply🔗

The following silly example uses two rewrites in a row to get from [u, v] to [y, z].

Since this is a common pattern, we might like to pull it out as a lemma that records, once and for all, the fact that equality is transitive.