Robert Soeldner (Jan 28 2021 at 14:37): 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: Apr 20 2024 at 04:02 UTC