Double negation

Stream: new members

[Omnikar]

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

[Eric Wieser]

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]

How do I get access to that from the code?

[Kevin Buzzard]

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

[Omnikar]

The theorem

[Ruben Van de Velde]

Are you using lean3 or lean4?

[Omnikar]

4

[Mario Carneiro]

The not_not theorem is available in Std.Logic

[Mario Carneiro]

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

[Omnikar]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

it goes in the lakefile.lean

[Mario Carneiro]

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

[Mario Carneiro]

or

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

[Mario Carneiro]

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

[Omnikar]

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

[Mario Carneiro]

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

[Omnikar]

I don't know what lake is…

[Mario Carneiro]

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

[Mario Carneiro]

it is the build system for lean 4

[Mario Carneiro]

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

[Omnikar]

Okay

[Mario Carneiro]

it's built in to lean

[Mario Carneiro]

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

[Omnikar]

Yeah I do have it

[Mario Carneiro]

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

[Mario Carneiro]

there is an example of adding mathlib4 further down

[Omnikar]

Okay, thanks