什么是不执行任何操作的tactic？搜索empty tactic、null tactic未获解答

你搜索的empty tactic、null tactic都不是这类工具的通用命名，这类不改变证明状态、无任何执行副作用的tactic通用名称是noop tactic（取自计算机领域通用的“no operation”缩写），不同主流证明辅助工具都有对应的原生实现，常见使用场景如下：

• Coq：对应的无操作tactic是idtac，它不会修改当前证明目标，也不会抛出错误，最常用的场景包括：
  • 作为分支占位符，还没想好当前分支的证明逻辑时先填idtac保证代码结构合法
  • 配合条件tactic使用，作为分支中不需要执行操作时的占位项
  • 调试证明过程时，在中间插入idtac "调试信息"来打印当前目标上下文和自定义提示内容
• Isabelle：对应的无操作tactic是succeed，它会直接返回成功状态，不修改任何证明状态，常被用在tactic组合子的逻辑分支中
• Lean 3/4：对应的无操作tactic是skip，仅做占位使用，不产生任何证明副作用，适合填充未完成的证明分支，避免语法报错
• Agda：在交互式证明中对应的无操作占位是?，如果是tactic层面的无操作，可以使用id策略，不会改变当前证明状态

注意不要将这类无操作tactic和会失败的空tactic混淆，比如Coq中的fail会直接抛出证明失败，和idtac的作用完全相反

内容的提问来源于stack exchange，提问作者sdpoll