Theorem Marketplace

Theorem Details

-- Prove that from P ∨ Q and ¬P, we can conclude Q

theorem disj_elim (P Q : Prop) : (P ∨ Q) → (¬P) → Q := by sorry

Bounty: 0.002 ETH

Status: Closed

Proof

-- Prove that from P ∨ Q and ¬P, we can conclude Q

theorem disj_elim (P Q : Prop) : (P ∨ Q) → (¬P) → Q := by
  intros hPQ hNotP
  cases hPQ with
  | inl hP =>
    -- Case where P is true
    exfalso                     -- Derive a contradiction
    apply hNotP                 -- Use the assumption ¬P
    exact hP                    -- Contradicts hP : P
  | inr hQ =>
    -- Case where Q is true
    exact hQ                    -- We can directly conclude Q

Back to Bounties