Long invariants

Stream: general

[Martin Dvořák]

[soft question]
How do you structure proofs which are based on invariants that are too long to state?

I am formalizing this proof:
https://github.com/madvorak/grammars/blob/main/informal/KleeneStar.pdf

The critical part, originally called Lemma 2, is stated here:
https://github.com/madvorak/grammars/blob/58466a1ead6fc9ad3f989915e03f94777fe45363/src/unrestricted/closure_properties/unary/star_RE.lean#L373

Naturally, I want to make a lemma for each case (of six in total), and possibly even more granularity. If I take the goal for each case and literally extract the goal (with the necessary context) into a new lemma, I will end having something very similar to lines 375–389 in each of the lemma statement. That would be a lot of boilerplate code.

What can I do about it? There are a few options that came to my mind.
(1) Fuck DRY. Just copy the invariant into each lemma statement.
(2) Turn the invariant into a definition. Then unfold the definition inside each proof.
(3) Carefully pass only those terms (disjuncts that can result from the given case) into each lemma. Then I cannot apply the lemma directly; I will have to do cases on the output of the lemma in order to map them into how the overall invariant is satisfied in each case.

Any recommendation, please?

[Anne Baanen]

I would go for option 1, if the invariant does not have any use outside of these lemmas. Otherwise 2 might be a good option. Basically I'd try and avoid mathematically unnecessary clutter like cases.

[Anne Baanen]

For comparison, the hairiest invariant I ever had to set up was in the chain docs#submodule.basis_of_pid_aux → docs#submodule.nonempty_basis_of_pid → docs#submodule.exists_smith_normal_form_of_le: in this proof you have to do induction in submodule.basis_of_pid_aux on essentially its own result. Maybe this gives some inspiration?

[Martin Dvořák]

Wow! You managed to prove submodule.basis_of_pid_aux in circa 100 lines. Hence you didn't need to copy the invariant into any other lemma. Am I right?

[Anne Baanen]

I guess that's one way to say it: I managed to put the invariant into the statement of one definition so it didn't have to be repeated across all usages.

[Martin Dvořák]

Which definition are you talking about?

[Anne Baanen]

I mean submodule.basis_of_pid_aux

[Martin Dvořák]

My point was that you didn't need and didn't have motivation to extract the invariant into a definition because you found a pretty compact proof. I am not that good at proving things concisely, hence I will have a lot of lemmata with my invariant.