Theory Monad_Normalisation.Monad_Normalisation

(*  Title:      Monad_Normalisation.thy
    Author:     Manuel Eberl, TU München
    Author:     Joshua Schneider, ETH Zurich
    Author:     Andreas Lochbihler, ETH Zurich

Normalisation of monadic expressions.
*)

section ‹Normalisation of monadic expressions›

theory Monad_Normalisation
imports "HOL-Probability.Probability"
keywords "print_monad_rules" :: diag
begin

text ‹
  The standard monad laws
  \begin{gather}
    \label{eq:return:bind}
    return a ⤜ f = f a›
    \\
    \label{eq:bind:return}
    x ⤜ return = x›
    \\
    \label{eq:bind:assoc}
    (x ⤜ f) ⤜ g = x ⤜ (λa. f a ⤜ g)›
  \end{gather}
  yield a confluent and terminating rewrite system.
  Thus, when these equations are added to the simpset, the simplifier can normalise monadic 
  expressions and decide the equivalence of monadic programs (in the free monad).

  However, many monads satisfy additional laws.
  In some monads, it is possible to discard unused effects
  \begin{gather}
    \label{eq:discard}
    x ⤜ (λ_. y) = y›
  \end{gather}
  or duplicate effects
  \begin{gather}
    \label{eq:duplicate}
    x ⤜ (λa. x ⤜ f a) = x ⤜ (λa. f a a)›
  \end{gather}
  or commute independent computations
  \begin{gather}
    \label{eq:commute}
    x ⤜ (λa. y ⤜ f a) = y ⤜ (λb. x ⤜ (λa. f a b))›.
  \end{gather}
  For example, @{typ "_ option"} satisfies \eqref{eq:duplicate} and \eqref{eq:commute},
  @{typ "_ set"} validates \eqref{eq:commute}, and
  @{typ "_ pmf"} satisfies \eqref{eq:discard} and \eqref{eq:commute}.
  Equations \eqref{eq:discard} and \eqref{eq:duplicate} can be directly used as rewrite rules.%
  \footnote{%
    If they both hold, then \eqref{eq:commute} holds, too cite"LochbihlerSchneider2016ITP".
  }
  However, the simplifier does not handle \eqref{eq:commute} well because \eqref{eq:commute} is a
  higher-order permutative rewrite rule and ordered rewriting in the simplifier can only handle 
  first-order permutative rewrite rules.
  Consequently, when \eqref{eq:commute} is added to the simpset, the simplifier will loop.

  This AFP entry implements a simproc for the simplifier to simplify HOL expressions over commutative
  monads based on ordered rewriting.  This yields a decision procedure for equality of monadic 
  expressions in any (free) monad satisfying any of the laws (\ref{eq:discard}--\ref{eq:commute}).
  If further commutative operators show up in the HOL term, then the ordered rewrite system need not
  be confluent and the simproc only performs a best effort.  We do not know whether this general case
  can be solved by ordered rewriting as a complete solution would have to solve the graph isomorphism
  problem by term rewriting cite"Basin1994IPL".
›

ML_file ‹monad_rules.ML›

subsection ‹Usage›

text ‹
  The monad laws \eqref{eq:return:bind}, \eqref{eq:bind:return}, \eqref{eq:bind:assoc}, \eqref{eq:commute}
  must be registered with the attribute @{attribute monad_rule}. 
  The simproc does not need \eqref{eq:discard} and \eqref{eq:duplicate}, so these properties need not
  be registered, but can simply be added to the simpset if needed.
  The simproc is activated by including the bundle monad_normalisation›.

  Additionally, distributivity laws for control operators like @{const If} and @{const case_nat} 
  specialised to ⤜› can be declared with the attribute @{attribute monad_distrib}.
  Then, the simproc will also commute computations over these control operators.

  The set of registered monad laws can be inspected with the command @{command print_monad_rules}.
›

subsection ‹Registration of the monads from the Isabelle/HOL library›

lemmas [monad_rule] = Set.bind_bind

lemma set_bind_commute [monad_rule]:
  fixes A :: "'a set" and B :: "'b set"
  shows "A  (λx. B  C x) = B  (λy. A  (λx. C x y))"
  unfolding Set.bind_def by auto

lemma set_return_bind [monad_rule]:
  fixes A :: "'a  'b set"
  shows "{x}  A = A x"
  unfolding Set.bind_def by auto

lemma set_bind_return [monad_rule]:
  fixes A :: "'a set"
  shows "A  (λx. {x}) = A"
  unfolding Set.bind_def by auto

lemmas [monad_rule] = Predicate.bind_bind Predicate.bind_single Predicate.single_bind

lemma predicate_bind_commute [monad_rule]:
  fixes A :: "'a Predicate.pred" and B :: "'b Predicate.pred"
  shows "A  (λx. B  C x) = B  (λy. A  (λx. C x y))"
  by (intro pred_eqI) auto


lemmas [monad_rule] = Option.bind_assoc Option.bind_lunit Option.bind_runit

lemma option_bind_commute [monad_rule]:
  fixes A :: "'a option" and B :: "'b option"
  shows "A  (λx. B  C x) = B  (λy. A  (λx. C x y))"
  by (cases A) auto

lemmas [monad_rule] =
  bind_assoc_pmf
  bind_commute_pmf
  bind_return_pmf
  bind_return_pmf'

lemmas [monad_rule] =
  bind_spmf_assoc
  bind_commute_spmf
  bind_return_spmf
  return_bind_spmf


subsection ‹Distributive operators›

lemma bind_if [monad_distrib]:
  "f A (λx. if P then B x else C x) = (if P then f A B else f A C)"
by simp

lemma bind_case_prod [monad_distrib]:
  "f A (λx. case y of (a,b)  B a b x) = (case y of (a,b)  f A (B a b))"
by (simp split: prod.split)

lemma bind_case_sum [monad_distrib]:
  "f A (λx. case y of Inl a  B a x | Inr a  C a x) =
    (case y of Inl a  f A (B a) | Inr a  f A (C a))"
by (simp split: sum.split)

lemma bind_case_option [monad_distrib]:
  "f A (λx. case y of Some a  B a x | None  C x) =
    (case y of Some a  f A (B a) | None  f A C)"
by (simp split: option.split)

lemma bind_case_list [monad_distrib]:
  "f A (λx. case y of []  B x | y # ys  C y ys x) = (case y of []  f A B | y # ys  f A (C y ys))"
by (simp split: list.split)

lemma bind_case_nat [monad_distrib]:
  "f A (λx. case y of 0  B x | Suc n  C n x) = (case y of 0  f A B | Suc n  f A (C n))"
by (simp split: nat.split)


subsection ‹Setup of the normalisation simproc›

ML_file ‹monad_normalisation.ML›

simproc_setup monad_normalisation ("f x y") = K Monad_Normalisation.normalise_step
declare [[simproc del: monad_normalisation]]

text ‹
  The following bundle enables normalisation of monadic expressions by the simplifier.
  We use @{attribute monad_rule_internal} instead of monad_rule[simp]› such that
  the theorems in @{thm [source] monad_rule} get dynamically added to the simpset instead of
  only those that are in there when the bundle is declared.
›

bundle monad_normalisation = [[simproc add: monad_normalisation, monad_rule_internal]]

end