我想要针对这些简单的推理规则使用 Ltac 策略。
在 Modus Ponens 中，如果我有H:P->Qand H1:P, Ltac mp H H1将添加Q到上下文为H2 : Q.
在 Modus Tollens 中，如果我有H:P->Qand H1:~Q, then Ltac mt H H1将添加H2:~P结合上下文。
我已经为“肯定前件”写了一个，但在先例也是一种暗示的复杂情况下它不起作用。
Ltac mp H0 H1 :=
let H := fresh "H" in
apply H0 in H1 as H.
编辑：我在另一个看似不相关的问题中找到了 Modus Ponens 的答案（用 Coq 重写假设，保留蕴涵 https://stackoverflow.com/questions/47520531/rewrite-hypothesis-in-coq-keeping-implication），其中“简化”版本apply是用generalize.
Ltac mp H H0 :=
let H1 := fresh "H" in
generalize (H H0); intros H1.
不过，我仍然希望 Modus Tollens 能够给出答案。
这是一种解决方案：
Ltac mt PtoQ notQ notP :=
match type of PtoQ with
| ?P -> _ => pose proof ((fun p => notQ (PtoQ p)) : ~ P) as notP
end.
该策略要求用户提供两个输入假设和输出假设的明确名称。我用type of PtoQ构建提取类型P从输入含义中得出，然后提供一个明确的术语(fun p => notQ (PtoQ p)类型的P -> False，其定义等于~ P。显式类型归属: ~ P用于使上下文看起来更漂亮，如果没有它，Coq 会将输出假设的类型显示为P -> False.
顺便说一句，我会使用类似这样的东西来实施肯定取件策略：
Ltac mp PtoQ P Q :=
pose proof (PtoQ P) as Q.
又是在这里PtoQ and P参数是输入假设的名称和Q是要添加到上下文中的名称。
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
