在Coq中使关系关联的最佳方法

Question

我有一个关系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).

你觉得怎么样?

Answer 1

如果您还知道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'.