-
Notifications
You must be signed in to change notification settings - Fork 51
/
Copy pathgr.v
109 lines (87 loc) · 3.11 KB
/
gr.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
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
(* 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.
Require Import Laws.
Require Import Group_definitions.
Section group_trivialities.
Variable U : Type.
Variable Gr : Group U.
Let G : Ensemble U := G_ U Gr.
Let star : U -> U -> U := star_ U Gr.
Let inv : U -> U := inv_ U Gr.
Let e : U := e_ U Gr.
Definition G0 : forall a b : U, In U G a -> In U G b -> In U G (star a b) :=
G0_ U Gr.
Definition G1 : forall a b c : U, star a (star b c) = star (star a b) c :=
G1_ U Gr.
Definition G2a : In U G e := G2a_ U Gr.
Definition G2b : forall a : U, star e a = a := G2b_ U Gr.
Definition G2c : forall a : U, star a e = a := G2c_ U Gr.
Definition G3a : forall a : U, In U G a -> In U G (inv a) := G3a_ U Gr.
Definition G3b : forall a : U, star a (inv a) = e := G3b_ U Gr.
Definition G3c : forall a : U, star (inv a) a = e := G3c_ U Gr.
Hint Resolve G1.
Hint Resolve G2a G2b G2c.
Hint Resolve G3a G3b G3c.
Hint Resolve G0.
Theorem triv1 : forall a b : U, star (inv a) (star a b) = b.
intros a b; try assumption.
rewrite (G1 (inv a) a b); auto.
rewrite G3c; auto.
Qed.
Theorem triv2 : forall a b : U, star (star b a) (inv a) = b.
intros a b; try assumption.
rewrite <- (G1 b a (inv a)); auto.
rewrite (G3b a); auto.
Qed.
Theorem resolve : forall a b : U, star b a = e -> b = inv a.
intros a b H'1.
cut (star (star b a) (inv a) = inv a).
rewrite <- (G1 b a (inv a)); auto.
rewrite (G3b a); auto.
rewrite (G2c b); auto.
rewrite H'1.
rewrite (G2b (inv a)); auto.
Qed.
Theorem self_inv : e = inv e.
apply resolve; auto.
Qed.
Theorem inv_star : forall a b : U, star (inv b) (inv a) = inv (star a b).
intros a b.
apply resolve.
rewrite <- (G1 (inv b) (inv a) (star a b)).
rewrite (G1 (inv a) a b).
rewrite (G3c a).
rewrite (G2b b); auto.
Qed.
Theorem cancellation : forall a b : U, star a b = a -> b = e.
intros a b H'.
cut (star (inv a) (star a b) = b).
rewrite H'.
rewrite (G3c a); auto.
rewrite (G1 (inv a) a b).
rewrite (G3c a); auto.
Qed.
Theorem inv_involution : forall a : U, a = inv (inv a).
intro a; apply resolve; auto.
Qed.
End group_trivialities.
Hint Resolve G1.
Hint Resolve G2a G2b G2c.
Hint Resolve G3a G3b G3c.
Hint Resolve G0.
Hint Resolve triv1 triv2 resolve self_inv inv_star inv_involution.