My Weblog

Blog about programming and math

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

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

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

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

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

intros a b H. destruct a. destruct b.
reflexivity. discriminate.
destruct b. discriminate. reflexivity.

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

intros b c. destruct b.
Case "b = true".
  simpl. intros H. split.
  rewrite <- H.
Case "b = false".
  simpl. intros H.

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]



August 22, 2014 - Posted by | Programming | , ,

No comments yet.

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: