Link Search Menu Expand Document


To build a proof of $A \land B$, we needs proofs of $A$ and $B$. In Lean, this is accomplished by And.intro.

example : (a : A) (b : B) : A  B := And.intro a b

For elimination, we use And.left and And.right to extract proofs from A ∧ B.

example : (h : A  B) : A := And.left h 
example : (h : A  B) : B := And.right h 


For the or-introduction rules, we have

example : (a : A)  : A  B := Or.inl h 
example : (b : B)  : A  B := Or.inr h 

For $\lor$-elimination we need
three things :

  1. $A \lor B$
  2. A proof $A \vdash C$
  3. A proof $B \vdash C$ Let’s see what it looks like in Lean.
#check Or.elim 
-- ∀ {a b c : Prop}, a ∨ b → (a → c) → (b → c) → c

So to use Or.elim we need three proofs:

  1. r : A ∨ B
  2. p : A → C
  3. q : B → C

Let’s see a one direction of a commutativity of in Lean and at the same time get some sense of how to build up a proof in steps. Often Lean can “fill in” arguments from the context. You can ask it by placing a _. Let’s see what happens here.

example (h : A  B) : B  A := Or.elim h _ _  

The infoview might look something like

don't know how to synthesize placeholder for argument 'right'
A B : Prop
h : A  B
 B  B  A

don't know how to synthesize placeholder for argument 'left'
A B : Prop
h : A  B
 A  B  A

Lean is asking for our proofs of B → B ∨ A and A → B ∨ A. Remember that the are functions that turn any proof of B into a proof of B ∨ A and the same with A to B ∨ A. We can fill in the proof by providing such functions using or eliminations.

example (h : A  B) : B  A := 
  Or.elim h (fun (a:A) => Or.inr a) (fun (b:B) => Or.inl b)


We can eliminate a bi-implication into two implications.

example (h : A  B) : A  B := 
example (h : A  B) : B  A := Iff.mpr

Here mp stands for “Modus ponens” and mpr for the “reverse”.

To introduce a bi-implication, we need proofs of A → B and B → A.

#check Iff.intro -- ∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b)

Some examples

example (h : A  B  C) : A  C := fun (a : A) => And.right (h a)
example : A  B  A  B := fun (p : A  B) => Or.inl (And.left p)
example  (h : A  B) : B  B := And.intro (And.right h) (And.right h)