How does Lean figure out this proof?

Stream: new members

[Eric Rodriguez]

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)

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

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]

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

[Eric Rodriguez]

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

[Eric Rodriguez]

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]

You need open mytype

[Mario Carneiro]

this is mentioned in a later code block

[Eric Rodriguez]

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

[Mario Carneiro]

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]

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]

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