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

Stream: new members

[Eduardo Cavazos]

Question posted to stackoverflow:

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

Thanks for any suggestions!

[Johan Commelin]

@Eduardo Cavazos Have you tried by tauto!?

[Johan Commelin]

@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]

@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),
       classical.by_contradiction
         (λ (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]

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

[Eduardo Cavazos]

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,
            by_contradiction
                (λ hnpx : ¬ p x,
                    hnExnpx ⟨x, (λ hpx : p x, hnpx hpx)⟩)))

[Eduardo Cavazos]

Thank you @Simon Hudon !

[Simon Hudon]

My secret identity was discovered :)

[Simon Hudon]

You're welcome!

[Johan Commelin]

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

[Eduardo Cavazos]

@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]

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]

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

[Eduardo Cavazos]

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]

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

[Mario Carneiro]

Use the leanpkg.path file instead

[Mario Carneiro]

which is set up by the leanpkg command

[Mario Carneiro]

If you put in the leanpkg.path file:

builtin_path
path ../mathlib/src

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

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

[Eduardo Cavazos]

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]

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

[Mario Carneiro]

otherwise it uses your user global settings

[Johan Commelin]

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

[Bryan Gin-ge Chen]

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

[Eduardo Cavazos]

@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]

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

[Eduardo Cavazos]

Hmm... if I do:

leanpkg new lean_test

at a Windows command prompt, I get:

failed to start child process

[Bryan Gin-ge Chen]

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]

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

[Eduardo Cavazos]

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]

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]

how do you figure?

[Mario Carneiro]

oh, a bat file

[Mario Carneiro]

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

[Eduardo Cavazos]

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

Yup!

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

[Mario Carneiro]

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]

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]

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]

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]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Daniel Keys]

Will do, thanks!