# My Weblog

## List with concatenation operation is monoid.

We will try to prove in Coq that list with concatenation ( ++ ) is monoid. Monoid is set S with binary operation $\bullet$ with following properties.
1). Closure.

$\forall a, b \in S,\hspace{1 mm} \exists c \in S \hspace{1 mm}such \hspace{1 mm}that\hspace{1 mm} c = a \bullet b.$

2). Associativity.

$\forall a, b, c \in S \hspace{1 mm} then \hspace{1 mm} a \bullet ( b \bullet c ) = ( a \bullet b) \bullet c$

3) Identity.

$\exists e \in S \hspace{1 mm} such \hspace{1 mm} that \hspace{1 mm} \forall a \in S,\hspace{1 mm} e \bullet a = a \bullet e = a$

Proof in Coq.

Require Import List.

Theorem Closure : forall ( X : Type ) ( l1 l2 : list X ) , exists ( l3 : list X ),
l1 ++ l2 = l3.
Proof.
intros X l1 l2. exists ( l1 ++ l2) .
reflexivity.
Qed.

Theorem Association : forall ( X : Type ) ( l1 l2 l3 : list X ) ,
l1 ++ ( l2 ++ l3 ) = ( l1 ++  l2 ) ++ l3.
Proof.
intros X l1 l2 l3.
simpl. rewrite -> app_assoc_reverse. reflexivity.
Qed.

Theorem Existence_identity_left : forall ( X : Type ) ( l : list X ), exists e,
e ++ l = l.
Proof.
intros X l. exists nil. simpl.
reflexivity.
Qed.

Theorem Existence_identify_right : forall ( X : Type ) ( l : list X ) , exists e,
l ++ e = l.
Proof.
intros X l. exists nil.
apply app_nil_r.
Qed.



We don’t need to prove the closure property because all the functions in Coq is total. See thec discussion . Source code on github[1] and other proofs from software foundation[2].
[1] https://github.com/mukeshtiwari/Coq/blob/master/Monoid.v
[2] https://github.com/mukeshtiwari/Coq/blob/master/Poly.v

September 10, 2014

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

August 22, 2014