## Stream: general

### Topic: finish is complete for propositional logic

#### Kenny Lau (Aug 18 2020 at 16:59):

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 (Aug 18 2020 at 17:04):

finish is not a general propositional logic prover

#### Mario Carneiro (Aug 18 2020 at 17:05):

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

#### Kenny Lau (Aug 18 2020 at 17:07):

well the docstring says finish is complete for propositional logic

#### Kenny Lau (Aug 18 2020 at 17:08):

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

#### Jeremy Avigad (Aug 18 2020 at 21:13):

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 (Aug 18 2020 at 22:49):

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

Last updated: May 16 2021 at 05:21 UTC