Zulip Chat Archive

Stream: new members

Topic: Prove false from not true?


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?

Andrew Ashworth (Oct 05 2018 at 21:38):

are you in term mode or tactic mode?

Kenny Lau (Oct 05 2018 at 21:39):

if h : ¬true then exact h trivial

Abhimanyu Pallavi Sudhir (Oct 05 2018 at 21:39):

Oh ok -- thanks, that works.

Abhimanyu Pallavi Sudhir (Oct 05 2018 at 21:48):

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

Abhimanyu Pallavi Sudhir (Oct 05 2018 at 21:49):

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

Kenny Lau (Oct 05 2018 at 21:50):

trivial

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?

Abhimanyu Pallavi Sudhir (Oct 05 2018 at 21:52):

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

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.

Andrew Ashworth (Oct 05 2018 at 21:53):

exfalso is an eliminator

Andrew Ashworth (Oct 05 2018 at 21:54):

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

Chris Hughes (Oct 05 2018 at 21:58):

My favourite is induction h if h : false

Kenny Lau (Oct 05 2018 at 21:59):

my favourite is cases h

Charles Rezk (Oct 06 2018 at 00:31):

Where can I get help for installing lean?

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".

Charles Rezk (Oct 06 2018 at 00:33):

OK how do I do that?


Last updated: Dec 20 2023 at 11:08 UTC