使用COQ中的运算符和操作员的通勤性

发布于 2025-01-18 06:44:44 字数 658 浏览 2 评论 0原文

我正在尝试使用逻辑和操作员的通勤性在COQ中证明某些内容。我对这个简短的示例进行了编码：

Axiom ax1 : A /\ B.
Theorem th1 : B /\ A.
Proof.
  pose proof (ax1) as H.
  symmetry.
  apply H.
Qed.

我在证明中使用axiom（ax1），然后卡在对称命令上。这是我目前的目标：

1 subgoal
H : A /\ B
______________________________________(1/1)
B /\ A

当我使用对称命令时，我会收到以下错误：

Tactic failure:  The relation and is not a declared symmetric relation. Maybe you need to require the Coq.Classes.RelationClasses library.

我当前的解决方案是破坏假设H，分开目标并将正确的子疗法应用于正确的子go。它需要很大的空间，无法使用和交换性有些沮丧。

所以我有一些问题：对称是与交换性关系使用的正确命令吗？如果是，我该如何修复代码以使其正常工作？如果没有，是否有一种方法可以使用和操作员的通勤性？

原文

I’m trying to prove something in Coq using the commutativity of the logic AND operator. I coded this short example:

Axiom ax1 : A /\ B.
Theorem th1 : B /\ A.
Proof.
  pose proof (ax1) as H.
  symmetry.
  apply H.
Qed.

I use axiom (ax1) in my proof, and I get stuck on the symmetry command. This is my current goal:

1 subgoal
H : A /\ B
______________________________________(1/1)
B /\ A

When I use the symmetry command, I get the following error:

Tactic failure:  The relation and is not a declared symmetric relation. Maybe you need to require the Coq.Classes.RelationClasses library.

My current solution is to destruct hypothesis H, split the goal, and apply the right sub-hypothesis to the right subgoal. It takes a lot of space and is a bit frustrating to not be able to use AND commutativity.

So I’ve some questions: is symmetry the right command to use with a commutative relation? If yes, how can I fix my code for it to work? If not, is there a way to use the commutativity of the AND operator?

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

美煞众生 2025-01-25 06:44:44

您可以为任何关系做对称策略工作……只要您首先证明它是对称的。这是在标准库中进行平等的（这就是为什么Symmetry在开箱即用的原因），但不能用于和。
因此，如果要使用它，则必须自己执行此操作，例如：

Require Import RelationClasses.

Instance and_comm : Symmetric and.
Proof.
  intros A B [].
  now split.
Qed.

RealationClasses标准库的模块声明symmetric typeclass，coq时使用您称之为对称策略。接下来，我们证明和确实是对称的，并将其声明为Symmetric类的实例。完成此操作后，对称按照您的期望工作。

You can make the symmetry tactic work for any relation… as long as you show first that it is symmetric. This is done in the standard library for equality (which is why symmetry works for it out of the box), but not for and.
So if you want to use it, you have to do it yourself, like so:

Require Import RelationClasses.

Instance and_comm : Symmetric and.
Proof.
  intros A B [].
  now split.
Qed.

The RelationClasses module of the standard library declares the Symmetric typeclass, which is used by Coq when you call the symmetry tactic. Next we prove that and is indeed symmetric, and declare this as an instance of the Symmetric class. Once this is done, symmetry works as you expect it to.

回复收藏 0 原文

冷︶言冷语的世界 2025-01-25 06:44:44

对称策略专门用于推理相等性（a = b iff b = a）。

我不知道交换运算符的通用机制，但你可以用这样的东西找到你需要的引理：（

Search _ (?a /\ ?b <-> ?b /\ ?a)

我作弊：最初，我使用 -> 并只切换到 <-> 当没有找到任何东西时！）

在基础库中只有一个这种形式的引理，它被称为 and_comm。您应该能够用它来解决剩余的证明义务：apply and_comm。

The symmetry tactic is specifically for reasoning about equalities (a = b iff b = a).

I don't know of general machinery for commutative operators, but you can find the lemma you need with something like this:

Search _ (?a /\ ?b <-> ?b /\ ?a)

(I cheated: originally, I used -> and only switched to <-> when that didn't find anything!)

There's exactly one lemma of this form in the base library and it's called and_comm. You should be able to solve your remaining proof obligation with it: apply and_comm.

回复收藏 0 原文

~没有更多了~