Agda-like Equational Reasoning in Coq using Tactic Notations

I am used to the idea that there are two major styles of mechanised proofs: Agda-style proofs that effectively spell out the proof terms and Coq-style proofs that are constructed using tactics.

I like Coq’s approach since it allows me to poke my goals with tactics interactively and to think less hard about the exact way some lemma should be applied. However, proof scripts very quickly become impossible to understand without stepping through them interactively. In Agda, proofs are often written in equational reasoning style using mixfix proof combinators, like that:

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm m zero =
  begin
    m + zero
  ≡⟨ +-identityʳ m ⟩
    m
  ≡⟨⟩
    zero + m
  ∎
+-comm m (suc n) =
  begin
    m + suc n
  ≡⟨ +-suc m n ⟩
    suc (m + n)
  ≡⟨ cong suc (+-comm m n) ⟩
    suc (n + m)
  ≡⟨⟩
    suc n + m
  ∎

This lemma proves commutativity of addition of natural numbers by structural induction, justifying the equational reasoning steps with the ≡⟨ necessary lemmas ⟩.

I find Agda’s style much friendlier to the naked eye. Why can’t I have it in Coq? Well, actually, I can! Here is a Coq proof of the same theorem that closely mimics the Agda one:

Theorem plus_comm :
  forall (m n : nat), m + n = n + m.
Proof.
  intros m n.
  induction n.
  - `Begin
     (m + 0).
    ≡⟨ now rewrite <- plus_n_O ⟩
     (m).
    ≡⟨ reflexivity ⟩
     (0 + m)
    `End.
  - `Begin
     (m + S n).
    ≡⟨ now rewrite plus_n_Sm ⟩
     (S (m + n)).
    ≡⟨ now rewrite IHn ⟩
     (S (n + m)).
    ≡⟨ reflexivity ⟩
     (S n + m)
    `End.
Qed.

Neat, isn’t it? We invoke the induction tactic generating two subgoals, with which we deal in the same style that we used in Agda! To achieve this, we need two ingredients: one somewhat arcane (but standard) tactic and Tactic Notations to make it look prettier.

Tactic Notations + stepl = Equational Reasoning!

Coq proofs consist of tactics which when invoked generate the actual proof terms that are type-checked by Coq. This is great, but since the proof terms are hidden, it is not always straightforward to understand a proof script without stepping through it interactively. What I wanted to have instead is a neat way to spell out intermediate proof terms literally and use tactics to justify the rewriting steps connecting these intermediate terms. To do that, we can use a rather obscure tactic stepl term by tactic which does exactly what we want: transforms the left hand-side of the current equality goal into the term we supply with a tactic we give. To make it look more like Agda, we throw in some pretty Unicode characters and put the justifying tactic first by using a Tactic Notation:

Tactic Notation
  "≡⟨ " tactic(proof) "⟩" constr(rhs) :=
  (stepl rhs by proof).

Note how the arguments are passed to the notation: the proof is specified to be an Ltac term (tactic), and rhs — a kernel term (constr).

This approach is of course not the perfect emulation of Agda-style equational reasoning since it does not support holes and inherits Coq’s stepwise proof editing style, i.e. it is not as easy to switch between forward and backward reasoning as in Agda. Though it is still possible to sketch proofs and skip steps, since one could use the admit tactic as justification for any rewriting step. More importantly, we gain something which Agda does not have: between rewriting step we can use the usual Coq interactive proof style of transforming the goal with tactics to experiment and find the next rewriting step; after that we could petrify the interactive proof exploration into a sequence of clear equational reasoning steps.

A quick Google search gives a number of hits on how to use equational reasoning in Coq, but most of the projects seem to be developing some heavy machinery and are not straightforward to use. Among the first hits however is this gist, which is very lightweight and has given me the initial inspiration. It is much more limited though since the trick it proposes does not allow skipping proof steps with admit.

I have used this style to prove that Free Rigid Selective is a lawful instance of Applicative, you may take a look at the proof scripts here.

Since this post has been inspired by a Github Gist, I’ve put the accompanying Coq code in one too; here is how to do lightweight equational reasoning in Coq.