## Stream: new members

### Topic: example : ¬ (∃ x, ¬ p x) → (∀ x, p x)

#### Eduardo Cavazos (Nov 02 2019 at 07:01):

Question posted to stackoverflow:

https://stackoverflow.com/q/58668917/268581

Thanks for any suggestions!

#### Johan Commelin (Nov 02 2019 at 07:09):

@Eduardo Cavazos Have you tried by tauto!?

#### Johan Commelin (Nov 02 2019 at 07:11):

@Eduardo Cavazos Here is a way to get hints from Lean itself.

lemma foo : your_statement := by tauto!

#print foo


That way you can see how Lean would prove these. You can then try to optimise the proof.

#### Johan Commelin (Nov 02 2019 at 07:15):

@Eduardo Cavazos Voila:

import tactic

lemma foo (X : Type) (p : X → Prop) :
¬ (∃ x, ¬ p x) → (∀ x, p x) :=
begin
finish,
end

#print foo


This tells me that you can prove your example in TPIL term-mode style as follows:

theorem foo : ∀ (X : Type) (p : X → Prop), (¬∃ (x : X), ¬p x) → ∀ (x : X), p x :=
λ (X : Type) (p : X → Prop),
eq.mpr (id (imp_congr_eq (propext not_exists) (eq.refl (∀ (x : X), p x))))
(λ (a : ∀ (x : X), ¬¬p x) (x : X),
(λ (a_1 : ¬p x),
(λ (X : Type) (p : X → Prop) (x : X) (a_1 : ¬p x) (a : ∀ (x : X), p x),
false.rec false (false_of_true_eq_false (eq.trans (eq.symm (eq_true_intro (a x))) (eq_false_intro a_1))))
X
p
x
a_1
(eq.mp (forall_congr_eq (λ (x : X), auto.not_not_eq (p x))) a)))


#### Mario Carneiro (Nov 02 2019 at 07:19):

Looking at automated proofs is not the best way to find a good manual proof

#### Eduardo Cavazos (Nov 02 2019 at 07:25):

Here's what I came up with based on Simon's hint on stackoverflow:

example : ¬ (∃ x, ¬ p x) → (∀ x, p x) :=
(assume hnExnpx : ¬ (∃ x, ¬ p x),
(λ x,
or.elim (em (p x))
(λ hpx : p x, hpx)
(λ hnpx : ¬ p x,
false.elim (hnExnpx (exists.intro x (λ hpx : p x, hnpx hpx))))))


Then simplifying it a bit (use by_contradiction instead of (em (p x)) and an anonymous constructor for the exists.intro):

example : ¬ (∃ x, ¬ p x) → (∀ x, p x) :=
(assume hnExnpx : ¬ (∃ x, ¬ p x),
(λ x,
(λ hnpx : ¬ p x,
hnExnpx ⟨x, (λ hpx : p x, hnpx hpx)⟩)))


#### Eduardo Cavazos (Nov 02 2019 at 07:27):

Thank you @Simon Hudon !

#### Simon Hudon (Nov 02 2019 at 07:27):

My secret identity was discovered :)

You're welcome!

#### Johan Commelin (Nov 02 2019 at 07:39):

Looking at automated proofs might not be the best way, but they can certainly provide hints when you are stuck.

#### Eduardo Cavazos (Nov 02 2019 at 07:49):

@Johan Commelin Thanks for demonstrating that. It's good to know that that sort of thing is available. Now I'll have to look up what all those new functions in the generated proof mean as many of them haven't yet been introduced in TPIL by chapter 4. :stuck_out_tongue_wink:

#### Mario Carneiro (Nov 02 2019 at 07:50):

At some point you will have to learn how to look at the library itself; lean gives you a way to define new lemmas and there are a ton of lemmas in lean and mathlib, far more than will be covered in TPIL

#### Mario Carneiro (Nov 02 2019 at 07:51):

The logic.basic file of mathlib contains a bunch of theorems like this one

#### Eduardo Cavazos (Nov 02 2019 at 07:54):

I hope I installed mathlib correctly! Everything seems to work. I basically just set the LEAN_PATH environment variable to contain these three entries:

...\lean-3.4.2-windows\lib\lean\leanpkg
...\lean-3.4.2-windows\lib\lean\library
...\mathlib\src


Where ... is a longer part of the path on my filesystem.

#### Mario Carneiro (Nov 02 2019 at 07:54):

Don't set the LEAN_PATH environment variable (ignore the recommendation that lean gives, it's out of date)

#### Mario Carneiro (Nov 02 2019 at 07:54):

Use the leanpkg.path file instead

#### Mario Carneiro (Nov 02 2019 at 07:55):

which is set up by the leanpkg command

#### Mario Carneiro (Nov 02 2019 at 07:56):

If you put in the leanpkg.path file:

builtin_path
path ../mathlib/src


#### Mario Carneiro (Nov 02 2019 at 07:57):

then it should all work (the path to mathlib is relative to the leanpkg.path file)

#### Mario Carneiro (Nov 02 2019 at 07:58):

But if the LEAN_PATH env var is set, it will override the leanpkg.path file, meaning that repos which use it won't work on your machine

#### Eduardo Cavazos (Nov 02 2019 at 08:02):

@Mario Carneiro , thanks for the tips. I don't see a leanpkg.path file in my Lean installation.

#### Mario Carneiro (Nov 02 2019 at 08:03):

It is autogenerated by leanpkg when you run e.g. leanpkg new but you can just create a file in your project directory called leanpkg.path and those contents and lean will use it

#### Mario Carneiro (Nov 02 2019 at 08:04):

the file has to be in some parent of the directory where your lean files are stored

#### Eduardo Cavazos (Nov 02 2019 at 08:06):

Hmm... If I create a new buffer in vscode which isn't yet saved to a file, but is in 'lean' mode, where will vscode look for the 'leanpkg.path' file?

#### Mario Carneiro (Nov 02 2019 at 08:07):

It uses your project root, if you have "opened a folder" in vscode

#### Mario Carneiro (Nov 02 2019 at 08:07):

otherwise it uses your user global settings

#### Johan Commelin (Nov 02 2019 at 08:09):

@Eduardo Cavazos https://github.com/leanprover-community/mathlib/blob/master/docs/install/windows.md might be relevant

#### Bryan Gin-ge Chen (Nov 02 2019 at 08:10):

The mathlib doc page on Lean projects has a useful set of commands.

#### Eduardo Cavazos (Nov 02 2019 at 08:19):

@Johan Commelin Yup, I saw those directions. Setting LEAN_PATH seemed easier than all that. :-) But now I know about leanpkg.path so I'll look into using that now.

#### Eduardo Cavazos (Nov 02 2019 at 08:20):

@Bryan Gin-ge Chen That page does indeed seem helpful (also linked from the page that @Johan Commelin posteed). Thanks!

#### Eduardo Cavazos (Nov 02 2019 at 08:28):

Hmm... if I do:

leanpkg new lean_test


at a Windows command prompt, I get:

failed to start child process


#### Bryan Gin-ge Chen (Nov 02 2019 at 08:36):

What shell are you using on windows? I remember people running into this error when they didn't use the bash shell that comes with git for windows.

#### Mario Carneiro (Nov 02 2019 at 08:37):

I use the MSYS2 shell on windows; the git bash shell doesn't work for me

#### Eduardo Cavazos (Nov 02 2019 at 08:38):

What shell are you using on windows? I remember people running into this error when they didn't use the bash shell that comes with git for windows.

Just the basic Windows Command Prompt. I'll give one of the other shells a try.

#### Eduardo Cavazos (Nov 02 2019 at 08:43):

However, there is a leanpkg.bat file in the Lean bin directory which seems to imply that the authors intended for it to be run from the standard Windows Command Prompt.

#### Mario Carneiro (Nov 02 2019 at 08:43):

how do you figure?

oh, a bat file

#### Mario Carneiro (Nov 02 2019 at 08:45):

Can you run lean --version from the command line?

#### Eduardo Cavazos (Nov 02 2019 at 08:48):

Can you run lean --version from the command line?

Yup!

C:\temp>lean --version
Lean (version 3.4.2, commit cbd2b6686ddb, Release)


#### Mario Carneiro (Nov 02 2019 at 08:52):

you might also try lean --run lean/leanpkg/leanpkg/main.lean but I don't have high hopes for using the windows command prompt

#### Eduardo Cavazos (Nov 02 2019 at 08:57):

Using git bash seems to work:

\$ leanpkg new lean_test_a
> mkdir -p lean_test_a
> cd lean_test_a
> mkdir src
> git init -q
> git checkout -b lean-3.4.2
Switched to a new branch 'lean-3.4.2'
configuring lean_test_a 0.1


#### Daniel Keys (Feb 01 2020 at 16:17):

This also gives me trouble in tactic mode:

open classical
variables (α : Type) (p q : α → Prop)
variable a : α

theorem T05_1 : ¬ (∃ x, ¬ p x) → (∀ x, p x) :=
(assume hnExnpx : ¬ (∃ x, ¬ p x),
(λ x, or.elim (em (p x))
(λ hpx : p x, hpx)
(λ hnpx : ¬ p x,
false.elim (hnExnpx (exists.intro x (λ hpx : p x, hnpx hpx))))))
#check T05_1
include a
theorem T05_2 : ¬ (∃ x, ¬ p x) → (∀ x, p x) :=
begin
intro hnExnpx,
cases (em (p a) ) with hpa hnpa,
{
exact hpa
},
{ }
end


To my understanding, a is an arbitrary element of α so hpa should fill the goal. It may be that I don't write the term correctly, though! Or maybe my understanding is wrong. Or both!

#### Patrick Massot (Feb 01 2020 at 16:28):

No, a is not arbitrary at this stage. The tactic state on the error line means a is a fixed element its type.

#### Daniel Keys (Feb 01 2020 at 16:29):

I could guess that, but not sure how to go about it.

#### Patrick Massot (Feb 01 2020 at 16:35):

I just had a look at the actual statement of T05_2. What is a doing there?

#### Patrick Massot (Feb 01 2020 at 16:37):

Remove that include a and start the proof with intros h x, by_contradiction H,. I need to go. Have fun!

#### Daniel Keys (Feb 01 2020 at 16:39):

Will do, thanks!

Last updated: May 13 2021 at 06:15 UTC