Lean 4 Beginner Tutorial

Go to some directory and type:

replace "butters" with the project name. This will create a new butters subdirectory. Go inside it, and type:

This will take some time and is needed in order to setup Mathlib4. Now start VSCode:

It could need a "cache rebuild" (see the messages.) Then we are ready. The first time it may take a lot of time to "react".

From this point, *.lean source files may be created to contain proofs. We usually add the following import at the beginning of each Lean source file:

We’ll begin with the proof of a trivial "existential" fact:

This assertion may be formally written this way:

The sorry "wildcard" signals that we do not have (yet) a proof for the assertion. In complex proofs some parts may be marked with sorry in order to allow their incremental development.

For proving the existence, we should provide a "witness" term, in this case consisting of a value 5, and a proof that its self product gives 25:

The term ⟨5, h⟩ is a term which uses that witness, where h is an auxiliary proof for the existentially applied formula instantiated to the witness 5.

The h auxiliary proof is built using the rfl tactic which asserts that two terms identified as "the same" are equal; the technical name for this identification is "definitional equality", also known as "judgmental equality" and as "computational equality".

In our example, the product 5 * 5 may be reduced to the simpler number 25 (which in turn may be expressed as 25 applications of the "successor" function to zero, as usually explained in lambda calculi.)

Note that since rfl is a tactic, it is written after the by keyword.

Tactics may be written in the following lines after by, but must have a higher indentation:

The rfl tactic https://leanprover-community.github.io/mathlib4_docs/Std/Tactic/Relation/Rfl.html depends on the rfl theorem (propositional definition) documented in https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#rfl

The related Eq.refl is similar to rfl but expects an explicit argument. Below we use #check to inspect the type of an expression (see the response in the "Lean Infoview" window of VSCode):

A more general way to prove assertions consists in "applying" theorems with apply; the rfl tactic is an abbreviation of the application of the rfl theorem, but there is also a related refl theorem, and the "equality" class Eq also provides a reflection theorem:

From the Lean documentation: "The norm_num tactic is specifically designed to handle numerical proofs. It cannot be used to simplify or prove goals involving non-numerical expressions or types."

The simp tactic is a more powerful one which includes the norm_num functionality:

The proofs with a name are called theorems or lemmas:

Note the exact tactic which is a stricter version of apply, requiring an almost perfect match of the goal to the theorem. Later will see that apply allows the "partial" application of theorems to a goal, effectively transforming it into (hopefully) simpler ones.

The theorems present distinct proofs of the same assertion. Lean considers them as definitionaly equal:

That means that the usage of any of these theorems may be used indistinguishably; this notion is known as "proof irrelevance".

The theorem names may be used as proof terms. Here we use ex_aux1 in order to trivially prove the auxiliary hypothesis h:

But h is no longer needed:

That is, h was a theorem created "on the fly" inside the example proof (whose scope was also restricted to the proof.)

Lean is keen to deduce the arguments from the usage context; the underscore works as a wildcard to hint such a deduction:

Given the witness 5, it is possible to employ an abbreviation for inserting tactics as needed:

This tactic may be employed to provide the witness and automatically create the associated proof term:

Note that use 5 is not a proof term but the application of a tactic; that is the reason it must be prefixed by the by keyword.

In the following example, the witness 5 is not enough for Lean to build the proof term:

After the use 5 there is a remaining non trivial goal (it can be seen just moving the cursor after use 5 and checking the informational view in VSCode in the "Tactic state" zone):

In the previous example the remaining goal was the trivial 5 * 5 = 25 which was automatically accepted being a definitional equality.

Now, the remaining goal may be solved with a further application of the norm_num or simp tactics:

Now let’s try to provide a proof without appealing to norm_num nor simp. After use 5 the remaining goal:

is the conjunction of the assertions 5 * 5 + 1 = 26 and 5 > 4. The constructor tactic divides this goal into the constituting subgoals. The first one is a definitional equality as discussed previously, so it may be solved with the rfl tactic. The second one is definitionaly equivalent to

Also, five is the successor of four: 5 = Nat.succ 4, so we may apply the theorem Nat.lt.base:

The closing application may be made more clear with the exact tactic, which by itself does not try to deduce the parameter of Nat.lt.base, so it must be explicitly provided (that is, unlike the apply case, it is not enough to specify exact Nat.lt.base without the 4.)

The show tactic is used to provide a hint to Lean (and to an ocassional reader) about the current goal or subgoal which is being proved. In the following proof it is used to detail the subgoals created by the constructor tactic:

Alternatively to constructor the And.intro (introduction rule) may be applied:

Since the rfl and exact solve the two goals "derived" from the current one, it would be handy to indent the formers with respect to the later, but this is not allowed (since the derived goals replaced the conjunction at the same "level".) The "dot" syntax may be employed to force the indentation:

Consider the following trivial and equivalent proofs for a statement on three real numbers (which is valid on any ring):

The add_comm_sub points to a theorem which relates the addition, the subtraction and the commutativity:

Note that the theorem body may be obtained by typing #print add_comm_sub.

Now, if we are to deal with several real variables, instead of declaring their types in every example, we may set their type in a region of the file using the variable keyword inside a section…​end block:

A more interesting question is how we discovered the add_com_sub theorem? besides navigating in the Mathlib documentation, we may ask Lean to provide a hint for suitable theorems using the syntax:

in the Lean infoview, we obtain this helpful message: Try this: exact add_comm_sub a b c.

In line with these suggestions, regarding the Lean tactics (like apply) a good heuristic may be found in the "Hitchhiker’s Guide to Logical Verification":

Now we’ll prove a standard algebraic identity from elementary school: Given the reals a and b, the following holds:

We’ll use the rewrite or rw tactic, in which the proof goal is gradually rewritten using auxiliary equality theorems like the previously mentioned add_comm_sub. That is, rw [t] assumes there is a t theorem with the form A = B (also for A ↔ B); the proof goal must have some subexpression matching the "A" pattern, and a new goal emerges using the "B" pattern as replacement. The syntax rw [←t] looks for some subexpression following "B" to be replaced for "A".

The next proof is a bit long but not very difficult to follow. By the way, we are not asserting that this is the minimal one:

The "right hand side" of the goal is rewritten as needed, and its value is shown as comments. In practice, the reader should follow the proof hovering the cursor over the rewriting theorems and looking the changing goal in the "Lean Infoview" panel. In the following proofs of this document we will not show the goal transformation at this detail level, so the user should get used to read the Lean Infoview.

The proof expands the products of the second member of the identity using mul_add, sub_mul and add_sub. The resulting expression contains terms obviously cancelable.

Using pow_two we convert the a ^ 2 to a * a (in two places) and later the same conversion is done for b. Then ←pow_three converts a * (a * a) into a ^ 3 (note the arrow to apply the conversion in reverse direction); the same is done for b.

Sometimes a theorem pattern appears at several points of the goal expression, and rw applies to the first one. If this is not desired, it is possible to provide some arguments to the theorem to disambiguate the target replacement subexpression; see for example the usage of sub_right_comm.

Finally, a number of theorems are applied in order to reorder the terms which is a bit convoluted since we have additions, subtractions and those operations are binary, so there are many implicit parenthesis which force a careful reassociation con commutation. The key insight is to ask Lean for the required theorems using apply? as previously explained.

The following proof is even more involved but may be more interesting. It rewrites the binomial a ^ 3 - b ^ 3 in order to achieve the factored expression of the second member. We prove a couple of helper hypothesis (which may be considered internal lemmas) using have:

Note that the add_and_sub_to_diff hypothesis is valid for any three expressions of real type, so we define as processing three (generic) real numbers to be provided as parameters. Just for clarity, we used the new variable names x, y and z (though it could be fine with a, b and c as shown in h_dif_sq.) Note the use of rfl in the the proof, which leverages the fact that a - b is the same as a + (-b) by definition.

Using this hypothesis, another one is proved: a ^ 2 - b * b = (a + b) * (a - b), and finally the identity is proved with its help.

A third variant uses the calc tactic which is used to prove statements of the form A = B by a chain of partial proofs of A = X1, X1 = X2…​ XN = B.

Note that the proof of h_dif_sq employs calc as a proof term and not as a tactic (so no by keyword is present before it.) That is, calc works as a tactic and as a proof term.

Finally, the best method for the present case is to employ the ring tactic, which automates proofs for expressions involving rings:

As a practice for the reader, let’s prove a related theorem:

Some proofs below:

The last proof leverages the linarith tactic, which is used to verify if an equality or inequality may be satisfied using linear arithmetic operations based in the context hypothesis. Using linarith by default employs all the available hypothesis in order to prove the target, but may get too slow if there are many of them. In that case, it is faster to use linarith only […​] for restricting its process to the specified hypothesis; also, is good for understanding the facts that are being used by the tactic.

Now consider the previous identity for the naturals:

In standard math this requires that a ≥ b, otherwise the subtraction is undefined. In Lean such subtraction is allowed but defined as zero:

So, this identity is valid in Lean even without needing to add the extra hypothesis a ≥ b.

We may not use the ring tactic since the naturals do not form a ring. There is a ring_nf tactic which is a bit more powerful and may deal with simple cases involving subtractions with naturals when there is no need to introduce the mentioned extra hypothesis. We combine these tactics in the following proof, which transforms the second member until we get "simple" cancelable terms to apply ring_nf:

Lean provides a divisibility operator '∣' which is obtained typing a backslash followed by the pipe key: \|:

From an equality like c * a = b it follows that a divides b and that c also divides b. There is a theorem which helps in the first case:

It is trivial to prove the second case:

We need this implementation since there is no corresponding theorem Dvd.intro_right (at least in the current version of Mathlib.) Another approach consists of implementing a new theorem dvd_intro_right1 for further usage:

Having to write dvd_intro_right1 5 20 4 h is cumbersome, since all the variables could be deduced from the h expression. A better alternative is to specify the variables in braces {…​}, which is a hint to Lean to deduce their values from the accompanying expressions (like h); so the proof consists in the term dvd_intro_right2 h:

Now the variables are "implicit". As another iteration we may create a section declaring the implicit variables with braces, which is useful when there are several theorems leveraging such declarations:

In Lean there is a function gcd for the greatest common divisor; also, there is a definition for coprimality corresponding to gcd m n = 1:

Let’s review the Nat.Coprime.dvd_mul_right theorem:

The type is of biconditional form, from which it is possible to extract the conditional forms in "left to right" direction using the mp suffix, and the "right to left" direction with the mpr suffix. The following theorems illustrate the mp direction (assume that they are in a section with the implicit a, b, c, and d variables):

At this point we recommend the great Logic and Proof online book, which at this time is based on Lean 3: https://lean-lang.org/logic_and_proof/; the basics of "natural deduction" and "propositions as types" ideas are described in detail.

Here we’ll not explain this topic but leave a brief citation for the interested:

In Lean the propositions we want to prove are codified by a type; the proof for any of these propositions correspond to a term of that type.

So the existence of a term of the type corresponding to the proposition does mean that a proof is available, hence is valid (or in an informal sense, simply "true".) There could be more than one term with the proposition’s type, which means that more than one proof is available for it.

Converselly, when there is no corresponding term for the proposition’s type, then the proposition is not (yet) proved.

In order to prove that the proposition is not valid (i.e. that is "false"), we must prove its negation; that is, for the proposition P (with type P) we must provide a term with type ¬P.

The type which contains the proposition’s types is Prop (a type of types.) So the elements of Prop are an infinity of types corresponding to the propositions, which may be proved or not.

As previously commented the proposition’s types which have at least one proof (term) may be considered valid or "true", and those which (provably) not, may be regarded as not valid or "false". But this is just an informal interpretation which is not codified in Lean.

Anyway, Lean provides a Bool type having exactly the two values true and false, which may be used to build of terms in the same way as numeric constants and variables.

The authoritative Theorem Proving in Lean 4 has also a chapter which shows how to deal with logic arguments in Lean 4: https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html ; here we do a quick review mostly oriented to the available syntax which (in our opinion) is daunting at first.

Since we are dealing with classical logic, we may leverage this section to introduce basic set theory: the set operations are defined in terms of logical connectives which relate the element ownership relation.

This is a basic theorem for which we provide several term proofs:

The And.left and And.right structure members provide the conjunction components (where And.left conj may be abbreviated as conj.left, same with And.right.)

Note the ⟨…​ , …​⟩ abbreviated syntax to "build" a conjunction, and the usage of .1 and .2 to mean .left and .right.

Next we introduce proofs using tactic mode leveraging the And.comm theorem and the previously introduced constructor tactic:

The following examples prove the equivalence of the commuted conjunctions using previously reviewed methods. Note the usage of the @ prefix to switch the implicit arguments of And.comm into explicit ones:

Now we show the commutativity of set intersection; take a moment to compare with the equivalence of conjunctions:

The next examples prove the disjunction commutativity with explicit terms and tactic mode:

Now we prove a bit more complex assertion with a proof term and with tactics:

The corresponding set statements are also proved (this is an exercise taken from Mathematics in Lean at https://leanprover-community.github.io/mathematics_in_lean/C04_Sets_and_Functions.html ):

Another important relation is proved by a proof term and by tactics. Note that the implication associates to the right, so p → q → r is the same as p → (q → r):

The following proof illustrates the fact that ¬p is defined as p → False:

For sets, the "set complement" of a set corresponds to the elements which don’t belong to such set:

A corresponding set-theory assertion using the set complement for the negation:

The following theorem is proved in several ways. The first two makes use of the law of the excluded middle (em) which states that for any proposition p, then p ∨ ¬p holds; we provide a proof term and then a tactic proof.

The following proof makes use of the propext axiom and a theorem about equality. From Core.lean:

"The axiom of propositional extensionality. It asserts that if propositions a and b are logically equivalent (i.e. we can prove a from b and vice versa),then a and b are equal, meaning that we can replace a with b in all contexts."

The last proof makes use of the tauto tactic which splits the assumptions' connectives solving the goal by applying the simplified assumptions and reflectivity:

A corresponding set theorethical statement is proved below:

Note that the hypothesis (xInU: α) is needed since the assertion is valid only if the α type is not empty (else, the only existing set would be empty as its complement.)

Lean provides a "predicate" Nonempty which may be used to signal that α is not empty, so a "default value" of this type may be produced.

Now, for illustration below we provide some (sub-efficient) proofs for another logical statement. The right triangle ▸ provides a rewriting capability suitable for building proof terms:

In this section we add some examples involving quantifiers. These examples were taken from the Logic and Proof book (previously referred.)

We’ll define some predicates to be employed in the examples; they are propositions which hold for some domain objects (of some type); that is, given some object a : α then a predicate P signals that some property holds for a (that is, P a may or not be the case.) So, the valid propositions (Prop) are a function of the α typed objects:

The universal quantifier presents an structure similar to an implication, so it may be built from an intro block. Also, it may be "eliminated" providing a concrete element following a pattern similar to modens ponens; in the first example the quantifier is eliminated in order to deal with a plain conjunction from which its left (.1) member is used to build the required proof term. In the second example of the quantifiers in the hypothesis are also eliminated using the witness w: α term created by the previous intro:

The existential quantifier was previously explored; here we add more examples:

As explained previously, the negation is just an implication to False:

The set theory may be worked with quantifiers and the ownership relation. Here a propositional example and a corresponding statement in set theory using the universal quantifier:

Another one dealing with logical negation and set complement:

The following example deals with a binary predicate:

The next example introduces a function f:

Let’s prove the following statement for naturals a, b, c and d:

One proof is based in the and_iff_not_or_not which corresponds to a "de Morgan" law; also, the x < y propositions are rewritten as ¬ (y ≤ x) with lt_iff_not_ge:

As an exercise we now provide a more "structural" proof which in some sense is more general (even if longer in this instance); the constructor tactic was reviewed before for "splitting" goals in conjunctive form, but it also may be employed in biconditional goals transforming them into two reciprocal conditionals:

Both conditionals are proved as usual thru the introduction of an assumption with "intro". Observe the proof of negated arguments by constructing a False (or contradiction), since ¬ p is defined as p → False, following a common pattern in natural deduction.

Also, note the use of the Or.inl and Or.inl constructors corresponding to the "or introduction" natural deduction rules. Later we’ll leverage these constructors in order to prove disjunctive sentences with "proof by cases".

In the following variant of the last example, for the first conditional we introduce the contradiction tactic as an alternative to providing an explicit construction of False (like exact hor adOrcb); the contradiction tactic looks for contradictions between all the current context hypothesis.

In the reverse conditional, after the final constructor we have the ¬(a < d) and ¬(c < b) goals; just for illustration, both are solved with distinct tactics oriented to pattern matching: the already described cases is applied to the hand conjunction in order to extract the first member had from the And.intro constructor. The match tactic provides the ⟨a, b⟩ syntax to extract the conjunction components:

The next iteration introduces a small variant for the first conditional with the by_contra tactic, which converts the goal to a negated hypothesis, and replaces the former for False. The second use of by_contra does not introduce a named (negated) hypothesis as in the previous case, but it may be applied to Or.inr by the apply …​ ; assumption pattern, which tries with all the context hypothesis, even the unnamed ones.

The same pattern for unmamed hypothesis is applied in the reverse conditional.

As the last iteration, we will show how to "repeat" some blocks of the proof. We note that for each conditional there are two similar blocks of tactics whose repetition may be automated:

The first conditional is a bit more complex since two distinct constructors are applied: Or.inl and Or.inr. The first | t1 | t2 …​ pattern instructs Lean to try the tactics t1, t2…​ until the first succeeds. As saw in the previous example, in both conditionals two repetitions are needed to satisfy the corresponding goals.

For this example, introducing repetitions may be overkill; in our opinion, the main problem with these "tactic combinators" is that the proof context changes are more difficult to follow in the Info View.

As another application we now review the proof by contrapositive:

The not_imp_not theorem provides a form of this argument; its "symmetric" is also easy to obtain:

A generalization of this argument corresponds to (p ∧ r → ¬q) ↔ (p ∧ q → ¬r) which we’ll prove now as theorem gen_cpos; we’ll prove one direction in an auxiliary theorem (or lemma) named cpaux:

In logic arguments usually suffices to provide proof terms, as shown in the following equivalent version:

As usual, Mathlib provides a tactic for this kind of argumentation named contrapose which converts p → q into ¬q → ¬p (and adds some basic transformation like "pushing the negations"); the reverse way is obtained with the contrapose! variant. The following listing uses it to provide another proof for the same theorem; observe the syntax ⟨p,q⟩ to build a conjunctive expression:

The contrapose tactic may be applied to a hypothesis, in passing switching places with the goal. The following proof uses this pattern:

Note the pattern matching of the transformed expressions: those are made (just for illustration) with the have and rcases tactics.

Using all these ideas we’ll prove a theorem with a "negative" statement:

As an illustration of the previously generalized contrapositive argumentation, we’ll first prove an equivalent theorem:

"If the positive naturals a, b, c, and d are such that gcd(b,c) = 1 and a * b = c * d, then it is not true that either of a < d or c < b."

By de Morgan: ¬ (a ∨ b ) ↔ ¬a ∧ ¬b, and since by definition ¬ (x < y) is the same as y ≤ x, then we rewrite the statement this way:

Now follows a proof of this theorem named eqAndDes which is based in two lemmas, which also rely in two previous theorems:

Using this result is easy to prove the original "Negative statement". For this we rearrange the last theorem statement using the generalized contrapositive argument: the equation a * b = c * d will be switched to the conclusion in negated form, and the previous conclusion returns as an hypothesis in its original (disjunctive) form:

The inequality a * b ≠ c * d is the same as ¬(a * b = c * d) so is also the same as a * b = c * d → False; then the conditional is proved introducing the h hypothesis which "activates" the equation, and the previous eqAndDes theorem may be applied. It is clear that this results in d ≤ a ∧ b ≤ c (assumption hx in context.)

The example showcases a proof by cases used in order to "split" the disjunction hor: the cases tagged by inl and inr (corresponding to the Or.inl and Or.inr constructors) result in new hypothesis had and hcb (for a < d and c < b respectively.) Both contradict the previously obtained hx by applying the "antisymmetry" of the ordering in the naturals:

That is, both cases of the disjunction result in False, as required by the negated statement.

The next variant uses the by_contra tactic which and the previous deMorgan1 theorem:

The last two lines may be replaced by:

The following is another version of the same example, but now we make explicit use of the proof by contrapositive theorem gen_cpos:

To apply gen_cpos.mp we need to have a goal in conditional form, which we construct in the imp hypothesis. After proving it (leveraging eqAndDes, the contrapositive), the original theorem is easily proved. The constructor <;> assumption pattern applies the first tactic, then the second one is applied on each of the generated goals (the conjunction components in this case are in the context hypothesis.)

Now we provide another application of gen_cpos which avoids the auxiliary conditional imp. In this case, we construct an explicit expression with a direct application to gen_cpos; as there is no suitable conditional in the context, we must provide explicitly its arguments (or at least some of them.)

But the arguments are marked implicit for gen_cpos (remember they are {p q r : Prop}), so it is an error to provide them in explicit form.

As shown before, for this situation Lean provides the @ prefix to switch the implicit arguments into explicit ones. So we provide gcd b d = 1, a * b = c * d and a < d ∨ c < b into @gen_cpos.

Note that in this particular case, the last two arguments to @gen_cpos may be replaced by a wildcard (underscore) and Lean is able to deduce its contents by the context.

As another example prove that

Note that this is a "negated" statement to prove, in which we attempt to achieve False:

The key theorem is LE.le.eq_or_gt employed to establish a disjunction from an inequality:

The example’s inequality is satisfied for any natural, even zero, so the hq hypothesis is not needed. Now we start from the Nat.eq_zero_or_pos theorem which states:

We’ll use this example to show a slight variant for the cases tactic which uses the case keyword and excludes the with:

When there is no need for the case variables, it is possible to exclude the case …​ statements (see for example https://lean-lang.org/theorem_proving_in_lean4/tactics.html) for more details. In our opinion, the existence of these syntactic variants is confusing when arguably don’t provide substantial ergonomic gains nor substantial comparative functionality.

The match tactic is a variant which also allows the evaluation of several cases. In this example it may provide a more straightforward proof:

The following proof introduces the by_cases tactic: this requires a new hypothesis which must be proved for whether it is true or false:

Here we introduce the cases q = 0 and q ≠ 0; the former is easy to prove by rewriting; the later is forked in two subcases q = 1 and q ≠ 1; again, the former is proven in the same way, remaining the later which (at last) is forked in the cases q = 2 and q ≠ 2.

The surviving case corresponds to q ≠ 0, q ≠ 1 and q ≠ 2, which allows the direct application of the theorem

to conclude 3 ≤ q. From this we may follow the previous solutions, but to show another way we prove that 9 ≤ q ^ 2 with:

In order to help Lean to discover our intentions, we hint that the real proof is for 3 ^ 2 ≤ q ^ 2 with show.

As a slight variation the following proof uses the same h name for the cases, so they become non directly addressable. If employs the common pattern by apply theorem <;> assumption, which applies the context assumptions to the theorem as suitable:

For the second inequality we now rewrite with Nat.pow_two to get 3 * 3 ≤ q * q and apply Nat.mul_le_mul as before.

Now for another "trivial" example:

The following proof is built from the trichotomy law: for naturals a and b it is true that a < b ∨ a = b ∨ a > b.