日本ソフトウェア科学会第 35 回大会 (2018 年度) 講演論文集

Experimenting with Monadic Equational
Reasoning in Coq
Reynald Aﬀeldt

David Nowak

In order to prove properties of low-level programs in a proof-assistant, it is common to proceed by refining
an abstract model into a deep encoding of the program. Here, we lay the groundwork for exploring thealternative approach consisting in reasoning directly on a shallow encoding of the program to be verified.
For that purpose, we mechanize in the Coq proof-assistant an approach by Gibbons and Hinze for monadic
equational reasoning. The main idea of our mechanization is to formalize monads and their algebraic laws
like it is done for mathematical structures so as to take advantage of Coq’s rewriting capabilities. This
leads to a mechanization with little overhead that adds the possibility for rigorous model instantiations. In
this paper, we explain the key ideas of our mechanization, discuss in particular the probability monad, andgive a denotational semantics to a small imperative programming language with a combination of the state
and trace monads. The latter application leads us to extend monadic equational reasoning with equations
linking a state monad with a trace monad.

tive tactics and it indeed experimentally met some

1 Introduction

success (e.g., [16] [18]).

1. 1 Motivation

approach relies on a combination of monads andMost of the time, thisOur ultimate goal is to use the Coq proof-

Hoare logic (e.g., [17]). There is however anotherassistant to reason about low-level languages (e.g.,

approach based on monads to reason about pro-produce formal proofs of functional correctness ofgrams: monadic equational rewriting, an approach

programs). For that purpose, the approach that isbest explained by Gibbons and Hinze [12]. We be-

usually taken is to proceed via a deep embedding

lieve that it is worth exploring because the rewrit-of the target language. This requires substantial

ing tactics of Coq have been polished over the years

instrumentations of syntax and semantics, result-and are now powerful enough to gear huge formal

ing in technical lemmas that are diﬃcult to use,developments; for example, proofs in the Mathe-

which in turn call for meta-programming (using

matical Components library (MathComp) essen-

Ltac in Coq). The alternative approach consist-tially rely on rewriting [15].

ing of using a shallow embedding bears the promise

As a preliminary step towards the verificationof a more direct access to the proof-assistant na-

of low-level programs, in this paper, we mechanize monadic equational rewriting. Our goal is to

Coq における Monadic 等式推論の実験
This is an unrefereed paper. Copyrights belong to
the Author(s).
アフェルト・レナルド, 産業技術総合研究所, National Institute of Advanced Industrial Science and Technology.
ノヴァック・ダヴィッド, フランス国立科学研究センター・
リール大学, CNRS/University of Lille.

make sure that we can produce formal proofs basedon monadic equational reasoning that are at least
as pleasant as pencil-and-paper proofs. For that
purpose, we mechanize in Coq the paper by Gibbons and Hinze [12], as well as related work [11] [23].

This provides us with a solid mechanization of al-• We use Coq canonical structures [20].

We

gebraic eﬀects such as failures, exceptions, non-use them in particular to formalize the hier-determinism, states, probabilities (and more), thatarchy of algebraic eﬀects (see Sect. 3) using

are key to formalize the semantics of low-level lan-

packed classes [10], a methodology used in theguages.

MathComp library to formalize the hierar-

It should be noted that the formalization ofchy of mathematical structures. We also use

monadic equational reasoning is already interest-

canonical structures to formalize probabilities

ing in itself. Its correctness can be tricky (for ex-(see Sect. 5).

ample, the early [12] needed to be patched in [1]) so• We use the SSReflect tactics and li-that mechanized tools are certainly welcome. Therebraries [14].

SSReflect tactics emphasize

is also an interest in formal frameworks to reason

proof by rewriting, making it easier to mimic

about Haskell-like programs in Coq (e.g., [7]) so

monadic equational reasoning.

that a proper mechanization of monadic equational

flect library for lists is closer to the Haskell

reasoning could actually be readily useful.

library than Coq’s standard library: it al-

The SSRe-ready provides Haskell-like notations (e.g., no1. 2 Contributions

tation for comprehension) and more functions

We formalize the theory of algebraic eﬀects(e.g., allpairs, a.k.a. cp in Haskell). Also, wefrom [12] (see Sections 3 and 4) and even extend

benefit from other SSReflect/MathComp-it by providing formal models (see Sect. 5).

compatible libraries to formalize the model of

We mechanize numerous examples: all the examples from [12], most examples from [11] (which
overlaps and complements [12]), and also somethe probability monad (the theory of finitely
supported distributions comes from [4]).
• We benefit from the real numbers of the

The result is

Coq standard library: they provide tactics

very satisfactory. The formal proofs closely matchto deal automatically with reals despite their

their pencil-and-paper counterparts (discrepancies

axiomatic encoding.

are minor, see Sect. 7. 2).

tics field, fourier, and nstaz are important

examples from related work [23].

Proofs can actually

be made even shorter thanks to the terseness of

In particular the tac-in practice to compute probabilities.

Coq’s tactic language and its automation capabilities (Sect. 2 provides a simple example, see thecode [5] for more).

2 A Simple Example of Monadic Equational Reasoning in Coq

Last, we extend our mechanization with otherWe start with a simple example of monadic equa-monads and present an application that provides ational reasoning taken from [12]. It establishes theshallow encoding of a semantics using monads (seeequivalence between a functional implementation

Sect. 6).

of the product of integers (product below) with amonadic version (fastproduct). In [12], the proof is

1. 3 Formalization Approach

carried out by a series of rewritings that we have

Our successful mechanization owes much to thereproduced (faithfully) in Fig. 1 (on the left). Let

level of details provided by the authors using

us comment on the equivalent Coq mechanizationmonadic equational reasoning in their papers. It

that is displayed on the right of Fig. 1.

is also the result of appropriate technical choices:

We first define the product of natural numbers

Original proof (Sect. 5.1 of [12])Coq proof (lhs of the goal, tactics inbetween)

fastprod xs

fastproduct s=J definition of fastprod K=J rewrite /fastproduct K

catch (work xs) (return 0)

Catch (work s) (Ret 0)=J specification of work K=J rewrite /work K

catch (if 0 ∈ xs then failCatch (if 0 \in s then Failelse return (product xs)) (return 0)

else Ret (product s)) (Ret 0)=J lift out the conditional K=J rewrite lift_if if_ext K

if 0 ∈ xs then catch fail (return 0)((if 0 \in s then Catch Fail (Ret 0)

else catch (return (product xs)) (return 0)

else Catch (Ret (product s)) (Ret 0))=J laws of catch, fail, and return K=J rewrite catchfailm catchret K

if 0 ∈ xs then return 0 else return (product xs)(if 0 \in s then Ret 0 else Ret (product s))=J arithmetic: 0 ∈ xs ⇒ product xs = 0 K=J case: ifPn => // /product0 K

if 0 ∈ xs then return (product xs)(Lemma product0 s : O \in s -> product s = O.)else return (product xs)

Ret 0=J redundant conditional K=J move <- K

return (product xs)

Ret (product s)

Figure 1

Comparison between a proof from [12] and its Coq formalization

as follows:that it never throws an unhandled exception, canDefinition product (s : seq nat) :=foldr muln 1 s.

be compared to its pencil-and-paper counterpart in

A “faster” product can be implemented using the
failure monad (with operator Fail) and the exception monad (with operator Catch):
Definition work
{M : failMonad} (s : seq nat) : M nat :=if O \in s then Fail else Ret (product s).
Definition fastproduct{M : exceptMonad} s : M nat :=Catch (work s) (Ret O : M _).

Fig. 1. One can observe that both proofs are essentially the same, though in practice the Coq proof
script will be streamlined in two lines of code (ofless than 80 characters):
Lemma fastproductE s : fastproduct s = Ret (product s).
Proof.
rewrite /fastproduct /work lift_if if_ext catchfailm.
by rewrite catchret; case: ifPn => // /product0 <-.
Qed.

The formalization of the failure monad is explained

The fact that we achieve the same conciseness asin the next section (Sect. 3). The exception monadinherits†1 from the failure monad to which it adds

the pencil-and-paper proof on this example is notin particular the following properties:of all the examples in [12], even the longer andVariables (M : exceptMonad).
Lemma catchfailm : forall A,
left_id Fail (@Catch M A).
Lemma catchret : forall A x,
left_zero (Ret x : M _) (@Catch M A).

more complicated Monty Hall problem and tree-

The formal proof that fastproduct is pure, i.e.,

because it is short. In fact, the same can be said

relabeling example (see [5]).
The formal proof above relies on a formalizationof monads organized as a hierarchy in such a waythat properties of a monad at a lower level (say,monad) can be enjoyed by monads at higher levels†1 Inheritance is also explained in the next section(Sect. 3).

(such as exceptMonad). How to achieve this is thepurpose of the next section.

record with a function of type Type -> Type and a
proof that this function belongs to the class of fail-3 Formalization of Algebraic Eﬀects in
Coq
The heart of our mechanization is a formalizationof a hierarchy of monads and their algebraic laws.
It is implemented using packed classes [10]. In thissection, we explain the formalization using an example: the combination of the failure monad andthe choice monad into the non-determinism monad.
The next section (Sect. 4) provides an overview of
the complete hierarchy.

ure monads:(* Module MonadFail *)Record mixin_of (M : monad) : Type := Mixin {fail : forall A, M A ;_ : Laws.left_zero (@Bind M) fail }.
Record class_of (m : Type -> Type) := Class {base : Monad.class_of m ;mixin : mixin_of (Monad.Pack base) }.
Structure t := Pack {m : Type -> Type ; class : class_of m }.
Notation failMonad := t.
Coercion baseType : failMonad >-> monad.
Canonical baseType.

Failure monads are furthermore coerced to monads
and made canonical.

3. 1 The Type of Monad and its Extension
as a Packed Class
The class of monads is formalized as a dependent
record (class_of, in the module†2 Monad) with twoconstructors (ret and bind) satisfying the monadlaws. The type of monads monad (a notation for
Monad.t) is a pair of a Type -> Type function thatsatisfies the class_of interface:(* Module Monad *)Record class_of (m : Type -> Type) : Type :=Class {
ret : forall A, A -> m A ;bind : forall A B, m A -> (A -> m B) -> m B ;_ : Laws.left_neutral bind ret ;_ : Laws.right_neutral bind ret ;_ : Laws.associative bind }.
Record t : Type := Pack {m : Type -> Type ; class : class_of m }.
Notation monad := t.
Coercion m : monad >-> Funclass.

It is cumbersome to use the fail operator of themixin directly. For this reason, it is redefined (asop_fail) so that its type features record projections

w.r.t. the monad. This is actually under this form
that we will use the fail operator (through the notation Fail):(* in Module MonadFail *)Definition op_fail (M : t) : forall A, m M A :=let: Pack _ (Class _ (Mixin x _)) := M
return forall A, m M A in x.
Arguments op_fail {M A} : simpl never.
Notation Fail := op_fail.

Likewise, the property that Fail is a left-zero ofBind is better wrapped as an additional lemma:(* outside of Module MonadFail *)Variable (M : failMonad).
Lemma bindfailm :Laws.left_zero (@Bind _) (@Fail M).

The purpose of the coercion from the type monad is

3. 2 Combination of Eﬀects: Failure andto let one write M A when M has the type monad, M

Choice into Non-determinism

being then understood as the projection m M.
The failure monad is formalized by providing a

Similarly to the failure monad, let us define
the choice monad.

It extends the type monadmixin with a fail operator and the property thatwith the operator alt (pencil-and-paper notation:

the latter is a left-zero of sequential composition.

·  ·) which is associative and such that Bind left-

The class of failure monads are monads that more-

distributes over it:

over satisfy the corresponding mixin (see class_of(* Module MonadAlt *)Record mixin_of (M : monad) : Type := Mixin {alt : forall A, M A -> M A -> M A ;_ : forall A, associative (@alt A) ;_ : Laws.bind_left_distributive (@Bind M) alt }.

below). The type of failure monads is a dependent†2 We use modules just for the name-space.

Record class_of (m : Type -> Type) : Type :=Class {
base : Monad.class_of m ;mixin : mixin_of (Monad.Pack base) }.
Structure t := Pack {m : Type -> Type ; class : class_of m }.
Definition op_alt M := (* omitted *) .
Notation Alt := op_alt.
Notation altMonad := t.

Let [~i] be an infix Coq notation for the nondeterministic choice:

As a consequence of the use of packed classes, it
becomes possible for monads to enjoy the notations
and properties of the monads from which they derive. For instance, in the example just below, it becomes possible with a monad of type nondetMonad touse in combination (1) the Fail definition and the[~i] notation, and (2) the properties of failMonadwith a monad of type nondetMonad:by first specifying the additional properties of theLemma test_canonical (M : nondetMonad)
A (a : M A) (b : A -> M A) :a [~i] (Fail >>= b) = a [~i] Fail.
Proof.
by rewrite bindfailm.
Qed.

non-deterministic choice (the fact that Fail is a unit

Looking (with, say, Set Printing All) at the proofof choice) as a new mixin (see mixin_of just below)

term reveals that Coq has introduced calls toand then declaring a class that combines this mixin

MonadNondet.baseType and alt_of_nondet appropri-with the class of failure monads and choice monads

ately. This shows that packed classes achieve at(class_of below):

the same time both notation overloading and in-(* Module MonadNondet *)Record mixin_of (M : failMonad)(a : forall A, M A -> M A -> M A) : Type :=Mixin {
_ : Laws.left_id (@Fail M) a ;_ : Laws.right_id (@Fail M) a}.
Record class_of (m : Type -> Type) : Type :=Class {
base : MonadFail.class_of m ;mixin : MonadAlt.mixin_of(Monad.Pack (MonadFail.base base)) ;ext : @mixin_of (MonadFail.Pack base)(@MonadAlt.alt _ mixin)}.
Structure t : Type := Pack {m : Type -> Type ; class : class_of m }.
Notation nondetMonad := t.

heritance, thus providing the main ingredients to

Notation "x '[~i]' y" := (Alt x y).

The non-determinism monad is a combination ofa failure monad with a choice monad. This is done

We provide canonical structures so that monads oftype nondetMonad can be seen as monads of type
failMonad or altMonad:(* in Module Nondet *)Definition baseType (M : t) :=MonadFail.Pack (base (class M)).
Coercion baseType : nondetMonad >-> failMonad.
Canonical baseType.
Definition alt_of_nondet (M : nondetMonad) :=MonadAlt.Pack (MonadAlt.Class(mixin (class M))).
Canonical alt_of_nondet.

the formalization of monadic equational reasoning.

4 The Hierarchy of Monads
The hierarchy of monads and their algebraic lawsthat we formalize is essentially the one from [12],with minor adjustments dictated by [11] and [1].
The result is displayed in Fig. 2.
We have already explained monad, failMonad,altMonad,and nondetMonad in Sect. 3. 2, andexceptMonad in Sect. 2. The combination of eﬀects

to form other monads is achieved similarly to thenon-determinism monad: we use one existing classas the base, extend it with an existing mixin, andpossibly add properties as a new mixin.
Prose explanations about each monad can befound in the literature. Here follows a short reading
guide. See the code [5] for details.
• altMonad is the choice monad already seen in
Sect. 3. 2.

The examples of [12] relying on

non-deterministic choice use this monad. However, the combination of non-determinism andFigure 2

Hierarchy of monads formalized. This includes the monads from Gibbons etal. [12] [11] [1]. See Table 1 for an overview of the algebraic laws.

probability in altProbMonad requires idempotence and commutativity [11].

Idempotence

and commutativity are also required in related
work [23].

We have therefore inserted themonad altCIMonad in the hierarchy.
• We saw exceptMonad in the example of Sect. 2.
It is explained in Sect. 5 of [12].

in Sect. 9.1 of [12]. freshMonad provides an operator to generate fresh labels.
• traceMonad and stateTraceMonad are the topic
of Sect. 6. 1.
Our formalization [5] includes all the examples
from [12], as well as examples from [11] and [23].
This includes in particular the eight queens puz-

• The state monad stateMonad and the state

zle from [12], several variants of the Monty Hall

monad with non-determinism nondetStateMonadproblem from [12] and [11] (to illustrate the various

are explained in Sect. 6 of [12]. We come backprobability monads), and the tree-relabeling ex-

to stateMonad in Sect. 6. 1.

ample from [12] that originally motivated monadic• The probability monad probDrMonad was origi-

equational reasoning.

nally explained in Sect. 8 of [12]. The main
diﬀerence with [12] is that we extract fromthe probability monad probDrMonad the monad

5 Formalization

of

the

Probability

Monad and its Model

probMonad as an intermediate step. probDrMonadIn the previous sections, we explained how we for-extends probMonad with right distributivity ofmalized a hierarchy of monads that mostly comesbind (· ≫= ·) over probabilistic choice (· ◁ · ▷ ·).

from [12]. In this section, we provide more details

The reason is that this latter property is notabout the formalization of the probability monad.

compatible with distributivity of probabilistic

The formalization of the probability monad is in-choice over non-deterministic choice (·  ·) andteresting because it shows that using Coq makes it

therefore needs to be put aside so as to be ablepossible to complete the work by Gibbons et al. by

to form altProbMonad by combining probMonadshowing how to provide rigorous models. In Sect. 4

and altMonad (the issue is explained in [1]). Weof [11], the model of the probability monad is in-come back to probMonad in Sect. 5.

formally explained in terms of the datatype Dist of• exceptProbMonad combines probability and ex-

probability-weighted lists that does not take into

ception and comes from Sect. 7.1 of [11].

account permutations, zero-weighted/repeated ele-

• freshMonad and failFreshMonad are explained

ments, etc. However (as hinted at by Gibbons etInterface
monad

Operators
Ret
Bind/>>=/>>

failMonadaltMonad

FailAlt/[~i]altCIMonadnondetMonadexceptMonadCatchstateMonad

Get
Put

Axiomsbindretf (left neutral)bindmret (right neutral)bindA (associativity)
bindfailm (fail left-zero of bind)
alt_bindDl (bind left-distributes over alt)
altA (associativity)
altmm (idempotence)
altC (commutativity)
altmfail (fail right-id of alt)altfailm (fail left-id of alt)
catchfailm (fail left-id of catch)catchmfail (fail right-id of catch)catchA (associativity)
catchret (ret left-zero of catch)putget, getputskip, putput, getget (see Sect. 6. 1. 1)bindmfail (fail right-zero of bind)
alt_bindDr (bind right-distributes over choice)nondetStateMonadfreshMonadfailFreshMonad

FreshdistinctprobMonad

Choicefailfresh_bindmail (fail right-zero of bind)assert (distinct M) \o Symbols = Symbols
choicemm (idempotence)
choice0, choice1 (identity laws)
choiceA (quasi associativity)
choiceC (skewed commutativity)
prob_bindDl (bind left-distributivites over choice)prob_bindDr (bind right-distributes over choice)choiceDr (prob. choice right-distributes over nondet. choice)catchDl (catch left-distributes over choice)probDrMonad
altProbMonadexceptProbMonad
traceMonadMarkstateTraceMonadRun
runret, runbind, runget, runput, runmark (see Sect. 6. 1. 3)
Table 1 Summary of monad operators and their algebraic laws (mostly coming from [12])al.), it takes a bit more eﬀort to provide an initial

1
2

model.

mprobability m+n, etc.

probability, [Pr of INR m / INR (m + n)] for theThis is under the condi-tion that we equip Coq with appropriate canonical
5. 1 The Probability Monadstructures. For example, here follows the registra-

The first step towards a formal model of the prob-

tion of the proof 0 ≤ 0 ≤ 1 that makes it possible

ability monad is to provide a type Prob.t of proba-

to write [Pr of 0]:

bilities (reals between 0 and 1):

Lemma OO1 : (R0 <= R0 <= R1)%R.
Canonical prob0 := Prob.mk OO1.

Module Prob.
Record t := mk {p :> R ;H : (0 <= p <= 1)%R }.
Definition H' (p : t) := H p.
Arguments H' : simpl never.
Notation "[Pr 'of' q ]" := (@mk q (@H' _)).

The significance of this definition and this notation is that it makes it possible to succinctly write:[Pr of 0] for the 0 probability, [Pr of / 2] for the

The above datatype and notation lead us to thefollowing mixin (the one of probMonad from Fig. 2):
Record mixin_of (M : monad) : Type := Mixin {choice : forall (p : Prob.t) A, M A -> M A -> M A
where "mx <| p |> my" := (choice p mx my) ;_ : forall A (mx my : M A),
mx <| [Pr of 0] |> my = my ;_ : forall A (mx my : M A),
mx <| [Pr of 1] |> my = mx ;_ : forall A p (mx my : M A),

mx <| p |> my = my <| [Pr of p.~] |> mx ;_ : forall A p, idempotent (@choice p A) ;_ : forall A (p q r s : Prob.t) (mx my mz : M A),(p = r * s :> R /\ s.~ = p.~ * q.~)%R ->mx <| p |> (my <| q |> mz) =(mx <| r |> my) <| s |> mz ;_ : forall p, Laws.bind_left_distributive(@Bind M) (choice p) }.
p.~ is a notation for the real p̄ = 1 − p, which hap-pens to be a probability when p is (and can thus
be handled by the probability notation [Pr of ...]
thanks to an appropriate canonical structure declaration).

5. 2 A Model Using Probability Distributions
Providing a formal model for the monad seen in
the previous section (Sect. 5. 1) amounts to instantiate its interface with concrete objects.
5. 2. 1 Probability Distributions
In [2] [3] [4], we introduced a formalization ofprobability distributions over a finite type (A below
has type finType) based on the following definition:
Record dist := mkDist {pmf :> A -> R+ ;pmf1 : \rsum_(a in A) pmf a = 1%R}.

The first field is a probability mass function with
non-negative outputs coupled with a proof that theoutputs sum to 1.
5. 2. 2 Formal Model of Monads
Providing a formal model of monads amounts toprovide concrete implementation for Ret and thebind operator†3 . For instance, the bind operator
can be defined using distributions as follows:(* Module DistBind *)Variables (A B : finType)(p : dist A) (g : A -> dist B).
Definition f b := \rsum_(a in A) p a * (g a) b.
Definition d : dist B := ...

(f : A -> dist B) (g : B -> dist C) :DistBind.d (DistBind.d m f) g =DistBind.d m (fun x => DistBind.d (f x) g).

Completing the model with Ret and its properties
is not diﬃcult.
5. 2. 3 Formal Model of the Probability
MonadLast, we need to provide an implementation for
the interface of the probability monad seen in
Sect. 5. 1. For instance, the probabilistic choice operator corresponds to the construction of a new distribution d from two distributions d1 and d2 biased
by a probability p:(* Module ConvexDist *)Variables (A : finType) (d1 d2 : dist A) (p : R).
Definition f a := (p * d1 a + p.~ * d2 a)%R.
Definition d : dist A := ...

This implementation of probabilistic choice can further be proved to have the expected properties, forexample, skewed commutativity:
Lemma quasi_commute (d1 d2 : dist A) p
(Hp : 0 <= p <= 1) (Hp' : 0 <= p.~ <= 1) :d d1 d2 Hp = d d2 d1 Hp'.

We see here that using Prob.t (instead of, say,the mere type for reals R) is crucial to provide amodel.

6 An Application to Program Semantics
In this section, we extend the approach ofmonadic equational reasoning to the formalizationof program semantics. For that purpose, we add
a trace monad to the hierarchy of [12] (see Fig. 2).
Below, we explain how we compose it with the statemonad. The purpose of the trace monad is to beable to express properties over the trace of a program. For example, if the trace includes nonces, wemight want to prove that they are all distinct.

This operator can further be proved to satisfy themonad laws, for example, associativity:

6. 1 The State-Trace Monad

Lemma DistBindA A B C (m : dist A)

The state-trace monad is the result of combining†3 The type of monad in Sect. 3. 1 used Type -> Type.
In this section, we need to specialize it to
finType -> Type.

a state monad with a trace monad. We start byrecalling the interface of the state monad.

6. 1. 1 The State Monad

6. 2 Semantics of an Imperative Language

The state monad denotes computations that

Here we are considering a small imperative lan-transform a state (of type S below). It comes withguage with a global state and a primitive to emit ana Get function to yield a copy of the state and aevent. In practice, emitting an event might consist

Put function to overwrite it. These functions arein printing a message.

constrained by four axioms whose usage is demon-

6. 2. 1 Operational and denotational se-

strated by Gibbons and Hinze with the eight queens
puzzle ( [11], Coq formalization in [5]):Record mixin_of (M : monad) (S : Type) : Type :=Mixin {
get : M S ;put : S -> M unit ;_ : forall s s', put s >> put s' = put s' ;_ : forall s, put s >> get = put s >> Ret s ;_ : get >>= put = skip ;_ : forall k : S -> S -> M S,
get >>= (fun s => get >>= k s) =get >>= fun s => k s s }.

6. 1. 2 The Trace MonadOur trace monad just extends monads with aMark operator to record events:
Record mixin_of T (m : Type -> Type) : Type :=Mixin { mark : T -> m unit }.

Its semantics becomes apparent in the run interfaceof the next section (Sect. 6. 1. 3).
6. 1. 3 The Run Interface
The run interface extends the state monad simultaneously with a Run operator and a Mark operator.
The meaning of the Run operator is captured byseveral axioms that give a meaning to each oper-

mantics
We define the higher-order abstract syntax [24]of the language as follows:
Inductive program : Type -> Type :=| p_ret : forall {A}, A -> program A| p_bind : forall {A B},
program A -> (A -> program B) -> program B| p_cond : forall {A},bool -> program A -> program A -> program A| p_get : program S| p_put : S -> program unit
| p_mark : T -> program unit.

We give it a small-step semantics specified with
continuation in the style of Compcert [6]. We distinguish two kinds of continuations: stop for stopping, and seq (Notation: ·;·) for sequencing:
Inductive continuation : Type :=| stop : forall (A : Type), A -> continuation| seq : forall (A : Type),
program A -> (A -> continuation) ->continuation.

We can then define the step ternary relation that
relates a state to the next one and optionally an
event:
Definition state : Type := S * continuation.

ator involved in the monad. Here follows the runinterface; the Mark operator is abstracted as op:
Record mixin_of T S (M : stateMonad S)(op : T -> M unit) : Type := Mixin {run : forall A,
M A -> S * seq T -> A * (S * seq T) ;_ : forall A (a : A) s, run (Ret a) s = (a, s) ;_ : forall A B (m : M A) (f : A -> M B) s,run (Do{ a <- m ; f a}) s =let: (a', s') := run m s in run (f a') s' ;_ : forall s l, run Get (s, l) = (s, (s, l)) ;_ : forall s l s',run (Put s') (s, l) = (tt, (s', l)) ;_ : forall t s l,run (op t) (s, l) = (tt, (s, l ++ [:: t]))}.

Inductive step :state -> option T -> state -> Prop :=| s_ret : forall s A a (k : A -> _),step (s, p_ret a ; k) None (s, k a)
| s_bind : forall s A B p f (k : B -> _),step (s, p_bind p f ; k) None(s, p ; fun a : A => f a ; k)
| s_cond_true : forall s A p1 p2 (k : A -> _),step (s, p_cond true p1 p2 ; k) None(s, p1 ; k)
| s_cond_false : forall s A p1 p2 (k : A -> _),step (s, p_cond false p1 p2 ; k) None(s, p2 ; k)
| s_get : forall s k,
step (s, p_get ; k) None (s, k s)
| s_put : forall s s' k,
step (s, p_put s' ; k) None (s', k tt)| s_mark : forall s t k,

step (s, p_mark t ; k) (Some t) (s, k tt).

correctness and completeness of the small-step se-

Its reflexive and transitive closure step_star of typemantics with respect to the denotational semantics

state -> list T -> state -> Prop is defined as one

denotation {A : Type} (p : program A) : M A (seeexpects. We prove that step is deterministic andFile smallstep monad.v of [5]).

that step_star is confluent and deterministic.
In order to give our language a denotational se-

6. 2. 2 The need for a small piece of deep
embeddingmantics, we instantiate the class stateTraceMonad in

More precisely, correctness and completeness (ofthe obvious manner. We first provide the definition

the denotational semantics denotation w.r.t. theof the base monad:

operational semantics step_star) require that we

Let m : Type -> Type :=fun A => S * list T -> A * (S * list T).
Program Definition MONAD : monad := Monad.Pack(@Monad.Class m(fun A a => fun s => (a, s)) (* ret *)(fun A B m f => fun s =>let (a, s') := m s in f a s') (* bind *)_ _ _).

prove the two following lemmas on emitted events:

Second, we provide an implementation of the markfunction for the trace monad:
Program Definition TRACE :=@MonadTrace.Mixin T MONAD(fun log s => (tt, (s.1, s.2 ++ [log]))).

Next, we provide an implementation of the statemonad:
Program Definition STATE := @MonadState.ClassS m (Monad.class MONAD)(@MonadState.Mixin S MONAD(* get *) (fun s => (s.1, s))(* put *) (fun s' s => (tt, (s', s.2)))_ _ _ _).

Lemma denotation_prefix_preserved
A (p : program A) : forall s s' l1 l a,
Run (denotation p) (s, l1) = (a, (s', l)) ->exists l2, l = l1 ++ l2.
Lemma denotation_prefix_independent
A (p : program A) s l1 l2 :Run (denotation p) (s, l1 ++ l2) =let res := Run (denotation p) (s, l2) in(res.1, (res.2.1, l1 ++ res.2.2)).

They respectively state that: once an event is emitted it cannot be deleted; and the remaining execution of a program does not depend on the previouly emitted events. Those are natural properties that ought to be true for any monadic code,and not only the monadic code that results fromthe denotation of a program p. But this is not
the case with our above instantiation of the class

Last, we bundle the above monads together withstateTraceMonad. Indeed, the class specifies thosean implementation of the run interface:primitives that should be implemented but do not

Program Definition STATETRACE :=@MonadStateTrace.Pack T S m(@MonadStateTrace.Class T S m STATE TRACE(@MonadStateTrace.Mixin T S(MonadState.Pack STATE)_ (* mark *)(fun A (m : MONAD A) (s : S * list T) => m s)(* run *) _ _ _ _ _)).

It is important to note here that the primitives
get and put can only read and update the global

state (of type S) but not the list of emitted events(of type list T). Only the primitive mark has access to the list of emitted events but it can neither read nor overwrite it: it can only add a newevent log to the list. This is necessary to prove theprevent one to add other primitives that might
break the above properties of emitted events. This
is why we restrict those properties to monadic code(denotation p) resulting from the denotation of aprogram p, thus allowing us to prove them by induction on the syntax. One way to overcome thislimitation would be to include the syntactic restriction into the instatiation. That is to say thatthe previous definition of the monad functor m as
fun A => S * list T -> A * (S * list T) would be

extended with a program p and a proof that its denotation is equal to the function. That is to say it
would become:fun A => {f : S * list T -> A * (S * list T) &{ p : program A | denotation p = f }}7 Some Technical Aspects of the Formalization
7. 1 Rewriting Under Function Abstrac-

Do{ vs <- subs ys; Ret ((x :: x0) ++ vs)} =?g x0

Yet, Ret is still out of reach of rewrite. We could
open again the continuation but we use a “rewrite
under” tactic rewrite_ cat_cons to get:====================
Do{ x1 <- subs ys; Ret (x :: x0 ++ x1)} = ?g x0

Now we can close the goal by reflexivity and we

tions
In pencil-and-paper proofs of monadic equational
reasoning, whether a rewrite occurs under a lambda
or not does not make any diﬀerence, but Coq does
not natively allow for rewrites in the body of functions. Following [21], we provide a bit of automa-

are done. In practice, there is little need for Openand most situations can be handled directly without revealing the evar using rewrite_. We chose to
explain Open here because it shows how rewrite_ isimplemented.

tion (the tactics Open and rewrite_ below) for that
purpose. Let us consider for illustration a functionthat non-deterministically builds a subsequence of

7. 2 Minor Discrepancies between Coq
and Haskell
The diﬀerences between Coq and Haskell area list (Sect. 3.1 of [11]):
Context {M : altMonad} {A : Type}.
Fixpoint subs (s : seq A) : M (seq A) :=if s isn't h :: t then Ret [::] else
let t' := subs t in fmap (cons h) t' [~i] t'.

folklore. Coq functions must terminate, so that

We want to prove the following lemma:

is really terminating. See for example the func-

Lemma subs_cat (xs ys : seq A) :subs (xs ++ ys) = Do{us <- subs xs;
Do{vs <- subs ys; Ret (us ++ vs)}}.

tion perms that non-deterministically build a per-

The proof eventually leads to the following subgoal:ing) [12] [5]. Also, Coq functions need to be total====================
subs ((x :: xs) ++ ys) =Do{ x0 <- subs xs; Do{ us <- Ret (x :: x0);
Do{ vs <- subs ys; Ret (us ++ vs)}}}[~i] Do{ us <- subs xs; Do{ vs <- subs ys;
Ret (us ++ vs)}}and some Haskell functions cannot be formalized as

We want to turn the branchDo{ x0 <- subs xs; Do{ us <- Ret (x :: x0);
Do{ vs <- subs ys; Ret (us ++ vs)}}}we sometimes need an extra eﬀort (but only standard techniques) to convince Coq that a function

mutation of a list (it is not structurally terminat-such (e.g., foldr1).

8 Related Work
8. 1 About Monadic Equational Reasoning
Although enabling equational reasoning for rea-

intosoning about monadic programs seems to be a nat-Do{ x0 <- subs xs;
Do{ vs <- subs ys; Ret (x :: x0 ++ vs)}}ural idea, there does not seem to be much re-Since the target Ret is below Do{ x0 <- ...; ...},

lated work. Gibbons et al. seem to be the first to

rewrite bindretf fails.

Instead, we “open” thesynthesize monadic equational reasoning as an ap-

continuation with Open (X in subs xs >>= X) to get

proach [12] [11] [1]. This viewpoint is also adopted

the goalby other authors (e.g., [23] and [26]—the latter is====================
Do{ us <- Ret (x :: x0); Do{ vs <- subs ys;
Ret (us ++ vs)}} = ?g x0

about equational reasoning for probabilistic pro-on which rewrite bindretf now succeeds:====================

gramming).

8. 2 Formalization of Monads in Coq

This problem of rewriting under function ab-

Monads are widely used for modelling program-straction (discussed in Sect. 7. 1) is not specific toming languages with eﬀects. For instance, [9] con-monadic equational reasoning. For example, it also

tains a formalization in Coq of several monads andoccurs when dealing with the big operators of themonad transformers, each one associated with a so-

MathComp library, a situation for which [21] pro-called feature theorem. When monads are com-vides an automated solution.

bined, those feature theorems can then be easily

9 Conclusions and future work

combined to prove type soundness. In comparison,

We have fully formalized in the Coq proof as-

the work we formalize here contains more monads

sistant the monadic equational reasoning as advo-

but focus on equational reasoning on concrete pro-cated by Gibbons et al. Our approach is successful

grams instead of meta-theory on programming lan-in the sense that our Coq proofs match surpris-

guages.

ingly well their paper-and-pencil proofs. We have

Monads have been used in Coq to verify low-

shown the applicability of the approach by instan-level systems [17] [18] or for their modular verifica-

tiating the probability monad and formalizing thetion [19] based on free monads. We share the samedenotational semantics of an imperative language

original motivation: enable formal reasoning about

with the state-trace monad. The latter application

low-level programs using monads.

has led us to extend the work by Gibbons et al.

There are more formalizations of monads in otheron the state monad. This has also allowed us toproof-assistants. To pick one example that can be

expose a limitation of the approach. Indeed, equa-easily compared to our mechanization, one can findtions can specify what should do some primitives,a formalization of the Monty Hall problem in Is-

but cannot prevent the existence of other primitives

abelle [8] but using a diﬀerent theory called pGCL

following diﬀerent rules. We have thus proposed aand due to McIver and Morgan.

solution in Sect. 6. 2. 2 that consists in combining
the shallow embedding with a limited amount of

8. 3 About shallow and deep embedding

deep embedding.

Shallow and deep embedding have been widely

A natural direction for future work would be thecompared in functional programming, e.g., in [13],formalization of [25] as it would also be the con-and combinations of shallow and deep embedding

tinuation of our formalization of the trace monad

have been proposed, e.g., in [27].

in Sect. 6. 1. 2. The formalization of more monadic
equational reasoning examples [23] to improve the

8. 4 About Formalization Techniques

user experience is also underway.

We use packed classes [10] to formalize the hierarchy of algebraic eﬀects. It would be possible to

Acknowledgements

use other techniques. In fact, the first version of our

We acknowledge the support of the JSPS-CNRS

formalization was using a combination of telescopes

bilateral program “FoRmal tools for IoT sEcurity”

and canonical structures; it did not suﬀer prob-(PRC2199) and thank all the participants of thislems but packed classes are more disciplined. Coq’s

project for fruitful discussions, as well as Cyril Co-

type classes have been reported to replace canoni-

hen and Shinya Katsumata for comments about thecal structures in many situations, but we have notformalization of monads.

tested them here.

References[ 1 ] Abou-Saleh, F., Cheung, K.-H., and Gibbons,J.: Reasoning about Probability and Nondeterminism, POPL workshop on Probabilistic Programming
Semantics, January 2016.
[ 2 ] Aﬀeldt, R. and Hagiwara, M.: Formalization of
Shannon’s Theorems in SSReflect-Coq, 3rd Conference on Interactive Theorem Proving (ITP 2012),
Princeton, New Jersey, USA, August 13–15, 2012,
Lecture Notes in Computer Science, Vol. 7406,
Springer, Aug 2012, pp. 233–249.
[ 3 ] Aﬀeldt, R., Hagiwara, M., and Sénizergues, J.:
Formalization of Shannon’s Theorems, Journal ofAutomated Reasoning, Vol. 53, No. 1(2014), pp. 63–
103.
[ 4 ] Aﬀeldt, R., Hagiwara, M., Senizergues, J., Garrigue, J., Sakaguchi, K., Asai, T., Saikawa, T.,
and Obata, N.: A Coq formalization of information theory and linear error-correcting codes, https://github.com/affeldt-aist/infotheo, 2018.
[ 5 ] Aﬀeldt, R. and Nowak, D.: A Coq formalizationof monadic equational reasoning, https://github.
com/affeldt-aist/monae, 2018.
[ 6 ] Appel, A. W. and Blazy, S.: Separation logic forsmall-step Cminor, Theorem Proving in Higher Order Logics, 20th Int. Conf. TPHOLs 2007, Lecture
Notes in Computer Science, Vol. 4732, Springer,
2007, pp. 5–21.
[ 7 ] Breitner, J., Spector-Zabusky, A., Li, Y.,
Rizkallah, C., Wiegley, J., and Weirich, S.: Ready,Set, Verify!
Applying hs-to-coq to real-world
Haskell code (Experience Report), ICFP 2018,2018. To appear.
[ 8 ] Cock, D.: Verifying probabilistic correctness in
Isabelle with pGCL, 7th Systems Software Verification, Sydney, Australia, Nov 2012, pp. 1–10.
[ 9 ] Delaware, B., Keuchel, S., Schrijvers, T., andd. S. Oliveira, B. C.: Modular monadic meta-theory,
In Morrisett and Uustalu [22], pp. 319–330.
[10] Garillot, F., Gonthier, G., Mahboubi, A., andRideau, L.: Packaging Mathematical Structures,
Theorem Proving in Higher Order Logics, 22ndInternational Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings,
Berghofer, S., Nipkow, T., Urban, C., and Wenzel, M.(eds.), Lecture Notes in Computer Science,Vol. 5674, Springer, 2009, pp. 327–342.
[11] Gibbons, J.: Unifying Theories of Programmingwith Monads, Unifying Theories of Programming,
4th International Symposium, UTP 2012, Paris,
France, August 27-28, 2012, Revised Selected Papers, Wolﬀ, B., Gaudel, M., and Feliachi, A.(eds.),
Lecture Notes in Computer Science, Vol. 7681,
Springer, 2012, pp. 23–67.
[12] Gibbons, J. and Hinze, R.: Just do it: simple monadic equational reasoning, Proceeding of
the 16th ACM SIGPLAN international conference
on Functional Programming, ICFP 2011, Tokyo,

Japan, September 19-21, 2011, Chakravarty, M.
M. T., Hu, Z., and Danvy, O.(eds.), ACM, 2011,
pp. 2–14.
[13] Gibbons, J. and Wu, N.: Folding domain-specificlanguages: deep and shallow embeddings (functional Pearl), Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, Gothenburg, Sweden, September 1-3,
2014, Jeuring, J. and Chakravarty, M. M. T.(eds.),
ACM, 2014, pp. 339–347.
[14] Gonthier, G., Mahboubi, A., and Tassi, E.: A
Small Scale Reflection Extension for the Coq system, Technical report, INRIA, 2008. Version 17(Nov 2016).
[15] Gonthier, G. and Tassi, E.: A Language ofPatterns for Subterm Selection, Interactive Theorem Proving - Third International Conference, ITP
2012, Princeton, NJ, USA, August 13-15, 2012.
Proceedings, Beringer, L. and Felty, A. P.(eds.),
Lecture Notes in Computer Science, Vol. 7406,
Springer, 2012, pp. 361–376.
[16] Greenaway, D.: Automated Proof-Producing Abstraction of C Code, PhD Thesis, University of New
South Wales, Sydney, Australia, Jan 2015.
[17] Jomaa, N., Nowak, D., Grimaud, G., and Hym,
S.: Formal proof of dynamic memory isolation
based on MMU, Science of Computer Programming, Vol. 162(2018), pp. 76–92.
[18] Jomaa, N., Torrini, P., Nowak, D., Grimaud, G.,
and Hym, S.: Proof-Oriented Design of a Separation
Kernel with Minimal Trusted Computing Base, 18th
International Workshop on Automated Verificationof Critical Systems (AVOCS 2018), Jul 2018, Oxford, United Kingdom. Electronic Communicationsof the EASST Open Access Journal, 2018.
[19] Letan, T., Régis-Gianas, Y., Chiﬄier, P., andHiet, G.: Modular Verification of Programs with Effects and Eﬀet Handlers in Coq, 22nd international
symposium on formal methods (FM 2018), Oxford,
United Kingdom, Jul 2018.
[20] Mahboubi, A. and Tassi, E.: Canonical Structures for the Working Coq User, 4th International
Conference on Interactive Theorem Proving (ITP
2013), Rennes, France, July 22–26, 2013, Lecture
Notes in Computer Science, Vol. 7998, Springer,
2013, pp. 19–34.
[21] Martin-Dorel, E.:
ssr-under-tac, https://github.com/erikmd/ssr-under-tac, 2016.
[22] Morrisett, G. and Uustalu, T.(eds.): ACM
SIGPLAN International Conference on Functional
Programming, ICFP’13, Boston, MA, USA September 25 - 27, 2013, ACM, 2013.
[23] Mu, S.-C.: Functional Pearls, Reasoning and
Derivation of Monadic Programs, A Case Study ofNon-determinism and State, Jul 2017. Submitted
for publication. Available at http://flolac.iis.
sinica.edu.tw/flolac18/files/test.pdf (last access: 2018/07/29).

[24] Pfenning, F. and Elliott, C.: Higher-Order
Abstract Syntax, Proceedings of the ACM SIGPLAN’88 Conference on Programming Language
Design and Implementation (PLDI), Atlanta,
Georgia, USA, June 22-24, 1988, Wexelblat,
R. L.(ed.), ACM, 1988, pp. 199–208.
[25] Piróg, M. and Gibbons, J.: Tracing monadic
computations and representing eﬀects, Proceedings
Fourth Workshop on Mathematically Structured
Functional Programming, MSFP@ETAPS 2012,
Tallinn, Estonia, 25 March 2012., Chapman, J. andLevy, P. B.(eds.), EPTCS, Vol. 76, 2012, pp. 90–
111.
[26] Shan, C.-C.: Equational reasoning for probabilistic programming, POPL 2018 TutorialFest, Jan
2018.
[27] Svenningsson, J. and Axelsson, E.: Combining deep and shallow embedding of domain-specificlanguages, Computer Languages, Systems & Structures, Vol. 44(2015), pp. 143–165.