Zulip Chat Archive

Stream: new members

Topic: Double negation


Omnikar (Sep 25 2022 at 15:11):

Is there a builtin theorem for ¬¬p ↔ p?

Eric Wieser (Sep 25 2022 at 15:29):

The #naming guide would lead you to docs#not_not. Searching "double negation" in the top right box in the docs would also find that

Omnikar (Sep 25 2022 at 15:31):

How do I get access to that from the code?

Kevin Buzzard (Sep 25 2022 at 15:41):

Access to the naming guide, the docs or the theorem?

Omnikar (Sep 25 2022 at 15:44):

The theorem

Ruben Van de Velde (Sep 25 2022 at 15:47):

Are you using lean3 or lean4?

Omnikar (Sep 25 2022 at 15:48):

4

Mario Carneiro (Sep 25 2022 at 15:53):

The not_not theorem is available in Std.Logic

Mario Carneiro (Sep 25 2022 at 15:54):

docs4#not_not (this says it's in Mathlib.Logic.Basic and that will still work but the docs are out of date)

Omnikar (Sep 25 2022 at 15:59):

So what code do I actually type to get it? Sorry, I'm completely new to Lean

Mario Carneiro (Sep 25 2022 at 16:00):

Have std4 or mathlib4 as a dependency, then import Std.Logic or import Mathlib.Logic.Basic at the top of the file, then use not_not

Omnikar (Sep 25 2022 at 16:01):

And… how do I add a dependency? :sweat_smile:

Mario Carneiro (Sep 25 2022 at 16:02):

it goes in the lakefile.lean

Mario Carneiro (Sep 25 2022 at 16:02):

require std from git "https://github.com/leanprover/std4" @ "main"

Mario Carneiro (Sep 25 2022 at 16:02):

or

require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "master"

Mario Carneiro (Sep 25 2022 at 16:03):

see for example the lakefile for mathlib4, which depends on std4: https://github.com/leanprover-community/mathlib4/blob/master/lakefile.lean

Omnikar (Sep 25 2022 at 16:03):

So I create a file called "lakefile.lean" and paste that in?

Mario Carneiro (Sep 25 2022 at 16:04):

you should already have one if you used lake to create your project

Omnikar (Sep 25 2022 at 16:04):

I don't know what lake is…

Mario Carneiro (Sep 25 2022 at 16:04):

https://github.com/leanprover/lake#creating-and-building-a-package

Mario Carneiro (Sep 25 2022 at 16:04):

it is the build system for lean 4

Mario Carneiro (Sep 25 2022 at 16:05):

it's required if you want to have more than one file and any dependencies other than core lean

Omnikar (Sep 25 2022 at 16:05):

Okay

Mario Carneiro (Sep 25 2022 at 16:05):

it's built in to lean

Mario Carneiro (Sep 25 2022 at 16:05):

so you should already have it, try lake --help

Omnikar (Sep 25 2022 at 16:05):

Yeah I do have it

Mario Carneiro (Sep 25 2022 at 16:06):

so just follow the instructions linked there to make a new project and that should set you up with an appropriate lakefile

Mario Carneiro (Sep 25 2022 at 16:06):

there is an example of adding mathlib4 further down

Omnikar (Sep 25 2022 at 16:07):

Okay, thanks


Last updated: Dec 20 2023 at 11:08 UTC