## 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

:-)

#### 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


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


aah

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)


satisfied?

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

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

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

great

see you

:P

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

in the computing department?

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

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

oh

use java for OOP

oh

oh

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?

heh

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

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

push for lean

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

Of couse

(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.

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

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

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?

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

curriculum

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: May 12 2021 at 05:19 UTC