Stream: new members

Topic: Converting a sequent to Lean

Kieran Beltran (Oct 24 2021 at 13:01):

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

#backticks

Kyle Miller (Oct 24 2021 at 18:40):

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.

Last updated: Dec 20 2023 at 11:08 UTC