## Stream: new members

### Topic: On the side of logic

#### Dan Stanescu (Feb 20 2020 at 14:20):

Hi everyone: The manual online has this example among the problems at the very end of chapter 3:

example : P ∨ ¬P :=  sorry


and states classical reasoning is needed. I came up with the following:

variable P : Prop
local attribute [instance] classical.prop_decidable
example : P ∨ ¬P :=
begin
push_neg at h,
apply h.left, exact h.right,
end


but am wondering if someone with a stronger foundation in logic could comment: is there a more first-principles proof than this?

#### Donald Sebastian Leung (Feb 20 2020 at 14:23):

A simpler proof would just use classical.em. If you really want to prove it from first principles then you would probably have to somehow derive it from propext, quot.sound and classical.choice (all of which the built-in classical.em depends on)

#### Dan Stanescu (Feb 20 2020 at 14:23):

Also, watching a Coq video inspired me to try this:

-- prove Peirce <-> em
def peirce := ∀ P Q : Prop,  (( P → Q ) → P ) → P
def lem := ∀ P : Prop, P ∨ ¬P

theorem peirce_imp_em : peirce → lem :=
begin
unfold peirce,
intros pei P,
have H1 := pei (P ∨ ¬P),
have H2 : P ∨ ¬P → P ∨ ¬P, from self_to_self (P ∨ ¬P),


but I'm having trouble completing this proof because of what appears to be not enough knowledge of Lean. Anyone can help?

#### Dan Stanescu (Feb 20 2020 at 14:24):

@Donald Sebastian Leung Right, using classical.em is very easy because it is totally equivalent. But it's not very illuminating.

#### Donald Sebastian Leung (Feb 20 2020 at 14:25):

Dan Stanescu said:

Donald Sebastian Leung Right, using classical.em is very easy because it is totally equivalent. But it's not very illuminating.

True - the first principles proof would probably need all 3 of those axioms as I mentioned above (which I have not attempted to prove).

#### Rob Lewis (Feb 20 2020 at 14:26):

The answer kind of depends on what "first principles" you want to start from. If your first principles are "the axioms of Lean including its version of choice," the argument can be seen here: https://github.com/leanprover-community/lean/blob/master/library/init/classical.lean

#### Rob Lewis (Feb 20 2020 at 14:26):

It's not trivial to follow.

#### Dan Stanescu (Feb 20 2020 at 14:27):

@Rob Lewis Great, I'll take a look. I'm just wondering what the authors of the manual meant by a proof at that point.

#### Donald Sebastian Leung (Feb 20 2020 at 14:28):

Dan Stanescu said:

Also, watching a Coq video inspired me to try this:

-- prove Peirce <-> em
def peirce := ∀ P Q : Prop,  (( P → Q ) → P ) → P
def lem := ∀ P : Prop, P ∨ ¬P

theorem peirce_imp_em : peirce → lem :=
begin
unfold peirce,
intros pei P,
have H1 := pei (P ∨ ¬P),
have H2 : P ∨ ¬P → P ∨ ¬P, from self_to_self (P ∨ ¬P),


but I'm having trouble completing this proof because of what appears to be not enough knowledge of Lean. Anyone can help?

I've probably done this in Coq before since I completed Chapter 6 of Logical Foundations quite a while ago but I can't remember off the top of my head. Anyway, if you decide to attempt that exercise then you should completely avoid classical reasoning

#### Anne Baanen (Feb 20 2020 at 14:30):

My suggestion is to show ¬¬(P ∨ ¬P) without using classical reasoning, then use one of the various classical axioms (e.g. Peirce) to show that this implies P ∨ ¬P.

#### Rob Lewis (Feb 20 2020 at 14:32):

Dan Stanescu said:

Rob Lewis Great, I'll take a look. I'm just wondering what the authors of the manual meant by a proof at that point.

Honestly, I have no idea :) the easier exercise is to prove it using classical.by_contradiction (avoiding classical.em and any of the tactics that will use classical logic implicitly).

#### Rob Lewis (Feb 20 2020 at 14:33):

In your tactic proof, by_contradiction is fine, but push_neg is cheating.

#### Bryan Gin-ge Chen (Feb 20 2020 at 14:35):

In fact, tactics aren't introduced at all until chapter 5, so the intended proof should probably be in term mode.

#### Rob Lewis (Feb 20 2020 at 14:36):

To clarify: by "cheating" I don't mean that it's using classical logic, I mean that it's doing some reasoning you may want to practice.

#### Dan Stanescu (Feb 20 2020 at 14:43):

Thanks to all! I did get hooked to tactics before term mode because of my initial contact with Lean being through some YouTube videos, but I should turn back to term mode.
@Anne Baanen Either way I still have trouble producing in Lean the required term to which I could apply Peirce. Nevertheless, thanks for the advice!

#### Donald Sebastian Leung (Feb 20 2020 at 14:46):

I did get hooked to tactics before term mode ...

Understandable, IMO constructing a proof using tactics is much more pleasant than doing it in term mode, especially when you get to use black magick automation :wink: It sometimes makes me wonder how it feels to be an Agda developer ...

#### Kevin Buzzard (Feb 20 2020 at 15:33):

Dan Stanescu said:

...because of my initial contact with Lean being through some YouTube videos...

Oh wow. What YouTube videos are driving people here? I keep meaning to put up some simple 5 minute videos doing basic stuff but somehow never seem to get around to it.

#### Martin Kleiven (Feb 20 2020 at 15:37):

Definitely do that!

I was introduced to LEAN by your talk "The Future of Mathematics" which hit first page on /r/programming, and later the article on chalkdust.

Something like https://wwwf.imperial.ac.uk/~buzzard/lean_together/lean_intro.mp4 demonstrating different aspects of lean would be nice. I want to show everyone else how cool lean is but my competency is not quite there yet!

#### Kevin Buzzard (Feb 20 2020 at 15:38):

ha ha if you get competent then you can make the videos yourself :-) There are some professional video people at Imperial who I want to work with but unfortunately they want to make professional videos and I just want to knock up some random rough and ready thing.

#### Martin Kleiven (Feb 20 2020 at 15:46):

That's something I have considered. I find, in addition to the formal abstracts project, the promise of using lean for education is very interesting.

I wonder if it is possible to use lean as a back-end for some kind of user-friendly graphical interface for learning proofs that wouldn't require any programming.

#### Kevin Buzzard (Feb 20 2020 at 15:54):

There is already something like this in Coq I believe?

#### Donald Sebastian Leung (Feb 20 2020 at 15:55):

Kevin Buzzard said:

There is already something like this in Coq I believe?

Yeah, probably GeoCoq/GeoProof or something like that

#### Donald Sebastian Leung (Feb 20 2020 at 15:55):

But it's specific to geometry, I believe

#### Kevin Buzzard (Feb 20 2020 at 15:58):

Really nicely done, GUI where you can pull in things like induction etc

#### Martin Kleiven (Feb 20 2020 at 15:59):

I couldn't find anything thus far, ProofGeneral looks like something but it's not specific to Coq, plus it runs inside Emacs

#### Dan Stanescu (Feb 20 2020 at 16:00):

@Kevin Buzzard I started by looking at some videos by Zachary Goldstein. There's a big lack of videos on Lean. Apart from those, the only other ones were Scott Morisson's install guide and a talk about proving compilers correct I think.

#### Patrick Massot (Feb 20 2020 at 16:02):

Kevin means https://www.edukera.com/

#### Martin Kleiven (Feb 20 2020 at 16:02):

That's true. I'm not sure if there's a point in spending too much effort if lean 4 is on the way and contains breaking changes

#### Martin Kleiven (Feb 20 2020 at 16:02):

Thanks @Patrick Massot, I'll have a look :)

#### Donald Sebastian Leung (Feb 20 2020 at 16:04):

Patrick Massot said:

Kevin means https://www.edukera.com/

Just out of interest, how much of what Coq can do can this GUI do? Would I be able to, for example, define my own inductive data type?

No.

#### Patrick Massot (Feb 20 2020 at 16:05):

You can only do exercises, and only the exercises that were created by the creators of this site.

#### Donald Sebastian Leung (Feb 20 2020 at 16:05):

Aha, I see

Interesting nonetheless

#### Patrick Massot (Feb 20 2020 at 16:06):

At least last time I checked, teachers using this website couldn't create any new exercise.

#### Donald Sebastian Leung (Feb 20 2020 at 16:08):

Speaking of GUIs teaching the fundamentals of proof, it reminds me of The Incredible Proof Machine

Basically, it reduces propositional logic and its inference rules to connecting components in a circuit

#### Dan Stanescu (Mar 16 2020 at 18:50):

Tried recently to talk my colleagues in the philosophy department into looking at Lean, which I think would be a great benefit to students, and got feedback of this kind:

We are using Lemmon’s natural deduction system, which has only ten primitive rules and a particular way of keeping track of dependencies. For example, our rule of conditional proof (conditionalization) has, in contrast to many others, a built-in formal relevance condition that is expressed in dependency numbers. Would Lean be able to mimic such a rule?


I don't think there is any problem. Since I'm not at all familiar with Lemmon's system (apart from Wikipedia) though and pretty new to Lean as well, is there someone with a solid background in formal logic who could comment on whether Lean would have trouble there or not?

#### Jesse Michael Han (Mar 16 2020 at 21:37):

the #explode command will attempt to print proof terms in such a tabular format

#### Chris B (Mar 16 2020 at 21:55):

You can also pretty explicitly enumerate and reference named items using term mode/structured proofs.

example (a b c : Prop) : (a → b) → (b → c) → a → c :=
assume h1 : a → b,
assume h2 : b → c,
assume h3 : a,
have h4 : b, from h1 h3,
show c, from h2 h4


The exact definition of "relevance condition" they're using is probably something more involved, maybe you can get them to send you an example?

#### Dan Stanescu (Mar 22 2020 at 16:46):

Jesse Michael Han said:

the #explode command will attempt to print proof terms in such a tabular format

Where is #explode hiding? It looks like my Lean installation (version 3.4.2) can't find it.

#### Kevin Buzzard (Mar 22 2020 at 16:48):

import tactic

def x := 3



#### Kevin Buzzard (Mar 22 2020 at 16:48):

The def is to work around the fact that you can't have a #something directly after the imports.

#### Kevin Buzzard (Mar 22 2020 at 16:49):

import tactic.explode would also work

#### Dan Stanescu (Mar 22 2020 at 16:52):

The first time I see this, but if I only have import tactic it doesn't work. It does work if I have:

import tactic.explode

def x := 3



#### Kevin Buzzard (Mar 22 2020 at 16:53):

I don't know what works in 3.4.2, I tend to keep up to date with Lean and mathlib. The new tooling makes this really easy. Just go into the root directory of your project folder and type leanproject up. I was doing this with 3.7.something

#### Dan Stanescu (Mar 22 2020 at 16:58):

I'm a little confused with versions. The Lean GitHub page seems to say that 3.4.2 is the latest version (obviously not true, so I don't know what I'm doing wrong there) and doing update-mathlib just keeps the same 3.4.2 version without a leanproject command.

#### Kevin Buzzard (Mar 22 2020 at 16:58):

You are using a frozen repo and frozen tooling.

#### Kevin Buzzard (Mar 22 2020 at 16:59):

Lean 3 development now happens over at https://github.com/leanprover-community ; there is a non-MS community fork.

#### Kevin Buzzard (Mar 22 2020 at 17:00):

here is where to start.

#### Kevin Buzzard (Mar 22 2020 at 17:00):

MS are developing Lean 4 and have lost interest in supporting Lean 3 any more, so some of the amazing people here on this chat are doing the bug fixes etc.

#### Kevin Buzzard (Mar 22 2020 at 17:02):

I think it should be made much clearer on the fork README that this is a community fork and in active development.

#### Kevin Buzzard (Mar 22 2020 at 17:03):

@Wojciech Nawrocki don't you think that the README on the community fork need a serious update? It should be made clear that the fork is not MS-endorsed but that it is in active development.

#### Kevin Buzzard (Mar 22 2020 at 17:04):

Oh -- I guess this is kind of there in the "IMPORTANT" coment :-)

#### Kevin Buzzard (Mar 22 2020 at 17:05):

Would it be normal to say the current release number at the top of the README? "3.7.2c" or whatever?

#### Patrick Massot (Mar 22 2020 at 17:08):

In particular, Leo's version does mention the community fork very visibly.

#### Mario Carneiro (Mar 22 2020 at 17:08):

I think it would help to have the current version in the readme as well, to put the 3.4.2 in context

#### Kevin Buzzard (Mar 22 2020 at 17:08):

OK. I misread the "important" comment on the commuity fork as saying "This is 3.4.2 and it will not change any more"

#### Kevin Buzzard (Mar 22 2020 at 17:08):

That was what prompted my comment.

#### Mario Carneiro (Mar 22 2020 at 17:09):

there should also be a link to leanprover/lean repo somewhere on the readme. I am surprised to see that leanprover-community/lean is not actually a fork according to github

#### Kevin Buzzard (Mar 22 2020 at 17:11):

Maybe the very first line of the README should make it clear that this is a fork of the official repo, whatever Github claims, and that the current version is whatever it is.

#### Mario Carneiro (Mar 22 2020 at 17:13):

I think the "Important:" comment should lead with the community version. Something like:

Lean 3.7.2 Community Edition
Important: This fork is maintained and updated by the Lean community. The last official release for Lean 3.x is Lean 3.4.2, which can be found here. The Lean developers are currently developing Lean 4.