How to prove trivial truth table thing

Stream: new members

[Emma Hasson]

Hello, can someone please help me to prove this:

lemma triv_prop (P Q R : Prop) : (P ∧ Q) ↔ ((P ∧ (Q ∧ R)) ∨ (P ∧ (Q ∧ (¬ R)))) := sorry,

[Kevin Buzzard]

import tactic

lemma triv_prop (P Q R : Prop) : (P ∧ Q) ↔ ((P ∧ (Q ∧ R)) ∨ (P ∧ (Q ∧ (¬ R)))) :=
begin
  tauto!,
end

It's difficult to answer your question helpfully because I don't have enough information. Is this homework? Do you want to know how to do it from first principles? Did you play the relevant levels in the natural number game? (Proposition world)

This proof just says "this is some tautology in logic and we have a tactic for that, so you don't need to think". But perhaps the thinking is the part of the process you're interested in. I can't tell yet :-)

[Emma Hasson]

It's part of a larger proof I'm working on and I was getting stuck on a simple bit exemplified by this lemma. I had tried tauto, but wasn't aware of the ! variant. Thank you!

[Kevin Buzzard]

Oh yeah, tauto doesn't do it because it's not true constructively. Here's a first principles proof which does an explicit case split on R:

import tactic

lemma triv_prop (P Q R : Prop) : (P ∧ Q) ↔ ((P ∧ (Q ∧ R)) ∨ (P ∧ (Q ∧ (¬ R)))) :=
begin
  split,
  { rintro ⟨hP, hQ⟩,
    by_cases hR : R,
    { left,
      exact ⟨hP, hQ, hR⟩,
    },
    { right,
      exact ⟨hP, hQ, hR⟩, } },
  { rintro (⟨hP, hQ, hR⟩ | ⟨hP, hQ, hR⟩),
    { exact ⟨hP, hQ⟩, },
    { exact ⟨hP, hQ⟩, } }
end

[Kevin Buzzard]

If you try proving it using tauto and then hover your mouse over tauto you can see the documentation for it, which mentions tauto!.