Proof by cases

Stream: new members

[Mark R. Tuttle]

Is there an easier way to prove this example?

variable (a a' b b': Nat) (p: Prop)

theorem eq: a = a' ∧ b = b' → p := by sorry
theorem neq: a ≠ a' ∨ b ≠ b' → p := by sorry

example: p := by
  by_cases h: a ≠ a' ∨ b ≠ b'
  . apply (neq a a' b b' p)
    simp [h]
  . simp at h  -- Use ← direction of De Morgan ¬(𝐴∧𝐵) ↔ ¬𝐴 ∨ ¬𝐵
    apply (eq a a' b b' p)
    simp [h]

I learned a lot from this example. I learned about by_cases. I learned that the choice of h is important (use the antecedent of neq and not the antecedent of eq) because the forward direction of De Morgan requires classical (see classical reasoning).

[Anders Larsson]

I could get rid of two the two simp [h] rows.

variable (a a' b b': Nat) (p: Prop)

theorem eq: a = a' ∧ b = b' → p := by sorry
theorem neq: a ≠ a' ∨ b ≠ b' → p := by sorry


example: p := by
  by_cases h: a ≠ a' ∨ b ≠ b'
  . exact (neq a a' b b' p) h
  . simp at h  -- Use ← direction of De Morgan ¬(𝐴∧𝐵) ↔ ¬𝐴 ∨ ¬𝐵
    exact (eq a a' b b' p) h

[Filippo A. E. Nuccio]

You can avoid by_cases (which is probably not a great idea, since you learnt it ...)

import Mathlib

variable (a a' b b': Nat) (p: Prop)

theorem eq: a = a' ∧ b = b' → p := by sorry
theorem neq: a ≠ a' ∨ b ≠ b' → p := by sorry

example: p := by
  apply neq a a' b b'
  by_contra!
  apply_rules [eq]

[Filippo A. E. Nuccio]

Actually that can be improved to

import Mathlib

variable (a a' b b': Nat) (p: Prop)

theorem eq: a = a' ∧ b = b' → p := by sorry
theorem neq: a ≠ a' ∨ b ≠ b' → p := by sorry

example: p := by
  have : And _ _ := ⟨eq a a' b b' p, neq a a' b b' p⟩
  tauto