Converting a sequent to Lean

Stream: new members

[Kieran Beltran]

I am trying to convert a sequent described on page 23 of Huth and Ryan to Lean
appreciate a little guidance on a couple steps
point 6 → elim 1,5
point 8 ¬ intro 4-7 based upon the contradiction
-- from page 23 in Huth and Ryan
-- sequent (p ∧ ¬ q) → r, ¬r, p ⊢ q

-- 1 (p ∧ ¬ q) → r premise
-- 2 ¬r premise
-- 3 p premise
-- 4 ¬q assumption (by contradiction)
-- 5 p ∧ ¬q and.intro 3,4
-- 6 r → elim 1,5
-- 7 false ¬ elim 6,2
-- 8 ¬¬q ¬ intro 4-7
-- 9 q ¬¬ elim 8

variables p q r : Prop

example (hpnqr : (p ∧ ¬q) → r) (hnr : ¬r) (hp : p) : q :=
assume hnq : ¬q,
show false, from (hnr ?r (and.intro(hp hnq) hpnqr)),
?? hnnq : ¬¬ q,
show q

TIA -Kieran

[Eric Wieser]

#backticks

[Kyle Miller]

I tried translating the sequent proof somewhat directly:

example {p q r : Prop} (h1 : (p ∧ ¬q) → r) (h2 : ¬r) (h3 : p) : q :=
begin
  -- steps 1-3 are already assumptions
  have h8 : ¬¬q,
  { intro h4,
    have h5 : p ∧ ¬q := and.intro h3 h4,
    have h6 : r := h1 h5,
    have h7 : false := h2 h6,
    exact h7, },
  have h9 : q := of_not_not h8,
  exact h9,
end

I wrote it as a tactic proof, but it's not hard to translate it to a proof term from here.