Zulip Chat Archive

Stream: lean4

Topic: Tactic for absurdity


view this post on Zulip Calvin Lee (Feb 26 2021 at 00:11):

Are there any tactics for showing absurdity? I find my self often doing exact _ where _ is some witness of falsehood

view this post on Zulip Mario Carneiro (Feb 26 2021 at 00:28):

What's wrong with exact? If you have a proof term already then that's the most straightforward option even in lean 3

view this post on Zulip Mario Carneiro (Feb 26 2021 at 00:28):

if your goal is not literally False but your proof term is then I will sometimes use cases e instead of exact false.rec e

view this post on Zulip Mario Carneiro (Feb 26 2021 at 00:29):

If you are referring specifically to the lean 3 contradiction tactic, I would expect that doesn't exist but it is a pretty simple tactic that can go in the mathlib prelude


Last updated: May 07 2021 at 13:21 UTC