Coq:含意传递性的Ltac (即a.假设三段论)

Question

这个问题是关于我正在做的一个项目，也就是用Coq编码原则。原则推导出推理规则，其中之一是系统：

∀P Q R:支柱，P→Q，Q→R : P→R

我正在尝试创建一个Ltac脚本来编码Syll推断表单。(奇利帕拉2019年)的以下MP策略非常有效：

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

在这里，我认为"=>“右边的策略是H1在H2中的应用。现在，相关的系统策略不起作用：

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)。实际上，系统Ltac基本上是应用于定理Trans2_16的证明(见下文)。因此，我不知道为什么将代码转换为Ltac脚本不起作用。

也许我误解了Ltac比赛所做的，以及"=>“右边的战术应该是什么。但从Coq手册的角度来看，问题可能在于策略的左边，可能是因为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.

Answer 1

我不知道你想让这个策略怎样发挥作用。如果我们是这样开始的：

Variables P Q R S : Prop.

Goal (P -> Q) -> (S -> Q) -> (Q -> R) -> P -> R.
  intros A B C.

然后目标是：

  A : P -> Q
  B : S -> Q
  C : Q -> R
  ============================
  P -> R

你想让Syll A C做什么？

它应该解决这个目标吗？它是否应该将C修改为R？它是否应该在上下文中添加一个类型为D的新术语(即命名为P -> R )？

例如，如果您想要一个解决目标的策略，可以使用apply

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

如果您想在上下文中添加一个新术语，可以使用assert来构造它

Ltac Syll H1 H2 N:=
  match goal with 
  | [ H1 : ?P -> ?Q, H2 : ?Q -> ?R |- ?P -> ?R ] =>
    assert (N: P -> R) by (intros p; apply (H2 (H1 p)))
  end.

还请注意，如果Syll不以H1和H2作为参数，Coq将自行找到用来构造证明的假设。