# My Weblog

## Proving Theorems in Coq

I recently started learning Coq from Software Foundations and I must say it’s highly addictive. Coq is theorem prover. When I started learning, the very first thing came to my mind is how is it possible for computer to prove theorem ?  In mathematics, a theorem is a statement that has been proven on the basis of previously established statements, such as other theorems—and generally accepted statements, such as axioms[1]. From Coq’Art, Page 3 “The Coq system is not just another programming language. It actually makes it possible to express assertion about the values being manipulated. These value may range over mathematical objects or over programs”. Great so let me write a program and prove some properties using Coq.  The definition of Boolean and couple of functions over boolean

```Inductive bool : Type :=
| true : bool
| false : bool.

Definition negb ( b : bool ) : bool :=
match b with
| true => false
| false => true
end.

Definition andb ( x : bool ) ( y : bool ) : bool :=
match x with
| true => y
| false => false
end.

Definition orb ( x : bool ) ( y : bool ) : bool :=
match x with
| false => y
| true => true
end.

Definition xorb ( x : bool ) ( y : bool ) : bool :=
match x, y with
| true, true => false
| false, false => false
| _, _  => true
end.

```

Once we have some definitions, We can try to assert some properties about these functions. One assertion about XOR If output of xor is false it means both the inputs have same value. Lets write this theorem in Coq

```Theorem xorb_equalleft : forall a b : bool, xorb a b = false -> a = b.
```

When Coq process this theorem, goal looks like this

```1 subgoals, subgoal 1 (ID 97)

============================
forall a b : bool, xorb a b = false -> a = b

```

and proof of the theorem is

```Proof.
intros a b H. destruct a. destruct b.
reflexivity. discriminate.
destruct b. discriminate. reflexivity.
Qed.
```

Once the proof is complete, we will get the message from Coq “No more subgoals. xorb_equalleft is defined”. Lets define one more assertion about AND function. If the output of andb function is true it means both inputs are true.

```Theorem andbc_true : forall b c : bool, andb b c = true -> b = true /\ c = true.
```

Coq proof of this assertion is

```Proof.
intros b c. destruct b.
Case "b = true".
simpl. intros H. split.
reflexivity.
rewrite <- H.
reflexivity.
Case "b = false".
simpl. intros H.
discriminate.
Qed.
```

We have proved both the theorems but what is destruct, reflexivity, split and discriminate ? These are tactics and Coq is interactive theorem prover so you have to guide it towards goal using tactics. Source code on github[2]. Famous Theorems proved in Coq[3]. Certified Dependent type programming[4]

Advertisements

August 22, 2014