Lean

We will use the proof assistant [Lean 4][lean] for some required activities.

(If something in this guide does not work, it is probably because I missed it while upgrading this guide from Lean 3 to Lean 4.

[Install Lean 4 on your machine][lean-start] to use with [VS Code].

As always: seek help on Zulip, probably in the #proofassistants channel.

How can I share my code to get feedback or ask something about it?

Attacking (the goal)

If my goal is already on my givens

Lean: exact d where d is the label of the given, or just use a plain assumption and Lean will try to find a given that matches your goal.

(⇒): If my goal is an implication P ⇒ Q

Text:

Suppose P ⁽ʰᵖ⁾.

Lean: intro hp where hp is the name you are choosing to label this given.

Effects:

(∧): If my goal is a conjunction P ∧ Q

Text:

Split (the proof/goal in two parts).
Part-L:
  ⋮ [proof of P here (from the same givens)]
Part-R:
  ⋮ [proof of Q here (from the same givens)]

Lean: split

Effects: our proof splits in two parts, copy-pasting the current fivens in each and: the first part has P as its goal, while the second one has the goal Q. We must prove both parts.

(∨): If my goal is a disjunction P ∨ Q

I must choose one of the two alternatives: the left (P) or the right (Q).

(∀): If my goal is a universal proposition (∀x:A)[ φ(x) ]

I request an arbitrary object of type A, which I get to name in an appropriate way (let’s say a). Now I need to prove that such abitrary object satisfies φ, in other words I need to prove φ(a).

Text: «Let a : A.»
Lean: intro a
Effect: O alvo vira φ(a).

(∃): If my goal is an existencial proposition (∃x:A)[ φ(x) ]

I need to find an object of such type A (my witness) and then prove that it is indeed valid. Notice that, unlike the previous case in which I only choose a name of an arbitrary object, here I need to specify the object myself. In the example that follows w stands for some object of type A.

Text: «I choose w : A. Now I will prove φ(w)».
Lean: use w
Effect: The goal becomes φ(w).

(=): If my goal is an equation of the form t = t.

Text: «Immediate (by reflexivity of (=)).»
Lean: refl Effect: ∎ (Ends this proof.)

(=): If my goal is an equationo s = t.

We need to compute using substitutions of equals by equals in s until we reach t or vice versa. Alternatively we can manipulate both sides to reach the same object.

Text: «We compute: […computation goes here…]»
Lean: see below how to use equations; then see how to use calc which is a mode that resembles much closer the human «We compute: …» style.

(¬): If my goal is a negation ¬P

Then it is actually an implication: P ⇒ ⊥; which means you already know what to do.

(⇔): If my goal is a logical equivalence P ⇔ Q

Then it is actually a conjunction: (P ⇒ Q) ∧ (Q ⇒ P); which means you already know what to do.

How to use your givens

(∨): To use a disjunction P ∨ Q

Text: «Separate in cases by P ∨ Q. Case-L: […]. Case-R: […].»
Effect: Two new “games” are created where all Givens/Goal are copied-pasted with the exception of the given P ∨ Q which becomes just P on the first and just Q on the second. We need to complete both proofs.

Beware: each of these new games has its one scope, so changes/effects that happen inside one proof do not affect the other.

Lean: rcases hor where hor is the label of the disjunction we want to use. To give new labels to the local hypotheses of each case (for exemplo hp for P in Case-L and hq for Q in Case-R) use rcases hor with (hp | hq).

(∧): To use a conjunction P ∧ Q

Text: Writing «Extract the left part of P∧Q.» we obtain P in our givens. Similarly for the right. Note: nobody really writes something as low-level as this in their text: we are used to doing both such extractions automatically as soon as we have a conjunction in our givens.

Lean: let ⟨hl, hr⟩ := h to obtain both parts simultaneously as hl and hl, but see also the «Using givens on the fly» section below.

It is better to give our own names for each part, which we do thus: rcases h with ⟨hp , hq⟩ obtaining the givens hp : P and hq : Q.

Warning: the word «cases» that Lean uses for this is confusing since it does not correspond to the word «cases» we use in our human-language proofs.

(⇒): To use an implication P ⇒ Q

Forward reasoning: we can apply it on (a proof of) P to obtain a (proof of) Q, but in order to do so we need to provide it with such a (proof of) P.

Text: «Since P⇒Q and P, therefore Q.» or «Apply P⇒Q on P to obtain Q.»

Effect: We gain Q on our givens.

Lean: have hq : Q := hpq hp where hq is the label I have chosen for the given I am about to gain, and hpq is the label of my given P→Q and hp is the label of my P.

It is very common to use implications in “backward reasoning”: if our goal is Q and we have P⇒Q we can say that we will obtain our goal by applying the implication P⇒Q, in which case all that is left to do is prove its premise, P.

Text: «The result follows by applying P⇒Q. All that remains is to prove P.»

Effect: the goal changes from Q to P.

Lean: apply hpq onde novamente hpq é o rótulo da implicação P→Q que temos nos dados.

(¬): To use a negation ¬P

Again: a negation ¬P is the implication P⇒⊥. Which means you already know how to use it.

(∀): To use a “universal” (∀x:A)[ φ(x) ]

This is like a factory of propositions: you give it any object a of type A and it gives you back the proposition that your object a satisfies φ, i.e., you gain (a proof of) the proposition φ(a). This is often called instantiation or specialization.

Text: «Since (∀x:A)[ φ(x) ], apply it on a : A to obtain φ(a).»

Lean: such objects are (dependent) functions (x : A) → φ(x) and we use them accordingly: having a : A and h : ∀ (x : A), P x, the aplication of h on a (which we denote by h a) is of type P a, in other words, a proof that a has property P.

(∃): To use an existential (∃x:A)[ φ(x) ]

Since we know that there exist objects with some property, we have the right to request such an object, and we get to pick a valid name for it.

Text: «Let a : A such that φ(a).»

Lean: such objects are (dependent) pairs (a : A) × P a and we use them accordingly: let ⟨w,hw⟩ := h, in which w is the name we chose for the witness we are requesting and hw the name of the proof/fact that w is indeed an object that satisfies φ.

(=), (⇔): To use an equation s = t or an equivalence P⇔Q

We substitute equals for equals and equivalents for equivalents.

Lean: use the rewrite tactic rw [heq] where heq is the name of the equality you want to use.

Obs: Lean performs substitutions from left to right (replacing s by t). To replace from right to left use ← before the name of the equation you are using like rw [← heq].

Obs: Lean tries to use the specified equation to perform substitution on the goal. If you want to perform such substitution on a given, specify it by adding at h, where h is the label of the given.: rw [heq] at h.

Tip: we can apply more than one rwrites with a single tactic: rw [h₁, ←h₂, …, hₙ]

Lean: we may use rw for equivalences in the same way. Additionally, remember that an equivalence (⇔) is just a conjunction, so we can use it accordingly as well.

Using givens on the fly

Observe that we can use our givens to create new “on the fly”: having f : A → B and a : A then the term f a denotes the application of the implication/function f on the given a and therefore it is a (term/proof) B. Thus, if our goal was to prove B we can write exact f a to close it. The same thing applies to all of the connectives; for example if h : P∧Q then h.left : P e h.right : Q, etc.

Conversion mode

If you feel the need to navigate on your givens and goals and rewrite or simplify some (sub)expressions of theirs, see how to use conv. Although it is never necessary to do so, there are people who cannot survive without it, and can it feel very limiting/frustrating if you are not allowed to “just do this” any time you feel like it.

Ex Falso Quodlibet

Also known as: «I have managed to explode the world and therefore my goal has died with it.»

Text: «I will find a contradiction.»

Lean: exfalso

Effect: The goal becomes ⊥.

Maybe we already have an obvious contradiction in our givens. To ask for Lean to discover it and use it to end the proof we have the tactic contradiction.

Induction

Text: «By induction on n.»

Lean: induction n with w hw where w is the name of the object of which we know the I.H. and hw is the label of such hypothesis.

Obs: if you manage to prove your theorem without using the inductive hypothesis, this is because it was not really necessary to use induction. Maybe you did not even need to separate in cases based on the constructors; or if you did, in the “recursive” constructors you did not need to use a recursive call / inductive hypothesis. You can achieve this simpler for by cases n where n is a natural numbers (or any other object of an inductively defined type) to separate it in all possible forms. This looks like using the following disjunction: a natural number n is either of this form or that form. To name the matching object use something like: cases n with n'.

Tips

  1. Instead of using intro h, intro h', intro h'' etc., use intro h h' h''.
  2. Take advantage of nested patterns to achieve intros and extractions. For example, if your goal is P ∧ Q → R → S ∧ T → G you can intro everything and simultaneously “unpack” the conjunctions like this: intro ⟨hp, hq⟩ hr ⟨hs, ht⟩.
  3. The rcases that we have seen to use conjunctions and disjunctions allows nested pattern-matching of abitrary depth: if you want to use a given like P ∨ (Q ∧ (R ∨ S)) we can use the following with pattern: rcases h with (hp | ⟨hq , (hr | hs)⟩). Voilà!
  4. To repeat a tactic for as long as it is applicable use repeat { tactic }.
  5. The inverse process of intro is revert: use revert h₁ … hₙ to move such hypotheses from your givens to become premises in your goal. This is very useful when you want to use induction early, before introducing some of the variables in order to have a stronger I.H. (since it carries with it all those ∀’s). But for this we also have the “specialized” induction n generalizing z₁ … zₙ where z₁,…zₙ are variables in our context (givens) that we want to “gain as ∀’s” in our inductive hypotheses.
  6. Use injection when you want to “cancel the constructors” in an equation on your goal. For example, the goal Sn=Sm would become n=m. If you have such an equation on your givens labeled as h then use injection h with h₁ … hₙ in order to gain as new givens all corresponding/inferred equations. In this example, if we have h : succ n = succ m then by using injection h with h' we obtain the new given h' : n = m.
  7. If you would like to add some P to your givens, all you need to do is prove it. Use have h : P where h is the label of your choice for the given you are about to gain (once you manage to prove it from your current context). Lean will create a new game/subproof with goal P and if you manage to prove it you get h : P on the givens of your original proof. In words: «I accept to give you what you want as long as you provide a proof from what you already have.»
  8. You can claim that you will manage to prove a goal by applying a certain given h using the apply h tactic. This will match your current goal with the conclusion of h, creating as new goal(s) all that is required for h to work in this way. (See «Backwards use» of usage of (⇒) above for a specific example.)
  9. To ask lean for suggestions on what you could apply, use apply?.

I want to see the implicit parentheses, can I?

Yes. Use the following line on your code:

set_option pp.parens true

to see the implicity parentheses starting from this line, and swap true for false to go back to omitting them.

Lean can be too forgiving

By default, if a fresh variable shows up free somewhere, Lean will implicitly declare it so that the whole expression makes sense. This may be convenient in some cases but it can also help you shoot yourself in the foot: consider what happens if you want to refer to something you have already defined, called oi and you end up mistyping it as ol. The desired behaviour of Lean in this case is surely to complain that ol has never been declared/defined and has no idea what you are talking about, helping you spot the typo. Instead, the default behaviour is to act as if it is some new name that you want to use and implicitly declare it to be of the inferred appropriate type. I strongly urge you to deactivate this, thus: set_option autoImplicit false. Note that you can turn it back on by replacing false with true when it is convenient.

I liked these option, what else is there?

To see and search options use #help option.

Non-constructive witchcraft

Try to prove your theorems without appealing to the following sorceries. Consider that the moment a proof uses such an invocation it becomes tainted (or tinted) with a non-computational/non-constructive stain. Any proof that uses such proof ends up being contaminated as well.

⛤ LEM (Law of Excluded Middle)

LEM is the assumption that all propositions are decidable, i.e., that for any P you can consider that you have P ∨ ¬P. Invoking LEM on P, we obtain P∨¬P, which we then normally use (as the disjunction that it is) to separate in cases.

Text: «(By LEM) We separate in cases P and ¬P. Case P: […]. Case ¬P: […].»

Lean: by_cases h : P where P is the proposition we choose and h the label of the corresponding hypothesis in each case.

⛤ RAA (Reductio Ad Absurdum)

Having any proposition $P$ as a goal, suppose its negation ¬P and try to obtain a contradiction (⊥). (And then lie about what it is you actually proved: you have proven ¬P ⇒ ⊥ (i.e., ¬¬P), and yet you are claiming you have proven P.)

Text: «I will show that assuming not P, we reach a contradiction.»

Effect: You gain ¬P on your givens; the goal becomes ⊥.

Lean: by_contradiction hboom where hboom is the label we choose for this given. Lean also understands the abbreviation by_contra.

⛤ CONTRA (Contrapositive)

Having to prove that P⇒Q, assume that ¬Q and prove ¬P. (And then lie about what it is you actually proved: you have proven ¬Q⇒¬P, and yet you are claiming you have proven P⇒Q.)

Text: «I will show the contrapositive.»

Lean: contrapose.

Effect: Your original goal P⇒Q changes for the (weaker) ¬Q⇒¬P.

Tip: there is also contrapose! which will also push negations inwards (push_neg).

Tip: there is also contrapose h which will: move a hypothesis h to your goal as a premise, swap the goal with its contrapositive, introduce the premise of the new goal (i.e., the negation of the original goal in place of h. In other words it is you saying: it is enough to show that the negation of my goal implies the negation of this (h) assumption.

Now what?

Want to do more math in Lean? See [Theorem Proving in Lean][lean-tpil] and [Mathematics in Lean][lean-mil]. Want to lean how to program (in) Lean, create your own tactics, write your own programs, etc.? See [Functional Programming in Lean][lean-fpil].