finish is complete for propositional logic

Stream: general

[Kenny Lau]

import tactic.finish

example {p : Prop} : p ∨ ¬p :=
by finish -- works, so `finish` is classical

example {p q : Prop} : p ↔ p ∧ q ∨ p ∧ ¬q :=
by finish -- fails?

example {p q : Prop} : p ↔ p ∧ q ∨ p ∧ ¬q :=
by by_cases q; finish -- workaround

[Mario Carneiro]

finish is not a general propositional logic prover

[Mario Carneiro]

tauto makes the claim to be this, although I think there are also some failing goals IIRC

[Kenny Lau]

well the docstring says finish is complete for propositional logic

[Kenny Lau]

aha, tauto! solves the goal (cc. @Kevin Buzzard )

[Jeremy Avigad]

Yes, finish is complete for propositional logic. The problem is that it does not expand the iff by default. This works:

example {p q : Prop} : p ↔ p ∧ q ∨ p ∧ ¬q :=
by finish [iff_def]

[Jalex Stark]

what are the atoms of propositional logic? Is it [→, ∧, ∨, true, false]?