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
|
Require Import Coq.Classes.Morphisms.
Require Import Crypto.Util.Tactics.RewriteHyp.
Require Import Crypto.Algebra.Hierarchy.
Section Monoid.
Context {T eq op id} {monoid:@monoid T eq op id}.
Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
Local Infix "*" := op.
Local Infix "=" := eq : eq_scope.
Local Open Scope eq_scope.
Lemma cancel_right z iz (Hinv:op z iz = id) :
forall x y, x * z = y * z <-> x = y.
Proof using Type*.
split; intros.
{ assert (op (op x z) iz = op (op y z) iz) as Hcut by (rewrite_hyp ->!*; reflexivity).
rewrite <-associative in Hcut.
rewrite <-!associative, !Hinv, !right_identity in Hcut; exact Hcut. }
{ rewrite_hyp ->!*. reflexivity. }
Qed.
Lemma cancel_left z iz (Hinv:op iz z = id) :
forall x y, z * x = z * y <-> x = y.
Proof using Type*.
split; intros.
{ assert (op iz (op z x) = op iz (op z y)) as Hcut by (rewrite_hyp ->!*; reflexivity).
rewrite !associative, !Hinv, !left_identity in Hcut; exact Hcut. }
{ rewrite_hyp ->!*; reflexivity. }
Qed.
Lemma inv_inv x ix iix : ix*x = id -> iix*ix = id -> iix = x.
Proof using Type*.
intros Hi Hii.
assert (H:op iix id = op iix (op ix x)) by (rewrite Hi; reflexivity).
rewrite associative, Hii, left_identity, right_identity in H; exact H.
Qed.
Lemma inv_op x y ix iy : ix*x = id -> iy*y = id -> (iy*ix)*(x*y) =id.
Proof using Type*.
intros Hx Hy.
cut (iy * (ix*x) * y = id); try intro H.
{ rewrite <-!associative; rewrite <-!associative in H; exact H. }
rewrite Hx, right_identity, Hy. reflexivity.
Qed.
End Monoid.
Section Homomorphism.
Context {T EQ OP ID} {monoidT: @monoid T EQ OP ID }.
Context {T' eq op id} {monoidT': @monoid T' eq op id }.
Context {phi:T->T'}.
Local Infix "=" := eq. Local Infix "=" := eq : type_scope.
Class is_homomorphism :=
{
homomorphism : forall a b, phi (OP a b) = op (phi a) (phi b);
is_homomorphism_phi_proper : Proper (respectful EQ eq) phi
}.
Global Existing Instance is_homomorphism_phi_proper.
End Homomorphism.
Section HomomorphismComposition.
Context {G EQ OP ID} {monoidG:@monoid G EQ OP ID}.
Context {H eq op id} {monoidH:@monoid H eq op id}.
Context {K eqK opK idK} {monoidK:@monoid K eqK opK idK}.
Context {phi:G->H} {phi':H->K}
{Hphi:@is_homomorphism G EQ OP H eq op phi}
{Hphi':@is_homomorphism H eq op K eqK opK phi'}.
Lemma is_homomorphism_compose
{phi'':G->K}
(Hphi'' : forall x, eqK (phi' (phi x)) (phi'' x))
: @is_homomorphism G EQ OP K eqK opK phi''.
Proof using Hphi Hphi' monoidK.
split; repeat intro; rewrite <- !Hphi''.
{ rewrite !homomorphism; reflexivity. }
{ apply Hphi', Hphi; assumption. }
Qed.
Global Instance is_homomorphism_compose_refl
: @is_homomorphism G EQ OP K eqK opK (fun x => phi' (phi x))
:= is_homomorphism_compose (fun x => reflexivity _).
End HomomorphismComposition.
|
