calculational proof of equivalence of two propositions

Stream: lean4

[Bulhwi Cha]

import Mathlib.Logic.Basic

example (p q r : Prop)
      : (p ∧ q ∧ ¬r) ∨ (p ∧ ¬q ∧ r) ∨ (¬p ∧ q ∧ r) ∨ (p ∧ q ∧ r)
      ↔ (p ∧ q) ∨ (p ∧ r) ∨ (q ∧ r) := calc
    (p ∧ q ∧ ¬r) ∨ (p ∧ ¬q ∧ r) ∨ (¬p ∧ q ∧ r) ∨ (p ∧ q ∧ r)
  ↔ (p ∧ q ∧ ¬r) ∨ (p ∧ ¬q ∧ r) ∨ (¬p ∧ q ∧ r) ∨
    (p ∧ q ∧  r) ∨ (p ∧  q ∧ r) ∨ ( p ∧ q ∧ r) := by repeat rw [or_self]
_ ↔ ((p ∧ q ∧ ¬r) ∨ (p ∧ q ∧ r)) ∨
    ((p ∧ ¬q ∧ r) ∨ (p ∧ q ∧ r)) ∨
    ((¬p ∧ q ∧ r) ∨ (p ∧ q ∧ r)) :=
      by rw [← @or_assoc (¬p ∧ q ∧ r), @or_comm ((¬p ∧ q ∧ r) ∨ (p ∧ q ∧ r)),
             ← @or_assoc (p ∧ ¬q ∧ r), ← @or_assoc (p ∧ ¬q ∧ r),
             @or_comm ((p ∧ ¬q ∧ r) ∨ (p ∧ q ∧ r)), ← @or_assoc (p ∧ q ∧ ¬r),
             ← @or_assoc (p ∧ q ∧ ¬r), or_assoc]
_ ↔ (( p ∧ q) ∧ (¬r ∨ r)) ∨
    (( p ∧ r) ∧ (¬q ∨ q)) ∨
    ((¬p ∨ p) ∧   q ∧ r) := by conv =>
      lhs
      congr
      . simp [← and_assoc, ← and_or_left]
      . congr
        . simp [@and_comm _ r, ← and_assoc, ← and_or_left]; rw [@and_comm r]
        . rw [← or_and_right]
_ ↔ (p ∧ q) ∨ (p ∧ r) ∨ (q ∧ r) := by conv =>
      lhs
      congr
      . rw [eq_true (em' r), and_true]
      . congr
        . rw [eq_true (em' q), and_true]
        . rw [eq_true (em' p), true_and]

[Bulhwi Cha]

Is there any way to write a calculational proof shorter than mine?

[Mario Carneiro]

does by tauto count?

[Mario Carneiro]

can confirm this works

import Mathlib.Tactic.Tauto

example (p q r : Prop)
      : (p ∧ q ∧ ¬r) ∨ (p ∧ ¬q ∧ r) ∨ (¬p ∧ q ∧ r) ∨ (p ∧ q ∧ r)
      ↔ (p ∧ q) ∨ (p ∧ r) ∨ (q ∧ r) := by tauto

[Bulhwi Cha]

Oh, thanks! Now I'm blaming myself for not having thought about using the tauto tactic.

[Bulhwi Cha]

But is it the only way to shorten my proof?

[Mario Carneiro]

here's another brute-force-ish proof:

example (p q r : Prop)
      : (p ∧ q ∧ ¬r) ∨ (p ∧ ¬q ∧ r) ∨ (¬p ∧ q ∧ r) ∨ (p ∧ q ∧ r)
      ↔ (p ∧ q) ∨ (p ∧ r) ∨ (q ∧ r) := by
  by_cases p <;> by_cases q <;> by_cases r <;> simp [*]

[Bulhwi Cha]

I should take a closer look at Lean's tactics.

[Mario Carneiro]

and here's a more "conceptual" proof most similar to your calc proof:

import Mathlib.Logic.Basic

example (p q r : Prop)
      : (p ∧ q ∧ ¬r) ∨ (p ∧ ¬q ∧ r) ∨ (¬p ∧ q ∧ r) ∨ (p ∧ q ∧ r)
      ↔ (p ∧ q) ∨ (p ∧ r) ∨ (q ∧ r) :=
  calc
    (p ∧ q ∧ ¬r) ∨ (p ∧ ¬q ∧ r) ∨ (¬p ∧ q ∧ r) ∨ (p ∧ q ∧ r)
      ↔ (p ∧ q ∧ ¬r ∨ p ∧ q ∧ r) ∨ (p ∧ ¬q ∧ r ∨ p ∧ q ∧ r) ∨ ¬p ∧ q ∧ r ∨ p ∧ q ∧ r :=
      by simp only [or_assoc, or_left_comm, or_self]
    _ ↔ (p ∧ q ∧ (¬r ∨ r)) ∨ (p ∧ (¬q ∨ q) ∧ r) ∨ ((¬p ∨ p) ∧ q ∧ r) :=
      by simp only [or_and_right, and_or_left]
    _ ↔ (p ∧ q) ∨ (p ∧ r) ∨ (q ∧ r) := by simp only [em', and_true, true_and]

[Bulhwi Cha]

Thanks again. Your last proof gave me some lessons:

• Don't forget to use left and right commutativity.
• Use parentheses carefully.
• Get a better understanding of how tactics work under the hood.