4

我想为这些简单的推理规则提供 Ltac 策略。

在 Modus Ponens 中，如果我有H:P->Q和H1:P，Ltac mp H H1将添加Q到上下文中作为H2 : Q.

在 Modus Tollens 中，如果我有H:P->Qand H1:~Q，那么Ltac mt H H1将添加H2:~P到上下文中。

我已经写了一个用于 ponens 的方法，但它不适用于先例也是暗示的复杂情况。

Ltac mp H0 H1 := let H := fresh "H" in apply H0 in H1 as H.

编辑：我在另一个看似不相关的问题中找到了 Modus Ponens 的答案（在 Coq 中重写假设，保持暗示），其中“简化”版本apply是用generalize.

Ltac mp H H0 := let H1 := fresh "H" in generalize (H H0); intros H1.

不过，我仍然会感谢 Modus Tollens 的回答。

4

1 回答 1

1

这是一种解决方案：

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.

顺便说一句，我会使用这样的东西来实现 modus ponens 策略：

Ltac mp PtoQ P Q := 
  pose proof (PtoQ P) as Q.

这里，PtoQ和P参数同样是输入假设Q的名称，并且是要添加到上下文中的名称。

于 2018-10-22T19:25:31.540 回答