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: