Coq to Haskell

Lately I spent some time learning Coq. It is a very useful programming language, but guess what? It has no IO!

So, once we prove our theorems, what do we do? We extract our code!

Let’s pick a language that has IO, for example Haskell.

For fun, let’s try to prove the following and extract the definitions to Haskell:
The sum of a list containing natural numbers is always greater than or equal to 0.

But, in order to prove this, we must define everything on a core level, that is:
1. We need to define what a list is
2. We need to define what a natural number is

We can, but we won’t do that since they are already defined in Coq itself. So we’ll just go ahead and use “list” and “nat” in our code.

Here’s the definition of our recursive function that will calculate the sum of all the elements in a list of natural numbers:

Fixpoint my_sum (l : list nat) : nat :=
  match l with
  | nil     => 0
  | x :: l' => x + my_sum l'
  end.

It’s a pretty straight-forward definition. Let’s write some examples:

Example my_sum1 : my_sum [1 ; 2 ; 3] = 6.
Proof.
  simpl. reflexivity.
Qed.

Example my_sum2 : my_sum [] = 0.
Proof.
  simpl. reflexivity.
Qed.

Example my_sum3 : my_sum [1] = 1.
Proof.
  simpl. reflexivity.
Qed.

And now, for the proof of our theorem:

(* Sum of a list of naturals will always produce a result greater than or equal to 0 *)
Theorem my_sum_nat_gt_0 : forall l : list nat, 0 <= my_sum l.
Proof.
  intros l.
  induction l.
  - (* base *) simpl. reflexivity.
  - (* i.h. *) simpl. case a.
    + (* zero *) simpl. exact IHl.
    + (* S n  *) intros n. rewrite IHl. exact (Plus.le_plus_r (S n) (my_sum l)).
Qed.

Cool! Now for the final part, which is the extraction:

Require Extraction.
Extraction Language Haskell.
Recursive Extraction my_sum.

And finally, our Haskell code generated by the commands above:

data Nat =
   O
 | S Nat

data List a =
   Nil
 | Cons a (List a)

add :: Nat -> Nat -> Nat
add n m =
  case n of {
   O -> m;
   S p -> S (add p m)}

my_sum :: (List Nat) -> Nat
my_sum l =
  case l of {
   Nil -> O;
   Cons x l' -> add x (my_sum l')}

We can now use our function my_sum for which we know our theorem to be true, and we can use it in a programming language that supports IO.

Pretty cool stuff, right? 🙂

Bonus: You can’t do these kind of proofs in Haskell itself, since it has no support for dependent types (we’ll cover that in a future post).

MU puzzle

The MU puzzle is an example of a Formal system we will take a look at, as described by Douglas Hofstadter in his book Gödel, Escher, Bach.

We’re given a starting string MI, and some transformation rules.

Here are the transformation rules:

Nr.	Formal rule			Informal explanation	Example
1.	x`I`	→	x`IU`	Add a `U` to the end of any string ending in `I`	`MI`	to	`MIU`
2.	`M`x	→	`M`xx	Double the string after the `M`	`MIU`	to	`MIUIU`
3.	x`III`y	→	x`U`y	Replace any `III` with a `U`	`MUIIIU`	to	`MUUU`
4.	x`UU`y	→	xy	Remove any `UU`	`MUUU`	to	`MU`

Here is an example usage to derive MIIU from MII for some of the transformation rules:

MI (an axiom)
MII (by rule 2)
MIIII (by rule 2)
MIIIIIIII (by rule 2)
MUIIIII (by rule 3)
MUUII (by rule 3)
MII (by rule 4)
MIIU (by rule 1)

More formally, we can represent the MU puzzle as follows:

Language
1. The set of symbols is { M, I, U }.
2. A string is a grammatical sentence (wff) if its first word is M, and no other words are Ms. E.g.: The following strings are grammatical sentences: M, MIUIU, MUUUIII.
MI is the starting string, thus an axiom.
The inference rules are the transformation rules we’ve just defined above.

The question now is, can we convert MI to MU using the transformation rules?

In order to answer this, we will use invariant (a property that holds true whenever we apply some of the rules) with induction to prove our claim.

What would be a good invariant here?

Let’s suppose we can somehow get to MUIIIU. Now, if we apply rule 3 to it, we get MUUU. Apply rule 4, and pure win!

Note that, in order to be able to apply rule 3, we need to have the number of subsequent I’s to be divisible by 3. So let’s have our invariant say that “There are no subsequent I’s in the string that are divisible by 3”.

1. For the starting axiom, we have one I. Invariant OK.
2. Applying rule 2 will be doubling the number of I’s, so we can have: I, II, IIII, IIIIIII (in particular, 2^n I’s). Invariant OK.
3. Applying rule 3 will be reducing the number of I’s by 3. But note that 2^n – 3 is still not divisible by 3. Invariant OK.

So we’ve shown that with the starting axiom MI it is not possible to get to MU. But, what if we have a different starting axiom? Or even, different rules? 🙂

But if we look carefully, we’ve used a different formal system to reason about MU (i.e. divisibility by 3). This is because the puzzle cannot be solved in its own system. Otherwise, an algorithm would keep trying different inference rules of MU indifinitely (not knowing that MU is impossible).

In general, for any formal system there’s this limitation. Gödel’s theorem shows that there’s no formal system that can contain all possible truths, because it cannot prove some truths about its own structure.

So, having experience with different formal systems and combining them as needed can be useful 🙂

Formal systems

This post is a generalization to one of my previous posts, Hierarchy of logical systems.

Wikipedia states the following definition of a formal system:

A formal system is any well-defined system of abstract thought based on the model of mathematics

More formally, a formal system is consisted of:

A formal language, i.e.
1. A finite set of symbols, that can be used for constructing formulas (i.e. finite strings of symbols).
2. A grammar, which tells how well-formed formulas (abbreviated wff) are constructed out of the symbols.
A set of axioms.
A set of inference rules.

Once we defined a formal system, other systems can extend it.

For example, the ZFC set theory is based on first-order logic, which itself is based on propositional logic which is a formal system.

In general, we often put our focus on which parts of mathematics can be formalized in particular formal systems, rather than trying to find a theory in which all of mathematics can be developed, for the reason below.

Gödel’s incompleteness theorem states that there doesn’t exist* a formal system that is both complete and consistent.

Note that the statement above is about systems that allow expressing arithmetic of natural numbers (e.g. Peano, ZFC, but first-order logic also has some paradoxes if we allow self-referential statements).

In other words, for every such formal system, we will have either:

There will be statements that are true in that system, but which cannot be proved to be true inside the system (incomplete).

A quick example is the statement “This statement is not provable”.
The statement can either be true or false:
True: It is not provable.
False: It is provable, but we’re trying to prove something false.
Thus the system is incomplete, because some truths are unprovable.
There will be a theorem in the system that is contradictory (inconsistent).

We can start with the following statement: “This statement is false”.

This statement is true if and only if it is false, and therefore it is neither true nor false (inconsistent).

The proof above tells us that we should keep thinking about our formal systems outside of their own definition, i.e. as the famous saying goes to think outside of the box, in order to improve our systems. Similarly to how we sometimes do meta-thinking to improve ourselves.

In conclusion, formal systems are our attempt to abstract models, whenever we reverse engineer nature in attempt to understand more. They may be imperfect, but can be very useful for our understanding.

We will look at an example of a formal system in my next post.

Intuitionistic logic

According to Wikipedia:

In type theory, a system has inductive types if it has facilities for creating a new type along with constants and functions that create terms of that type. The feature serves a role similar to data structures in a programming language and allows a type theory to add concepts like numbers, relations, and trees. As the name suggests, inductive types can be self-referential, but usually only in a way that permits structural recursion.

Let’s look at how Coq defines False/True and false/true (as per Mike Nahas’ tutorial) in terms of inductive types:

Inductive False : Prop := .

Inductive True : Prop :=
  | I : True.

Inductive bool : Set :=
  | true : bool
  | false : bool.

False/True are Prop(s), where False has no constructors (i.e. it is the bottom type for which no proof exists), and True has one constructor.
false/true are bool(s), where both of them are a constructor for bool.

Coq also has definitions for both Prop and bool, e.g. for comparison we use eq and eqb respectively.
The definitions of them are:

eq  : ?A -> ?A -> Prop where ?A : [ |- Type]
eqb : bool -> bool -> bool

But there are some fancy lemmas for converting some of them, e.g. one example is:

Nat.eqb_eq : forall n m : nat, (eqb n m) = true <-> (eq n m)

If we now take a look at the modus ponens theorem:
Theorem modus_ponens : (forall A B : Prop, A -> (A -> B) -> B).
We can clearly see that A and B are Prop(s), and not bool(s).

So even though there is some similarity between bool and Prop, they are fundamentally different. bool can be looked as either being true or false (and can also be computed a value for), and Prop as either provable or not (no computation). The logical system that depends on Prop at the fundamental level is called Intuitionistic logic, and the distinction from classical logic can be noticed easily.

This logic closely mirrors the notion of constructive proof, where for a proof we need to provide the actual object that satisfies it. As a result, the law of excluded middle (P or not P) is not defined in Intuitionistic logic. As we said, Prop cannot be true or false (i.e. doesn’t represent truth), rather True or False (i.e. represents the fact that we have a direct proof or not).

For a propostion x : Prop, a valid proof would be proof_x : x, that is an object of type x. To demonstrate what I mean by this, let’s see how a proof in Coq looks:

Inductive x : Prop.
Variable proof_x : x.

Theorem a_random_proof_exists : exists a, a.
Proof.
  exists x.
  exact proof_x.
Qed.

Inhabitants of Prop (e.g. x) are types whose inhabitants are proofs of logical statements (e.g. proof_x). Note that (a : b : c) means exactly the same as (a : b) and (b : c), that is a has a type of b, and b has a type of c. (proof_x : x : Prop) means that x is a logical proposition and proof_x is its proof. This is very close to BHK interpretation, where:

A proof of P ∧ Q is a pair <a, b> where a is a proof of P and b is a proof of Q.
A proof of P ∨ Q is a pair <a, b> where a is 0 and b is a proof of P, or a is 1 and b is a proof of Q.
A proof of P → Q is a function f that converts a proof of P to a proof of Q.
A proof of ∃x ∈ S : φ(x) is a pair <a, b> where a is an element of S, and b is a proof of φ(a).
A proof of ∀x ∈ S : φ(x) is a function f that converts an element a of S into a proof of φ(a).
The formula ¬P is defined as P → ⊥, so a proof of it is a function f that converts a proof of P into a proof of ⊥.
There is no proof of ⊥.

If we try to print the definitions of “and” and “or” in Coq, here’s what we get:

Print and. (* Inductive and (A B : Prop) : Prop :=  conj : A -> B -> A /\ B *)
Print or.  (* Inductive or (A B : Prop) : Prop :=  or_introl : A -> A \/ B | or_intror : B -> A \/ B *)

It’s the famous product and sum types, which line up well with the BHK interpretation above. But what about ->? Whoops, it’s just a notation:

Locate "->". (* Notation "A -> B" := forall _ : A, B : type_scope *)

This is a notation for non-dependent product, contrast to the case of (forall x : A, B) where x is a sub-term of B.

So all of this is fancy, we have types that can extend types. However, one might ask, why construct such a logical system?

Given this system, we know that if there is a constructive proof that an object exists, that constructive proof may be used as an algorithm for generating an example of that object (relation to Curry–Howard correspondence between proofs and algorithms). One reason that this particular aspect of intuitionistic logic is so valuable is that it enables the usage of proof assistants, i.e. Coq.

So, have fun and make sure your types match! 🙂

Hierarchy of logical systems

This post is a generalization to one of my previous posts, Abstractions with Set Theory.

At its core, mathematical logic deals with mathematical concepts expressed using formal logical systems.

These systems, though they differ in many details, share the common property of considering only expressions in a fixed formal language.

Here’s the hierarchy of these logical systems:

Propositional logic
This branch of logic is concerned with the study of propositions (whether they are True or False) that are formed by other propositions with the use of logical connectives.

The most basic logical connectives are AND $\land$ , OR $\lor$ , and NOT $\lnot$ .

The connectives are commutative. Here are their values (T stands for True, F for false):
$T \land T = T$ , everything else is F.
$F \lor F = F$ , everything else is T.
$\lnot F = T$ , $\lnot T = F$ .

We can also use variables to represent statements.

For example, we can say “a = Salad is organic”, and thus a is a True statement.
Another example is “a = Rock is organic”, and thus a is a False statement.
“a = Hi there!” is neither a True nor a False statement.

Propositional logic defines an argument to be a list of propositions. For example, given the two propositions $A \lor B, \lnot B$ we can conclude A.

An argument is valid iff for every row where the propositions are True, the conclusion is also True.

An easy way to check the validity of this argument is to use the definitions above and draw a table with all possible values of A and B.
```
A	B	A OR B	NOT B
F	F	F		T
F	T	T		F
T	F	T		T
T	T	T		F
```
In this case, the row where all of the propositions are true is 3. We see that the conclusion A is also True, so the argument is valid and will hold for any value we put in place of A or B.

Besides using tables to check for values, we can also construct proofs given a natural deduction system.

We can use the system’s rules to either prove or disprove a statement.
First-order logic
This logical system extends propositional logic by additionally covering predicates and quantifiers.

A predicate P(x) takes as an input x, and produces either True or False. For example, having “P(x) = x is a organic”, then P(Salad) is True, but P(Rock) is False.

Note that in set theory, P would be a subset of a relation, i.e. $P \subseteq A \times \{ True, False \}$ . When working with other systems we need to be careful, as this is not the case with FOL. In the case of FOL, we have P(Salad) = True, P(Rock) = False, etc as atomic statements (i.e. they cannot be broken down into smaller statements).

There are two quantifiers introduced: forall (universal quantifier) $\forall$ and exists (existential quantifier) $\exists$ .

In the following example the universal quantifier says that the predicate will hold for all possible choices of x: $\forall x P(x)$
In the following example the existential quantifier says that the predicate will hold for at least one choice of x: $\exists x P(x)$
Second-order logic, …, Higher-order (nth-order) logic
First-order logic quantifies only variables that range over individuals; second-order logic, in addition, also quantifies over sets; third-order logic also quantifies over sets of sets, and so on.

For example, Peano’s axioms (the system that defines natural numbers) are a mathematical concept expressed using a combination of first-order and second-order logic.

This concept consists of a set of axioms for the natural numbers, and all of them (except the ninth, induction axiom) are statements in first-order logic.

The base axioms can be augmented with arithmetical operations of addition, multiplication and the order relation, which can also be defined using first-order axioms.

The axiom of induction is in second-order, since it quantifies over predicates.

In my next post we’ll have a look at intuitionistic logic, a special logical system based on type theory.