week11-exercises-skeleton.lean

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


section foo

variables A B : Prop

example : A ∧ B → B ∧ A := _

end foo

section foo

variables A B : Type

example : A × B → B × A := _

end foo


section foo

variables A B : Prop

example : A ∨ B → B ∨ A := _

end foo

section foo

variables A B : Type

example : A ⊕ B → B ⊕ A :=
λ x : A ⊕ B,
 sum.elim _ _ x

end foo

/-
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 foo

variables A B C : Prop

example : A ∧ (B ∨ C) → A ∧ B ∨ A ∧ C:= _

end foo


section foo

variables A B C : Type
-- look at the construction of the function of type
-- A ⊕ B → B ⊕ A above for help on how to start
example : A × (B ⊕ C) → A × B ⊕ A × C:= _

end foo