如何解决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 举报,一经查实,本站将立刻删除。