Jose Balado

Stream: new members

[Jose Balado]

Hi, I am Jose, working as a web developer with a degree in Philosophy and interested in Mathematical Logic. I recently learned about Automatic Theorem Provers, and after trying several of them, Lean seamed like the easiest to install and run, with very good documentation.

My knowledge of Mathematical Logic is kind of basic and I am going through a tutorial called Theorem Proving in Lean, so I wonder if I could find somewhere the solutions for the exercises.
Working right now with 3.6. Examples of Propositional Validities, but I am strugling with this one, even if I was able to solve the previous problems:
¬(p ∨ q) ↔ ¬p ∧ ¬q

I solved the previous one like this:

example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) :=
iff.intro
(assume hpqr : (p ∨ q) → r, show (p → r) ∧ (q → r), from
  ⟨(assume hp : p, show r, from hpqr(or.inl hp)),
   (assume hq : q, show r, from hpqr(or.inr hq))⟩)
(assume hprqr : (p → r) ∧ (q → r), show (p ∨ q) → r, from
  (assume hpq : p ∨ q, show r, from
    or.elim hpq
    (assume hp : p, show r, from hprqr.left hp)
    (assume hq : q, show r, from hprqr.right hq)
  )
)

So , please, any place where I could find the solutions, or perhaps anyone so kind as to show me how to prove this ¬(p ∨ q) ↔ ¬p ∧ ¬q.
Also, not sure if it is right to post here these basic questions.

Thanks,
Jose

[Kevin Buzzard]

This is a perfect place to post basic questions.

[Kevin Buzzard]

Do you know tactic mode?

[Kevin Buzzard]

By the way, Lean is an Interactive Theorem Prover, not an Automatic one. You have to do a lot of the work yourself. Actually, Lean bills itself as trying to bridge the gap between the two, IIRC.

[Jose Balado]

No sorry, Tactics comes later. Should I take a look there first?

[Kevin Buzzard]

Here is a proof:

 import tactic.finish

 example (p q : Prop) : ¬(p ∨ q) ↔ ¬p ∧ ¬q := by finish

[Kevin Buzzard]

The finish tactic is part of the automatic story rather than the interactive story :-)

[Jose Balado]

thanks for clarification about Automatic/Interactive :slight_smile:

[Jose Balado]

I really don't now how to manipulate ¬(p ∨ q).
Will I need tactics to solve the rest of the 3.6 theorems?

[Kevin Buzzard]

You don't need tactics to solve anything, it's just that I find that some beginners prefer tactic mode.

[Kevin Buzzard]

I'm writing some more proofs; hang on.

[Kevin Buzzard]

You can put ¬(p ∨ q) in single backticks to make it look nicer.

[Kevin Buzzard]

The way to manipulate it is to think of it as (p or q) implies false

[Kevin Buzzard]

Here's a term mode proof:

 example (p q : Prop) : ¬(p ∨ q) ↔ ¬p ∧ ¬q :=
 ⟨λ h, ⟨λ hp, h $ or.inl hp, λ hq, h $ or.inr hq⟩, λ hn h, or.elim h hn.1 hn.2⟩

[Jose Balado]

Nice, thanks a lot.
I usually prefer to go back myself to the documentation, but because you are just here, prefer to answer you as soon as possible.
Where can I find how that $ thing works?

[Kevin Buzzard]

Here's a tactic mode proof.

example (p q : Prop) : ¬(p ∨ q) ↔ ¬p ∧ ¬q :=
begin
  -- goal is an iff so let's split it
  split,
  { -- ¬(p ∨ q) → ¬p ∧ ¬q
    intro hnpq,
    split,
    { intro hp,
      apply hnpq,
      left,
      assumption
    },
    { intro hq,
      apply hnpq,
      right,
      assumption
    }
  },
  { -- ¬p ∧ ¬q → ¬(p ∨ q)
    intro hnpnq,
    cases hnpnq with hnp hnq,
    intro hpq,
    cases hpq,
      contradiction,
      contradiction
  }
end

[Kevin Buzzard]

If you cut and paste that into VS Code and turn on "info view: display goal" (ctrl-shift-enter) and then click around, you will be able to see Lean's tactic state at any point in the proof.

[Kevin Buzzard]

$ is just function composition at super-low priority. In practice you can use it instead of brackets. Instead of f (g x) you can write f $ g x

[Kevin Buzzard]

example (p q : Prop) : ¬(p ∨ q) ↔ ¬p ∧ ¬q :=
⟨λ h, ⟨λ hp, h (or.inl hp), λ hq, h (or.inr hq)⟩, λ hn h, or.elim h hn.1 hn.2⟩

[Jesse Michael Han]

$ is the third line of code in core.lean:

notation f ` $ `:1 a:0 := f a

f $ blah blah blah takes everything on the right and feeds it as a single argument to the left.

[Kevin Buzzard]

There's a $-free version

[Patrick Massot]

By the way, Lean is an Interactive Theorem Prover, not an Automatic one.

Actually Lean used to be a fully automatic theorem prover. You would post any statement here and, a few seconds later, Mario would output a Lean proof. Unfortunately, after a long struggle, Mario's advisor found a way to make him do the work he was actually supposed to do. So we lost this automation.

[Kevin Buzzard]

We need to automate him.

[Jesse Michael Han]

maybe Lean has the I/O capability for setting up a tactic so that every time by mario is called, he gets PMed with the proof state on Zulip...

maybe an April Fools Day project

[Jose Balado]

Thanks, will take a look at the Tactics mode, looks really interesting. Now I am not sure if to keep working as I was or redo all the 3.6 theorems that I solved using tactics.
o.k pretty simple that $, thanks

[Kevin Buzzard]

One of the exercises in the tactic mode chapter is "now go back and do all the exercises in tactic mode"

[Jose Balado]

Thanks a lot to all for your answers, not completely sure about that answer mentioning certain Mario :)

[Mario Carneiro]

No one mentioned the obvious answer:

import logic.basic
example (p q : Prop) : ¬(p ∨ q) ↔ ¬p ∧ ¬q := not_or_distrib

For obvious reasons, this isn't a great way to answer homework problems, but it's also important to know that all of these are already proven in the library, and you should never be proving it yourself when it comes up in a more complicated example

[Mario Carneiro]

Also, your first example is actually a generalization of the second one. If you give it a name, you have a one line proof like so:

variables {p q r : Prop}
theorem or_imp_distrib : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) :=
iff.intro
(assume hpqr : (p ∨ q) → r, show (p → r) ∧ (q → r), from
  ⟨(assume hp : p, show r, from hpqr(or.inl hp)),
   (assume hq : q, show r, from hpqr(or.inr hq))⟩)
(assume hprqr : (p → r) ∧ (q → r), show (p ∨ q) → r, from
  (assume hpq : p ∨ q, show r, from
    or.elim hpq
    (assume hp : p, show r, from hprqr.left hp)
    (assume hq : q, show r, from hprqr.right hq)
  )
)
example (p q : Prop) : ¬(p ∨ q) ↔ ¬p ∧ ¬q := or_imp_distrib

[Jose Balado]

Thanks Mario, really interesting your last example. example (p q : Prop) : ¬(p ∨ q) ↔ ¬p ∧ ¬q := or_imp_distrib
but this doesn't work for me:

import logic.basic
example (p q : Prop) : ¬(p ∨ q) ↔ ¬p ∧ ¬q := not_or_distrib

file 'logic/basic' not found in the LEAN_PATH

Will check that later

[Patrick Massot]

It suggests you didn't install mathlib

[Jose Balado]

I am using VS Code, how can I install mathlib? Any link with instructions?

[Jose Balado]

And Elan extension, it seems it automatically installed Lean

[Kevin Buzzard]

Try the readme here: https://github.com/leanprover-community/mathlib . If it is not all easy please let us know. I am really hoping it's getting to the point where it's all easy.

[Jose Balado]

Thanks Kevin, will let you know as soon as I install it

[Kevin Buzzard]

You'll probably let me know that everything has gone orange and it's taking ages to compile.

[Kevin Buzzard]

Make sure you figure out the update_mathlib magic sauce

[Jose Balado]

Sorry @Kevin Buzzard , I was unable to install mathlib. I don't use python so probably I am doing something wrong, but after installing pip, and setuptools with the --user option, I was able to run this command and it all seemed fine:

curl https://raw.githubusercontent.com/leanprover-community/mathlib/master/scripts/remote-install-update-mathlib.sh -sSf | sh

but this mathlib scripts are already added to $PATH in .profile doesn't seem to work on Linux Mint/Ubuntu.

And when I go to ~/.mathlib/bin and execute ./update-mathlib I got this error:

/home/aris/.local/lib/python3.5/site-packages/requests/__init__.py:91: RequestsDependencyWarning: urllib3 (1.25.1) or chardet (3.0.4) doesn't match a supported version!
  RequestsDependencyWarning)
Error: No leanpkg.toml found

If I download the repository mathlib-scripts-###-###-###.tar.gz and run ./update-mathlib.py
I got this:

/home/aris/.local/lib/python3.5/site-packages/requests/__init__.py:91: RequestsDependencyWarning: urllib3 (1.25.1) or chardet (3.0.4) doesn't match a supported version!
  RequestsDependencyWarning)
Traceback (most recent call last):
  File "./update-mathlib.py", line 25, in <module>
    lib = leanpkg['dependencies']['mathlib']
KeyError: 'mathlib'

Will it be possible to manually copy that definition directly not_or_distrib or perhaps manually copy the folder logic from mathlib to where my exercises are and import the logic library with import?
Thanks

[Patrick Massot]

you are meant to run update-mathlib inside your project root folder

[Patrick Massot]

Could you please try that and report here?

[Jose Balado]

Thanks Patrick, if I run inside my project: update-mathlib

/home/aris/.local/lib/python3.5/site-packages/requests/__init__.py:91: RequestsDependencyWarning: urllib3 (1.25.1) or chardet (3.0.4) doesn't match a supported version!
  RequestsDependencyWarning)
Error: No leanpkg.toml found

[Patrick Massot]

I need more info: where exactly did you run that command, and what is the content of that directory?

[Jose Balado]

but I had manually update-mathlib to the . bashrc file

export PATH="$HOME/.elan/bin:$PATH"
export PATH="$HOME/.mathlib/bin:$PATH"

[Jose Balado]

The content is just a file called: 3.Propositions_and_Proofs.lean

[Patrick Massot]

Then this is not a project

[Jose Balado]

is a folder where I run this project using VSCode

[Patrick Massot]

did you use leanpkg new?

[Patrick Massot]

We cannot do much for you if you don't follow the instructions at https://github.com/leanprover-community/mathlib/blob/master/docs/elan.md#scenario-1-start-a-new-package

[Jose Balado]

Ah, thanks Patrick, that must be it

[Patrick Massot]

The end of those instructions is outdated in the sense that it doesn't use update-mathlib, but everything up to installation of uncompiled mathlib is ok

[Jose Balado]

Didn't know that way of running Lean, will work on that, thanks.
I was simply using VSCode to run Lean, a little like in the browser, and following Theorem Proving in Lean.
Will try that

[Kevin Buzzard]

We cannot do much for you if you don't follow the instructions at https://github.com/leanprover-community/mathlib/blob/master/docs/elan.md#scenario-1-start-a-new-package

We need to make it easier for beginners.

[Patrick Massot]

Yes I know

[Patrick Massot]

Now my teaching and my perfectoid spaces are done, I firmly intend to come back to this

[Kevin Buzzard]

Can't we make some Lean sample project, and host it on community mathlib?

[Kevin Buzzard]

A sample project with Lean 3.4.2 and mathlib some version guaranteed to be (a) relatively close to master and (b) update-mathlib must work? And a src directory with a random theorem, like a maths proof involving equivalence relations or something.

[Kevin Buzzard]

And also a file in it called CLICK_HERE_TO_INSTALL_ALL_LEAN_THINGS.exe

[Kevin Buzzard]

and then we just tell people to clone it and click on the right thing

[Kevin Buzzard]

and it installs VS Code and the Lean extension and it all just works

[Patrick Massot]

This is not so easy to do in a platform-independent way

[Patrick Massot]

@Jose Balado did you follow the instruction? Anything you hide from us is preventing us to improve the instructions from beginners.

[Jose Balado]

Thanks Patrick will let you know as soon as possible, but not sure if today :)

[Jose Balado]

Well, I think if I had read everything I would have realized about that. The thing is that that the elan plugin for VSCode makes things so simple to start working that I didn't even put more attention to the rest of the README.md. I was just very happy reading Theorem Proving in Lean and doing proofs of theorems.
I of course had a vague idea that there should be a way to create packages and link libraries in Lean, but didn't really worry about that.
Some time ago I tried to install Agda, but gave up as soon as I was able to magically run Lean through VSCode.
I think what you are proposing of a sample project and just click here and have everything working would be fantastic, mostly for people that are completely on their own, without an instructor or any one to help you by your side.

[Patrick Massot]

I really don't understand how long it can take to run this leanpkg +3.4.2 new my_playground, cd my_playground, leanpkg add leanprover/mathlib and update-mathlib

[Patrick Massot]

On my machine it literally takes less than ten seconds if I copy paste the commands

[Jose Balado]

Well yes, I tried that, and to that point it worked, but to be sure I need understand what I am doing, try to prove a theorem, import that library, and see if everything is working.

[Patrick Massot]

Ah ok. The next step is to fire VScode, go to File menu/Open folder, select my_playgroun. Create inside my_playgroung/src a file called test.lean and type in that file, for instance,

import topology.basic
#check topological_space

[Jose Balado]

give me 30 minutes

[Jose Balado]

Hi @Patrick Massot , sorry for delay, it is working: I can see this message on the Lean messages window:

topological_space : Type u_1 → Type u_1

thanks a lot for your help!!!

[Patrick Massot]

No problem! In the end, did you do anything not covered by documentation?

[Jose Balado]

I suppose this works because I first run:

curl https://raw.githubusercontent.com/leanprover-community/mathlib/master/scripts/remote-install-update-mathlib.sh -sSf | sh

[Jose Balado]

And it was a little bit tricky on my system to make it work

[Patrick Massot]

Why was it tricky?

[Jose Balado]

Mostly because of python, I had to install pip, and setuptools. Discovered the need to add this option --user

[Jose Balado]

just running curl didn't work, but I guess it is something related with how Python is installed in Ubuntu

[Patrick Massot]

Do you have output to paste?

[Patrick Massot]

This kind of things is hard to test because it's hard to find a computer lacking python and pip

[Patrick Massot]

I guess we should be serious about it and use virtual machines with stripped down linux

[Jose Balado]

No sorry, I closed the windows, but I will install this in another computer. So could try to copy and paste

[Jose Balado]

Ubuntu has Python installed, and should have pip too

[Jose Balado]

but setuptools was not there

[Jose Balado]

Also, I had to add this to .bashrc file, they were added to .profile but didn't work

export PATH="$HOME/.elan/bin:$PATH"
export PATH="$HOME/.mathlib/bin:$PATH"

[Patrick Massot]

Did you source .profile?

[Patrick Massot]

or logout/login?

[Jose Balado]

yes, I logout and login, that worked only when I added it to .bashrc

[Jose Balado]

Also, it is not the first time I have problems with Python, for the rest, really easy to install

[Bryan Gin-ge Chen]

.profile is ignored if you have .bash_profile, I noticed this on my mac as well.

[Jose Balado]

I don't have .bash_profile, but I know there are differences in behavior between different Unix related to this.

[Patrick Massot]

I think all this is really hard to get right on all computers (and I'm not even thinking about Windows). At some point we'll have to give up on this weird setup and package stuff on a per Linux distribution basis (plus the MacOS thing)

[Jose Balado]

sorry Patrick, you were right about login/logout, after restarting the computer, I no longer need to include it into .bashrc, for sure it would work just closing the session, but I usually don't do that, I usually open too many things, and I don't know how to open a login console inside a graphical session

[Patrick Massot]

I know it's a pain to close a session simply to install something.

[Patrick Massot]

That's clearly unsatisfying

[Jose Balado]

Hi @Patrick Massot , these are the commands to install all Python dependencies needed for Mathlib.
Operating system version: Linux Mint 18.3 Sylvia

sudo apt install python3-pip
// update to latest pip
pip3 install --user --upgrade pip
// open new terminal
pip install --user setuptools
// log out/login from the user session
curl https://raw.githubusercontent.com/leanprover-community/mathlib/master/scripts/remote-install-update-mathlib.sh -sSf | sh

Caveat: Now pip command refers to pip3 not to pip2

[Patrick Massot]

Thanks Jose! Hopefully the missing setuptools error was fixed yesterday, and all this should be unnecessary (except for the last line).