Zulip Chat Archive

Stream: new members

Topic: How does Lean figure out this proof?

Eric Rodriguez (Mar 27 2021 at 19:03):

In TPIL 8.5, there's this mysterious line:

mutual inductive even, odd
with even :   Prop
| even_zero : even 0
| even_succ :  n, odd n  even (n + 1)
with odd :   Prop
| odd_succ :  n, even n  odd (n + 1)

open even odd

theorem not_odd_zero : ¬ odd 0.

I've never seen the full stop after a statement before, but somehow it makes Lean come up with the full proof that ¬odd 0 is true (can even see it with #print not_odd_zero, which is impregnable but uses dcases_on). How does it do this?

Kevin Buzzard (Mar 27 2021 at 19:49):

The equation compiler can see that the only way to prove odd n only works when n is a successor, so it can see that there can be no constructor for odd 0. It's very good at stuff like this!

Kevin Buzzard (Mar 27 2021 at 19:50):

The full stop just means "this is the end of the proof" ie "we did all the cases"

Eric Rodriguez (Mar 27 2021 at 19:54):

Wow, it keeps being more and more powerful. Very cool!

Eric Rodriguez (Mar 28 2021 at 10:47):

Also Kevin, thanks for the great blog-post on no-confusion, it was really helpful — just wanted to say that the definition by the eqn compiler of mytype_equal' doesn't work anymore with invalid pattern, 'AA' already appeared in this pattern; so may be worth just editing it out

Mario Carneiro (Mar 28 2021 at 10:53):

You need open mytype

Mario Carneiro (Mar 28 2021 at 10:53):

this is mentioned in a later code block

Eric Rodriguez (Mar 28 2021 at 10:54):

urgh of course it's something dumb, sorry for the bother

Mario Carneiro (Mar 28 2021 at 10:54):

without that, it's interpreting AA as a variable name and the error says you can't have the same variable twice in a pattern

Mario Carneiro (Mar 28 2021 at 10:57):

There's nothing wrong with reporting a bug in a code block in a blog post, perhaps @Kevin Buzzard can add the open line there so that people don't get confused in the future

Kevin Buzzard (Mar 28 2021 at 11:36):

Fixed -- thanks!

Some of those early blog posts of mine were written as I was learning the theory myself, and I wrote something when I had understood it and didn't know of a reference which was helpful to me as a mathematician. Now I kind of get what's going on with Lean in general so I tend not to write those "beginner-type-theory" posts any more. If you or anyone else has any requests I'd be happy to have a go at writing something...

Last updated: Dec 20 2023 at 11:08 UTC