Zulip Chat Archive

Stream: general

Topic: proving lt from decidability

Adam Kurkiewicz (Apr 05 2018 at 08:04):

I'd like to show the following lemma:

def  big_not_zero (a : nat) (P : 1  < a) : a ≠  0  :=
λ Pp : a =  0, have olt0 : 1  <  0, from eq.subst Pp P,
false.elim (nat.decidable_lt 1  0)

Concretely, I'd like to get a proof of false from nat.decidable_lt 1 0. But I don't understand how to use decidabilty in lean.

Kevin Buzzard (Apr 05 2018 at 08:08):

example : 1 < 0 → false := dec_trivial

Kevin Buzzard (Apr 05 2018 at 08:09):

I'm not saying these things are easy to use though :-)

Kevin Buzzard (Apr 05 2018 at 08:10):

def  big_not_zero (a : nat) (P : 1  < a) : a ≠  0  :=
λ Pp : a =  0, have olt0 : 1  <  0, from eq.subst Pp P,
(show  1  <  0  → false, by exact dec_trivial) olt0

Kevin Buzzard (Apr 05 2018 at 08:10):

and as you can see, I'm certainly no master of them myself.

Kenny Lau (Apr 05 2018 at 08:12):

def big_not_zero (a : nat) (P : 1 < a) : a ≠ 0 :=
λ h, nat.not_lt_zero 1 $ h ▸ P

Kenny Lau (Apr 05 2018 at 08:12):

\> implying I'm a master of them

Kevin Buzzard (Apr 05 2018 at 08:12):

:-)

Adam Kurkiewicz (Apr 05 2018 at 08:12):

Thank you! What is exact?

Kevin Buzzard (Apr 05 2018 at 08:13):

by puts me into tactic mode

Kevin Buzzard (Apr 05 2018 at 08:13):

exact is a tactic

Kenny Lau (Apr 05 2018 at 08:13):

@Adam Kurkiewicz just do from dec_trivial instead of by exact dec_trivial

Kenny Lau (Apr 05 2018 at 08:13):

there's no need to go into tactic mode

Kevin Buzzard (Apr 05 2018 at 08:13):

I have trouble getting out of tactic mode

Adam Kurkiewicz (Apr 05 2018 at 08:14):

@Kenny Lau not working exact tactic failed, type mismatch, given expression has type

Kevin Buzzard (Apr 05 2018 at 08:14):

def  big_not_zero (a : nat) (P : 1  < a) : a ≠  0  :=
λ Pp : a =  0, have olt0 : 1  <  0, from eq.subst Pp P,
(show  1  <  0  → false, from dec_trivial) olt0

Kevin Buzzard (Apr 05 2018 at 08:14):

works for me

Adam Kurkiewicz (Apr 05 2018 at 08:14):

nevermind, that works.

Adam Kurkiewicz (Apr 05 2018 at 08:15):

I'm surprised this is not working

def  big_not_zero (a : nat) (P : 1  < a) : a ≠  0  :=
λ Pp : a =  0, have olt0 : 1  <  0, from eq.subst Pp P,
dec_trivial olt0

Kevin Buzzard (Apr 05 2018 at 08:15):

def  big_not_zero (a : nat) (P : 1  < a) : a ≠  0  :=
begin
intro H,
rw H at P,
revert P,
exact dec_trivial
end

Kevin Buzzard (Apr 05 2018 at 08:15):

aah

Kevin Buzzard (Apr 05 2018 at 08:16):

tactic mode

Kevin Buzzard (Apr 05 2018 at 08:16):

makes it all look so easy

Kenny Lau (Apr 05 2018 at 08:16):

I'm surprised this is not working

def  big_not_zero (a : nat) (P : 1  < a) : a ≠  0  :=
λ Pp : a =  0, have olt0 : 1  <  0, from eq.subst Pp P,
dec_trivial olt0

dec_trivial takes no argument

Adam Kurkiewicz (Apr 05 2018 at 08:16):

@Kevin Buzzard Where did you learn tactic mode from? last few chapters of lean tutorial?

Kevin Buzzard (Apr 05 2018 at 08:17):

Tactic mode chapter

Kevin Buzzard (Apr 05 2018 at 08:17):

I have no idea why TPIL spends so long teaching people term mode

Adam Kurkiewicz (Apr 05 2018 at 08:17):

Fair enough, I didn't last that long :D

Kevin Buzzard (Apr 05 2018 at 08:17):

For a beginner tactic mode is the bomb

Kevin Buzzard (Apr 05 2018 at 08:17):

you can see what you're doing at all times

Kevin Buzzard (Apr 05 2018 at 08:18):

what the goal is, what the hypotheses are

Kevin Buzzard (Apr 05 2018 at 08:18):

and you can try simp on every line in case it does the job

Adam Kurkiewicz (Apr 05 2018 at 08:18):

I like term mode, at least I have an illusion I understand what's going on :)

Kevin Buzzard (Apr 05 2018 at 08:18):

you have far more powerful tools available to you in tactic mode

Kevin Buzzard (Apr 05 2018 at 08:18):

and then later on you can start figuring out what the tools are doing

Kevin Buzzard (Apr 05 2018 at 08:19):

and how they're doing it

Kevin Buzzard (Apr 05 2018 at 08:19):

You say "I don't understand decidability or how to use it"

Kevin Buzzard (Apr 05 2018 at 08:19):

I say "dec_trivial invokes a great tactic"

Kevin Buzzard (Apr 05 2018 at 08:20):

so your problems are solved in the short term

Kevin Buzzard (Apr 05 2018 at 08:20):

and then in the longer term you can start wondering about what it's doing and how it's doing it

Kevin Buzzard (Apr 05 2018 at 08:20):

My method is more robust than Kenny's

Kenny Lau (Apr 05 2018 at 08:21):

My method is more robust than Kenny's

yeah right

Kevin Buzzard (Apr 05 2018 at 08:21):

because his solution relies on you knowing that there's a theorem in the library

Kevin Buzzard (Apr 05 2018 at 08:21):

called nat.not_lt_zero

Kenny Lau (Apr 05 2018 at 08:21):

implying one shouldn't know about theorems in the library

Kevin Buzzard (Apr 05 2018 at 08:21):

whereas mine just relies on you being aware that stuff like this is decidable and there's a tactic which does it

Kevin Buzzard (Apr 05 2018 at 08:21):

I am saying mine is more robust.

Kevin Buzzard (Apr 05 2018 at 08:22):

I am not saying anything about whether it's a good idea to know the library

Kevin Buzzard (Apr 05 2018 at 08:22):

What if tomorrow Adam wants to prove 2<1->false?

Kevin Buzzard (Apr 05 2018 at 08:23):

We all know it's decidable

Kevin Buzzard (Apr 05 2018 at 08:23):

and you and I know we can use no_confusion or all sorts of other tricks

Kevin Buzzard (Apr 05 2018 at 08:23):

but dec_trivial just does the job

Kenny Lau (Apr 05 2018 at 08:23):

def big_not_zero' (a : nat) (P : 1 < a) : a ≠ 0 :=
λ h, (show ¬1 < 0, from dec_trivial) (h ▸ P)

Kenny Lau (Apr 05 2018 at 08:23):

satisfied?

Adam Kurkiewicz (Apr 05 2018 at 08:24):

It's good advice Kevin, I'll learn the tactic mode.

Kenny Lau (Apr 05 2018 at 08:24):

alright

Kevin Buzzard (Apr 05 2018 at 08:24):

I think you should start with tactic mode and move on to term mode later.

Kevin Buzzard (Apr 05 2018 at 08:24):

It's what they do in Software Foundations

Kevin Buzzard (Apr 05 2018 at 08:24):

and it's what I'm doing in the book I'm writing on doing maths in Lean

Kevin Buzzard (Apr 05 2018 at 08:25):

but this is because my book is targetting mathematicians who have no idea what this lambda business is all about

Kevin Buzzard (Apr 05 2018 at 08:25):

because typically they will know no functional programming

Kenny Lau (Apr 05 2018 at 08:25):

let's replace matlab with haskell

Kevin Buzzard (Apr 05 2018 at 08:25):

They do that next door

Kevin Buzzard (Apr 05 2018 at 08:25):

in the computing department

Kenny Lau (Apr 05 2018 at 08:25):

great

Kenny Lau (Apr 05 2018 at 08:25):

see you

Kenny Lau (Apr 05 2018 at 08:26):

Kevin Buzzard (Apr 05 2018 at 08:26):

in the computing department?

Kenny Lau (Apr 05 2018 at 08:26):

right

Kevin Buzzard (Apr 05 2018 at 08:26):

Remember I'm on the curriculum review committee!

Kevin Buzzard (Apr 05 2018 at 08:26):

But I don't think I can push for Haskell for mathematicians

Kevin Buzzard (Apr 05 2018 at 08:26):

I am currently pushing for Python

Kenny Lau (Apr 05 2018 at 08:26):

i'm just kidding

Kenny Lau (Apr 05 2018 at 08:26):

but python is already there

Kevin Buzzard (Apr 05 2018 at 08:26):

but not maths in python

Kevin Buzzard (Apr 05 2018 at 08:26):

just general python

Kevin Buzzard (Apr 05 2018 at 08:26):

i.e. teach them classes etc

Kenny Lau (Apr 05 2018 at 08:27):

OOP python is the worst lol

Kevin Buzzard (Apr 05 2018 at 08:27):

Kenny Lau (Apr 05 2018 at 08:27):

use java for OOP

Kevin Buzzard (Apr 05 2018 at 08:27):

Kenny Lau (Apr 05 2018 at 08:27):

pee

Kevin Buzzard (Apr 05 2018 at 08:27):

Should I push for java?

Kevin Buzzard (Apr 05 2018 at 08:27):

Why would a mathematician want to learn java?

Kenny Lau (Apr 05 2018 at 08:27):

heh

Kevin Buzzard (Apr 05 2018 at 08:27):

I think we should just teach them tactic mode ;-)

Kenny Lau (Apr 05 2018 at 08:27):

push for lean

Kenny Lau (Apr 05 2018 at 08:28):

problem solved

Kevin Buzzard (Apr 05 2018 at 08:28):

I think that some of them might want to compute something at some point

Kevin Buzzard (Apr 05 2018 at 08:28):

maybe they do that in the applied maths parts or something

Kevin Buzzard (Apr 05 2018 at 08:28):

I have no idea what they do there

Kevin Buzzard (Apr 05 2018 at 08:28):

but I don't think it's theorems

Johannes Hölzl (Apr 05 2018 at 08:28):

Of couse

Johannes Hölzl (Apr 05 2018 at 08:29):

(deleted)

Kevin Buzzard (Apr 05 2018 at 08:29):

I think they figure out what f(10) is if they know some differential equation satisfied by f, and also they know f(0)

Kenny Lau (Apr 05 2018 at 08:29):

@Johannes Hölzl wrong chat

Adam Kurkiewicz (Apr 05 2018 at 08:34):

@Kevin Buzzard I'd say teaching OOP is a bad idea. OOP is kind of dying at the moment anyway -- very few new languages actually have rich OOP features (rust, golang), and even in python very little new stuff gets written using OOP.

We've got a great new guy at Glasgow, who's teaching first year programming in python. He uses jupyter notebooks and shows applications of computation to multiple different problems (simulating fireworks, solving Travelling Salesman, etc.). I've done a guest lecture on Nim this year (https://github.com/picrin/nim_game/tree/master/lab_material/lab17_student_material).

I think that's a more productive use of student's time than teaching them OOP.

Kenny Lau (Apr 05 2018 at 08:35):

I insisted to not use jupyter

Kenny Lau (Apr 05 2018 at 08:35):

even in the exam :P

Kenny Lau (Apr 05 2018 at 08:35):

python -m pip install numpy

Kevin Buzzard (Apr 05 2018 at 08:36):

So I am in the maths department at Imperial College London and we're having a top-to-bottom curriculum review, and amongst the things that can change is that we can completely rethink what we teach to the undergraduates in terms of programming.

Kevin Buzzard (Apr 05 2018 at 08:36):

So I am definitely genuinely interested in hearing people's opinions.

Kevin Buzzard (Apr 05 2018 at 08:36):

However we are definitely focussed on what mathematicians should need to know

Kevin Buzzard (Apr 05 2018 at 08:37):

in the sense of "what people who employ mathematicians want them to know"

Adam Kurkiewicz (Apr 05 2018 at 08:37):

You'd obviously want to modify the content a little bit to make it more mathsy, but I think coding up an optimal algorithm to play Nim is definitely a worthy thing to teach first year mathematicians.

Kevin Buzzard (Apr 05 2018 at 08:37):

Your link doesn't work btw

Adam Kurkiewicz (Apr 05 2018 at 08:39):

Ah, it's hidden from students cause it has solutions :D. one moment

Kevin Buzzard (Apr 05 2018 at 08:39):

don't worry

Kevin Buzzard (Apr 05 2018 at 08:39):

I don't want to disrupt

Adam Kurkiewicz (Apr 05 2018 at 08:44):

That's the task statement: lab17-3.html

There are ~7 specific python template files, which walk them through a solution, and they have to implement each one.

Each file gets automatically checked using something called "CMS", I believe stands for "Contest Management System". Checking uses a regular test suite.

Adam Kurkiewicz (Apr 05 2018 at 08:46):

Happy to share everything if you'd like, but at the moment I'm tethering and the internet is a bit slow.

Kevin Buzzard (Apr 05 2018 at 08:46):

honestly don't worry

Kevin Buzzard (Apr 05 2018 at 08:47):

I can imagine what is there

Kevin Buzzard (Apr 05 2018 at 08:47):

I always imagine stuff like nim as being in the recreational mathematics box

Kevin Buzzard (Apr 05 2018 at 08:48):

i.e. stuff they do outside of regular maths

Kevin Buzzard (Apr 05 2018 at 08:48):

but I am not 100% sure whether I have this in the right box

Kevin Buzzard (Apr 05 2018 at 08:49):

python has ^ -- do you let them use this or force them to code their own?

Adam Kurkiewicz (Apr 05 2018 at 08:54):

I let them use that after they've learned how it works.

Kevin Buzzard (Apr 05 2018 at 08:56):

Just the opposite of what I did with my kids

Kevin Buzzard (Apr 05 2018 at 08:56):

I asked them how to compute powers in python and let them be completely confused for 15 minutes

Adam Kurkiewicz (Apr 05 2018 at 08:56):

it's generally a problem with teaching python, it has everything and students sometimes just solve things with one-liners, without ever understanding it.

Kevin Buzzard (Apr 05 2018 at 08:56):

just like tactic mode ;-)

Kenny Lau (Apr 05 2018 at 08:57):

I don't normally use numpy and sympy :P

Kevin Buzzard (Apr 05 2018 at 08:57):

Kenny, what do we teach the 1st years?

Kevin Buzzard (Apr 05 2018 at 08:57):

Currently

Kevin Buzzard (Apr 05 2018 at 08:57):

Do they import a lot of libraries?

Kevin Buzzard (Apr 05 2018 at 08:57):

scipy?

Kenny Lau (Apr 05 2018 at 08:58):

numpy and sympy

Kenny Lau (Apr 05 2018 at 08:58):

I thought you're the head of curiculum reform

Kenny Lau (Apr 05 2018 at 08:58):

curriculum

Kenny Lau (Apr 05 2018 at 08:58):

words

Kevin Buzzard (Apr 05 2018 at 09:00):

I'm just on the committee

Kevin Buzzard (Apr 05 2018 at 09:00):

my job is to decide what to do in the future

Kenny Lau (Apr 05 2018 at 09:00):

well you're the acting head of the department

Kevin Buzzard (Apr 05 2018 at 09:00):

I don't want to pollute my understanding by knowing what we currently do

Kevin Buzzard (Apr 05 2018 at 09:01):

Maybe I should go and fill in forms :-/

Kenny Lau (Apr 05 2018 at 09:02):

how many goddam forms do you have

Kevin Buzzard (Apr 05 2018 at 09:02):

they come in at a rate faster than I can fill them in

Kenny Lau (Apr 05 2018 at 09:02):

what are those forms

Kevin Buzzard (Apr 05 2018 at 09:03):

I had to do a risk assessment form for Ana because she's pregnant. 6 pages of questions such as how much radioactive material there was in the department etc. Life is great when you're a manager.

Kevin Buzzard (Apr 05 2018 at 09:04):

OK I'm going to fill in more right now

Kenny Lau (Apr 05 2018 at 09:04):

life is always great

Andrew Ashworth (Apr 05 2018 at 09:43):

I think between python, R, and Matlab, that's quite enough for a maths student... in a way I'm a little sad you can't get by without just pen, paper, and coffee pot

Patrick Massot (Apr 05 2018 at 19:42):

@Kevin Buzzard I'd say teaching OOP is a bad idea. OOP is kind of dying at the moment anyway -- very few new languages actually have rich OOP features (rust, golang), and even in python very little new stuff gets written using OOP.

We've got a great new guy at Glasgow, who's teaching first year programming in python. He uses jupyter notebooks and shows applications of computation to multiple different problems (simulating fireworks, solving Travelling Salesman, etc.). I've done a guest lecture on Nim this year (https://github.com/picrin/nim_game/tree/master/lab_material/lab17_student_material).

I think that's a more productive use of student's time than teaching them OOP.

What is this crazyness? Where did you see OOP dying?

Patrick Massot (Apr 05 2018 at 19:42):

I guess this is what Haskell people say?

Patrick Massot (Apr 05 2018 at 19:43):

But what about the real world?

Moses Schönfinkel (Apr 05 2018 at 19:49):

OOP is definitely not dying in the industry.

Patrick Massot (Apr 05 2018 at 19:54):

Yes, this very much sounds like functional programming academic fantasy

Sebastian Ullrich (Apr 05 2018 at 19:56):

To say that OOP is dying is certainly hyperbole, but none of the languages mentioned are particularly functional...

Moses Schönfinkel (Apr 05 2018 at 20:00):

Go doesn't even have generics, speaking of modern design...

Patrick Massot (Apr 05 2018 at 20:02):

Go certainly looks awful

Patrick Massot (Apr 05 2018 at 20:04):

I never saw Rust but the wikipedia page features quite a occurrences of Haskell and ML

Patrick Massot (Apr 05 2018 at 20:10):

Let's discuss something more productive: @Sebastian Ullrich am I correct in thinking that the nightly download link on https://leanprover.github.io/download/ is no longer relevant and should not be used anymore?

Chris Hughes (Apr 05 2018 at 20:13):

Let's discuss something more productive: @Sebastian Ullrich am I correct in thinking that the nightly download link on https://leanprover.github.io/download/ is no longer relevant and should not be used anymore?

Is there a new download link. It took me ages to update lean today, because MSYS didn't know where my c compiler was, and neither did I.

Patrick Massot (Apr 05 2018 at 20:13):

https://github.com/leanprover/lean-nightly/releases

Patrick Massot (Apr 05 2018 at 20:14):

You need to compare with https://github.com/leanprover/mathlib/blob/master/leanpkg.toml#L4

Patrick Massot (Apr 05 2018 at 20:14):

(my understanding is it's not yet more automatic, but this is already great progress)

Sebastian Ullrich (Apr 05 2018 at 20:15):

@Patrick Massot Correct. We're still waiting on AppVeyor enabling cron builds for us before we can make it official

Patrick Massot (Apr 05 2018 at 20:16):

Thanks

Last updated: Dec 20 2023 at 11:08 UTC