A Quick Tutorial on Setoids in Coq

A setoid is a type T and an equivalence relation (=) : T -> T -> Prop=. Coq has some built-in automation facilities for working with setoids that can make your life a lot easier.

Building a setoid

Let's suppose we wanted to implement a quick-and-dirty version of finite sets on some type A. One option is to use list A, but lists have two properties that get in the way: ordering and duplication. Building a Setoid allows us to abstract away these features, and consider two lists equivalent if they have the same elements.

Context {A : Type}.

Definition equiv_list (l1 l2 : list A) : Prop :=
  ∀ a : A, In a l1 <-> In a l2.

To register our new equivalence with Coq and reap the benefits of automation, we make list A an instance of the Setoid typeclass:

Instance ListSetoid : Setoid (list A) :=
  { equiv := equiv_list }.
Proof.
  split.

At this point, we're dropped into proof mode and our goal is to prove that equiv_list is an equivalence relation. To see the full proof, see the Coq source for this post (we use some setoid-related automation to prove this goal).

Immediately, we gain access to a few tactics that work for normal equality, like reflexivity, symmetry (plus symmetry in [...]), and transitivity.

setoid_rewrite

The #1 benefit to using setoids is access to the setoid_rewrite tactic. Rewriting is one of the most powerful features of the tactic language, and using setoids allows us to expand its reach.

Suppose we have l1 l2 : list A. If we have l1 = l2 (where = is Coq's built-in equality), we can replace l1 with l2 in all contexts:

Lemma hd_eq (l1 l2 : list A) : l1 = l2 -> hd l1 = hd l2.
Proof.
  intros l1eql2.
  now rewrite l1eql2.
Qed.

This isn't true if we just know l1 = l2= (where == is notation for list_equiv). However, there are certain contexts in which they are interchangeable. Suppose further that A has decidable equality, and consider the following remove function:

Context {deceq : ∀ x y : A, {x = y} + {x ≠ y}}.

Fixpoint remove (x : A) (lst : list A) : list A :=
  match lst with
  | nil => nil
  | cons y ys =>
    match deceq x y with
    | left  _ => remove x ys
    | right _ => y :: remove x ys
    end
  end.

Since this removes all occurrences of x in lst, we should be able to prove

∀ x l1 l2, l1 == l2 -> remove x l1 = remove x l2

We state this lemma a bit oddly:

Instance removeProper : Proper (eq ==> equiv ==> equiv) remove.

This concisely states "given two equal inputs x y : A and two equivalent lists l1 l2 : list A, remove x l1 is equivalent to remove y l2". In other words, remove respects equality on A (trivially -- every Coq function respects equality) and the equivalence relation == (AKA equiv) on list A.

Once we have an Instance of Proper, we can use setoid_rewrite to replace replace remove x l1 with remove x l2, even when they appear nested in the goal statement:

Instance revProper : Proper (equiv ==> equiv) (@rev A).
Proof.
  [...]
Qed.

Lemma remove_rev_remove {a b : A} {l1 l2 : list A} :
  l1 == l2 -> rev (remove a l1) == rev (remove a l2).
Proof.
  intros H.
  now setoid_rewrite H.
Qed.

We can even compose Proper instances automatically:

Require Import Coq.Program.Basics.
Local Open Scope program_scope.

Instance rev_remove_Proper : ∀ a, Proper (equiv ==> equiv) (@rev A ∘ remove a).
Proof.
  apply _.
Qed.

The benefits of setoid rewriting continue to increase with the complexity of the goal.