1

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

∀ PQR : 道具, P→Q, Q→R : P→R

我正在尝试创建一个对 Syll 推理形式进行编码的 Ltac 脚本。以下来自（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))。事实上，基本上是 Syll 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.
4

1 回答 1

0

我不确定您希望该策略如何发挥作用。如果我们这样开始：

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不采用H1andH2作为参数，Coq 将自行找到用于构建证明的假设。

于 2020-09-14T08:03:26.620 回答