Stream: Coq users

Topic: Proving a tautology

Robert Soeldner (Jan 28 2021 at 14:37):

Hi,
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 ?

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.

Pierre-Marie Pédrot (Jan 28 2021 at 14:39):

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

Robert Soeldner (Jan 28 2021 at 14:43):

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

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

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: Sep 23 2023 at 14:01 UTC