Logic Gates

This is the level where Lean stops being “a functional language” and starts being a proof assistant. The whole idea rests on one move: statements are types, and proofs are values of those types.

Learning Goals

• Explain the difference between Bool and Prop in one sentence.
• Read theorem name : Statement := proof as an ordinary definition.
• Prove simple facts with rfl, decide, and trivial.
• Build and take apart ∧, ∨, and →.
• Understand why implication is literally a function type.

Two Different Worlds

Lean draws a sharp line between something you compute and something you prove. Both look like “true or false” at a glance, but they live in different universes.

1#check true          -- Bool.true : Bool
2#check (2 + 2 = 4)   -- 2 + 2 = 4 : Prop
3
4#check Bool          -- Bool : Type
5#check Prop          -- Prop : Type

1-- Bool: computed
2def isEven (n : Nat) : Bool := n % 2 == 0
3#eval isEven 4    -- true
4#eval isEven 7    -- false
5
6-- Prop: proven
7def IsEven (n : Nat) : Prop := n % 2 = 0
8#check IsEven 4   -- IsEven 4 : Prop
9
10theorem four_is_even : IsEven 4 := rfl

The Central Idea: Proofs Are Values

Look at that last line again. theorem four_is_even : IsEven 4 := rfl has exactly the shape of an ordinary definition: name : Type := value. That is not a coincidence or a pun. In Lean:

• A proposition is a type.
• A proof is a value of that type.
• To prove a statement is to construct a value of the corresponding type.

So 2 + 2 = 4 is a type, and rfl is a value that inhabits it. A false statement like 2 + 2 = 5is also a perfectly good type — it just has no values, and no amount of cleverness will produce one. “Unprovable” and “empty type” are the same thing.

Your First Proofs

rfl — true by computation

rfl stands for reflexivity: it proves a = b whenever the two sides reduce to literally the same thing. Lean runs both sides and checks.

1example : 2 + 2 = 4 := rfl
2example : "ab" ++ "c" = "abc" := rfl
3example : [1, 2].length = 2 := rfl

example is an anonymous theorem. Use it when you want to check something without cluttering the namespace with a name you will never reference.

decide — let Lean do the case check

Many propositions are decidable: there is an algorithm that settles them. decide runs that algorithm and, if the answer is yes, converts the result into a real proof.

1example : 2 + 2 = 4 := by decide
2example : 7 % 2 = 1 := by decide
3example : ¬(1 = 2) := by decide
4
5-- You can also just ask for the Bool answer
6#eval decide (2 + 2 = 4)   -- true
7#eval decide (2 + 2 = 5)   -- false

One wrinkle worth knowing now: decide cannot see through a def on its own. If you wrap a proposition in a definition, unfold it first.

1def IsBig (n : Nat) : Prop := n > 100
2
3-- theorem thousand_is_big : IsBig 1000 := by decide     -- fails!
4-- "failed to synthesize Decidable (IsBig 1000)"
5
6theorem thousand_is_big : IsBig 1000 := by
7  unfold IsBig   -- goal becomes  1000 > 100
8  decide

Why You Cannot #eval a Proposition

#eval (2 + 2 = 4) is an error, and now you can say precisely why. A proposition is a type, and types are not runtime values you can print. What you can evaluate is decide (2 + 2 = 4), which is the Bool that the decision procedure produces.

The bridge runs the other way too. When you use a Bool where Lean expects a Prop, it silently inserts = true.

1#check (isEven 4 = true)     -- isEven 4 = true : Prop
2example : isEven 4 = true := by decide

The Logical Connectives

Each connective has a proposition-building form and a corresponding way to construct or consume its proofs.

1#check (1 = 1 ∧ 2 = 2)    -- and
2#check (1 = 1 ∨ 1 = 2)    -- or
3#check ¬(1 = 2)           -- not
4#check (1 = 1 → 2 = 2)    -- implies
5#check (1 = 1 ↔ 2 = 2)    -- if and only if

Type these with \and, \or, \not, \to, \iff.

And: a pair of proofs

To prove P ∧ Qyou supply a proof of each side — and the syntax is the same anonymous constructor you used for structures in Level 4, because And is a structure.

1theorem both : 1 = 1 ∧ 2 = 2 := ⟨rfl, rfl⟩
2
3-- Taking one apart: .left / .right, or .1 / .2
4theorem left_of  (h : 1 = 1 ∧ 2 = 2) : 1 = 1 := h.left
5theorem right_of (h : 1 = 1 ∧ 2 = 2) : 2 = 2 := h.2
6
7-- Swapping the two halves
8example (p q : Prop) (h : p ∧ q) : q ∧ p := ⟨h.2, h.1⟩

Or: a choice of side

To prove P ∨ Q you must say which side you can prove. Or.inl takes the left, Or.inr the right.

1theorem eitherL : 1 = 1 ∨ 1 = 2 := Or.inl rfl

Implication is a function

Here the propositions-as-types idea earns its keep. A proof of P → Q is a function that converts any proof of P into a proof of Q. Not “analogous to” a function — the same arrow, the same lambda, the same rules you learned in Level 3.

1theorem impl : 1 = 1 → 2 = 2 := fun _ => rfl
2
3-- In tactic mode, intro is how you introduce the argument
4example (p q : Prop) (hp : p) (hq : q) : p ∧ q := by
5  exact ⟨hp, hq⟩

And since implication is a function type, ∀is a function type too — one whose return type is allowed to mention the argument.

1theorem all_add_zero : ∀ n : Nat, n + 0 = n := fun _ => rfl
2
3theorem exists_big : ∃ n : Nat, n > 3 := ⟨4, by decide⟩
4-- To prove an ∃ you supply a witness and a proof about it.

Tactic Mode

Everything above was written as a direct term. The by keyword drops you into tactic mode, where you build the proof by giving instructions instead. Both produce the same underlying value.

1example : 1 = 1 ∧ 2 = 2 := by
2  constructor    -- split the ∧ into two goals
3  · rfl          -- prove the first
4  · rfl          -- prove the second
5
6example (a b : Nat) (h : a = b) : b = a := by
7  rw [h]         -- rewrite using the hypothesis

Practice

1def IsPositive (n : Int) : Prop := n > 0
2
3#check IsPositive 3     -- IsPositive 3 : Prop
4
5theorem three_pos : IsPositive 3 := by
6  unfold IsPositive
7  decide

1def isVowel (c : Char) : Bool :=
2  c == 'a' || c == 'e' || c == 'i' || c == 'o' || c == 'u'
3
4#eval isVowel 'e'   -- true
5#eval isVowel 'z'   -- false

1theorem small_and : 2 < 3 ∧ 3 < 4 := ⟨by decide, by decide⟩
2
3theorem and_swap (p q : Prop) (h : p ∧ q) : q ∧ p := ⟨h.2, h.1⟩

Common Mistakes

• Trying to #eval a proposition. Wrap it in decide.
• Using decide on a statement about all naturals. Infinite case checks do not terminate. You want induction.
• Confusing = with ==. The first builds a Prop, the second computes a Bool.
• Expecting decide to unfold your definitions. It will not. unfold first.

Check Yourself

• Is 2 + 2 = 5 a valid Prop? What does it mean for it to be false?
• What kind of value is a proof of P → Q?
• Why does decide fail on ∀ n : Nat, n + 0 = n?
• How do you extract the right half of a proof of P ∧ Q?