Theorem Proving & Program Verification by Coq

Introduction

If we say that programming is through writing code, the combination of simple functions & components to realize the complex assembly, then proof is the combination of some simple proof steps to make the complex proof. Theorem proving tools like Coq & Isabelle allow us to describe mathematical definitions & mathematical proofs in the form of codes.

We use Coq here: Coq-Release@github.com. The online version of Coq is also able to be used. Here is a link to the official Coq documentation for review & reference, in order for readers’ better reading. This article only guarantees that readers can establish a preliminary understanding of formal theorem proving & program verification. If you’re looking for a book with a richer and more substantial introduction to get familiar with Coq, I recommend you read the “Software Foundations Vol.1: Logical Foundations” at least.

1. Proof Equation

Equation is one of the base of math, we started with a proof about group theory.

Module Group.
Class GroupOperator: Type := {
    tote_set: Type;
    zero: tote_set;
    add: tote_set -> tote_set -> tote_set;
    neg: tote_set -> tote_set;
}.

Notation "0" := (zero).
Notation "a + b" := (add a b).
Notation "- a" := (neg a).

Check forall (G: GroupOperator) (x y: tote_set), x + y = y + x.

First, we have to define which operations a group contains. We can write without these coq-reserve words such as Type or Class here. To define a group operation, you can define the set tote_set first, & then it should contain the unit element zero, the binary operation add & an inverse operation neg.

The key word Notation in coq helps describe the related properties by using refiner words.

At the lastest line, the order Check can be understood as asking computer to check if the expression is syntactically legal. The point is that it just does in syntax but not about the proof.

Class GroupProperties (G: GroupOperator): Prop := {
    associate: forall (a b c: tote_set), (a + b) + c = a + (b + c);
    left_unit_clear: forall (a: tote_set), 0 + a = a;
    left_inverstion_clear: forall (a: tote_set), (- a) + a = 0;
}.

We list 3 laws of the group, clearing left unit, clearing inverstion & associative law. It ’s useful to the next part.

1.1 Proving Right Inverse Property

Theorem right_inverstion_clear {G: GroupOperator} {GP: GroupProperties G}: 
(forall (a: tote_set), a + (- a) = 0).

The things after Theorem here needed to proof by us, Try to do!

Require Import Setoid.
Proof.
  intros a.
  rewrite <- (left_unit_clear (a + (- a))).
  rewrite <- (left_inverstion_clear (- a)) at 1.
  rewrite associate.
  rewrite <- (associate (- a)).
  rewrite left_inverstion_clear.
  rewrite left_unit_clear.
  rewrite left_inverstion_clear.
  reflexivity.
Qed.

Here is the classical proof in group theory, that’s derived from the two properties of left unit element & left inverse element, to right inverse element.

We use intros to get the theorem a + (- a) = 0 that awaits to be prooved at line 1. Then use the keyword rewrite to convert the existing properties of this equation, the arrow to the left is <- means to use properties to transform a certain item of the equation from left to right, the -> is opposite operation, followed by the parentheses after the property name Content is used to match corresponding items. If you want to operate only on the matching item at a certain position, you can use the keyword at; if you think that Coq will not cause ambiguity with a certain instruction, you can even ignore the content of the parentheses. Finally, the reflexivity. says that the equation is reflexive, & now the equation is exactly the same on both sides, so it’s all of the proof. The Qed. is the end of the Proof. above. We have done all the work of this stupid theorem.

If you have doubts about a part of this part of the code, please leave it to CoqIDE to run this proof, it will be intuitive to observe the equation change in the goal window on the right. Use the shortcut keys “Ctrl + $\uparrow$” and “Ctrl + $\downarrow$” to quickly switch the row up or down.

1.2 Proving Right Unit Property

Based on the fundamental properties & the results we have proved, it is easy to prove the right unit property corresponding to the left unit property. The right unit property can be expressed as the a + 0 = a.

Theorem right_unit_clear {G: GroupOperator} {GP: GroupProperties G}:
  forall (a: tote_set), a + 0 = a.
Proof.
  intros.
  rewrite <- (left_inverstion_clear (a)).
  rewrite <- associate, right_inverstion_clear, left_unit_clear.
  reflexivity.
Qed.

So it was proven that right unit property. It is possible to write multiple commands together in Coq as in the above code.

1.3 Proving Double Negation Property

Next prove the double negation signelimination property.

Theorem double_negation {G: GroupOperator} {GP: GroupProperties G}:
  forall (a: tote_set), - - a = a.
Proof.
  intros.
  rewrite <- (left_unit_clear (--a)).
  rewrite <- (right_inverstion_clear (a)).
  rewrite associate, right_inverstion_clear, right_unit_clear.
  reflexivity.
Qed.

2. Inductive Type, Recursive Definitions and Inductive proof

这几天不写了，待续。。。。

$$ \sum_{\sum_{\sum_{114514}^{1919810}}^{\sum_{114514}^{1919810}}}^{\sum_{\sum_{114514}^{1919810}}^{\sum_{114514}^{1919810}}} $$