Seminar 5 – Universal and Existential Quantifiers

Summary

During this seminar, we looked deeper into universal and existential quantifiers.

Understanding the quantifiers

Let $P$ be a property for variables of type $T$. Statements like $\exists (x : T) : P x$ involving the existential quantifier are equivalent to a pair $\langle x, h\rangle$ where $x : T$ and $h : P x$

Statements like $\forall (x : T) : P x$ involving the universal quantifier can be seen as a function that takes $x : T$ and maps it to a proof of $P x$. This is why we can often deal with universal quantifiers in the same way that we deal with implications, which are also functions. However, recall that an implication maps a proof of one proposition to a proof of another proposition, whereas the universal quantifier maps a term of some type to a proof of a property of this term.

Getting rid of quantifiers: decision table

	in goal ($\vdash ...$)	in hypothesis ($h : ...$)
universal: $\forall x : P x$	intro x	specialize h x apply h exact h x
existential: $\exists x : P x$	use x exact ⟨x, hx⟩	rcases h with ⟨x, hx⟩ obtain ⟨x, hx⟩ := h

The new tactics

The intro tactics introduces a new hypothesis, shortening the goal. We have already seen this tactic in the context for implication. Suppose that your goal is

⊢ ∀ x : P x

Then, if we run

intro y

we get

y : T
⊢ P y

The specialize tactic can be used to get rid of hypotheses involving existential quantifiers. Consider the following context:

y : T
h : ∀ (x : T) : P x

Then, running

specialize h y

changes the context to

y : T
h : P y

Similarly, if we have

x : T
h : ∀ (x : T) : P x
⊢ P x

we can run

apply h

exact h x

to solve the goal.

For existential quantifiers in the goal, we have the use tactic. Consider

⊢ ∃ x : P x

Then, running

use 42

turns the goal into

42 : T
⊢ P 42

If we see the existential quantifier as a pair of a term of type $T$ and a proof for this term satisfying $T$, then the use tactic introduces this term, and changes the goal to specifying the proof.

if we have the context and goal

x : T
h : P x
⊢ ∃ x : P x

then we can also solve it with

exact ⟨x, h⟩

Lastly, the rcases tactic lets us rewrite a context like:

h : ∃ x : P x

By running

rcases h with ⟨x, hx⟩

we change the context to

x : T
hx : P x

Alternatively, the obtain tactic combines have and rcases. We can achieve the same change of context with

obtain ⟨x, hx⟩ := h

Section 3.3: Negation

(update will follow)

Section 3.4: Conjuction and iff

(update will follow)

Section 3.5: Disjunction

(update will follow)

Next week

Lean is entirely built on dependent type theory. Therefore, we invited Malvin Gattinger next week to give an introduction to type theory. Be there to uncover the foundations of what we have been working on the past weeks.

As homework, try to finish chapter 3 on logic up till 3.5. We will skip 3.6, and continue with chapter 4 afterwards (skip 4.3 as well if you want).