Zulip Chat Archive

Stream: new members

Topic: TPiL 4.6, Q2


view this post on Zulip 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

view this post on Zulip 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, _

view this post on Zulip 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) _ _

view this post on Zulip 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 _

view this post on Zulip Kevin Buzzard (Dec 05 2019 at 01:00):

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

view this post on Zulip Kevin Buzzard (Dec 05 2019 at 01:01):

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

view this post on Zulip Kevin Buzzard (Dec 05 2019 at 01:02):

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

view this post on Zulip Kevin Buzzard (Dec 05 2019 at 01:04):

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

view this post on Zulip Kevin Buzzard (Dec 05 2019 at 01:05):

example : ( x, p x  r)  ( x, p x)  r :=
by finish, by finish

view this post on Zulip Kevin Buzzard (Dec 05 2019 at 01:14):

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 _, _⟩

view this post on Zulip 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

view this post on Zulip 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,
  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

view this post on Zulip 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

view this post on Zulip 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