Zulip Chat Archive

Stream: new members

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


view this post on Zulip Eduardo Cavazos (Nov 02 2019 at 07:01):

Question posted to stackoverflow:

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

Thanks for any suggestions!

view this post on Zulip Johan Commelin (Nov 02 2019 at 07:09):

@Eduardo Cavazos Have you tried by tauto!?

view this post on Zulip 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.

view this post on Zulip 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),
       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)))

view this post on Zulip Mario Carneiro (Nov 02 2019 at 07:19):

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

view this post on Zulip 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,
            by_contradiction
                (λ hnpx : ¬ p x,
                    hnExnpx x, (λ hpx : p x, hnpx hpx))))

view this post on Zulip Eduardo Cavazos (Nov 02 2019 at 07:27):

Thank you @Simon Hudon !

view this post on Zulip Simon Hudon (Nov 02 2019 at 07:27):

My secret identity was discovered :)

view this post on Zulip Simon Hudon (Nov 02 2019 at 07:28):

You're welcome!

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 02 2019 at 07:51):

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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Nov 02 2019 at 07:54):

Use the leanpkg.path file instead

view this post on Zulip Mario Carneiro (Nov 02 2019 at 07:55):

which is set up by the leanpkg command

view this post on Zulip Mario Carneiro (Nov 02 2019 at 07:56):

If you put in the leanpkg.path file:

builtin_path
path ../mathlib/src

view this post on Zulip Mario Carneiro (Nov 02 2019 at 07:57):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Nov 02 2019 at 08:07):

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

view this post on Zulip Mario Carneiro (Nov 02 2019 at 08:07):

otherwise it uses your user global settings

view this post on Zulip 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

view this post on Zulip Bryan Gin-ge Chen (Nov 02 2019 at 08:10):

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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Nov 02 2019 at 08:37):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Nov 02 2019 at 08:43):

how do you figure?

view this post on Zulip Mario Carneiro (Nov 02 2019 at 08:43):

oh, a bat file

view this post on Zulip Mario Carneiro (Nov 02 2019 at 08:45):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Daniel Keys (Feb 01 2020 at 16:29):

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

view this post on Zulip 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?

view this post on Zulip 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!

view this post on Zulip Daniel Keys (Feb 01 2020 at 16:39):

Will do, thanks!


Last updated: May 13 2021 at 06:15 UTC