From d6c96f9630b9ba80223b08958a597b47d35b431f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 18 Oct 2019 10:08:34 +0200
Subject: [PATCH] More about normalization in README.

---
 README.md | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/README.md b/README.md
index e96e620..536572e 100644
--- a/README.md
+++ b/README.md
@@ -80,6 +80,21 @@ Actris tactics are as follows:
   put `H : c ↣ prot1` and `H : c ↣ prot2` back into the contexts of the two
   respectively goals.
 
+The above tactics implicitly perform normalization of the protocol `prot` in
+the hypothesis `H : c ↣ prot`. For example, `wp_send` also works if there is a
+with protocol the `iProto_dual ((<?> y1 .. yn, MSG v; {{ P }}; END) <++> prot)`.
+Concretely, the normalization performs the following actions:
+
+- It re-associates appends (`<++>`), and removes left-identities (`END`) of it.
+- It moves appends (`<++>`) into sends (`<!>`), receives (`<?>`), selections
+  (`<+>`) and branches (`<&>`).
+- It distributed duals (`iProto_dual`) over append (`<++>`).
+- It unfolds `prot1` into `prot2` if there is an instance of the type class
+  `ProtoUnfold prot1 prot2`. When defining a recursive protocol, it is
+  useful to define a `ProtoUnfold` instance to obtain automatic unfolding
+  of the recursive protocol. For example, see `sort_protocol_br_unfold` in
+  [theories/examples/sort_br_del.v](theories/examples/sort_br_del.v).
+
 [HeapLang]: https://gitlab.mpi-sws.org/iris/iris/blob/master/HeapLang.md
 [ProofMode]: https://gitlab.mpi-sws.org/iris/iris/blob/master/ProofMode.md
 [ActrisProofMode]: theories/channel/proofmode.v
-- 
GitLab