Coq:如何添加有意义的提示?

Posted

技术标签:

【中文标题】Coq:如何添加有意义的提示?【英文标题】:Coq: How to add meaningful hints? 【发布时间】:2013-12-23 14:08:41 【问题描述】:

我是 Coq 的新手,可能做错了事。在我看来,我需要在编写人类可读的公理/定理和作为提示有用的公理/定理之间做出选择,因为在人类可读的形式中,它们“隐藏”了太多语法,自动策略失败使用它们。我想知道是否有什么方法可以两全其美。

我将举一个稍微详细的例子,否则我担心我将无法传达我的意思。

作为一项学习练习,我正在尝试进行群体理论。这是我的定义:

Variable G: Set.
Variable op: G -> G -> G.
Variable inv: G -> G.
Variable e:G.
Infix "+" := op.
Notation "- x" := (inv x).

Definition identity x := forall a:G, a + x = a /\ x + a = a.

Definition associative_law := forall a b c:G, a + (b + c) = (a + b) + c.
Definition identity_law := identity e.
Definition inverse_law := forall a:G, a + (-a ) = e /\ -a + a = e.
Definition group_laws:= associative_law /\ identity_law /\ inverse_law.
Axiom group_laws_hold: group_laws.

我试图让所有内容都易于阅读(至少对我而言)。所以说 e 是同一性的公理“隐藏”在两层抽象之后:“group_laws”和“identity”。

我也可以直接写这个公理(嗯,我需要一半):

 Axiom identity_law_holds: forall a:G, a + e = a.

现在,让我们以我们的群公理作为提示:

Hint Resolve group_laws_hold.

现在我尝试证明一个关于组的简单陈述 - 身份是唯一的:

Theorem identity_is_unique: forall x:G, identity x -> x = e.
Proof.
intros.
transitivity (op x e).
symmetry.

到目前为止,一切都很好。现在我当前的目标是“x + e = x”。如果我现在这样做

apply group_laws_hold.

这个目标将得到解决。然而,执行“auto”没有任何作用,可能是因为 Coq 无法识别“group_laws_hold”与“x + e = x”相关,因为“group_laws_hold”与“x + e”的语法不同= x"。

但是,如果我添加提示

Hint Resolve identity_law_holds.    

那么“自动”当然会起作用。但是,如果我将“identity_law_holds”稍微更改为更通用(更正确)的东西

 Axiom identity_law_holds: forall a:G, a + e = a /\ e + a = a.

那么“auto”又会失败。

所以我的问题是:有没有办法修复我的代码,使“auto”可以工作,但提示比我的“Axiom identity_law_holds: forall a:G, a + e = a”更一般?

【问题讨论】:

【参考方案1】:

eauto 能够进行一些规范化。 eauto不能做的是感应, 因为像and_ind 这样的归纳原理的结论是如此普遍 会减慢eauto 几乎停止。无论如何,eauto 使用 intros 在使用eapply 之前经常需要进行归纳之前 介绍任何东西。

您必须定义自己的不太一般的预测。

Lemma l1 : group_laws -> identity_law.
Proof. intros [? [? ?]]. eauto. Qed.

Lemma l2 : identity_law -> identity e.
Proof. eauto. Qed.

Lemma l3 : forall x, identity x -> forall a, a + x = a.
Proof. intros. einduction H. eauto. Qed.

Lemma l4 : forall x, identity x -> forall a, x + a = a.
Proof. intros. einduction H. eauto. Qed.

Hint Resolve eq_sym eq_trans group_laws_hold l1 l2 l3 l4.

Theorem identity_is_unique: forall x, identity x -> x = e.
Proof. info_eauto 7. Qed.

但你可以强制eauto 使用and_ind

Hint Extern 1 => eapply and_ind.

【讨论】:

以上是关于Coq:如何添加有意义的提示?的主要内容,如果未能解决你的问题,请参考以下文章

代码整洁之道第二章——有意义的命名

Coq:添加“强归纳”策略

GITHUB添加SSH内容

代码整洁之道

怎样设计接口

如何编写有意义的文档字符串?