Zulip Chat Archive

Stream: general

Topic: Long invariants


Martin Dvořák (Oct 31 2022 at 09:46):

[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 (Oct 31 2022 at 10:41):

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 (Oct 31 2022 at 10:42):

For comparison, the hairiest invariant I ever had to set up was in the chain docs#submodule.basis_of_pid_auxdocs#submodule.nonempty_basis_of_piddocs#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 (Oct 31 2022 at 11:03):

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 (Oct 31 2022 at 11:06):

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 (Oct 31 2022 at 11:08):

Which definition are you talking about?

Anne Baanen (Oct 31 2022 at 11:26):

I mean submodule.basis_of_pid_aux

Martin Dvořák (Oct 31 2022 at 11:32):

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.


Last updated: Dec 20 2023 at 11:08 UTC