### Typeful disjunctive normal form

This is the answer to last post’s puzzle. I gave an algorithm to put a formula in disjunctive normal form, and suggested to prove it correct in OCaml, thanks to GADTs. My solution happens to include a wealth of little exercises that could be reused I think, so here it is.

I put the code snippets in the order that I think is more pedagogical, and leave to the reader to reorganize them in the right one.

First, as I hinted previously, we are annotating formulas, conjunctions and disjunctions with their corresponding OCaml type, in order to reason on these types:

```type 'a atom = int

type 'a form =
| X : 'a atom -> 'a form
| And : 'a form * 'b form -> ('a * 'b) form
| Or : 'a form * 'b form -> ('a, 'b) union form

type 'a conj =
| X : 'a atom -> 'a conj
| And : 'a atom * 'b conj -> ('a * 'b) conj

type 'a disj =
| Conj : 'a conj -> 'a disj
| Or : 'a conj * 'b disj -> ('a, 'b) union disj
```

What we are eventually looking for is a function `dnf` mapping an `'a form `to a `'b disj`, but now these two must be related: they must represent two equivalent formulae. So, correcting what I just said: `dnf` must return the pair of a `'b disj` and a proof that `'a` and `'b` are equivalent. This pair is an existential type, which is easily coded with a GADT (we do similarly for conjunctions):

```type 'a cnj = Cnj : 'b conj * ('a, 'b) equiv -> 'a cnj
type 'a dsj = Dsj : 'b disj * ('a, 'b) equiv -> 'a dsj
```

Let’s leave out the definition of `equiv` for a while. Now the code from the previous post is fairly easily adapted:

```let rec conj : type a b. a conj -> b conj -> (a * b) cnj =
fun xs ys -> match xs with
| X x -> Cnj (And (x, ys), refl)
| And (x, xs) ->
let Cnj (zs, e) = conj xs ys in
Cnj (And (x, zs), lemma0 e)

let rec disj : type a b. a disj -> b disj -> (a, b) union dsj =
fun xs ys -> match xs with
| Conj c -> Dsj (Or (c, ys), refl)
| Or (x, xs) ->
let Dsj (zs, e) = disj xs ys in
Dsj (Or (x, zs), lemma1 e)

let rec map : type a b. a conj -> b disj -> (a * b) dsj =
fun x -> function
| Conj y ->
let Cnj (z, e) = conj x y in
Dsj (Conj z, e)
| Or (y, ys) ->
let Cnj (z, e1) = conj x y in
let Dsj (t, e2) = map x ys in
Dsj (Or (z, t), lemma2 e1 e2)

let rec cart : type a b. a disj -> b disj -> (a * b) dsj =
fun xs ys -> match xs with
| Conj c -> map c ys
| Or (x, xs) ->
let Dsj (z, e1) = map x ys in
let Dsj (t, e2) = cart xs ys in
let Dsj (u, e3) = disj z t in
Dsj (u, lemma3 e1 e2 e3)

let rec dnf : type a. a form -> a dsj = function
| X x -> Dsj (Conj (X x), refl)
| Or (a, b) ->
let Dsj (c, e1) = dnf a in
let Dsj (d, e2) = dnf b in
let Dsj (e, e3) = disj c d in
Dsj (e, lemma4 e1 e2 e3)
| And (a, b) ->
let Dsj (c, e1) = dnf a in
let Dsj (d, e2) = dnf b in
let Dsj (e, e3) = cart c d in
Dsj (e, lemma5 e1 e2 e3)
```

It seems more verbose, but since the functions now return existentials, we need to deconstruct them and pass them around. I abstracted over the combinators that compose the proofs of equivalence `lemma1``lemma5`, we’ll deal with them in a moment. For now, you can replace them by `Obj.magic` and read off their types with `C-c C-t` to see if they make sense logically. Look at the last function’s type. It states, as expected: for any formula $A$, there exists a disjuctive normal form $B$ such that $A \Leftrightarrow B$.

Now on this subject, what is it for two types to be equivalent? Well, that’s the “trick”: let’s just use our dear old Curry-Howard correspondence! `'a` and `'b` are equivalent if there are two functions `'a -> 'b` and `'b -> 'a` (provided of course that we swear to use only the purely functional core of OCaml when giving them):

```type ('a, 'b) equiv = ('a -> 'b) * ('b -> 'a)
```

Now we can state and prove a number of small results on equivalence with respect to the type constructors we’re using (pairs and unions). Just help yourself into these if you’re preparing an exercise sheet on Curry-Howard :)

```(* a = a *)
let refl : type a. (a, a) equiv =
(fun a -> a), (fun a -> a)

(* a = b -> b = a *)
let sym : type a b. (a, b) equiv -> (b, a) equiv =
fun (ab, ba) -> (fun b -> ba b), (fun a -> ab a)

(* a = b -> b = c -> a = c *)
let trans : type a b c. (b, c) equiv -> (a, b) equiv -> (a, c) equiv =
fun (bc, cb) (ab, ba) -> (fun a -> bc (ab a)), (fun c -> ba (cb c))

(* a = b -> c = d -> c * a = d * b *)
let conj_morphism : type a b c d. (a, b) equiv -> (c, d) equiv ->
(c * a, d * b) equiv = fun (ab, ba) (cd, dc) ->
(fun (c, a) -> cd c, ab a),
(fun (c, b) -> dc c, ba b)

let conj_comm : type a b. (a * b, b * a) equiv =
(fun (x, y) -> y, x), (fun (x, y) -> y, x)

(* (a * b) * c = a * (b * c) *)
let conj_assoc : type a b c. ((a * b) * c, a * (b * c)) equiv =
(fun ((x, y), z) -> x, (y, z)),
(fun (x, (y, z)) -> (x, y), z)

(* a = b -> c + a = c + b *)
let disj_morphism : type a b c d. (a, b) equiv -> (c, d) equiv ->
((c, a) union, (d, b) union) equiv =
fun (ab, ba) (cd, dc) ->
(function Inl c -> Inl (cd c) | Inr a -> Inr (ab a)),
(function Inl d -> Inl (dc d) | Inr b -> Inr (ba b))

(* (a + b) + c = a + (b + c) *)
let disj_assoc : type a b c. (((a, b) union, c) union,
(a, (b, c) union) union) equiv =
(function Inl (Inl a) -> Inl a
| Inl (Inr b) -> Inr (Inl b)
| Inr c -> Inr (Inr c)),
(function Inl a -> Inl (Inl a)
| Inr (Inl b) -> Inl (Inr b)
| Inr (Inr c) -> Inr c)

(* a * (b + c) = (a * b) + (a * c) *)
let conj_distrib : type a b c. (a * (b, c) union,
(a * b, a * c) union) equiv =
(function a, Inl b -> Inl (a, b)
| a, Inr c -> Inr (a, c)),
(function Inl (a, b) -> a, Inl b
| Inr (a, c) -> a, Inr c)
```

Finally, thanks to these primitive combinators, we can prove the lemmas we needed. Again, these are amusing little exercises.

```let lemma0 : type a b c d. (a * b, c) equiv -> ((d * a) * b, d * c) equiv =
fun e -> trans (conj_morphism e refl) conj_assoc

let lemma1 : type a b c d. ((a, b) union, d) equiv ->
(((c, a) union, b) union, (c, d) union) equiv =
fun e -> trans (disj_morphism e refl) disj_assoc

let lemma2 : type a c d u v. (a * c, u) equiv -> (a * d, v) equiv ->
(a * (c, d) union, (u, v) union) equiv =
fun e1 e2 -> trans (disj_morphism e2 e1) conj_distrib

let lemma3 : type a b c d e f. (a * b, c) equiv -> (d * b, e) equiv ->
((c, e) union, f) equiv -> ((a, d) union * b, f) equiv =
fun e1 e2 e3 ->
trans e3
(trans (disj_morphism e2 e1)
(trans (disj_morphism conj_comm conj_comm)
(trans conj_distrib
conj_comm)))

let lemma4 : type a b c d e. (a, c) equiv -> (b, d) equiv ->
((c, d) union, e) equiv -> ((a, b) union, e) equiv =
fun e1 e2 e3 -> trans e3 (disj_morphism e2 e1)

let lemma5 : type a b c d e. (a, c) equiv ->
(b, d) equiv -> (c * d, e) equiv -> ((a * b), e) equiv =
fun e1 e2 e3 -> trans e3 (conj_morphism e2 e1)
```

Note that I only needed the previous primitives to prove these lemmas (and as such to define my functions), so we can even make the type `equiv` abstract, provided that we are giving a complete set of primitives (which is not the case here). Although I’m not sure what it would buy us…

Anyway. That’s my solution! What’s yours?