Zulip Chat Archive

Stream: general

Topic: proving lt from decidability


view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:08):

example : 1 < 0 → false := dec_trivial

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:09):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:10):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 05 2018 at 08:12):

\> implying I'm a master of them

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:12):

:-)

view this post on Zulip Adam Kurkiewicz (Apr 05 2018 at 08:12):

Thank you! What is exact?

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:13):

by puts me into tactic mode

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:13):

exact is a tactic

view this post on Zulip Kenny Lau (Apr 05 2018 at 08:13):

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

view this post on Zulip Kenny Lau (Apr 05 2018 at 08:13):

there's no need to go into tactic mode

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:13):

I have trouble getting out of tactic mode

view this post on Zulip Adam Kurkiewicz (Apr 05 2018 at 08:14):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:14):

works for me

view this post on Zulip Adam Kurkiewicz (Apr 05 2018 at 08:14):

nevermind, that works.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:15):

aah

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:16):

tactic mode

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:16):

makes it all look so easy

view this post on Zulip 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

view this post on Zulip Adam Kurkiewicz (Apr 05 2018 at 08:16):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:17):

Tactic mode chapter

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:17):

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

view this post on Zulip Adam Kurkiewicz (Apr 05 2018 at 08:17):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:17):

For a beginner tactic mode is the bomb

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:17):

you can see what you're doing at all times

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:18):

what the goal is, what the hypotheses are

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:18):

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

view this post on Zulip Adam Kurkiewicz (Apr 05 2018 at 08:18):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:18):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:18):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:19):

and how they're doing it

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:19):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:19):

I say "dec_trivial invokes a great tactic"

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:20):

so your problems are solved in the short term

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:20):

My method is more robust than Kenny's

view this post on Zulip Kenny Lau (Apr 05 2018 at 08:21):

My method is more robust than Kenny's

yeah right

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:21):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:21):

called nat.not_lt_zero

view this post on Zulip Kenny Lau (Apr 05 2018 at 08:21):

implying one shouldn't know about theorems in the library

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:21):

I am saying mine is more robust.

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:22):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:22):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:23):

We all know it's decidable

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:23):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:23):

but dec_trivial just does the job

view this post on Zulip 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)

view this post on Zulip Kenny Lau (Apr 05 2018 at 08:23):

satisfied?

view this post on Zulip Adam Kurkiewicz (Apr 05 2018 at 08:24):

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

view this post on Zulip Kenny Lau (Apr 05 2018 at 08:24):

alright

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:24):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:24):

It's what they do in Software Foundations

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:25):

because typically they will know no functional programming

view this post on Zulip Kenny Lau (Apr 05 2018 at 08:25):

let's replace matlab with haskell

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:25):

They do that next door

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:25):

in the computing department

view this post on Zulip Kenny Lau (Apr 05 2018 at 08:25):

great

view this post on Zulip Kenny Lau (Apr 05 2018 at 08:25):

see you

view this post on Zulip Kenny Lau (Apr 05 2018 at 08:26):

:P

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:26):

in the computing department?

view this post on Zulip Kenny Lau (Apr 05 2018 at 08:26):

right

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:26):

Remember I'm on the curriculum review committee!

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:26):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:26):

I am currently pushing for Python

view this post on Zulip Kenny Lau (Apr 05 2018 at 08:26):

i'm just kidding

view this post on Zulip Kenny Lau (Apr 05 2018 at 08:26):

but python is already there

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:26):

but not maths in python

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:26):

just general python

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:26):

i.e. teach them classes etc

view this post on Zulip Kenny Lau (Apr 05 2018 at 08:27):

OOP python is the worst lol

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:27):

oh

view this post on Zulip Kenny Lau (Apr 05 2018 at 08:27):

use java for OOP

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:27):

oh

view this post on Zulip Kenny Lau (Apr 05 2018 at 08:27):

oh

view this post on Zulip Kenny Lau (Apr 05 2018 at 08:27):

pee

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:27):

Should I push for java?

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:27):

Why would a mathematician want to learn java?

view this post on Zulip Kenny Lau (Apr 05 2018 at 08:27):

heh

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:27):

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

view this post on Zulip Kenny Lau (Apr 05 2018 at 08:27):

push for lean

view this post on Zulip Kenny Lau (Apr 05 2018 at 08:28):

problem solved

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:28):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:28):

maybe they do that in the applied maths parts or something

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:28):

I have no idea what they do there

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:28):

but I don't think it's theorems

view this post on Zulip Johannes Hölzl (Apr 05 2018 at 08:28):

Of couse

view this post on Zulip Johannes Hölzl (Apr 05 2018 at 08:29):

(deleted)

view this post on Zulip 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)

view this post on Zulip Kenny Lau (Apr 05 2018 at 08:29):

@Johannes Hölzl wrong chat

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Apr 05 2018 at 08:35):

I insisted to not use jupyter

view this post on Zulip Kenny Lau (Apr 05 2018 at 08:35):

even in the exam :P

view this post on Zulip Kenny Lau (Apr 05 2018 at 08:35):

python -m pip install numpy

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:36):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:36):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:37):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:37):

Your link doesn't work btw

view this post on Zulip Adam Kurkiewicz (Apr 05 2018 at 08:39):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:39):

don't worry

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:39):

I don't want to disrupt

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:46):

honestly don't worry

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:47):

I can imagine what is there

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:47):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:48):

i.e. stuff they do outside of regular maths

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:48):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:49):

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

view this post on Zulip Adam Kurkiewicz (Apr 05 2018 at 08:54):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:56):

Just the opposite of what I did with my kids

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:56):

just like tactic mode ;-)

view this post on Zulip Kenny Lau (Apr 05 2018 at 08:57):

I don't normally use numpy and sympy :P

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:57):

Kenny, what do we teach the 1st years?

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:57):

Currently

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:57):

Do they import a lot of libraries?

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 08:57):

scipy?

view this post on Zulip Kenny Lau (Apr 05 2018 at 08:58):

numpy and sympy

view this post on Zulip Kenny Lau (Apr 05 2018 at 08:58):

I thought you're the head of curiculum reform

view this post on Zulip Kenny Lau (Apr 05 2018 at 08:58):

curriculum

view this post on Zulip Kenny Lau (Apr 05 2018 at 08:58):

words

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 09:00):

I'm just on the committee

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 09:00):

my job is to decide what to do in the future

view this post on Zulip Kenny Lau (Apr 05 2018 at 09:00):

well you're the acting head of the department

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 09:00):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 09:01):

Maybe I should go and fill in forms :-/

view this post on Zulip Kenny Lau (Apr 05 2018 at 09:02):

how many goddam forms do you have

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 09:02):

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

view this post on Zulip Kenny Lau (Apr 05 2018 at 09:02):

what are those forms

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 09:04):

OK I'm going to fill in more right now

view this post on Zulip Kenny Lau (Apr 05 2018 at 09:04):

life is always great

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Apr 05 2018 at 19:42):

I guess this is what Haskell people say?

view this post on Zulip Patrick Massot (Apr 05 2018 at 19:43):

But what about the real world?

view this post on Zulip Moses Schönfinkel (Apr 05 2018 at 19:49):

OOP is definitely not dying in the industry.

view this post on Zulip Patrick Massot (Apr 05 2018 at 19:54):

Yes, this very much sounds like functional programming academic fantasy

view this post on Zulip 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...

view this post on Zulip Moses Schönfinkel (Apr 05 2018 at 20:00):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 20:02):

Go certainly looks awful

view this post on Zulip Patrick Massot (Apr 05 2018 at 20:04):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Apr 05 2018 at 20:13):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 20:14):

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

view this post on Zulip Patrick Massot (Apr 05 2018 at 20:14):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Apr 05 2018 at 20:16):

Thanks


Last updated: May 12 2021 at 05:19 UTC