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.


In order to formally prove the aforementioned five implications in Coq, we have
  1. formalized in the file iota.v the 'precision embedding'   ι:ℤ∋p→2p∈ℝ   and its properties;
  2. 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;
  3. 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
  1. download and compile first iota.v (producing iota.vo),
  2. then core.v (producing core.vo),
  3. 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:
  1. 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.
  2. Open Scope R_scope declares that the file uses 'Reals' library's naming space.
  3. 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).
  4. 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.
  5. 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.