Formal Verification of Trisection in Exact Real Computation using the Coq Proof Assistant
Supplement to MACIS 2017
contribution On Formal Verification in Exact Real Computation:
Section 3.3 there introduces an algorithm in Exact Real Computation;
Section 6 presents Hoare Triples over a two-sorted structure to formally prove its correctness;
and Section 7 describes a formal verification, using the Coq Proof Assistant,
of five implications that connect the aforementioned Hoare Triples
via precondition strengthening and postcondition weakening.
The present web page provides in three files the full source code
for this formal verification:
written by Sewon Park,
KAIST, School of Computing
with assistence and advice from Prof. Gyesik Lee,
Hankyong National University.
Organisation
In order to formally prove the aforementioned five implications in Coq, we have
- formalized in the file
iota.v
the 'precision embedding'
ι:ℤ∋p→2^{p}∈ℝ
and its properties;
- formalized in the file
core.v
some facts about continuous real functions with a unique and simple root,
to be used in the main proof;
- and, finally, in the main file
trisection.v
proved the five implications.
Verifying proofs (compiling)
The proofs of the five implications employed in our Hoare-style
deduction of correctness of trisection is contained in
trisection.v.
You may simply
- download and compile first iota.v
(producing iota.vo),
- then core.v
(producing core.vo),
- then download
trisection.v
and compile each proof line by line
(possibly after adjusting the path to the aforementioned .vo files).
Additional remarks for Coq novices
You can see various tags in the files. We explain informally the meaning of each tag:
- Require Import imports a library (a pack of definitions and lemmas) which provides
already proven rules of inference and definitions; e.g., Coq.Reals provides axiomatized real
numbers and their axioms and proven rule of inferences.
- Open Scope R_scope declares that the file uses 'Reals' library's naming space.
- Parameter defines universally quantified variables within the section they are declared;
Hence, putting Parameter f : R -> R in the beginning saves us from to start every statement
with forall f : R -> R, Q f; it is enough to write simply Q f
(where Q is some predicate).
- Lemma is a logical statement; the five Lemmas in the file
trisection.v are the five implications which
need to be proven to constitute formal verification of Trisection.
- Proof ... Qed are a block which forms a formal proof of its above Lemma;
It is basically a sequence of axioms and rules of inference, so-called tactics.
Compiling a proof means checking validity of application of each tactic that is used;
for an instance, compiling a line of commutativeeal checks whether an axiom of
commutativity of real numbers can be applied in the current context.
Also, the compiler would reject Qed when the lemma is not solved yet. Hence, compiling the
file is verifying formal proofs of the file; compiler not complaining with a sequence of
tactics ended by Qed. means that the sequence is forms a proof of the lemma.