`using`关键字对`blast`的作用？为何两种调用方式效果不同？

• using XXX的核心作用是在调用blast前，把XXX（可以是定理、假设、本地事实等）直接加入当前证明的上下文环境。当blast启动证明搜索时，它会把这个上下文里的所有内容当作可用前提来用，就像你提前手动声明了这个事实一样。这也是为什么using XXX apply blast能完成证明——blast能直接拿到XXX来辅助推理。

• 而apply (blast mod: XXX)是完全不同的逻辑：blast的mod参数是用来调整它内部的推理规则集合的，比如intro指定优先用引入规则、elim指定优先用消除规则、del是移除某些规则，带!是强制应用这些调整。但XXX作为事实，根本不属于blast的推理规则范畴，所以不管你怎么设置mod的参数，blast都不会把XXX当作前提来用，自然没法完成证明。

举个直白的例子：假设你有定理P → Q，当前目标是证明Q，且已知P。using P apply blast会把P放进上下文，blast就能结合P → Q和P直接推出Q；但apply (blast mod: P)相当于告诉blast“把P当成推理规则来用”，这本身就不符合mod参数的设计逻辑，所以完全无效。

简单总结：using给blast送“推理素材”，mod参数是给blast定“推理规矩”，两者根本不是一回事。

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