Chapter 3 done - ex 3.6.12 is harder than I expected

Stream: Analysis I

[Rado Kirov]

I have been slogging away at chapter 3 exercises every night for 2-3 hours in the last month and finally finished all of Chapter3. It was lots of fun, I learned a lot of more about Lean than what I knew from the tutorials I read, and I am getting really hooked on formalization. Big thanks to everyone that answered my questions here. I am not university affiliated, and have no other place to discuss this (other than with Claude).

Sadly, the last 1-2 weeks were spend almost exhaustively on exercise 3.6.12 i) - finally closed it today, but it is a 500 line proof (I don't golf) that only compiles with set_option maxHeartbeats 1500000.

https://github.com/rkirov/analysis/blob/856821e029ae309d70efd7e5eb4929189d6d2d59/analysis/Analysis/Section_3_6.lean#L2749

I knew eventually I will have to learn how to style my proofs better and deal with performance improvements, but a bit surprised how quickly I ended up in that territory (given how basic the math involved is).

The theorem is asking to show (Permutations (n + 1)).card = (n + 1) * (Permutations n).card, where Permutations are bijective functions from Fin (n + 1) to Fin (n + 1). The proof goes something like this:

• define an explicit map F, it takes a permutation f and splits into \< f n, f' \>, where f' is same as f but subtracts one from all f x values that are above f n. Thus f' is Fin n \to Fin n function.
• prove f' is injective
• prove f' is surjective
• prove F is injective, by getting two f' and g' and showing they must have come from the same f.
• prove F is surjective, by starting with f', and generate a new f by undoing the removal of fx. For this new f, show that it is a bijection, then show that F f = \< f n, f'\>.
• now the cardinalities are the same

Not trivial, but still surprising how painful it all became at the end (especially with the performance problems). Note this very similar to the proof for card_erase and that was a great work up to it.

Some specific surprises/areas of improvement for me:

• the high number of additional Fin lemmas I needed. Despite Fin being so simple, there are so many permutations of paths between Fin, Object, \N and each can have _injective theorems, diagram commutes theorems, etc. see https://github.com/rkirov/analysis/blob/856821e029ae309d70efd7e5eb4929189d6d2d59/analysis/Analysis/Section_3_5.lean#L882-L943 Should I upstream them all (have to learn how to name them better)?
• learn how to refactor Lean proofs - despite knowing how work with 1000+ loc programs and how to refactor them into shape, I find myself struggling doing the same with lean code. On a very basic level, refactoring code begins with take a common expression and given it a name - a new variable, function. But in lean, I find that new lets actually pollute the proof state if they dont' come with just the right theorems. But it is hard to figure out which theorems to add right away - there could be more than actually needed. For example I learned from card_erase to add hf_def theorem right after defining f - https://github.com/rkirov/analysis/blob/856821e029ae309d70efd7e5eb4929189d6d2d59/analysis/Analysis/Section_3_6.lean#L2762-L2789 but I am not sure that is the precisely most useful shape of theorem (there are many variations like .val version instead of toNat)?

[Rado Kirov]

Any general advice for general lean refactoring 500+ loc proofs. Pulling out theorems is hard when dependent types make so much of the proof state interdependent.

Is there a way to tell Lean something like set i = <some complex expression> and if <complex expression> pops up during some simplification rewrite it back to i throughout the whole proof. This of course should be turned off when I am writing helper theorems for i.

Somewhat more concretely in the monster proof above I kept seeing Fin_embed n (n+1) (by omega) i so I defined i': Fin (n + 1) := Fin_embed _ _ (by omega) i with hi' but now I had the second problem of when to work with i' vs i and if my proof had a mixture it became even harder to see what to do next. So I wasn't even sure if that extra variable helped me write cleaner more readable proof. Is there a way to be consistent here?

[Ruben Van de Velde]

set i := ... with hi and simp [← hi] maybe?

[Terence Tao]

There is also the tactic refold_let though I personally haven't used it (I tend to just leave these terms expanded and rely on definitional equality to allow rewriting etc. to still work even if visually it doesn't look like it will)

[Terence Tao]

It may possibly be helpful to define functions on all of Nat rather than Fin n but assign junk values to the natural numbers beyond n. This is less elegant mathematically but can remove one layer of casting in the whole process.

[Terence Tao]

eg count permutations from Nat to Nat that fix everybody above n, and only at the end show that this is in bijection to permutations on Fin n. This should remove the need for a ton of Fin lemmas

[Terence Tao]

Or maybe even do it on Mathlib's Nat first so that one gains access to all sorts of toys like linarith and omega, and then biject it back to SetTheory.Set.Nat and then to Fin

[Terence Tao]

Of course Mathlib already has the permutation cardinality calculation at docs#Nat.card_perm and a few other places, so that's an even shorter option, though not in the spirit of the exercise, :grinning_face_with_smiling_eyes:

[Rado Kirov]

It may possibly be helpful to define functions on all of Nat rather than Fin n but assign junk values to the natural numbers beyond n. This is less elegant mathematically but can remove one layer of casting in the whole process.

That's a neat idea, will give it a try sometimes to see how the proof looks.