Link Search Menu Expand Document
Math 300

Conjunction

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

Disjunction

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'
context:
A B : Prop
h : A ∨ B
⊢ B → B ∨ A

don't know how to synthesize placeholder for argument 'left'
context:
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)

Bi-implication

We can eliminate a bi-implication into two implications.

example (h : A ↔ B) : A → B := Iff.mp 
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)