Posted on 2018-03-17. patch theory coq

One of the open-source projects I have been working on for several years is a library that computes diffs between JSON values and produces RFC-6902 patches. Trying to go beyond what the specification proposes, I want my diff tool to generate patches that can be inverted. To this end, I just added fields to some patch operations so that missing information is remembered. I convinced myself that the fields I added are enough to invert any patch, but this is a mere conjecture. There must be a way to be sure that it works. The problem of making sure that a patch can be inverted is actually very interesting to dive into. That is how I started to investigate the area and spent the last few months to do it from time to time.

In the saga starting with this post, I want to expose how I implemented one patch theory using Coq, proved some properties on it, and applied it on an RFC-6902 implementation. There will be some theory, and, I hope, a lot of fun.

This episode defines the problem and the base theoretical tools that will be used to develop the theory.

• Patch theories
  • Darcs
  • Inverse semigroups
• Coq
  • Type classes
  • Encoding inverse semigroups
  • Proving facts about inverse semigroups
• Conclusion

Patch theories

The point of this saga is not to make a comprehensive list of existing patch theories here, but I came across several approach to the problem of formalizing patch operations. Most of them use category theory to model patches and their operations. An overview of papers I found are:

• A Categorical Theory of Patches;
• Homotopical Patch Theory;
• Type-correct changes — a safe approach to version control implementation;
• Camp Patch Theory.

The main (and almost only) source for this bibliography is the Darcs website.

Darcs

Darcs is a decentralized version control system (DVCS). The approach taken by this DVCS is different from the popular git and used-to-be-popular mercurial in that repositories are purely sequences of patches. There is no snapshot of the versioned documents at all.

This is interesting in our case because, darcs only is about managing patches. An more interestingly, the darcs developers have elaborated a patch theory to prove some properties on darcs repositories. Several attempts and approaches have been tested, and one in particular kept my attention. The theory developed in this approach is interesting because it does not make any assumption on the patch format you use, nor on the objects you patch. It is fully described in the theory section of the darcs wiki. It relies only on mathematical objects, namely inverse semigroups. More on this in a few paragraphs.

A big advantage of only handling mathematical abstract structures is that we can prove a lot of property for our system on a really abstract level, and once it is done, instantiate the theory for our concrete patch format. In this saga, I will first develop the theory in Coq at an abstract level, and in the end I will instantiate everything for a concrete patch system. At each step, instantiating a theory will only require us to prove that assumptions of the theory are met.

In the remainder I will expose some parts of the theory as described in the aforementioned paper. If you want more details, you can always refer to it.

Inverse semigroups

Here come the math stuffs! Don’t worry, it won’t be too much, but still, it is math.

A semigroup is defined by a set of elements and an associative binary operation over elements in the set. More formally, for a set $S$ and binary operation $\otimes : S \times S \rightarrow S$, if $\otimes$ satisfies:

$\forall x, y, z \in S, x \otimes (y \otimes z) = (x \otimes y) \otimes z$

Then $(S, \otimes)$ defines a semigroup. An interesting side-effect of the fact that $\otimes$ is associative allows us in the following to drop the use parentheses, making notations a bit lighter (yes, this is a very mathematical consideration…).

This structure will be the base of the entire theory, and the intuition behind it is that applying a patch will be defined as the $\otimes$ operation, that operates over values to patch. This is actually a simplified presentation, as we will see in the following.

Another important property I am interested in is patch inversion, which means that the operation should allow to perform the inverse modifications of a patch. This is where inverse semigroups come in the game. An inverse semigroup is a semigroup where for each element in the set, there exists a unique element, called pseudo-inverse. Formally, if $(S, \otimes)$ defines a semigroup, and if

$\forall x \in S, \exists! x^{-1} \in S, x \otimes x^{-1} \otimes x = x \text{ and } x^{-1} \otimes x \otimes x^{-1} = x^{-1}$

then $(S, \otimes)$ defines an inverse semigroup. This is called a pseudo-inverse and not an inverse because we do not necessarily have an identity element $\overline{1}$ for $\otimes$, such that $x \otimes x^{-1} = \overline{1}$.

Patches may not always be defined for a given value. This is the case when we try to apply a patch on a value that does not meet the patch structural hypotheses (e.g. trying to apply a batch that adds a line in a non existing file). To handle such cases, we can define a zero element that inhibits the operator $\otimes$. An element $\overline 0$ of $S$ is a zero if

$\forall x \in S, x \otimes \overline 0 = \overline 0 \otimes x = \overline 0$

If such an element exist, we can define an inverse semigroup with zero as the triple $(S, \otimes, \overline 0)$.

The last definition we will use for now is the one of idempotent element. An idempotent is a element $x$ of $S$ such that

$x \otimes x = x$

These definitions will be sufficient to state and prove a bunch of properties on inverse semigroups. We will come to them shortly, but first I’d like to introduce another tool that will be sued throughout this saga to develop the theory: Coq.

Coq

Coq is a formal proof assistant. It assists you into formalizing theories and proving them by ensuring that your reasoning is correct, based on axioms, definitions and theorems. This is a tool I personally enjoy using, often in the context of proving properties on programming languages, but it can be used for a wide range of fields, from IT security to the proof of the four colors theorem. A personal particular kuddo goes to CompCert, a verified compiler for a (huge) C subset, written in Coq with all transformations proved from parsing to assembler code generation.

To interactively test the code provided in this saga, you can use CoqIde or other interface tools.

The tool has evolved to a full-fledged programming language with the addition of a lot of features over the years. One of them got my attention: type classes.

Type classes

Type classes are a way to add constraints to values to implement ad hoc polymorphism. They are really popular in the Haskell programming language, for which the entire standard library is defined using them. Lately they also gain popularity in Scala to replace the more rigid inheritance mechanism in a lot of libraries.

When I discovered that this feature was added to Coq, I couldn’t wait to find an application so that I can play with them. And I found it with this project! If you want to find more details on how type classes can be used in Coq, you can read a good tutorial online. In this saga, I will only quickly introduce them by example on applying them to our problem.

Encoding inverse semigroups

We saw earlier what it means to define a semigroup. This definition can be conveniently written using a type class in Coq. The full development

Class Semigroup {X: Type} {op: X -> X -> X}: Type :=
  op_assoc : forall (x y z: X), op x (op y z) = op (op x y) z .

Here we define the class Semigroup over type X and operation op as a single constraint op_assoc. Type classes can be instantiated for a particular set and operation. When it is instantiated a proof that each constraint is met must be provided. For example, the instantiation if Semigroup with natural numbers and the multiplication operation is done as follows:

Instance NatSemigroup : @Semigroup nat Nat.mul.
Proof.
  intros x y z. apply mult_assoc.
Qed.

This one is easy to instantiate because the associativity is already proved in the standard Coq.Arith.Mult module. We will see more complex instantiations later when applying this to our patches. In this case there is only one goal to prove, because we only defined the op_assoc constraint, later we will see type classes with more goals to prove.

A type class may have sub classes, adding new constraints. This is the case of the inverse semigroup we defined earlier. An inverse semigroup is a semigroup with one more constraint: there is a pseudo-inverse for each element. Using type classes and sub classes, we can easily define what it means to be an inverse semigroup in Coq.

Class InverseSemigroup {X: Type} {op: X -> X -> X} `(SG: Semigroup X op): Type :=
  has_pseudo_inverse : forall x, exists! x', op x (op x' x) = x /\ op x' (op x x') = x'.

The concept of type class fits well here to encode our structures. Once we proved some $(X, \otimes)$ defines a semigroup, we can use this exhibit to prove that it also defines an inverse semigroup. This is how type classes are used in all languages supporting them, and it is why they are powerful: they can be composed and are modular.

This defines a new type class InverseSemigroup that is a sub class of Semigroup. To prove that an instance is an InverseSemigroup, the first step will be to provide an instance of Semigroup for the set and operation, that will be referred to as SG.

The notation can become a bit bloated for classes with a lot of parameters. Fortunately, Coq has features that make it possible to infer some recurrent parameters. We can define general variables for X and op that are considered to be present in scope and are used whenever we do not provide them explicitly. We can write the definition as follows and let Coq infer what variables to use for X and op:

Generalizable Variables X op.

Class InverseSemigroup `(SG: Semigroup): Type :=
  has_pseudo_inverse : forall x, exists! x', op x (op x' x) = x /\ op x' (op x x') = x'.

The first line of the snippet above defines the names that are implicitly available. In the remainder of the development, we will work on inverse semigroup. In Coq we can define a Context that means: let’s say we have defined an inverse semigroup ISG.

Context `{ISG: InverseSemigroup}.

This context will be used in the definitions and proofs from now on.

To handle inverse semigroup with zero in Coq, we can define what it means to be a zero and create a type class that adds this zero to an inverse semigroup.

Definition is_zero z :=
  forall x, op x z = z /\ op z x = z.

Class InverseSemigroupz {z: X} `(ISG:InverseSemigroup X op): Type :=
  has_zero : is_zero z.

Context `{ISGZ:InverseSemigroupz}.

Finally we gave a definition of an idempotent, which we do as follows in Coq:

Definition idempotent (x: X) :=
  op x x = x.

Proving facts about inverse semigroups

We are now equipped with many structures and what is left is to state some properties, that will be used later to prove facts about patches. I won’t present all the properties here but will select some useful ones:

• $x \otimes x^{-1}$ is idempotent for all $x$ in $S$. This is interesting in our case if we interpret it as: applying a patch and its inverse and the patch and its inverse again is a noop.
• If $x$ is idempotent, then it is its own inverse.
• If $x$ and $y$ are idempotent, then so is $x \otimes y$.

They may appear a bit abstract for now, but we will see how to use them in our patch theory in the next episode. The purpose of exposing them here is to show how to encode these properties in Coq, using our type classes.

Definition pseudo_inverse x x' :=
  op x (op x' x) = x /\ op x' (op x x') = x'.

Lemma inv_idem :
  forall x x',
    pseudo_inverse x x' -> (idempotent (op x x') /\ idempotent (op x' x)).

This can be proved by expanding what it means to be idempotent and using the associativity property of op. You can step over the following proof to see how we proceed.

Proof.
  intros x x' H.
  unfold idempotent.
  split.
  - rewrite op_assoc.
    assert (op (op x x') x  = op x (op x' x)) by auto.
    rewrite H0. unfold pseudo_inverse in H. destruct H. rewrite H. reflexivity.
  - rewrite op_assoc.
    assert (op (op x' x) x'  = op x' (op x x')) by auto.
    rewrite H0. apply inv_inv in H.
    unfold pseudo_inverse in H. destruct H. rewrite H. reflexivity.
Qed.

The second fact is defined as follows in Coq:

Lemma idem_inv :
  forall x,
    idempotent x ->
      pseudo_inverse x x.
Proof.
  intros.
  unfold pseudo_inverse.
  split; repeat(rewrite H); reflexivity.
Qed.

It is proved by simply repeating the definition of an idempotent.

Finally the third fact can be defined as:

Lemma idem_op_idem :
  forall x y,
    idempotent x ->
      idempotent y ->
        idempotent (op x y).

I won’t go into details of the proof here, because it is much longer but the proof uses the previous facts and associativity property of the operation op.

Conclusion

That’s it for this first episode. I tried to be as clear as possible about my motivation and goal, and introduced a few mathematical constructs and facts that will be useful in the following.
You can download the full Coq developments here.
In the next episode we will define our complete abstract patch theory and prove elements on it, in particular facts about patch inversion and commuting patches.

In the meantime, I wish you all a happy Saint Patrick’s day, may the Holy Guinness guide your steps!