@claude add grind examples

[alok]

it's to be a workhorse tactic for filling stuff out.

see:

• https://lean-lang.org/doc/reference/latest/The--grind--tactic/#grind
• https://markushimmel.de/blog/my-first-verified-imperative-program/

make new issues with gh to have us give concrete examples for ai's benefit

[claude]

Claude finished @alok's task —— View job • claude/issue-101-20250707_184656 • Create PR ➔

---

Todo List

• Read CLAUDE.md for repository guidelines
• Research grind tactic from provided links
• Examine existing Lean files to understand code structure
• Create grind examples file
• Create GitHub issues documenting the examples (unable due to bash permissions - documented planned issues instead)
• Commit changes and provide PR link

Summary

I've created docs/GrindExamples.lean with 22 comprehensive examples of the grind tactic, demonstrating:

• Basic equality and congruence reasoning
• Arithmetic reasoning capabilities
• Custom lemmas with @[grind] attribute
• Comparisons with other tactics (simp, ring, linarith)
• Limitations and best practices

The file includes detailed comments explaining when to use grind and when other tactics are more appropriate.

To create the GitHub issues as requested, you'll need to grant bash permissions or create them manually with gh issue create. The planned issues would cover:

1. Basic equality and congruence reasoning
2. Arithmetic reasoning capabilities
3. Custom lemmas with @[grind] attribute
4. Comparison with other tactics
5. Limitations and best practices