我在假设中有陈述true <> false。我想证明CCD_ 2。我能解决它吗？问题是，它不是用矛盾来解决的。
我同意您应该提供一个更好的例子。话虽如此！你需要清楚。。。true <> false是高于底线(如假设(还是低于底线(目标(？
我假设这是一个目标，因为作为一个假设，它实际上并没有告诉你任何事情(这只是一种同义反复(。
如果是目标：
Goal (true <> false)
intros contra; discriminate.
处理矛盾有很多通用的方法。。判别和倒置是很常见的。但一个更清晰的例子会更好。
一般需要注意的是，A <> B只是A=B->False的一个符号，这就是为什么"；intros contra"；上面的方法是有效的，因为它推翻了假设。在你不确定该怎么办的情况下，你可以用引言把等式放在底线之上，然后得出矛盾。
如果你在行上面有true <> true之类的东西(这很重要(，那么你可以应用它。
示例
Goal (true <> true -> 0 = 1).
intros contra.
exfalso.
apply contra.
reflexivity.
exfalso清除当前目标，并将其替换为False——当你有一个不可能的目标，但你的假设存在矛盾时(在线上(，这很有用。CCD_ 8使用<gt；是->像我上面提到的那样是假的。