Lean assignment from Kenny

Stream: general

[Kenny Lau]

(optional) assignment for the people here who are too bored:
Consider this inductive type:

inductive nested : Type
| nest : list nested → nested

Level 1: Write a definition nested.cases_on' and prove its equational lemmas.
Level 2: Prove that this type has decidable equality (no, @[derive decidable_eq] won't work).
Level 3: Write a definition mem such that mem x (nest L) iff list.mem x L and prove that mem is well-founded.
Level 4: Prove that this type is denumerable (i.e. constructively countable).

[Kenny Lau]

(I've done levels 1-3 and will upload the code later)

[Kevin Buzzard]

Should this be a structure?

[Kenny Lau]

can you make it a structure?

[Kevin Buzzard]

I don't know. I only mention it because I am dimly aware that if you make something a structure then it does some of the work for you. And it only has one constructor...

[Kenny Lau]

I'm not sure whether inductive or structure comes with more tools, but I don't think you can make this a structure

[Kevin Buzzard]

I remember the days when I was bored. I have far too much to do nowadays to even contemplate being bored!

[Kenny Lau]

Answers: https://github.com/kckennylau/Lean/blob/master/nested.lean

[Kenny Lau]

here's a choice function:

[Kenny Lau]

def choice : Π x : nested, x ≠ nest [] → { z // z ∈ x }
| (nest [])       H := absurd rfl H
| (nest (hd::tl)) H := ⟨hd, (mem_def _ _).2 $ or.inl rfl⟩

[Kevin Buzzard]

Somebody should collect up these puzzles which appear here occasionally and make a little challenge page somewhere.

[Kenny Lau]

such as in your blog?

[Kenny Lau]

someone pointed out to me that my type is the type of all finite trees

[Kevin Buzzard]

Do you want to write a guest post about this problem? I look at it and I think "I'd like to work on that, but I am too busy trying to deal with the questions my UROP students are asking me".

[Kenny Lau]

I'm busy reading ANT and AM and all that :-)

[Kevin Buzzard]

I saw Mario explicitly pointing out in a conference talk that there was not enough number theory in mathlib. I say that we begin to concentrate on fixing this.

[Kenny Lau]

I'd say that among all things, the theory of fin.dim. vector spaces is a prerequisite

[Kevin Buzzard]

What exactly do you need? I have several people working on this.

[Kenny Lau]

determinant and trace, right

[Kevin Buzzard]

I have several people working on det too

[Kenny Lau]

Cayley-Hamilton would be great

[Kenny Lau]

I mean, you know much more ANT than me

[Kevin Buzzard]

right, indeed, that's precisely what I'm a world expert in :-)

[Kenny Lau]

then why are you asking me lol

[Kevin Buzzard]

I'm asking you to implement it ;-)