Logical equivalences in Haskell

The blogpost Classical Logic in Haskell established a way to prove equivalences between logical propositions and law of excluded middle by writing intances of Iso for the same propositions wrapped in a newtype. Vladimir’s post contain proofs of some important propositions. I had fun proving them myself. I wanted to continue with some more.

Recently, I did the Logic and Proof course to learn both proof techniques and Lean theorem prover. It was fun. So I picked few propositions from the exercises of the Propositional Logic in Lean chapter to try write equivalence proofs for them.

Below are the propositions as newtypes (their logical notations mentioned as comment) and subsequently the Iso instances to prove their equivalences with Lem. As mentioned in the original blogpost, one nice way to progress here is by taking clues from the type system itself in the form of typed holes.

Let’s set some language pragmas

Required Iso class from the original blogpost put inside a module so that it can be imported for rest of the sections

And now the propositions…

This is an IHaskell Notebook which is pretty cool for above kind of experiments. Much more feature rich than GHCi. I got the inspiration from Vaibhav Sagar who writes all his posts as IHaskell Notebooks.