Stream: Coq users

Topic: Proving a tautology

view this post on Zulip Robert Soeldner (Jan 28 2021 at 14:37):

I struggle to prove something of the form:

  H : (a \/ b\/ c) /\ d
  a /\ d

I thought I can use assumption or destruct on H but without success. Is there some tactic\ ... what do I miss ?

view this post on Zulip Guillaume Melquiond (Jan 28 2021 at 14:39):

This is not provable. However, doing destruct H (and then another destruct) is indeed the way to go to study the various cases.

view this post on Zulip Pierre-Marie P├ędrot (Jan 28 2021 at 14:39):

Don't wonder why, because this doesn't hold in general.

view this post on Zulip Robert Soeldner (Jan 28 2021 at 14:43):

Thank you for the fast reply guys. Rethinking this, it totally makes sense :P

view this post on Zulip Karl Palmskog (Jan 28 2021 at 14:48):

for goals with simple propositional formulas (or-and-not), you can typically use the tauto tactic as an oracle to check whether something is provable

view this post on Zulip Christian Doczkal (Jan 28 2021 at 15:44):

While on the topic of using tauto. I recall reading that tauto makes use of excluded middle if the corresponding library has been imported. Does someone know whether it does something smarter than exploiting Glivenko's theorem (i.e., apply a single double negation to the top and then prove the formula constructively)?

Last updated: Jan 28 2023 at 06:30 UTC