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

The injectivity/disjointness principles from the Tactics chapter apply to equality hypotheses too, and cases can exploit them directly:

There are more examples of this kind of reasoning yet to come.

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:

For the present example, both ways work. But in other situations, we may wind up with a conjunctive hypothesis in the middle of a 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").

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:

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.

Since inequality involves a negation, getting comfortable with it also often requires a little practice.

A useful trick: if you are trying to prove a nonsensical goal, apply ex_falso_quodlibet to change the goal to False. This makes it easier to use assumptions of the form ¬ a, and in particular of the form x ≠ y.

∀ α : Type, ∀ x y : α, x = y ∧ x ≠ y → False

∀ a b : Prop, a ∨ b → ¬ ¬ (a ∨ b)

∀ a b : Prop, a → (a ∨ ¬ ¬ b)

∀ a b : Prop, a ∨ b → (¬ ¬ a) ∨ (¬ ¬ b)

∀ a : Prop, 1 = 0 → (a ∨ ¬ a)

8.2.4. Truth🔗

Besides False, Lean's standard library also defines True, a proposition that is trivially true. To prove it, we use the constructor True.intro explicitly, or the anonymous constructor ⟨⟩, or the constructor tactic.

Unlike False, which is used extensively, True is used relatively rarely: it is trivial (and therefore uninteresting) to prove as a goal, and it provides no useful information when it appears as a hypothesis.

8.2.5. Logical Equivalence🔗

The handy "if and only if" connective, which asserts that two propositions have the same truth value, is a structure containing the two implication directions. a ↔ b is notation for Iff a b.

You can use Iff.mp to access the forward direction of the iff and Iff.mpr to access the backwards direction — these eliminate an iff — and Iff.intro to convert a goal of the form a ↔ b to two goals of the form a → b and b → a, which introduces an iff.

structure Iff (a b : Prop) : Prop
number of parameters: 2
fields:
  Iff.mp : a → b
  Iff.mpr : b → a
constructor:
  Iff.intro {a b : Prop} (mp : a → b) (mpr : b → a) : a ↔ b