Search code examples
functional-programmingcoqverification

Coq verification of factorial program through two implementations

I am newbie to coq and I am trying to verify the functionality of factorial program.

From my understanding, what I should do is to follow the standard Hoare Logic paradigm, start from the precondition, figure the loop invariant, and reason the postcondition. Something like this:

{{ X = m }} 
{{  FOL 1 }}
Y ::= 1;;
{{  FOL 2   }}
WHILE !(X = 0) DO  
    {{ FOL 3    }}
    Y ::= Y * X;;
    {{ FOL 4   }}
    X ::= X - 1
   {{ FOL 5  }}
END
{{ FOL 6 }}
{{ Y = m! }}

Here the FOL standards from "first order logic".

However, to my surprise, it seems that when verifying the factorial program with coq, the common way is to define the following two functions fact and fact_tr:

Fixpoint fact (n:nat) :=
match n with
| 0 => 1
| S k => n * (fact k)
end.

Fixpoint fact_tr_acc (n:nat) (acc:nat) :=
match n with
| 0 => acc
| S k => fact_tr_acc k (n * acc)
end.

Definition fact_tr (n:nat) :=
fact_tr_acc n 1.

and future proof the equivalence of these two functions:

Theorem fact_tr_correct : forall n:nat,
fact_tr n = fact n.

I learned such approach from here and here.

So here is my question:

  1. Can someone illustrate the motivation behind such "equality-based" verification approach? Are they still conceptually similar to the standard Hoare Logic based reasoning?

  2. Still, can I use coq to verify the correctness of factorial program following the "standard" Hoare logic based approach? Say by specifying the precondition, postcondition and inductively reasoning the whole program.

Solution

  • Notice that the underlying language of Coq's programs belongs to the family of (dependently-typed) functional languages, not imperative ones. Roughly, there is no state and statements, only expressions.

    The motivation behind "equality-based" approach is that simple functional programs can serve as specifications. And fact is certainly simple -- it is Coq speak for the definition of factorial via its fundamental recurrence relation. In other words, fact is a reference implementation, i.e. in this case it is an obviously correct implementation. While fact_tr_acc is an optimized one, whose correctness with respect to the specification we wish to establish.

    Yes, you can still verify the correctness of the imperative factorial program. E.g. the Software Foundations series shows how to encode imperative programs in Coq and verify their correctness using Hoare logic. See, in particular, the factorial exercise.