We present the design and implementation of the Small Scale Reflection proof methodology and tactic language (a.k.a. SSR) for the Lean 4 proof assistant. Like its Coq predecessor SSReflect, our Lean 4 implementation, dubbed LeanSSR, provides powerful rewriting principles and means for effective management of hypotheses in the proof context. Unlike SSReflect for Coq, LeanSSR does not require explicit switching between the logical and symbolic representation of a goal, allowing for even more concise proof scripts that seamlessly combine deduction steps with proofs by computation. In this paper, we first provide a gentle introduction to the principles of structuring mechanised proofs using LeanSSR. Next, we show how the native support for metaprogramming in Lean 4 makes it possible to develop LeanSSR entirely within the proof assistant, greatly improving the overall experience of both tactic implementers and proof engineers. Finally, we demonstrate the utility of LeanSSR by conducting two case studies: (a) porting a collection of Coq lemmas about sequences from the widely used Mathematical Components library and (b) reimplementing proofs in the finite set library of Lean's mathlib4. Both case studies show significant reduction in proof sizes.

翻译：我们介绍了面向Lean 4证明助手的小规模反射证明方法和策略语言（简称SSR）的设计与实现。与其Coq前身SSReflect类似，我们的Lean 4实现（称为LeanSSR）提供了强大的重写原则以及有效管理证明上下文中假设的手段。与Coq的SSReflect不同，LeanSSR无需在目标逻辑表示与符号表示之间显式切换，从而能够编写更简洁的证明脚本，无缝地将演绎步骤与基于计算的证明相结合。本文首先温和地介绍了使用LeanSSR结构化机械化证明的原则；其次，展示了Lean 4对元编程的原生支持如何使LeanSSR完全在证明助手中开发，显著提升了策略实现者和证明工程师的整体体验；最后，通过两个案例研究——(a) 从广泛使用的数学组件库移植一组关于序列的Coq引理，以及(b) 在Lean的mathlib4有限集合库中重新实现证明——展示了LeanSSR的实用性。两个案例均表明证明规模显著缩减。