## Stream: new members

### Topic: TPiL 4.6, Q2

#### Luis O'Shea (Dec 04 2019 at 23:02):

Exercise 2 in §4.6 of TPiL asks you to prove three examples. Below is my solution to the second of the three. It type-checks, but it seems long and cumbersome. Shortcomings include:

• I felt I needed to factor out a portion into a lemma (because it was getting a bit long)
• I used or.elim (classical.em r) but I felt it would have been better to use by_cases or cases_on (but couldn't figure it out)

Could anyone provide some comments, or suggestions on how to improve my mess?

variables {α : Type} {p : α → Prop} {r : Prop}

lemma l1 (h : ∀ x, p x ∨ r) (hnr : ¬r) : ∀ x, p x :=
assume x,
have p x ∨ r, from h x, this.elim
id
(assume hr, absurd hr hnr)

example : (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r :=
⟨ -- forward
assume h : (∀ (x : α), p x ∨ r),
or.elim (classical.em r)
or.inr
(assume hnr, or.inl (l1 h hnr)),
-- converse
assume h : (∀ (x : α), p x) ∨ r,
assume x : α, h.elim
(assume h2, or.inl (h2 x))
or.inr
⟩


#### Kevin Buzzard (Dec 05 2019 at 00:58):

import tactic.linarith -- just in case
variables {α : Type} {p : α → Prop} {r : Prop}

lemma l1 (h : ∀ x, p x ∨ r) (hnr : ¬r) : ∀ x, p x :=
λ x, _


#### Kevin Buzzard (Dec 05 2019 at 00:58):

lemma l1 (h : ∀ x, p x ∨ r) (hnr : ¬r) : ∀ x, p x :=
λ x, or.elim (h x) _ _


#### Kevin Buzzard (Dec 05 2019 at 00:59):

lemma l1 (h : ∀ x, p x ∨ r) (hnr : ¬r) : ∀ x, p x :=
λ x, or.elim (h x) id _


#### Kevin Buzzard (Dec 05 2019 at 01:00):

lemma l1 (h : ∀ x, p x ∨ r) (hnr : ¬r) : ∀ x, p x :=


#### Kevin Buzzard (Dec 05 2019 at 01:17):

example : (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r :=
⟨λ h, or_iff_not_imp_right.2 $λ h2 x, l1 h h2 _, λ h x, or.elim h (λ j, or.inl$ j x) or.inr⟩


#### Kevin Buzzard (Dec 05 2019 at 01:30):

import tactic.linarith
variables {α : Type} {p : α → Prop} {r : Prop}

lemma l1 (h : ∀ x, p x ∨ r) (hnr : ¬r) : ∀ x, p x :=
begin
intro x,
cases h x with hpx hnr,
exact hpx,
end

open_locale classical

example : (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r :=
begin
split,
{ by_cases hr : r,
simp [hr],
intro h,
left,
exact l1 h hr,
},
{ intros h x,
cases h,
{ left, exact h x},
{ right, exact h}
}
end


#### Kevin Buzzard (Dec 05 2019 at 01:34):

by_cases is a tactic, so it works in tactic mode.

example : (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r :=
begin
split,
{ by_cases hr : r,
simp [hr],
intro h,
left,
exact l1 h hr,
}, -- etc


#### Luis O'Shea (Dec 05 2019 at 01:49):

Thank you! It'll take me a little while to go through the above.

While I was trying to produce a term-based proof (and should have mentioned that), I am ultimately very interested in comparing tactic vs term approaches.

Last updated: May 13 2021 at 06:15 UTC