-
Notifications
You must be signed in to change notification settings - Fork 51
/
Copy pathLaws.v
48 lines (36 loc) · 1.83 KB
/
Laws.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
(* Contribution to the Coq Library V6.3 (July 1999) *)
(****************************************************************************)
(* *)
(* Group Theory in Coq *)
(* *)
(* *)
(* Coq V5.10 *)
(* *)
(* Gilles Kahn *)
(* *)
(* INRIA *)
(* Sophia-Antipolis *)
(* *)
(* January 1996 *)
(* *)
(****************************************************************************)
Require Import Ensembles.
Section Basic_laws.
Variable U : Type.
Variable op : U -> U -> U.
Definition commutative := forall x y : U, op x y = op y x.
Definition associative := forall x y z : U, op x (op y z) = op (op x y) z.
Definition left_neutral (e : U) := forall x : U, op e x = x.
Definition right_neutral (e : U) := forall x : U, op x e = x.
Definition left_inverse (inv : U -> U) (e : U) :=
forall x : U, op (inv x) x = e.
Definition right_inverse (inv : U -> U) (e : U) :=
forall x : U, op x (inv x) = e.
Variable D : Ensemble U.
Definition endo_function (f : U -> U) :=
forall x : U, In U D x -> In U D (f x).
Definition endo_operation (op : U -> U -> U) :=
forall x y : U, In U D x -> In U D y -> In U D (op x y).
End Basic_laws.
Hint Unfold endo_function endo_operation commutative associative left_neutral
right_neutral left_inverse right_inverse.