coq - 在 Coq 中形式化组的好方法

Question

我尝试在 Coq 中形式化组。我想尽可能地通用。我尝试做某事，但我对此并不满意。我发现了不同的实现，我不知道该选择哪一个。

例如我发现这个:

https://people.cs.umass.edu/~arjun/courses/cs691pl-spring2014/assignments/groups.html

(* The set of the group. *)
Parameter G : Set.

(* The binary operator. *)
Parameter f : G -> G -> G.

(* The group identity. *)
Parameter e : G.

(* The inverse operator. *)
Parameter i : G -> G.

(* For readability, we use infix <+> to stand for the binary operator. *)
Infix "<+>" := f (at level 50, left associativity).

(* The operator [f] is associative. *)
Axiom assoc : forall a b c, a <+> b <+> c = a <+> (b <+> c).

(* [e] is the right-identity for all elements [a] *)
Axiom id_r : forall a, a <+> e = a.

(* [i a] is the right-inverse of [a]. *)
Axiom inv_r : forall a, a <+> i a = e.

但为什么作者使用公理而不是定义？此外，我不喜欢在顶级有一些参数。

在 CoqArt 一书中，我发现了这个实现:

Record group : Type :=
{A : Type;
op : A→A→A;
sym : A→A;
e : A;
e_neutral_left : ∀ x:A, op e x = x;
sym_op : ∀ x:A, op (sym x) x = e;
op_assoc : ∀ x y z:A, op (op x y) z = op x (op y z)}.

关于这个定义我觉得这个定义是专门化的，因为如果我想定义monoïds，我会重新定义op_assoc或者neutre left。除此之外，
对于某些定理，我不需要使用组。例如，如果我想证明 right_inverse 与 left_inverse 相同，如果定律是结合的。

另一个问题是对于群体来说什么是好的公理:

使用中性元素作为公理或左中性元素

使用逆元素作为公理或左逆

什么是更方便的工作？

最后，如果我想证明一些其他定理，我可能需要一些语法糖来使用二元运算和逆元素。您对组的方便符号有什么建议？

目前我这样做了:

Definition binary_operation {S:Set} := S -> S -> S.


Definition commutative {S:Set} (dot:binary_operation) := forall (a b:S), dot a b = dot b a.

Definition associative {S:Set} (dot:binary_operation) := forall (a b c:S), dot (dot a b) c = dot a (dot b c).

Definition left_identity {S:Set} (dot:binary_operation) (e:S) := forall a:S,  (dot e a) = a.

Definition right_identity {S:Set} (dot:binary_operation) (e:S) := forall a:S,  (dot a e) = a.

Definition identity {S:Set} (dot:  binary_operation) (e:S) := left_identity dot e /\ right_identity dot e.

Definition left_inv {S:Set} (dot:binary_operation) (a' a e:S) := identity dot e -> dot a' a = e.

Definition right_inv {S:Set} (dot:binary_operation) (a' a e:S) := identity dot e -> dot a a' = e.

Definition inv {S:Set} (dot:binary_operation) (a' a e:S) := left_inv dot a' a e /\ right_inv dot a' a e.

我在 Coq 的代码源中找到了一个实现，但我不明白为什么它是一个好的实现: https://github.com/tmiya/coq/blob/master/group/group2.v

Answer 1

我无法提供完整的答案，但也许这可以对您有所帮助。

您的第一篇文章提供了足以证明练习的定义和公理，而无需过多关注“好”或“有用”的实现。这就是为什么是公理而不是定义。

如果您想“尽可能通用”，您可以使用 CoqArt 中的示例，或者使用 Variable 将您的组定义包装在一个部分中。而不是 Parameter .

Section Group.
(* The set of the group. *)
Variable G : Set.

(* The binary operator. *)
Variable f : G -> G -> G.

(* The group identity. *)
Variable e : G.

(* The inverse operator. *)
Variable i : G -> G.

(* For readability, we use infix <+> to stand for the binary operator. *)
Infix "<+>" := f (at level 50, left associativity).

(* The operator [f] is associative. *)
Variable assoc : forall a b c, a <+> b <+> c = a <+> (b <+> c).

(* [e] is the right-identity for all elements [a] *)
Variable id_r : forall a, a <+> e = a.

(* [i a] is the right-inverse of [a]. *)
Variable inv_r : forall a, a <+> i a = e.

如果你在本节中证明了一些定理，就像这样:

Theorem trivial : forall a b, a <+> e <+> b = a <+> b.
intros.
rewrite id_r.
auto.
Qed.

部分结束后，

End Group.

Coq 概括了它们

Check trivial.

trivial : forall (G : Set) (f : G -> G -> G) (e : G), (forall a : G, f a e = a) -> forall a b : G, f (f a e) b = f a b

至于你的最后一个例子，它可能不是关于群的实际定义，而是关于证明一个集合、一个二元运算和这个运算的四个公理定义了一个群。