# Zulip Chat Archive

## 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

#### Eric Wieser (Oct 24 2021 at 17:16):

#### 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