On the side of logic

Stream: new members

[Dan Stanescu]

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
    by_contradiction h,
    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]

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]

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,
    by_contradiction npOnp,
    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]

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

[Donald Sebastian Leung]

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]

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]

It's not trivial to follow.

[Dan Stanescu]

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

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,
    by_contradiction npOnp,
    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]

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]

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]

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

[Bryan Gin-ge Chen]

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

[Rob Lewis]

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]

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]

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]

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]

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]

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]

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]

There is already something like this in Coq I believe?

[Donald Sebastian Leung]

Kevin Buzzard said:

There is already something like this in Coq I believe?

Yeah, probably GeoCoq/GeoProof or something like that

[Donald Sebastian Leung]

But it's specific to geometry, I believe

[Kevin Buzzard]

I was thinking about something @Patrick Massot told me about.

[Kevin Buzzard]

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

[Martin Kleiven]

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]

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

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

[Martin Kleiven]

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]

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

[Donald Sebastian Leung]

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?

[Patrick Massot]

No.

[Patrick Massot]

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

[Donald Sebastian Leung]

Aha, I see

Interesting nonetheless

[Patrick Massot]

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

[Donald Sebastian Leung]

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]

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]

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

[Chris B]

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]

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]

import tactic

def x := 3

#explode mul_add

[Kevin Buzzard]

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

[Kevin Buzzard]

import tactic.explode would also work

[Dan Stanescu]

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

#explode mul_add

[Kevin Buzzard]

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]

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]

You are using a frozen repo and frozen tooling.

[Kevin Buzzard]

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

[Kevin Buzzard]

here is where to start.

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

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

[Kevin Buzzard]

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

[Patrick Massot]

I think both the community fork README and Leo's README are pretty clear already.

[Patrick Massot]

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

[Mario Carneiro]

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]

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]

That was what prompted my comment.

[Mario Carneiro]

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]

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]

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.

[Wojciech Nawrocki]

I made lean#158 for this.

[Kevin Buzzard]

Many thanks!