8.1.1. Equality Propositions🔗

The familiar equality operator = is a (binary) function that returns a Prop. The expression n = m is notation for Eq n m. Because Eq can be used with elements of any type, it is also polymorphic:

Eq.{u_1} {α : Sort u_1} : α → α → Prop

Equality turns out to be an inductively defined proposition, with a single constructor, Eq.refl, standing for the proof that anything is equal to itself. Recall from the Tactics chapter that the constructors of an inductive type are injective and disjoint, and that injection and contradiction let us exploit those facts about hypotheses concerning Nat, List, and so on. The very same injectivity and disjointness reasoning applies to a hypothesis of the form a = b. In fact, cases can carry out this reasoning directly on an equality hypothesis, without our having to name injection or contradiction. Here are a few examples.

(This is the same injectivity fact used above by the injection tactic in succ_inj'; here cases gets us the same conclusion in a single step.)

We'll see this same disjointness principle put to use again shortly, via contradiction, to prove 0 ≠ 1 in the Falsehood and Negation section below.

As a convenience, Lean will cast booleans to propositions by equating them to true, which is why checking them against Prop succeeds. For clarity, we will generally avoid relying on these implicit casts.

false = true : Prop

true = true : Prop

8.1.2. Quizzes🔗

Nat.pred 1 = 0

Nat.pred 1 = 0 : Prop

∀ n : Nat, (n + 1).pred = n

∀ (n : Nat), (n + 1).pred = n : Prop

∀ n : Nat, n.pred + 1

fun n : Nat => n.pred + 1

fun n => n.pred + 1 : Nat → Nat

fun n : Nat => n.pred + 1 = n

fun n => n.pred + 1 = n : Nat → Prop

3 + 2 == 5 : Bool

8.2.1. Conjunction🔗

The conjunction, or logical and, of propositions a and b is written a ∧ b; it represents the claim that both a and b are true.

The infix notation ∧ is actually just syntactic sugar for And a b. That is, And is a Lean operator that takes two propositions as arguments and yields a proposition.

And (a b : Prop) : Prop

The sole constructor for conjunction is And.intro, which concludes a ∧ b given that a and b hold individually.

And.intro {a b : Prop} (left : a) (right : b) : a ∧ b

We can apply And.intro to carry out proofs.

Rather than applying the constructor, we can explicitly provide the arguments to the constructor as an exact proof.

Lean can figure out which constructor to use just from the goal's type, so we don't have to name it ourselves. This is what the tactic constructor does automatically: it applies whatever constructor builds a value of the goal's type, leaving one subgoal per argument of that constructor. Since And has just one constructor, constructor always picks it here.

We can also use Lean's anonymous constructor notation ⟨..., ...⟩, which works on constructors for proofs as well.

The tactics we've just used — constructor, applying And.intro, and the anonymous constructor ⟨_, _⟩ — all conclude a ∧ b from proofs of a and b. We say that these tactics introduce a conjunction: they derive it as a logical consequence of hypotheses we already have.

We also sometimes want to go the other way: given a conjunctive hypothesis, use it to help prove something else, by extracting the two proofs it packages together. In Lean, this is done with obtain. We say that obtain eliminates a conjunction: it takes the conjunction apart to expose the proofs inside.

You've already seen the related terms construct and destruct (or destructure), used for building or taking apart a value via its constructors — e.g., destructuring a pair in Lists. Building a proof with a constructor like And.intro is one way to introduce a proposition; taking a proof apart via its constructors, as obtain does, is one way to eliminate a hypothesis. We'll use whichever pair of terms fits the context — "introduce"/"eliminate" when talking about a connective's proof rules, "construct"/"destruct" when talking about the underlying constructors.

We can also match on h right at the point where we introduce it, instead of introducing and then destructing it:

You may wonder why we bothered packing the two hypotheses n = 0 and m = 0 into a single conjunction, since we could also have stated the theorem with two separate premises:

For this specific theorem, both formulations are fine. But it's important to understand how to work with conjunctive hypotheses because conjunctions often arise from intermediate steps in proofs, especially in larger developments. Here's a simple example:

Another common situation is that we know a ∧ b but in some context we need just a or just b. In such cases we can use an underscore pattern _ to indicate that the unneeded conjunct should just be thrown away.

Conjunctions come with their own built-in projections, .left and .right, which we can use instead of pattern matching.

Finally, we sometimes need to rearrange the order of conjunctions and/or the grouping of multi-way conjunctions. We can see this at work in the proofs of the following commutativity and associativity theorems.

The anonymous constructor allows us to write a much shorter proof.

In the following proof of associativity, notice how projections can be chained in sequence to obtain components of nested conjunctions. Complete the proof.

8.2.2. Disjunction🔗

Another important connective is the disjunction, or logical or, of two propositions: a ∨ b is true when either a or b is. This infix notation stands for Or a b, where Or : Prop → Prop → Prop.

To eliminate a disjunctive hypothesis — i.e., to use it in a proof — we proceed by case analysis, which, as with other data types like Nat, is done using cases. The two cases are inl (for "left injection", or "in the left case") and inr (for "right injection", or "in the right case").

We can see in this example that, when we perform case analysis on a disjunction a ∨ b, we must separately discharge two proof obligations, each showing that the conclusion holds under a different assumption — a in the first subgoal and b in the second.

Rather than performing case analysis via cases, we can also use obtain to match on the two possible injections, much like with obtain and ∧.

Conversely, to introduce a disjunction — i.e., to show that it holds — it suffices to show that one of its sides holds. This can be done via the tactics left and right. As their names imply, the first one requires proving the left side of the disjunction, while the second requires proving the right side. Here is a trivial use...

... and here is a slightly more interesting example requiring both left and right:

8.2.3. Falsehood and Negation🔗

Up to this point, we have mostly been concerned with proving "positive" statements — addition is commutative, appending lists is associative, etc. We are sometimes also interested in negative results, demonstrating that some proposition is not true. Such statements are expressed with the logical negation operator ¬, which is prefix notation for Not.

To see how negation works, recall the principle of explosion from the Tactics chapter, which asserts that, if we assume a contradiction, then any other proposition can be derived.

Following this intuition, we could define ¬ a ("not a") as ∀ c, a → c. Lean makes an equivalent but slightly different choice, defining ¬ a as a → False, where False is a specific unprovable proposition defined in the standard library.

Not (a : Prop) : Prop

@[implicit_reducible] def Not : Prop → Prop :=
fun a => a → False

Eliminating a False hypothesis works differently from eliminating the connectives above. Since False carries no information, there's nothing to extract. Rather, since False is a contradictory proposition, the principle of explosion applies to it: using cases on a False in the context completes any goal:

The Latin ex falso quodlibet means, literally, "from falsehood follows whatever you like"; this is another common name for the principle of explosion.

Inequality is a very common form of negated statement, so there is a special notation for it: ≠, which is infix notation for Ne.

@[reducible] def Ne.{u} : {α : Sort u} → α → α → Prop :=
fun {α} a b => ¬a = b

It takes a little practice to get used to working with negation in Lean. Even though you may see perfectly well why a claim involving negation holds, it can be a little tricky at first to see how to make Lean understand it!

Here are proofs of a few familiar facts to help get you warmed up.