Coq：Ltac表示涵义的传递性也称为假设三段论

问题描述

这个问题是关于我正在做的一个项目，即用Coq编写 Principia Mathematica 。 原理导出了推理规则，其中之一是Syll：

∀P Q R：道具， P→Q，Q→R：P→R

我正在尝试创建一个Ltac脚本，以对Syll推理形式进行编码。来自（Chlipala 2019）的以下MP策略非常有效：

Ltac MP H1 H2 :=
  match goal with 
    | [ H1 : ?P -> ?Q,H2 : ?P |- _ ] => specialize (H1 H2)
end.

这里，我认为“ =>”右边的策略专门将H1应用于H2。现在，相关的Syll策略不起作用：

Ltac Syll H1 H2 :=
  match goal with 
     | [ H1 : ?P -> ?Q,H2 : ?Q -> ?R |- _ ] =>
        specialize Syll2_06 with ?P ?Q ?R;
        intros Syll2_06;
        apply Syll2_06;
        apply H1;
        apply H2
end.

应用此错误（在下面的示例中）是：

没有匹配的匹配子句。

我不确定为什么这是导致的错误。引入了经典逻辑，我证明了一个定理Syll2_06，即（P→Q）→（（Q→R）→（P→R））。实际上，在定理Trans2_16的证明中应用了Syll Ltac的基本原理（请参见下文）。因此，我不确定为什么将代码转换为Ltac脚本无效。

也许我误解了Ltac比赛在做什么，以及“ =>”右边的策略应该是什么。但是基于Coq manual，可能是策略的左侧是问题所在，也许是因为H1不适用于H2。

进一步的建议，特别是那些解释Ltac和/或我在思考方式上的错误的建议，将不胜感激。

Theorem Syll2_06 : ∀ P Q R : Prop,(P → Q) → ((Q → R) → (P → R)).
    
Ltac Syll H1 H2 :=
  match goal with 
     | [ H1 : ?P -> ?Q,H2 : ?Q -> ?R |- _ ] =>
        specialize Syll2_06 with ?P ?Q ?R;
        intros Syll2_06;
        apply Syll2_06;
        apply H1;
        apply H2
end. 
    
Ltac MP H1 H2 :=
  match goal with 
    | [ H1 : ?P -> ?Q,H2 : ?P |- _ ] => specialize (H1 H2)
end.

Theorem Trans2_16 : forall P Q : Prop,(P → Q) → (~Q → ~P).
Proof. intros P Q.
  specialize n2_12 with Q. intros n2_12a.
  specialize Syll2_05 with P Q (~~Q). intros Syll2_05a.
  specialize n2_03 with P (~Q). intros n2_03a.
  MP n2_12a Syll2_05a.
  specialize Syll2_06 with (P→Q)  (P→~~Q) (~Q→~P). intros Syll2_06a.
  apply Syll2_06a.
  apply Syll2_05a.
  apply n2_03a.
Qed.

Theorem Trans2_17 : forall P Q : Prop,(~Q -> ~P) -> (P -> Q).
Proof. intros P Q.
  specialize n2_03 with (~Q) P. intros n2_03a.
  specialize n2_14 with Q. intros n2_14a.
  specialize Syll2_05 with P (~~Q) Q. intros Syll2_05a.
  MP n2_14a Syll2_05a.
  Syll 2_03a Syll2_05a.
Qed.

解决方法

暂无找到可以解决该程序问题的有效方法，小编努力寻找整理中！

如果你已经找到好的解决方法，欢迎将解决方案带上本链接一起发送给小编。

小编邮箱:dio#foxmail.com (将#修改为@）