Prove sequent (with disjunctions) is valid

Stream: new members

[Kieran Beltran]

I am trying to validate a sequent including intro / elim disjunctions
(from Logic and Computer Science by Huth Ryan)

Having challenge with step 4... Any help appreciated.

-- Example 1.16  sequent q → r ⊢ p ∨ q → p ∨ r

-- 1        q → r                 premise

-- -- 2     p ∨ q                 assumption

-- -- -- 3    p                   assumption
-- -- -- 4  p ∨ r                 ∨i₁ 3

-- -- -- 5    q                   assumption
-- -- -- 6    r                   → e 1,5
-- -- -- 7  p ∨ r                 ∨i₂ 6

-- -- 8     p ∨ r                 ∨e 2, 3-4, 5-7

-- 9        p ∨ q → p ∨ r         →i 2-8

example {p q r : Prop} (h1: q → r) : p ∨ q → p ∨ r :=
begin
  {
  assume h2,                            -- p ∨ q
  {
  have h3: p,                           -- assume p
  have h4 : p ∨ r := or.inl h3,         -- ∨i₁ h3
  },
  {
  have h5: q,                           -- assume q
  have h6: r := h1 h5,                  -- → e h1,h5
  have h7 : p ∨ r := or.inr h6,         -- ∨i₂ h6
  },
  have h8 : p ∨ r := h2.elim (h4)(h7),  -- ∨e h2, 3-4, 5-7
  },
  have h9 : p ∨ q → p ∨ r := h2 h8,     -- →i 2-8

end

[Yakov Pechersky]

Your h3 and h5 don't have proofs. You need an or.elim h2, or or.cases_on h2 before h3. And have h3 will become assume h3

[Kieran Beltran]

Using the or elim w cases worked. Struggled with equivalent approach using h2.elim

Thanks for the suggestions.

example {p q r : Prop} (h1: q → r) : p ∨ q → p ∨ r :=
begin
  have h9 : p ∨ q → p ∨ r,

  intro h2,                 -- p ∨ q  or elim w cases
  cases h2 with h3 h5,      -- h3 : p, h5 : q
  { -- h3 : p
  left,
  have h4 : p ∨ r := or.intro_left r h3,
  exact h3,
  },
  { -- h5 : q
  right,
  have h6 := h1 h5,         -- h6 : r
  have h7 : p ∨ r := or.intro_right p h6,
  exact h6,
  },
  exact h9,

end

[Kevin Buzzard]

Why are you introducing h9 when it's exactly what you want to prove? Just delete that line and delete exact h9 from the end?

[Kevin Buzzard]

Why are you proving h4 when it's irrelevant and you never use it?

[Kevin Buzzard]

Same comment for h7

[Kieran Beltran]

Hi Kevin...Thanks for your response.

If you scroll to original thread, I was following a solution approach from Huth and Ryan's textbook for the validation of the sequent, and implementing the validation in Lean.

I understand the h9 point(s)...I'm not sure I understand what I would modify for h4 and h7 as you suggested.

[Kyle Miller]

@Kieran Beltran Kevin's point is that h4 and h7 aren't used at all, so they can be completely removed. This suggests that the translation isn't completely accurate.

This might be more faithful of a translation:

example {p q r : Prop} (h1: q → r) : p ∨ q → p ∨ r :=
begin
  -- goal is h9
  intro h2, -- p ∨ q, and set up →i 2-8
  -- goal is h8
  cases h2 with h3 h5, -- ∨e 2, 3-4, 5-7
  { -- h3 is p
    exact or.inl h3, }, -- ∨i₁ 3
  { -- h5 is q
    have h6 : r := h1 h5, -- → e 1,5
    exact or.inr h6, }, -- ∨i₂ 6
end