TPiL 4.6, Q2

Stream: new members

[Luis O'Shea]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

example : (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r :=
⟨_, _⟩

[Kevin Buzzard]

example : (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r :=
⟨by finish, by finish⟩

[Kevin Buzzard]

open_locale classical
-- I don't know the library as well as some
example (P Q : Prop) : (¬ Q → P) → P ∨ Q := by library_search
-- tells me about or_iff_not_imp_right

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

[Kevin Buzzard]

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]

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,
  contradiction,
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]

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]

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.