OmegaSequence.flatten

Stream: CSLib

[Ching-Tsun Chou]

See cslib#111. Your comments will be appreciated.

[Ching-Tsun Chou]

@Chris Henson: Thanks a lot for the comments! I'll incorporate them. As a practical matter, how did you spot all those opportunities for using grind to shorten the proofs? That's a skill I'd like to acquire.

[Chris Henson]

No problem. Here's a bit of a checklist of what I do:

• First write everything without grind annotations
• Begin by working backwards from each branch of the proof
• add = annotations to definitions and notation lemmas, which are probably safe
• Try backing up from anything that uses exact, cases, congr, etc.
• Try replacing simp and rw with grind.
• In cases where it's not possible to generate have a grind rule, you can use have beforehand to fill in arguments grind can't infer, but can use if you place in the local context
• Think about what E-matching you might need if an inferred pattern doesn't work. → and => are commonly helpful for inferring "forward" steps
• If the grind rules for each branch are reasonably overlapping, you can have have something like induction ... <;> grind [...]
• Similarly for existentials after you refine for data grind won't infer
• Finally, consider what lemmas are reasonably general enough and useful to add annotations to. Be careful of anything with a danger of recursion

[Fabrizio Montesi]

@Chris Henson I've recently switched from that approach to trying grind first. If it fails, I start writing the most obvious proof structure and try grind for every goal. Once I finally hit a place where grind works, I start going backwards and inspect why grind wasn't able to prove that goal. This often leads me to general lemmas that should really be proven separately and annotated with grind. Sometimes I manage to make everything a single call to grind, or a call to induction and then grind.

[Fabrizio Montesi]

(Recently as in a few weeks ago.. I really like grind doing the work for me. :⁠-⁠P)

[Chris Henson]

That seems reasonable too. One tangentially related point of pain is if a proof with grind later breaks and you've forgotten the regular proof structure. I've been saved a couple of times by being able to view the full proof in the commit history.

[Chris Henson]

And I agree, I am having a good experience so far. I am interested to try out the interactive mode being developed and see if that reshapes my strategies.

[Ching-Tsun Chou]

I just noticed that the Greek letter φ is used to denote the Euler totient function in the Nat namespace. Since the theory developed in Cslib/Foundations/Data/Nat/Segment.lean is also in the Nat namespace, its use of φ as a function name is potentially dangerous. So I have made a PR (cslib#116) to replaces all occurrences of φ by f and all previous occurrences of f by g. Could you review it? Thanks in advance!