Coq：Ltac 表示蕴涵的传递性（a.k.a。假设三段论）

Question

这个问题是关于我正在做的一个项目，即用Coq编写Principia Mathematica。 Principia已推导出推理规则，其中之一是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.

我在应用它时遇到的错误（在下面的示例中）是：

No matching clauses for match.

我不确定为什么会出现此错误。引入经典逻辑，我证明了一个定理Syll2_06，即(P→Q)→((Q→R)→(P→R))。事实上，基本上 Syll Ltac 被应用在定理 Trans2_16 的证明中（见下文）。所以我不确定为什么将代码转换为 Ltac 脚本不起作用。

也许我误解了 Ltac match 是做什么的，以及“=>”右边的策略应该是什么。但是根据 Coq manual 的观察，可能是策略的左侧有问题，可能是因为 H1 不适用于 H2。

进一步的建议，特别是解释 Ltac 的建议 and/or 我在思考它时的错误，将不胜感激。

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 吗？它是否应该在上下文中添加一个 P -> R 类型的新术语（即命名为 D）？

比如你想要一个战术来解决目标，你可以使用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 将自行找到使用哪些假设来构建证明。

Coq：Ltac 表示蕴涵的传递性（a.k.a。假设三段论）

Coq: Ltac for transitivity of implication (a.k.a. hypothetical syllogism)

match

implication

coq

ltac