在COQ中建立关系协会的最佳方法

发布于 2025-02-12 12:05:12 字数 504 浏览 0 评论 0原文

我有一个关系C，该C采用三个参数。它代表了我的理论的运作。因此C（A，B，C）代表A = B @ C，但是我没有（成功地）在COQ中定义该操作员，因此我仅使用关系C。我希望这种关系是关联的：（ D @ e） @ f = d @（e @ f）。我必须用C表示。我想到了两个公理，但是我不知道哪一个是最好的（如果它们都是正确的）。

Parameter Entity: Set.
Parameter C : Entity -> Entity -> Entity -> Prop.

Axiom asso1 : forall a c d e,
  ((exists b, C a b c /\ C b d e) <-> (exists f, C a d f /\ C f e c)).

Axiom asso2 : forall s t u a b c d,
  (C a s t -> C b a u -> C d s c -> C c t u -> b = d).

您如何看待它？

原文

I’ve a relation C that takes three parameters. It represents an operation of my theory. So C(a, b, c) represents a = b @ c, however I didn’t (succeed to) define this operator in Coq, so I use only the relation C. I want this relation to be associative: (d @ e) @ f = d @ (e @ f). And I have to express it with C. I thought of two axioms, but I don’t know which one is best (if they’re are both correct).

Parameter Entity: Set.
Parameter C : Entity -> Entity -> Entity -> Prop.

Axiom asso1 : forall a c d e,
  ((exists b, C a b c /\ C b d e) <-> (exists f, C a d f /\ C f e c)).

Axiom asso2 : forall s t u a b c d,
  (C a s t -> C b a u -> C d s c -> C c t u -> b = d).

What do you think about it?

分享到QQ

分享到微博

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

发布评论

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

赤濁 2025-02-19 12:05:12

如果您也知道C是功能关系（即，它代表一个函数），则两个公理都是等效的：每个输入对映射到唯一的输出。

(* A functional relation is one that is total and deterministic in the following sense: *)
Axiom total_C : forall a b, exists c, C c a b.
Axiom deterministic_C : forall a b c c', C c a b -> C c' a b -> c = c'.

Both axioms are equivalent if you also know that C is a functional relation (i.e., it represents a function): every input pair maps to a unique output.

(* A functional relation is one that is total and deterministic in the following sense: *)
Axiom total_C : forall a b, exists c, C c a b.
Axiom deterministic_C : forall a b c c', C c a b -> C c' a b -> c = c'.

回复收藏 0 原文

~没有更多了~