Zulip Chat Archive

Stream: general

Topic: finish is complete for propositional logic


view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 18 2020 at 17:04):

finish is not a general propositional logic prover

view this post on Zulip 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

view this post on Zulip Kenny Lau (Aug 18 2020 at 17:07):

well the docstring says finish is complete for propositional logic

view this post on Zulip Kenny Lau (Aug 18 2020 at 17:08):

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

view this post on Zulip 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]

view this post on Zulip 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