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₂]