waterfall 0.2.0

Waterfall 0.2.0 is the first release since the Lean-module port. import waterfall works in both module files and ordinary Lean files; the tactic syntax remains waterfall and waterfall?.

Changes since 0.1.0:

• Proof critics now propose repairs for blocked premises, implicit constructor witnesses, fixed inductive indices, and induction/generalization choices. The optional arithmetic-witness critic has a separately checked replay path. Bounded induction continuations and conditional fact composition extend the default search without benchmark-specific rules.
• Search planning schedules expensive closers and recursive preparation against the available effort and heartbeat budget. A focused indexed-inversion critic combines a sequence of structurally constrained inversions while preserving ordinary case-analysis alternatives.
• waterfall? now prefers named introductions, native case/induction commands, nested bullets, and ordinary solver calls when its checked replacement replays. It can still fall back to a proof term for operations that cannot be rendered cleanly.
• Two separately validated performance changes reduce work in the unchanged 2,284-invocation case-study/test corpus: revised trial/focusing/solver scheduling reduced summed internal tactic time by 12.65%, then first-result compilation of explicit grind parameters reduced it by a further 13.5% relative to that revision. Both comparisons retained every checked invocation at its existing budget. These are paired single-run measurements, not a claimed end-to-end build speedup.
• The implementation now uses Lean's module system and has a smaller explicitly tested export surface. The generic typed proof-planning/result interface was extended for programmatic users; in particular Mode.hooks now also accepts the supplied rule array. The user-facing tactic calls remain the same.
• Documentation and examples were consolidated into the Lean tutorial and Markdown-generated website.

The complete inductive-bench selection was rerun at this tag on 2026-09-24. Default search proved 1,615/2,631 theorem goals, including 1,455/2,202 Software Foundations goals, versus 1,594 and 1,451 respectively at dde8f2e. It proved exactly the same goals as the September 22 revision 8d7d84b. These are individual-goal measurements with the source theory available; preceding benchmark lemmas can be assumptions. See the measurement report.

The release is tested in CI with Lean 4.30.0 and 4.33.1. The package's pinned toolchain is 4.33.1.

waterfall 0.1.0

The first public release of waterfall, an ACL2-inspired Lean tactic for inductive proofs. It includes configurable search and committed modes, a single effort control, optional parallel search, proof-command suggestions, compiled examples, and documented Software Foundations evaluation.