Zulip Chat Archive

Stream: new members

Topic: Prove false from not true?


view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 05 2018 at 21:37):

Hi, I have an elementary question -- I'm proving something, and am down to having the proved statement "¬true", and the goal is "false". Is there a quick way to finish this?

view this post on Zulip Andrew Ashworth (Oct 05 2018 at 21:38):

are you in term mode or tactic mode?

view this post on Zulip Kenny Lau (Oct 05 2018 at 21:39):

if h : ¬true then exact h trivial

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 05 2018 at 21:39):

Oh ok -- thanks, that works.

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 05 2018 at 21:48):

By the way, is there a statement that automatically proves the goal "true"?

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 05 2018 at 21:49):

I.e. "anything -> true" just like ex falso is "false -> anything"

view this post on Zulip Kenny Lau (Oct 05 2018 at 21:50):

trivial

view this post on Zulip Andrew Ashworth (Oct 05 2018 at 21:52):

as an aside, I think trivial is named weirdly. Why does it exist when true.intro is the canonical name?

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 05 2018 at 21:52):

Thanks. Didn't know that could be used as a standalone statement.

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 05 2018 at 21:53):

Re:true.intro Doesn't that apply to exfalso too? false.elim having a special name.

view this post on Zulip Andrew Ashworth (Oct 05 2018 at 21:53):

exfalso is an eliminator

view this post on Zulip Andrew Ashworth (Oct 05 2018 at 21:54):

but yes, i also prefer using false.elim ;)

view this post on Zulip Chris Hughes (Oct 05 2018 at 21:58):

My favourite is induction h if h : false

view this post on Zulip Kenny Lau (Oct 05 2018 at 21:59):

my favourite is cases h

view this post on Zulip Charles Rezk (Oct 06 2018 at 00:31):

Where can I get help for installing lean?

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2018 at 00:32):

Feel free to ask in this chat! But we may want to use a different "thread".

view this post on Zulip Charles Rezk (Oct 06 2018 at 00:33):

OK how do I do that?


Last updated: May 06 2021 at 22:13 UTC