solutions-week11-exercises.lean

import data.sum  --for sum.elim
import logic.basic --for empty.elim
open sum


section exercise_1a

variables A B : Prop

example : A ∧ B → B ∧ A :=
assume x : A ∧ B,
and.intro (and.elim_right x) (and.elim_left x)

end exercise_1a

section exercise_1b

variables A B : Type

example : A × B → B × A :=
λ x : A × B,
 (x.2, x.1)

/-

On paper, we write the same term:

λ (x : A × B), (x.2, x.1) : A × B → B × A

-/

end exercise_1b

/- Exercise 1c:

The structure of the proof and the term are the same, with
keywords replaced:
assume = λ
and.intro = ( _ , _ )
and.elim_left = .1
and.elim_right = .2

-/

section exercise_2a

variables A B : Prop

example : A ∨ B → B ∨ A :=
assume x : A ∨ B,
or.elim x
  (assume a : A, or.intro_right B a)
  (assume b : B, or.intro_left A b)

end exercise_2a

section exercise_2b

variables A B : Type

example : A ⊕ B → B ⊕ A :=
λ x : A ⊕ B,
 sum.elim (λ a : A, inr a) (λ b : B, inl b) x

/-

On paper, we write the same term, using the notation [ f , g ] for sum.elim f g

λ (x : A + B), [ λ (a : A), inr a ,  λ (b : B), inl b] x

-/

end exercise_2b

/- Exercise 2c:

The structure of the proof and the term are the same, with
keywords replaced:
assume = λ
or.elim = sum.elim
or.intro_left = inl
or.intro_right = inr

Note:

or.elim and sum.elim are analogous, but they take the arguments in
a different order:
or.elim takes the proof of the disjunction as its first argument, whereas
sum.elim takes the term of type coproduct/sum as its third argument
-/


section exercise_3a

variables A B C : Prop

example : A ∧ (B ∨ C) → A ∧ B ∨ A ∧ C:=
assume h : A ∧ (B ∨ C),
 or.elim
  (and.elim_right h)
  (assume b : B, or.intro_left (A ∧ C) (and.intro (and.elim_left h) b))
  (assume c : C, or.intro_right (A ∧ B) (and.intro (and.elim_left h) c))

end exercise_3a


section exercise_3b

variables A B C : Type

example : A × (B ⊕ C) → A × B ⊕ A × C:=
λ x : A × (B ⊕ C),
 sum.elim 
  (λ b : B, inl (x.1 , b))
  (λ c : C, inr (x.1, c))
  x.2

/-

On paper, we write the same term, using the notation [ f , g ] for sum.elim f g

λ x : A × (B + C),
  [ λ b : B, inl (x.1 , b)  ,   λ c : C, inr (x.1, c)  ]  x.2

-/

end exercise_3b

/- Exercise 3c:

The structure of the proof and the term are the same, with
keywords replaced:
assume = λ
or.elim = sum.elim
or.intro_left = inl
or.intro_right = inr
and.intro = ( _ , _ )
and.elim_left = .1
and.elim_right = .2

-/