-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathabelian_proof_3.v
106 lines (86 loc) · 2.67 KB
/
abelian_proof_3.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
From Group Require Export group_theory.
Section test_proof.
(* Proof using the is_abelian notation. *)
Lemma boolean_implies_abelian : (forall x : group_theory.G, x <*> x = e) -> (is_abelian group_theory.G).
Proof.
intros.
(* sub-environment for showing commutativity *)
assert (forall (a b : group_theory.G), a <*> b = b <*> a).
intros.
assert ( (a <*> b) <*> (a <*> b) = e).
apply H.
assert ( a <*> b = a <*> b ).
reflexivity.
rewrite <- (mult_e a) in H1 at 2.
rewrite <- H0 in H1.
repeat rewrite mult_assoc in H1.
assert (a <*> a = e).
apply H.
assert (b <*> b = e).
apply H.
rewrite H2 in H1.
rewrite <- mult_assoc in H1.
rewrite H3 in H1.
rewrite e_mult in H1.
rewrite mult_e in H1.
exact H1.
(* Exit that sub-environment. *)
unfold is_abelian.
exact H0.
Qed.
(* Proof without is_abelian notation *)
Theorem t1 (G : group_theory.Group) (H: forall (x : group_theory.G), x <*> x = e) : (forall (a b : group_theory.G), a <*> b = b <*> a).
Proof.
intros.
(* assert ( a <*> b : A group_theory.G) *)
assert ( (a <*> b) <*> (a <*> b) = e).
apply H.
assert ( (a <*> b) = (a <*> b) ).
reflexivity.
rewrite <- (mult_e a) in H1 at 2.
rewrite <- H0 in H1.
repeat rewrite mult_assoc in H1.
assert ( (a <*> a) = e ).
apply H.
assert ( (b <*> b) = e ).
apply H.
rewrite H2 in H1.
rewrite <- mult_assoc in H1.
rewrite H3 in H1.
rewrite (e_mult b) in H1.
rewrite mult_e in H1.
exact H1.
Qed.
(* Proof using our custom tactics *)
Theorem t2 : (forall (x : group_theory.G), x <*> x = e) -> (forall (a b : group_theory.G), a <*> b = b<*>a).
Proof.
intros .
assert_and_simpl (a<*>b) (a<*>e<*>b).
user_assert_equal (a<*>e<*>b) (a<*>((a<*>b)<*>(a<*>b))<*>b ).
now rewrite <- (H (a<*>b)).
assert_and_simpl (a <*> (a <*> b <*> (a <*> b)) <*> b) (a<*>a<*>(b<*>a)<*>(b<*>b)).
user_assert_equal (a<*>a<*>(b<*>a)<*>(b<*>b)) (e<*>(b<*>a)<*>(b<*>b)).
now rewrite (H a).
user_assert_equal (e<*>(b<*>a)<*>(b<*>b)) (e<*>(b<*>a)<*>e).
now rewrite (H b).
group.
Qed.
(* Proof using our custom tactics *)
Theorem t3 : (forall (x : group_theory.G), x <*> x = e) -> (forall (a b : group_theory.G), a <*> b = b<*>a).
Proof.
intro.
assert (forall x: group_theory.G, x = (inv x)).
intro.
apply_result (right_mult_cancel x).
rewrite H.
group.
user_assert_equal (a<*>e<*>b) (a<*>((a<*>b)<*>(a<*>b))<*>b ).
now rewrite <- (H (a<*>b)).
assert_and_simpl (a <*> (a <*> b <*> (a <*> b)) <*> b) (a<*>a<*>(b<*>a)<*>(b<*>b)).
user_assert_equal (a<*>a<*>(b<*>a)<*>(b<*>b)) (e<*>(b<*>a)<*>(b<*>b)).
now rewrite (H a).
user_assert_equal (e<*>(b<*>a)<*>(b<*>b)) (e<*>(b<*>a)<*>e).
now rewrite (H b).
group.
Qed.
End test_proof.