Logic in Lean 1

I am going to learn the basics of logic and tactics required for writing proofs in Lean. For my textbook, I am continuing with "Introduction to Lean from Scratch: Hands-on Development of Formal Mathematics Libraries" (a guide published in Japan). In this post, we will cover fundamental logical concepts—propositions, implications, and negations—along with how to prove them.

1. Propositions

1.1 The Prop Type

In Lean, a proposition is represented by the Prop type. A proposition is a statement that can be determined to be either true or false. Let's check this with the following code:

#check Prop
#check (1 + 1 = 3)

1.2 Predicates

A predicate is a proposition that depends on a variable. Take a look at the following example. Since whether "n+3 equals 39" holds or not changes depending on the value of n, this statement is considered a predicate.

#check (fun n => n + 3 = 39)

1.3 Truth Values vs. Prop

#check True
#check False

True and False are not boolean values; they are propositions. Be careful with the distinction: lowercase true/false are boolean values (the Bool type), whereas uppercase True/False are propositions (the Prop type).

2. Simple Proofs

2.1 Self-Evident Propositions: The trivial Tactic

When proving a self-evident proposition, we use the trivial tactic. This tactic automatically tries a pre-registered list of multiple tactics one after another. It is used when a goal is, quite literally, trivial.

example : True := by trivial

2.2 Deriving a Conclusion from an Assumption: exact and assumption

If we already have a proof h : P for a proposition P, we can naturally show that P holds. Let's write a proof for this:

example (P : Prop) (h : P) : P := by
  exact h

The exact tactic takes an existing premise or a combination of functions to construct an object that matches the exact type of the goal, offering it up by saying, "Here is the proof!" In this case, since h is precisely the proof of P, the proof is complete.

The same operation can be achieved using the assumption tactic:

example (P : Prop) (h : P) : P := by
  assumption

3. Implication

3.1 What is Implication?

An implication represents "if P, then Q" and is written as P → Q. Intuitively, it means that if P holds, then Q must also hold.

Its logical meaning works as follows:

• If P holds and Q holds → P → Q is true
• If P holds but Q does not hold → P → Q is false
• If P does not hold → P → Q is automatically true (if the hypothesis is false, the implication is true regardless of the conclusion)

Let's verify this in practice:

#eval True → True    -- true
#eval True → False   -- false
#eval False → True   -- true
#eval False → False  -- true

3.2 Utilizing Implications: The apply Tactic

To use an implication in a proof, we use the apply tactic. If you have an assumption h : P → Q and your goal is Q, running apply h will change your goal to P. Let's try it out:

example (P Q : Prop) (h : P → Q) (hp : P) : Q := by
  apply h
  apply hp

The example above can also be written more concisely like this:

example (P Q : Prop) (h : P → Q) (hp : P) : Q := by
  exact h hp

3.3 Right-Associativity of Implication

In Lean, implications are right-associative. This means that when multiple implications follow each other, they are grouped from the right:

example (P Q R : Prop) : (P → Q → R) = (P → (Q → R)) := by
  rfl

Therefore, P → Q → R means exactly the same thing as P → (Q → R).

3.4 Proving an Implication: The intro Tactic

An essential tactic for proving an implication is intro. By using intro, you can move the antecedent P of an implication "if P, then Q" into your local context as a hypothesis, leaving you with only Q to prove. The argument given to the tactic assigns a name to this hypothesis; in the example below, it becomes h : P:

example (P Q : Prop) (hq : Q) : P → Q := by
  intro h
  exact hq

4. Negation

4.1 The Definition of Negation

Finally, let's talk about negation. Negation is represented by the ¬ symbol. Evaluating it behaves exactly as you would expect intuitively:

#eval ¬ True   -- false
#eval ¬ False  -- true

4.2 The Relationship Between Negation and Implication

Consider the classic mathematical reasoning: "Assuming P leads to a contradiction, therefore P is false." In Lean, this concept is expressed as follows:

example (P : Prop) : (¬ P) = (P → False) := by
  rfl

In other words, the negation ¬ P is definitionally identical to P → False. It simply means that if P were to hold, it would derive a contradiction (False).

4.3 Anything Follows from a Contradiction: The contradiction Tactic

This introduces an important principle. If your hypotheses contain both P and ¬ P, you have a clear contradiction. Once a contradiction exists, you can prove any arbitrary proposition. Lean provides the contradiction tactic specifically for this scenario:

example (P : Prop) (hnp : ¬ P) (hp : P) : False := by
  contradiction

The behavior of this tactic is equivalent to doing the following:

example (P : Prop) (hnp : ¬ P) (hp : P) : False := by
  apply hnp  -- Since ¬ P is P → False, proving P will yield False
  exact hp   -- P is proven by hp

4.4 Changing the Goal to Proving a Contradiction: The exfalso Tactic

No matter what your current goal is, you can use the exfalso tactic to change the proof's goal to "proving a contradiction (False)":

example (P Q : Prop) (hnp : ¬ P) (hp : P) : Q := by
  exfalso -- ⊢ False
  contradiction

This allows you to take an indirect proof approach (reminiscent of proof by contradiction): instead of proving the proposition directly, you show that assuming its negation leads to an absurdity.

Summary

We covered the following key points regarding the foundations of logic in Lean:

Code Repository

The code covered in this post is available in the following repository:

• https://github.com/ringring-creator/LearnLean

It documents my ongoing learning process, so please feel free to use it as a reference!