Examples
Let’s do some examples of predicate logic proofs in Lean to get comfortable with the new syntax and also introduce a few more useful tactics.
First, we prove that ∀ (x : α), P x → ∃ (y : α), P y
.
example (α : Type) : ∀ (x : α), P x → ∃ (y : α), P y := by
intro (a : α)
intro (h : P a)
exact ⟨a, h⟩
From out previous discussion, we would expect the final line to be exact Exists.intro a h
. Lean has a shorthard notation for intro rules. We can use French quotes (typed < >) to construct the term. Similarly, if we wanted an And.intro a b
, we could ⟨a, b⟩
. Like most notation it makes thing easier to write but can also make it harder to read.
Let’s look at the proof showing we can exchange quantifiers in one direction.
variable (α : Type)
variable (C : α → α → Prop)
example : Type) : (∃ (x:α), ∀ (y:α), C x y) → ∀ (v:α), ∃ (u:α), C u v := by
intro h v
-- introduce h : ∃ x, ∀ (y : α), C x y and v : α
apply Exists.elim h
-- we supply the existential statement and Lean now asks for a proof of
-- ⊢ ∀ (a : α), (∀ (y : α), C a y) → ∃ u, C u v
intro g f
-- we introduce f : ∀ (y : α), C g y and g : α
apply Exists.intro
-- we have new goals ⊢ C ?w v and ⊢ α
exact f v
-- this solves the first and Lean then infers the second
Note that we can introduce multiple terms just by including a spaced list of labels for them.
Next, if there does not exist a value making the predicate true, we can conclude it is false for all values.
variable (α : Type)
variable (P : α → Prop)
example : (¬ ∃ y, P y) → ∀ x, ¬ P x := by
intro h a n
exact h ⟨a,n⟩
Below we have another example of giving proofs using quantifiers.
variable (α : Type)
variable (P Q : α → Prop)
example : (∀ x, P x → ¬ Q x) → ¬ ∃ y, P y ∧ Q y := by
intro h n
apply Exists.elim n
intro a g
-- Here g : P x ∧ Q x
exact h a g.left g.right
-- Lean lets us use the shorthand g.left for And.left g and similarly
-- g.right for And.right g
Let’s do a basic example using functions and equality.
variable (α : Type)
variable (P : α → Prop)
example (f : α → α) (x y : α) (h₁ : x = y) (h₂ : P (f x)) : P (f y) := by
rw [←h₁]
-- the goal is now P (f x)
assumption
There a few things to notice in this proof. First, we have rw [←h₁]
with the backwards ←. Lean’s convention for rewriting using x=y
is to search for occurrences of x
and replace them with y
. If we tried rw [h₁]
, then Lean would return an error
tactic 'rewrite' failed, did not find instance of the pattern in the target
expression
Lean allows you to rewrite hypotheses in addition to goals but you need to specify the assumption to target. The following proof is also valid.
example (f : α → α) (x y : α) (h₁ : x = y) (h₂ : P (f x)) : P (f y) := by
rw [h₁] at h₂
-- now h₂ is P (f y)
assumption
This tells Lean to look for x
’s in h₂
and replace them with y
’s. In both cases, the assumption tactic tells Lean: one of the goals is an established fact in the context, figure out which and close the goal.
You can also feed Lean multiple terms to use for rewriting as a list.
variable (α : Type)
variable (x y z : α)
variable (P : α → Prop)
example (h₁ : x = y) (h₂ : z = x) (f : α → α) : f y = f z := by
rw [← h₁, h₂]