Using Bundled and Unbundled Typeclasses Simultaneously in Coq

bundled_unbundled.v

Require Import Utf8.
Require Import Coq.Program.Tactics.

(* When using typeclasses in Coq, people often debate over whether you should
use them bundled or unbundled.  Each has their own benefits in particular
situations.  However, you can actually use them both at the same time to get the
best of both worlds! *)

(* We start with defining several unbundled typeclasses for the sake of defining
groups. *)
#[universes(template)]
Class Plus U := {
    plus : U → U → U;
}.
#[universes(template)]
Class Zero U := {
    zero : U;
}.
#[universes(template)]
Class Neg U := {
    neg : U → U;
}.
Infix "+" := plus.
Notation "0" := zero.
Notation "- a" := (neg a).
Notation "a - b" := (a + -b).

Class PlusAssoc U `{Plus U} := {
    plus_assoc : ∀ a b c, a + (b + c) = (a + b) + c;
}.
Class PlusLid U `{Plus U} `{Zero U} := {
    plus_lid : ∀ a, 0 + a = a;
}.
Class PlusRid U `{Plus U} `{Zero U} := {
    plus_rid : ∀ a, a + 0 = a;
}.
Class PlusLinv U `{Plus U} `{Zero U} `{Neg U} := {
    plus_linv : ∀ a, -a + a = 0;
}.
Class PlusRinv U `{Plus U} `{Zero U} `{Neg U} := {
    plus_rinv : ∀ a, a - a = 0;
}.

(* Using these unbundled typeclasses, we can prove theorems like you normally
would for unbundled typeclasses. *)

Section Unbundled.

Context {U} `{
    p : Plus U,
    z : Zero U,
    n : Neg U,
    @PlusAssoc U p,
    @PlusLid U p z,
    @PlusRid U p z,
    @PlusLinv U p z n,
    @PlusRinv U p z n
}.

Theorem group_lcancel : ∀ a b c : U, a + b = a + c → b = c.
Proof.
    intros a b c eq.
    apply (f_equal (plus (-a))) in eq.
    do 2 rewrite plus_assoc in eq.
    rewrite plus_linv in eq.
    do 2 rewrite plus_lid in eq.
    exact eq.
Qed.

End Unbundled.
(* We have managed to keep the benefits of keeping things unbundled, where you
can prove theorems with a bunch of listed premises, but Coq will automatically
figure out which ones are actually needed.  Notice that group_lcancel doesn't
depend on PlusRid or PlusRinv, which wouldn't happen with a bundled aproach. *)
Check group_lcancel.

(* We can now bundle the unbundled typeclasses together into a single record. 
If you wish, you could probably make this a typeclass as well, although I
personally don't do so. *)
Record Group := make_group {
    group_U :> Type;
    group_plus : Plus group_U;
    group_zero : Zero group_U;
    group_neg : Neg group_U;
    group_plus_assoc : @PlusAssoc group_U group_plus;
    group_plus_lid : @PlusLid group_U group_plus group_zero;
    group_plus_rid : @PlusRid group_U group_plus group_zero;
    group_plus_linv : @PlusLinv group_U group_plus group_zero group_neg;
    group_plus_rinv : @PlusRinv group_U group_plus group_zero group_neg;
}.
(* By enabling these instances, we can use the unbundled notations and theorems
from above for bundled groups without any extra notational overhead. *)
Global Existing Instances group_plus group_zero group_neg group_plus_assoc
    group_plus_lid group_plus_rid group_plus_linv group_plus_rinv.

(* Now we can work with bundled groups while still using the unbundled theorems
proved above! *)

Section Bundled.

Context (G : Group).

Theorem group_lcancel2 : ∀ a b c d : G, a + b + c = a + b + d → c = d.
Proof.
    intros a b c d eq.
    do 2 rewrite <- plus_assoc in eq.
    do 2 apply group_lcancel in eq.
    exact eq.
Qed.

End Bundled.

(* And of course, using this bundled form of groups we can do what the bundled
approach does best: Defining operations on entire algebraic structures. *)

Program Definition group_product (G H : Group) : Group := {|
    group_U := (G * H);
    group_plus := {|plus a b := (fst a + fst b, snd a + snd b)|};
    group_zero := {|zero := (0, 0)|};
    group_neg := {|neg a := (-fst a, -snd a)|}
|}.
Next Obligation.
    split.
    intros a b c.
    cbn.
    do 2 rewrite plus_assoc.
    reflexivity.
Qed.
Next Obligation.
    split.
    intros a.
    cbn.
    do 2 rewrite plus_lid.
    destruct a; reflexivity.
Qed.
Next Obligation.
    split.
    intros a.
    cbn.
    do 2 rewrite plus_rid.
    destruct a; reflexivity.
Qed.
Next Obligation.
    split.
    intros a.
    cbn.
    do 2 rewrite plus_linv.
    reflexivity.
Qed.
Next Obligation.
    split.
    intros a.
    cbn.
    do 2 rewrite plus_rinv.
    reflexivity.
Qed.

(* While doing this is technically doable with an unbundled approach, the
computational complexity is exponential, and it can quickly slow down compile
times, whereas here you can see that group_product is just a function on Groups.
*)
Check group_product.