Proof fragility in Ch3.6

Stream: Analysis I

[Rado Kirov]

I just rebased my solutions on top of upstream main, and while most changes are trivial solutions for 3.6 are very broken in way that are hard to me to quickly fix. I need to spend more time thinking about what happened, but I think @Dan Abramov contributed a new simp form for Fin <-> Nat <-> Object embeddings, that is different than the one I used to work with. I can read his solutions to unblock myself, so not a big deal, just an interesting case to think about proof engineering and maintenance.

Here is an example, this is how the proof looks like after rebasing (very annoying that I can't easily see the proof state when it used to work

hx'' : ↑x = 0 -- expands to @Fin.toNat inst✝ 1 x : ℕ = 0
⊢ 0 = ↑x -- expands to @Subtype.val Object (fun x ↦ x ∈ Fin 1) x : Object
-- used to work
exact hx''.symm

I am guessing hx'' was simplifying to a statement about Objects previously.

Interesting example for my learning on how to write proofs better (now that I feel I can at least write some basic proofs in Lean) and on why Lean style matters for maintainability.

[Rado Kirov]

Fixed all proofs in 3.6, but surprisingly had to add some new cast theorems:

theorem SetTheory.Set.natToObject_toFin {n m: ℕ} (hm: (n:Object) ∈ Fin m):
    ((⟨n, hm⟩: Fin m) : ℕ) = n

theorem SetTheory.Set.toFin_iff_toNat_eq {n m n' m': ℕ} {hm: (n:Object) ∈ Fin m}
    {hm': (n':Object) ∈ Fin m'} :  ((⟨n, hm⟩: Fin m): Object) = ((⟨n', hm'⟩: Fin m'): Object) ↔ n = n'

I need to sit down and think properly what's a principled way to deal with all these statements about natural numbers, that can appear through casts in either of those types:

• matlib N
• the set of Nats
• Objects
• Fin sets

but because everything is injective one aways can move them around to the type needed. But the composition of casts are not defeq equal to the appropriate direct cast, so one has to apply the right proofs to simplify through casts.

Also sometimes one can't just peel off the outer cast because there might be incompatible inner type - e.g. ((<x, ...> : Fin n): Object) = ((<y, ...>: Fin m): Object) implies x = y, but one can't just apply object_inj. I need to think more about this, feels like there should be some tactic like push_cast that turns all statements into a normal form, not sure if simp can do it with appropriate annotations.

[Dan Abramov]

It’s possible some simp lemmas I added break reasonable things and should have the simp attribute removed (or left for aesop). I haven’t looked yet but if you have a candidate for what seems to be breaking things, lmk!

[Rado Kirov]

yeah, I wouldn't call my proofs "reasonable" :) they are obviously "my first proof" level of quality, and from now on every other solver will likely benefit from the new simps. I don't think anyone will ever write them the way I did, I only wrote them like this because I was bruteforcing through the proof state without thinking deeply about principles.

I think all new simps you added are valid, but I am curious if you used some heuristic/principle on which theorems need the attr vs ones that don't. Because we have isomorphisms between bunch of these objects:

• matlib N
• custom Nat
• Nat embedding in custom Objects
• Fin sets (technically the infinite union of those)

it doesn't seem there is an obvious direction for simps, so it's a bit of a design choice. We can push all numeric statements into mathlib N or push them all into Nat, etc with simp.

This is more a curious learning for me in general, as I am thinking about the basics of writing maintainable Lean proofs and similar proof engineering concerns. How should a core library identify and communicate such a choice, where there isn't appriori an obvious choice? How careful should the library be when changing that choice? Can the consumer write proofs that are more or less fragile in the face of a potential change here?