benediktahrens

theorem and_distrib' (A B C : Prop) :
(A ∧ C) ∨ (B ∧ C) → (A ∨ B) ∧ C :=
assume h : (A ∧ C) ∨ (B ∧ C),
or.elim h
  (assume k : A ∧ C, 
   and.intro
     (or.intro_left B (and.elim_left k))
     (and.elim_right k))
  (assume k : B ∧ C,
   and.intro

benediktahrens

--(a)

example (A B C : Prop) : A → (A → B → C) → B → C :=
assume a : A,
assume f : A → B → C,
assume b : B,
f a b

/-

benediktahrens

example (A B C D : Prop) :
  A ∨ B → (A → C) → (B → D) → C ∨ D :=
assume h : A ∨ B,
assume f : A → C,
assume g : B → D,
or.elim h
(assume a : A , or.intro_left D (f a))
(assume b : B, or.intro_right C (g b))

benediktahrens

theorem uncurry (A B C : Prop) : (A → (B → C)) → (A ∧ B → C) :=
assume h1 : A → (B → C),
assume h2 : A ∧ B,
h1 (and.left h2) (and.right h2)


theorem and_distribute (A B C : Prop) : A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C) :=
assume h1 : A ∧ (B ∨ C),
or.elim (and.right h1)

benediktahrens

/-

Overview of this lecture:

1. Proof strategies
2. Classical reasoning
3. Forward reasoning
4. Improving readability

benediktahrens

/- INSTRUCTIONS

In this exercise, you learn about
the introduction and elimination
rule of bi-implication


First, read the explanation given
below.
Then fill in the holes in the proofs

benediktahrens

/-REMARK

 Note that given hypothesis
    h : A ∧ B
 the AND-elimination (left)
    and.elim_left h
 can also be abbreviated as
    h.left

 Similar for (right):

benediktahrens

/- INSTRUCTIONS

In this exercise, you learn about
the introduction and elimination
rule of bi-implication


First, read the explanation given
below.
Then fill in the holes in the proofs

benediktahrens

------------------------------
----REMINDER------------------
------------------------------

/-
Last week we saw
1. intro and elim rules in Lean
2. first proofs in Lean

In particular, we saw how

benediktahrens

section exercise


--assume propositions A, B, C
variables A B C : Prop

-- A → B → C → (A ∧ B) ∧ (A ∧ C)
example : A → B → C → (A ∧ B) ∧ (A ∧ C) :=
  assume a : A,