Uinversal algebra in Coq

algebra.v

(* An initial attempt at universal algebra in Coq.
   Author: Andrej Bauer <[email protected]>

   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.

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

This is great stuff, thank you Andrej, just what I was looking for today.

I'm having trouble defining the coproduct of two algebras with this definition. Using McBride's many-sorted definition, it's fairly easy, but using the above I run into a problem with the arity argument having the wrong positivity.

Here's is Conor's formulation:

Record Signature (I O : Type) : Type := {
    Operations : O → Type;
    Arities    : forall o : O, Operations o → Type;
    Sorts      : forall (o : O) (op : Operations o), Arities o op → I
}.

Arguments Operations {I O} _ i.
Arguments Arities {I O} _ {_} op.
Arguments Sorts {I O} _ {_} {_} ar.

Infix "▷" := Signature (at level 60) : type_scope.

Definition sor {I O} (x y : I ▷ O) : I ▷ O :=
  match x with {| Operations := P₁
                ; Arities    := A₁
                ; Sorts      := s₁ |} =>
  match y with {| Operations := P₂
                ; Arities    := A₂
                ; Sorts      := s₂ |} =>
  {| Operations := λ x, (P₁ x + P₂ x)%type

   ; Arities := λ o op,
       match op with
       | inl op' => A₁ o op'
       | inr op' => A₂ o op'
       end

   ; Sorts := λ o op,
       match op with
       | inl op' => s₁ o op'
       | inr op' => s₂ o op'
       end
   |}
  end
  end.

Are you trying to take a coproduct of signatures or a coproduct of two algebras for a given signature? If the former, I'd first need to know what the category is (what are morphisms of signatures). If the later, I don't see a problem, other than you'd have to convince Coq to make a quotient (because a coproduct of two algebras is constructed by quotienting a free algebra).