A research blog about programming languages, formal logics, software development and their interactions, by Matthias Puech.

## Tag: proof

### 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.

Learning Coq is usually an enlightening experience. I know it first-hand, it can also be a quite frustrating one, because it seems at first to involve remembering quite a lot of arbitrarily-named tactics, that one might not fully understand the effect of. `discriminate` is one of them: “if you’re faced with an obvious inequality, just apply `discriminate`” they say. If you look at the proof term, however, it is far from trivial and involves a “trick”, a kind of “lie” that Pierre has become a specialist of. There is an intermediate step in the comprehension, that we put together with Chantal: decomposing the proof generated by discriminate. Here is a very easy proof that 1 ≠ 0, which does not require to understand neither proof terms nor return clauses in pattern-matching. Pure beginner Coq.