Skip to content

Instantly share code, notes, and snippets.

@pedrominicz

pedrominicz/Group.v

Last active April 22, 2020 01:24
Show Gist options
  • Save pedrominicz/8bf340a8842608d40293494fecdc93a8 to your computer and use it in GitHub Desktop.
Save pedrominicz/8bf340a8842608d40293494fecdc93a8 to your computer and use it in GitHub Desktop.
Download ZIP
Groups in Coq: uniqueness and cancellation.
Raw
Group.v
(* https://quanttype.net/posts/2016-02-16-elementary-algebra.html *)
(* This was written while reading chapter II of "Algebra: Chapter 0". *)
Class group (A : Type) := group_mk
{ id : A
; inv : A -> A
; op : A -> A -> A
; op_id_l : forall x, x = op id x
; op_id_r : forall x, x = op x id
; op_inv_l : forall x, id = op (inv x) x
; op_inv_r : forall x, id = op x (inv x)
; op_assoc : forall x y z, op x (op y z) = op (op x y) z
}.
Arguments id {A} {group}.
Arguments op {A} {group}.
Arguments inv {A} {group}.
Arguments op_id_l {A} {group}.
Arguments op_id_r {A} {group}.
Arguments op_inv_l {A} {group}.
Arguments op_inv_r {A} {group}.
Arguments op_assoc {A} {group}.
Notation "x * y" := (op x y).
Theorem id_unique_l {A} {G : group A} : forall id',
(forall x, x = id' * x) -> id' = id.
Proof. intros. rewrite H. rewrite <- op_id_r. reflexivity. Qed.
Theorem id_unique_r {A} {G : group A} : forall id',
(forall x, x = x * id') -> id' = id.
Proof. intros. rewrite H. rewrite <- op_id_l. reflexivity. Qed.
Theorem inv_unique_l {A} {G : group A} : forall x y,
x * y = id -> y = inv x.
Proof.
intros.
rewrite op_id_r.
rewrite <- H.
rewrite op_assoc.
rewrite <- op_inv_l.
apply op_id_l.
Qed.
Theorem inv_unique_r {A} {G : group A} : forall x y,
y * x = id -> y = inv x.
Proof.
intros.
rewrite op_id_l.
rewrite <- H.
rewrite <- op_assoc.
rewrite <- op_inv_r.
apply op_id_r.
Qed.
Theorem op_cancel_l {A} {G : group A} : forall x y a,
a * x = a * y <-> x = y.
Proof.
split; intros.
- rewrite op_id_l with x, op_id_l with y.
rewrite op_inv_l with a.
rewrite <- op_assoc, <- op_assoc.
apply f_equal.
assumption.
- rewrite H.
reflexivity.
Qed.
Theorem op_cancel_r {A} {G : group A} : forall x y a,
x * a = y * a <-> x = y.
Proof.
split; intros.
- rewrite op_id_r with x, op_id_r with y.
rewrite op_inv_r with a.
rewrite op_assoc, op_assoc.
apply (f_equal (fun x => x * inv a)) in H.
assumption.
- rewrite H.
reflexivity.
Qed.
Theorem op_inv {A} {G : group A} : forall x y,
inv (x * y) = inv y * inv x.
Proof.
intros.
rewrite op_id_l.
rewrite op_inv_l with (x * y).
rewrite <- op_assoc.
assert (x * y * (inv y * inv x) = id).
{ rewrite op_assoc.
rewrite <- op_assoc with x y (inv y).
rewrite <- op_inv_r.
rewrite <- op_id_r.
rewrite <- op_inv_r.
reflexivity. }
rewrite H.
apply op_id_r.
Qed.
Lemma square_id_inv {A} {G : group A} : forall x,
x * x = id -> x = inv x.
Proof.
intros.
rewrite op_inv_r with x in H.
apply op_cancel_l in H.
assumption.
Qed.
Theorem exercise_ii_1_4 {A} {G : group A} : forall x y,
(forall x, x * x = id) -> x * y = y * x.
Proof.
intros.
pose proof (fun x => square_id_inv x (H x)) as H'.
rewrite H' with x, H' with y.
rewrite <- op_inv with x y.
repeat rewrite <- H'.
reflexivity.
Qed.
Theorem op_unique {A} {G : group A} : forall x y1 y2 z,
x * y1 = z -> x * y2 = z -> y1 = y2.
Proof.
intros x y1 y2 z H1 H2.
rewrite <- H2 in H1.
apply op_cancel_l in H1.
assumption.
Qed.
Lemma op_inv_inv {A} {G : group A} : forall x,
inv (inv x) = x.
Proof.
intros.
rewrite op_id_l.
rewrite op_inv_l with (inv x).
rewrite <- op_assoc.
rewrite <- op_inv_l.
rewrite <- op_id_r.
reflexivity.
Qed.
Theorem exercise_ii_1_5 {A} {G : group A} : forall x y,
exists! z, x * z = y.
Proof.
intros.
exists (inv (inv y * x)).
split.
- rewrite op_inv.
rewrite op_assoc.
rewrite <- op_inv_r.
rewrite <- op_id_l.
apply op_inv_inv.
- intros.
rewrite op_inv.
apply op_cancel_l with x.
rewrite op_assoc.
rewrite <- op_inv_r.
rewrite <- op_id_l.
rewrite op_inv_inv.
symmetry.
assumption.
Qed.
Lemma square_id {A} {G : group A} : forall x,
x * x = x -> x = id.
Proof.
intros.
rewrite op_id_l with x.
repeat rewrite op_inv_l with x.
rewrite <- op_assoc.
apply f_equal.
assumption.
Qed.
Theorem exercise_ii_1_6_a {G : group bool} : forall x y,
x * y = xorb id (xorb x y).
Proof.
intros.
destruct id eqn:eq, (x * y) eqn:H, x, y; auto; try rewrite <- eq in H.
- rewrite <- op_id_l in H. congruence.
- rewrite <- op_id_r in H. congruence.
- rewrite <- op_id_l in H. congruence.
- apply square_id in H. congruence.
- apply square_id in H. congruence.
- rewrite <- op_id_l in H. congruence.
- rewrite <- op_id_r in H. congruence.
- rewrite <- op_id_l in H. congruence.
Qed.
Inductive tri := aa | bb | cc.
Definition op_tri id x y :=
match (id, x, y) with
| (aa, aa, y) => y | (bb, bb, y) => y | (cc, cc, y) => y
| (aa, x, aa) => x | (bb, x, bb) => x | (cc, x, cc) => x
| (id, aa, bb) => id | (id, bb, aa) => id
| (id, bb, cc) => id | (id, cc, bb) => id
| (id, cc, aa) => id | (id, aa, cc) => id
| (aa, bb, bb) => cc | (aa, cc, cc) => bb
| (bb, cc, cc) => aa | (bb, aa, aa) => cc
| (cc, aa, aa) => bb | (cc, bb, bb) => aa
end.
Lemma op_id_inv {A} {G : group A} : id = inv id.
Proof. rewrite op_id_l. apply op_inv_r. Qed.
Theorem exercise_ii_1_6_b {G : group tri} : forall x y,
x * y = op_tri id x y.
Proof.
intros.
destruct id eqn:eq, (x * y) eqn:H, x, y; auto;
try rewrite <- eq in H;
try (rewrite <- op_id_l in H; congruence);
try (rewrite <- op_id_r in H; congruence);
try (apply square_id in H; congruence);
try (
rewrite <- H in H;
try (rewrite <- op_assoc in H; apply op_cancel_l in H);
try (rewrite op_assoc in H; apply op_cancel_r in H);
apply square_id in H;
congruence).
- destruct (bb * cc) eqn:Hop.
+ rewrite eq in H.
rewrite <- Hop in H.
apply op_cancel_l in H.
congruence.
+ rewrite <- Hop in Hop.
rewrite <- op_assoc in Hop.
apply op_cancel_l in Hop.
apply square_id in Hop.
congruence.
+ rewrite <- Hop in Hop.
rewrite op_assoc in Hop.
rewrite H in Hop.
apply op_cancel_r in Hop.
congruence.
- destruct (cc * bb) eqn:Hop.
+ rewrite eq in H.
rewrite <- Hop in H.
apply op_cancel_l in H.
congruence.
+ rewrite <- Hop in Hop.
rewrite op_assoc in Hop.
apply op_cancel_r in Hop.
apply square_id in Hop.
congruence.
+ rewrite <- Hop in Hop.
rewrite <- op_assoc in Hop.
apply op_cancel_l in Hop.
apply square_id in Hop.
congruence.
- destruct (aa * cc) eqn:Hop.
+ rewrite <- Hop in Hop.
rewrite <- op_assoc in Hop.
apply op_cancel_l in Hop.
apply square_id in Hop.
congruence.
+ rewrite eq in H.
rewrite <- Hop in H.
apply op_cancel_l in H.
congruence.
+ rewrite <- Hop in Hop.
rewrite op_assoc in Hop.
apply op_cancel_r in Hop.
apply square_id in Hop.
congruence.
- destruct (cc * aa) eqn:Hop.
+ rewrite <- Hop in Hop.
rewrite op_assoc in Hop.
apply op_cancel_r in Hop.
apply square_id in Hop.
congruence.
+ rewrite eq in H.
rewrite <- Hop in H.
apply op_cancel_l in H.
congruence.
+ rewrite <- Hop in Hop.
rewrite <- op_assoc in Hop.
apply op_cancel_l in Hop.
apply square_id in Hop.
congruence.
- destruct (aa * bb) eqn:Hop.
+ rewrite <- Hop in Hop.
rewrite <- op_assoc in Hop.
apply op_cancel_l in Hop.
apply square_id in Hop.
congruence.
+ rewrite <- Hop in Hop.
rewrite op_assoc in Hop.
apply op_cancel_r in Hop.
apply square_id in Hop.
congruence.
+ rewrite eq in H.
rewrite <- Hop in H.
apply op_cancel_l in H.
congruence.
- destruct (bb * aa) eqn:Hop.
+ rewrite <- Hop in Hop.
rewrite op_assoc in Hop.
apply op_cancel_r in Hop.
apply square_id in Hop.
congruence.
+ rewrite <- Hop in Hop.
rewrite <- op_assoc in Hop.
apply op_cancel_l in Hop.
apply square_id in Hop.
congruence.
+ rewrite eq in H.
rewrite <- Hop in H.
apply op_cancel_l in H.
congruence.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment