在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)}.

在这个定义中,我认为定义是专门化的,因为如果我想定义单词,我将重新定义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.

平凡:forall(G:Set)(f:G - > G - > G)(e:G),(forall a:G,fae = a) - > forall ab:G,f(fae)b = fab

至于你的最后一个例子,它可能不是关于组的实际定义,而是关于证明该操作的集合,二元操作和四个公理定义一个组.