Quotients are crucial in mathematical practice, and it is a shame that they
are not available in Coq's standard library. There was a recent discussion on
the Coq GitHub page on
this issue and the consequences of implementing quotients like Lean does, where the eliminator for
function types has a reduction rule that breaks pleasant metatheoretic
properties such as subject reduction.
In this post, we are going to define quotients in Coq with three standard
axioms:
Functional extensionality
Propositional extensionality
Constructive definite description (also known as the axiom of unique choice)
Check @functional_extensionality_dep :
∀ AB (fg : ∀ x : A, Bx),
(∀ x : A, fx = gx) → f = g.
Check @constructive_definite_description :
∀ AP, (exists! x : A, Px) → {x : A | Px}.
As far as axioms go, these three are relatively harmless. In particular,
they are valid in any elementary
topos, which are generally regarded as a good universe for doing
constructive, higher-order reasoning. (Naturally, adding axioms in type theory
does not come for free: since they have no useful reduction behavior, our
quotients won't compute.)
SectionQuotient.
We define the quotient of T by an equivalence relation R as usual: it is
the type of equivalence classes of R.
The projection into the quotient is given by the Quot constructor below,
which maps x to its equivalence class Rx. This definition satisfies the
usual properties: Quotx=Quoty if and only if Rxy. The "if" direction
requires the principle of proof irrelevance, which is a consequence of
propositional extensionality.
Unique choice comes into play when defining the elimination principles for
the quotient. In its usual non-dependent form, the principle says that we can
lift a function f:T→S to another function quot→S provided that f is
constant on equivalence classes. We define a more general dependently typed
version, which allows in particular to prove a property Sq by proving that S(Quotx) holds for any x. The statement of the compatibility condition for
f is a bit complicated because it needs to equate terms of different types S(Quotx) and S(Quoty), which requires us to transport the left-hand side
along the equivalence Rxy.
SectionElim.
DefinitioncastAB (e : A = B) : A → B := matchewitherefl => idend.
We begin with an auxiliary result that uniquely characterizes the result of
applying the eliminator to an element q:quot. Thanks to unique choice, this
allows us to define the eliminator as a function quot_rect.
Lemmaquot_rect_subproof (q : quot) : exists! a : Sq, ∃ x (exq : Quotx = q), a = cast (congr1Sexq) (fx). Proof. case: (Quot_invq)=> x -> {q}. exists (fx); split=> [|a]; firstbyexistsx, erefl. case=> y [eyx -> {a}]. byrewrite (proof_irrelevance_eyx (eq_Quot (Quot_injeyx))) fP. Qed.
Hillel Wayne posted a challenge
to find out whether functional programs are really easier to verify than
imperative ones, as some claim. There were three problems, and I am posting Coq
solutions here (two of them by myself).
Padding
The first challenge was to prove the correctness of a padding function. Given a
padding character c, a length n and a sequence s, left_padcns should
pad s with c on the left until its size reaches n. If the original string
is larger than n, the function should do nothing. My implementation is
similar to other solutions on the web, and reuses functions and lemmas available
in the Math Comp libraries.
ImplicitTypes (c : char) (in : nat) (s : seqchar).
Definitionleft_padcns := nseq (n - sizes) c ++ s.
The call to nseq creates a constant sequence with the number of cs that
needs to be added, and appends that sequence to s. Note that subtraction is
truncated: n-sizes is equal to 0 when n<=sizes.
As the specification for left_pad, I am taking the properties that were
verified in the original
solution in Hillel's post, which was written in Dafny. My proofs are not
automated like in Dafny, but still fairly easy. (The statements are slightly
different because they use the nth function to index into a sequence, which
requires a default element to return when the index overflows.)
Interestingly, these properties completely characterize the result of
left_pad: any function f that satisfies the same specification must produce
the same output.
Lemmaleft_padPf :
(forallcns, size (fcns) = maxnn (sizes)) ->
(forallcnsi, i < n - sizes -> nthc (fcns) i = c) ->
(forallcnsi, nthc (fcns) (n - sizes + i) = nthcsi) -> forallcns, fcns = left_padcns.
Some fans of functional programming claim that it obviates the need for
verification, since the code serves as its own specification. Though exaggerate
(as we will see in the last problem), the claim does have a certain appeal: the
definition of left_pad is shorter and more direct than the specification that
we proved.
Unique
The second problem of the challenge asked to remove all duplicate elements from
a sequence. I decided not to include a solution of my own here, since the Math
Comp library already
provides a function undup that does this. We had to show that the set of
elements in its output is the same as in its input, and that no element occurs
twice, properties that are both proved in Math Comp (mem_undup and
undup_uniq). Hillel wrote that imperative programs had an advantage for this
problem because of its symmetry. I am not sure what was meant by that, but the
Dafny and the Coq proofs are comparable in terms of complexity. (To be fair,
Dafny has better automation than Coq, but this has probably little to do with
being functional or imperative: other functional provers fare better than Coq in
this respect as well.)
Fulcrum
The last problem was also the most challenging. The goal was to compute the
fulcrum of a sequence of integers s, which is defined as the index i that
minimizes the quantity fvsi shown below in absolute value.
ImplicitTypes (s : seqint) (n : int).
Definitionfvsi :=
\sum_(0 <= l < i) s`_l - \sum_(i <= l < sizes) s`_l.
The simplest way out would be to compute fvsi for all indices i and
return the index that yields the smallest value. Instead of writing this
program ourselves, we can just reuse the argmin function available in Math
Comp.
Unfortunately, this naive implementation runs in quadratic time, and the
problem asked for a linear solution. We can do better by folding over s and
computing the values of fvsi incrementally. With a left fold, we can
compute the fulcrum with four auxiliary variables defined in the state type
below, without the need for extra stack space. (This is a bit more efficient
than the original solution,
which had to store two sequences of partial sums.)
Recordstate := State { curr_i : nat; (* The current position in the list *) best_i : nat; (* The best fulcrum found so far *) curr : int; (* = fv s curr_i *) best : int; (* = fv s best_i *)
}.
On each iteration, the fulcrum_body function updates the state st given
n, the current element of the sequence. The main function, fulcrum, just
needs to provide a suitable initial state and return the final value of
best_i.
Definitionfulcrum_bodystn := letcurr' := n *+ 2 + st.(curr) in letcurr_i' := st.(curr_i).+1 in letbest' := if `|curr'| < `|st.(best)| thencurr'elsest.(best) in letbest_i' := if `|curr'| < `|st.(best)| thencurr_i'elsest.(best_i) in Statecurr_i'best_i'curr'best'.
To verify fulcrum, we first prove a lemma about foldl. It says that we
can prove that some property I holds of the final loop state by showing that
it holds of the initial state x0 and that it is preserved on every iteration
in other words, that I is a loop invariant. The property is
parameterized by a "ghost variable" i, which counts the number of iterations
performed.
LemmafoldlPTSf (s : seqT) x0 (I : nat -> S -> Prop) : I 0%Nx0 ->
(forallixa, (i < sizes)%N -> Iix -> Ii.+1 (fx (nthasi))) -> I (sizes) (foldlfx0s).
We complete the proof by instantiating foldlP with the fulcrum_inv
predicate below. This predicate ensures, among other things, that best_i
holds the fulcrum for the first i positions of the sequence s. Hence, when
the loop terminates, we know that best_i is the fulcrum for all of s.
So, is functional really better than imperative for verification? Though I am a
fan of functional languages, I will not attempt to offer a definitive answer.
It is true that simple programs such as left_pad are often as good (or better)
than their specifications, but some of those would be inefficient in practice,
and fast implementations such as fulcrum might be tricky to verify.
As mentioned in Hillel's post, the main issue when verifying imperative code is
aliasing: we must argue that every call preserves the assumptions made in other
parts of the code, something that comes for free with functional programming.
However, if a program only modifies local state (like the Dafny solutions did),
reasoning about this kind of interference becomes much more manageable.
Of course, nothing prevents us from combining the benefits of functional and
imperative programming. We can implement an efficient algorithm using mutable
state and verify it against a specification that mixes logic and pure functions.
Indeed, that is the strategy followed by the Dafny solution, and many frameworks
for verifying imperative code only allow pure functions in specifications.
Moreover, it is possible to define imperative languages within Coq and use the
logic to verify programs in this language; this is the essence of frameworks
such as VST or Iris.
Convincing Coq that a function terminates can be frustrating. When modeling
programming languages with subtyping, in particular, you might run into
situations where the contravariance of function types forces you to swap the
arguments of a recursive function. Coq does not know how to handle this
recursion pattern and rejects the definition. This post presents a technique
for dealing with such cases.
Suppose that we want to model a programming language with the following types:
Inductivetype :=
| Top(* Any value whatsoever, akin to Object in Java or Ruby *)
| Int
| Arrow (TS : type) (* Functions from T to S *).
Our language comes with a subtyping relation T<:S that tells when it
is safe to use elements of T in a context that expects elements of S. Its
definition is given below as an inductive declaration.
Inductivesubtype : type -> type -> Prop :=
| STTopT
: T <: Top
Since Top contains arbitrary values, it makes sense for it to be a
supertype of every other type in the language. Things get more interesting for
functions, as subtyping goes in opposite directions for arguments and results;
in common jargon, we say that subtyping treats arguments contravariantly and
results covariantly. If arguments worked covariantly, any function f of
type (Int→Int)→Int would also have the type Top→Int, since Int→Int<:Top. Thus, it would be possible to apply f to an Int, which has no
reason to be safe if f expects a function argument.
We would like to show that subtyping is decidable by expressing this relation as
a boolean function. Its definition is not difficult in principle, but the naive
attempt is rejected:
What happened? Recursive functions in Coq are always defined with respect to
a principal argument. In this case, the argument was marked as T using the
struct keyword, but it can usually be inferred by Coq automatically. For the
definition to be valid, all the recursive calls must be performed on principal
arguments that are subterms of the original principal argument. However, one of
the calls to subtypeb swaps its two arguments, leading to the above error
message.
Coq provides well-founded recursion to circumvent this rigid check, which
allows recursive calls whenever the arguments decrease according to a suitable
relation. In the case of subtypeb, for instance, we could show termination by
proving that the combined sizes of the two arguments decrease on every call.
However, there is a more direct route in this case: it suffices to add a flag to
the function to specify if we are computing subtyping in the correct or opposite
order. If we flip the flag on the first call, we do not need to swap the
arguments.
Fixpointsubtypeb_genbTS := matchT, Swith
| Top, Top => true
| Top, _ => ~~ b
| _ , Top => b
| Int, Int => true
| T1 ⟶ S1, T2 ⟶ S2 => subtypeb_gen (~~ b) T1T2 && subtypeb_genbS1S2
| _, _ => false end.
Finally, we can prove that the two definitions are equivalent using the
reflect predicate of Ssreflect. Showing that the inductive formulation
implies the boolean one is easy: we just proceed by induction on the relation.
Proving the converse is a bit more subtle, as it requires generalizing the
statement with subtypeb_gen.
Robert Rand and Anton Trunov proposed an alternative approach based on mutual
recursion, which I've included here for completeness. Notice how the two
recursive functions have different recursive arguments.