Skip to content

Instantly share code, notes, and snippets.

@andrejbauer andrejbauer/algebra.v
Last active Nov 21, 2018

Embed
What would you like to do?
Uinversal algebra in Coq
(* An initial attempt at universal algebra in Coq.
Author: Andrej Bauer <Andrej.Bauer@andrej.com>
If someone knows of a less painful way of doing this, please let me know.
We would like to define the notion of an algebra with given operations satisfying given
equations. For example, a group has of three operations (unit, multiplication, inverse)
and five equations (associativity, unit left, unit right, inverse left, inverse right).
*)
(* We will need function extensionalty. *)
Axiom funext : forall (X : Type) (Y : X -> Type) (f g : forall x, Y x),
(forall x, f x = g x) -> f = g.
(* We start by defining operation signatures. These describe the operations
of an algebra.
The main trick is that the arity of an operation is *not* a number
but rather a type. For instance, the arity of a binary operation
is a type with two elements. (And nothing prevents us from having
an infinite type as arity.)
*)
Record OpSignature :=
{
operation : Type ; (* (Names of) operations. *)
arity : operation -> Type (* Each operation has an arity. *)
}.
Arguments arity {_} _.
(* We shall consider algebras with given operations, but without equations.
We call these "operation algebras". *)
Record OpAlgebra (S : OpSignature) :=
{
carrier :> Type ;
op : forall o : operation S, (arity o -> carrier) -> carrier
(* no equations *)
}.
Arguments op {_} _ _ _.
(* We define the type of homomorphism between operation algebras A and B. *)
Record Hom {S : OpSignature} (A : OpAlgebra S) (B : OpAlgebra S) :=
{
map :> A -> B ; (* The underlying map *)
(* The underlying map commutes with operations: *)
op_commute : forall (o : operation S) (args : arity o -> A),
map (op A o args) = op B o (fun x => map (args x))
}.
(* The free algebra for a given signature [S] generated by [X]. *)
Inductive Tree (S : OpSignature) (X : Type) : Type :=
| generator : X -> Tree S X
| node : forall (o : operation S), (arity o -> Tree S X) -> Tree S X.
Arguments generator {_} {_} _.
Arguments node {_} {_} _.
Definition Free (S : OpSignature) (X : Type) : OpAlgebra S :=
{| carrier := Tree S X
; op := @node S X
|}.
Section Free_is_free.
(* We show that the free algebra has the desired universal property. *)
Hypothesis S : OpSignature.
Hypothesis X : Type.
Hypothesis A : OpAlgebra S.
Hypothesis h : X -> A.
Fixpoint induced_map (t : Tree S X) : A :=
match t with
| generator x => h x
| node o arg => op A o (fun i => induced_map (arg i))
end.
Definition induced_hom : Hom (Free S X) A.
Proof.
exists induced_map.
intros o arg.
reflexivity.
Defined.
(* Suggested by Hugo to make the rewrites below work. *)
Set Keyed Unification.
(* The induced homomorphism is unique. *)
Theorem from_free_unique (f g : Hom (Free S X) A) :
(forall x, f (generator x) = g (generator x)) -> forall t, f t = g t.
Proof.
intros eq_gen t.
induction t.
- apply eq_gen.
- rewrite op_commute.
rewrite op_commute.
f_equal.
now apply funext.
Qed.
End Free_is_free.
(* Now given some operations, described by an operation signature S,
we can define an equation signature which specifies some equations.
*)
Record EqSignature (S : OpSignature) :=
{
eq :> Type ; (* (names of) equations *)
(* each equation has an arity, which is the number of parameters appearing in it.
Again, we use a type instead of a number. *)
eq_arity : eq -> Type ;
(* Next we specify the equations. Note that they are polymorphic in the underlying algebra. *)
lhs : forall (A : OpAlgebra S) (e : eq), (eq_arity e -> A) -> A ; (* left-hand sides *)
rhs : forall (A : OpAlgebra S) (e : eq), (eq_arity e -> A) -> A ; (* right-hand sides *)
(* Moreover, we require that the lhs and rhs are natural transformations, i.e,
that they commute with homomorphism. This way it's impossible to write down
strange equations that involve something other than the operations. *)
lhs_natural :
forall (A B : OpAlgebra S) (f : Hom A B) (e : eq) (args : eq_arity e -> A),
f (lhs A e args) = lhs B e (fun i => f (args i)) ;
rhs_natural :
forall (A B : OpAlgebra S) (f : Hom A B) (e : eq) (args : eq_arity e -> A),
f (rhs A e args) = rhs B e (fun i => f (args i)) ;
}.
Arguments eq_arity {_} {_} _.
Arguments lhs {_} {_} {_} _ _.
Arguments rhs {_} {_} {_} _ _.
(* We can now define what it means to have an algebra for a signature S satisfying
equations E. *)
Record Algebra (S : OpSignature) (E : EqSignature S) :=
{
alg :> OpAlgebra S ;
equations : forall (e : E) (args : eq_arity e -> alg), lhs e args = rhs e args
}.
(* We define some handy arities. *)
Inductive nullary : Set := .
Inductive unary : Set := Only.
Inductive binary : Set := Fst | Snd.
Inductive ternary : Set := One | Two | Three.
(* Let us write down the definition of a group. As you can see this is extremely painful
and long. *)
(* Group operations *)
Inductive Group_operation :=
| one : Group_operation (* unit *)
| mul : Group_operation (* multiplication *)
| inv : Group_operation. (* inverse *)
Definition Group_arity (o : Group_operation) :=
match o with
| one => nullary
| mul => binary
| inv => unary
end.
(* The structure of a group, but without equations. *)
Definition GroupOp :=
{|
operation := Group_operation ;
arity := Group_arity
|}.
(* Auxiliary functions that will make it easier to write down equations. *)
Definition one' {G : OpAlgebra GroupOp} :=
op G one (fun i => match i with end).
Definition mul' {G : OpAlgebra GroupOp} (x y : G) :=
op G mul (fun i => match i with
| Fst => x
| Snd => y
end).
Definition inv' {G : OpAlgebra GroupOp} (x : G) :=
op G inv (fun _ => x).
(* There are five group equations. *)
Inductive Group_equation :=
| assoc : Group_equation
| unit_left : Group_equation
| unit_right : Group_equation
| inv_left : Group_equation
| inv_right : Group_equation.
(* The arities of group equations. *)
Definition Group_eq_arity (e : Group_equation) :=
match e with
| assoc => ternary
| unit_left => unary
| unit_right => unary
| inv_left => unary
| inv_right => unary
end.
(* The left-hand sides of group equations *)
Definition Group_lhs (A : OpAlgebra GroupOp) (e : Group_equation) :
(Group_eq_arity e -> A) -> A :=
match e with
| assoc => (fun args => mul' (args One) (mul' (args Two) (args Three)))
| unit_left => (fun args => mul' one' (args Only))
| unit_right => (fun args => mul' (args Only) one')
| inv_left => (fun args => mul' (inv' (args Only)) (args Only))
| inv_right => (fun args => mul' (args Only) (inv' (args Only)))
end.
(* The right-hand sides of group equations *)
Definition Group_rhs (A : OpAlgebra GroupOp) (e : Group_equation) :
(Group_eq_arity e -> A) -> A :=
match e with
| assoc => (fun args => mul' (mul' (args One) (args Two)) (args Three))
| unit_left => (fun args => args Only)
| unit_right => (fun args => args Only)
| inv_left => (fun args => one')
| inv_right => (fun args => one')
end.
(* The signature for group equations, we need to show they're natural. *)
Definition GroupEq : EqSignature GroupOp.
Proof.
refine
{|
eq := Group_equation ;
eq_arity := Group_eq_arity ;
lhs := Group_lhs ;
rhs := Group_rhs
|}.
(* A bit of Coq magic does the job. *)
- intros A B f [] args ;
(unfold Group_lhs, Group_rhs ;
repeat (unfold one', mul', inv';
rewrite op_commute; f_equal; apply funext;
intros []; try reflexivity)).
- intros A B f [] args ;
(unfold Group_lhs, Group_rhs ;
repeat (unfold one', mul', inv';
rewrite op_commute; f_equal; apply funext;
intros []; try reflexivity)).
reflexivity.
reflexivity.
Defined.
(* And finally, we can define what a group is. *)
Definition Group := Algebra GroupOp GroupEq.
Section BoolGroup.
(* Let us show that the booleans form a group with the xor as the group operation. *)
Definition xor (x y : bool) :=
match x with
| false => y
| true => (match y with false => true | true => false end)
end.
(* We first define the structure without equations. *)
Definition BoolOp : OpAlgebra GroupOp :=
{| carrier := bool ;
op := (fun (o : operation GroupOp) => match o with
| one => (fun args => false)
| mul => (fun args => xor (args Fst) (args Snd))
| inv => (fun args => args Only)
end
)
|}.
(** Then we define the group Bool by showing that BoolOp satisfies the group equations. *)
Definition Bool : Group.
Proof.
exists BoolOp.
intros [] args ; simpl; try (destruct (args Only) ; reflexivity).
destruct (args One); destruct (args Two); destruct (args Three); reflexivity.
Defined.
End BoolGroup.
Section Product.
(* Let us do a bit of general theory by showing that the algebras for a given signature
are closed under products. *)
(* The product of an I-indexed family of operation algebras. *)
Definition ProductOp {S : OpSignature} {I : Type} (A : I -> OpAlgebra S) :=
{| carrier := forall i, A i ;
op := (fun (o : operation S) args i => op (A i) o (fun j => args j i))
|}.
(* Projections are homomorphisms. *)
Definition Project {S : OpSignature} {I : Type} (A : I -> OpAlgebra S) (i : I) :
Hom (ProductOp A) (A i).
Proof.
exists (fun (x : ProductOp A) => x i).
reflexivity.
Defined.
(* The product of an I-indexed family og algebras. *)
Definition Product {S : OpSignature} {E : EqSignature S} (I : Type) :
(I -> Algebra S E) -> Algebra S E.
Proof.
intro A.
exists (ProductOp A).
intros e args.
apply funext.
intro i.
pose (L := lhs_natural _ E _ _ (Project A i) e args); simpl in L.
rewrite L.
pose (R := rhs_natural _ E _ _ (Project A i) e args); simpl in R.
rewrite R.
apply equations.
Defined.
End Product.
@williamdemeo

This comment has been minimized.

Copy link

commented Jul 20, 2018

Awesome! Thanks for showing us how to do this in Coq, Andrej!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.