Where the Coq lives

| Comments GitHub

Quotients in Coq

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 :
  ∀ A B (f g : ∀ x : A, B x),
    (∀ x : A, f x = g x) → f = g.

Check @propositional_extensionality :
  ∀ P Q, (PQ) → P = Q.

Check @constructive_definite_description :
  ∀ A P, (exists! x : A, P x) → {x : A | P x}.

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.)

Section Quotient.

We define the quotient of T by an equivalence relation R as usual: it is the type of equivalence classes of R.

Context (T : Type) (R : relation T) (RP : Equivalence R).

Record quot := Quot_ {
  quot_class : TProp;
  quot_classP : ∃ x, quot_class = R x;

The projection into the quotient is given by the Quot constructor below, which maps x to its equivalence class R x. This definition satisfies the usual properties: Quot x = Quot y if and only if R x y. The "if" direction requires the principle of proof irrelevance, which is a consequence of propositional extensionality.

Definition Quot (x : T) : quot :=
  @Quot_ (R x) (ex_intro _ x erefl).

Lemma Quot_inj x y : Quot x = Quot yR x y.
move=> e; rewrite -[R x y]/(quot_class (Quot x) y) e //=; reflexivity.

Lemma eq_Quot x y : R x yQuot x = Quot y.
move=> e; rewrite /Quot; move: (ex_intro _ y _).
suff ->: R y = R x.
  move=> ?; congr Quot_; exact: proof_irrelevance.
apply: functional_extensionality=> z.
apply: propositional_extensionality.
by rewrite /= e.

We can also show that Quot is surjective by extracting the witness in the existential.
Lemma Quot_inv q : ∃ x, q = Quot x.
case: q=> [P [x xP]]; exists x; move: (ex_intro _ _ _).
rewrite xP=> e; congr Quot_; exact: proof_irrelevance.

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 S q by proving that S (Quot x) 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 (Quot x) and S (Quot y), which requires us to transport the left-hand side along the equivalence R x y.

Section Elim.

Definition cast A B (e : A = B) : AB :=
  match e with erefl => id end.

Context (S : quotType) (f : ∀ x, S (Quot x)).
Context (fP : ∀ x y (exy : R x y), cast (congr1 S (eq_Quot exy)) (f x) = f y).

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.

Lemma quot_rect_subproof (q : quot) :
  exists! a : S q, ∃ x (exq : Quot x = q), a = cast (congr1 S exq) (f x).
case: (Quot_inv q)=> x -> {q}.
exists (f x); split=> [|a]; first by exists x, erefl.
case=> y [eyx -> {a}].
by rewrite (proof_irrelevance _ eyx (eq_Quot (Quot_inj eyx))) fP.

Definition quot_rect q : S q :=
  sval (constructive_definite_description _ (quot_rect_subproof q)).

Lemma quot_rectE x : quot_rect (Quot x) = f x.
rewrite /quot_rect.
case: constructive_definite_description=> _ [y [eyx /= ->]].
by rewrite (proof_irrelevance _ eyx (eq_Quot (Quot_inj eyx))) fP.

End Elim.

In the non-dependent case, the compatibility condition acquires its usual form.

Section Rec.

Context S (f : TS) (fP : ∀ x y, R x yf x = f y).

Definition congr1CE (A B : Type) (b : B) x y (e : x = y) :
  congr1 (λ _ : A, b) e = erefl :=
  match e with erefl => erefl end.

Definition quot_rec : quot -> S :=
  @quot_rect (λ _, S) f
    (λ x y exy, etrans
      (congr1 (λ p, cast p (f x)) (congr1CE S (eq_Quot exy)))
      (fP exy)).

Lemma quot_recE x : quot_rec (Quot x) = f x.
Proof. by rewrite /quot_rec quot_rectE. Qed.

End Rec.

End Quotient.

| Comments GitHub

A verification challenge

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).


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_pad c n s 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.
Implicit Types (c : char) (i n : nat) (s : seq char).

Definition left_pad c n s := nseq (n - size s) 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 - size s is equal to 0 when n <= size s.
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.)

Lemma left_pad1 c n s : size (left_pad c n s) = maxn n (size s).
by rewrite /left_pad size_cat size_nseq maxnC maxnE [RHS]addnC.

Lemma left_pad2 c n s i :
  i < n - size s ->
  nth c (left_pad c n s) i = c.
move=> bound.
by rewrite /left_pad nth_cat size_nseq bound nth_nseq bound.

Lemma left_pad3 c n s i :
  nth c (left_pad c n s) (n - size s + i) = nth c s i.
by rewrite /left_pad nth_cat size_nseq ltnNge leq_addr /= addKn.

Interestingly, these properties completely characterize the result of left_pad: any function f that satisfies the same specification must produce the same output.

Lemma left_padP f :
 (forall c n s, size (f c n s) = maxn n (size s)) ->
 (forall c n s i, i < n - size s -> nth c (f c n s) i = c) ->
 (forall c n s i, nth c (f c n s) (n - size s + i) = nth c s i) ->
  forall c n s, f c n s = left_pad c n s.
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.


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.)


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 fv s i shown below in absolute value.
Implicit Types (s : seq int) (n : int).

Definition fv s i :=
  \sum_(0 <= l < i) s`_l - \sum_(i <= l < size s) s`_l.

Definition is_fulcrum s i := forall j, `|fv s i| <= `|fv s j|.

The simplest way out would be to compute fv s i for all indices i and return the index that yields the smallest value. Instead of writing this program ourselves, we can just reuse the arg min function available in Math Comp.

Definition fulcrum_naive s :=
  [arg minr_(i < ord0 : 'I_(size s).+1) `|fv s i|].

Lemma fvE s i :
  fv s i = (\sum_(0 <= l < i) s`_l) *+ 2 - \sum_(0 <= l < size s) s`_l.

Lemma fv_overflow s i : fv s i = fv s (minn i (size s)).

Lemma fulcrum_naiveP s : is_fulcrum s (fulcrum_naive s).
rewrite /fulcrum_naive; case: arg_minrP=> //= i _ iP j.
move/(_ (inord (minn j (size s))) erefl): iP.
rewrite (_ : fv s (inord _) = fv s j) //= [RHS]fv_overflow.
by rewrite inordK ?ltnS ?geq_minr //.

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 fv s i 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.)

Record state := 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.

Definition fulcrum_body st n :=
  let curr' := n *+ 2 + st.(curr) in
  let curr_i' := st.(curr_i).+1 in
  let best' := if `|curr'| < `|st.(best)| then curr' else st.(best) in
  let best_i' := if `|curr'| < `|st.(best)| then curr_i' else st.(best_i) in
  State curr_i' best_i' curr' best'.

Definition fulcrum s :=
  let k := - foldl +%R 0 s in
  (foldl fulcrum_body (State 0 0 k k) s).(best_i).

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.

Lemma foldlP T S f (s : seq T) x0 (I : nat -> S -> Prop) :
  I 0%N x0 ->
  (forall i x a, (i < size s)%N -> I i x -> I i.+1 (f x (nth a s i))) ->
  I (size s) (foldl f x0 s).

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.

Variant fulcrum_inv s i st : Prop :=
| FlucrumInv of
 (st.(best_i) <= i)%N &
  st.(curr_i) = i &
  st.(best) = fv s st.(best_i) &
  st.(curr) = fv s i &
  (forall j, (j <= i)%N -> `|fv s st.(best_i)| <= `|fv s j|).

Lemma fulcrumP s : is_fulcrum s (fulcrum s).
rewrite /fulcrum; have ->: - foldl +%R 0 s = fv s 0.
  by rewrite /fv big_geq // (foldl_idx [law of +%R]) (big_nth 0) add0r.
set st := foldl _ _ _; suff: fulcrum_inv s (size s) st.
  case=> ???? iP j; rewrite [fv s j]fv_overflow; apply: iP.
  exact: geq_minr.
apply: foldlP=> {st}; first by split=> //=; case.
move=> i [_ best_i _ _] a iP [/= bP -> -> -> inv].
rewrite (set_nth_default 0 a iP) {a}.
have e: fv s i.+1 = s`_i *+ 2 + fv s i.
  by rewrite !fvE big_nat_recr //= [_ + s`_i]addrC mulrnDl addrA.
split=> //=; do 1?[by case: ifP; rewrite // -ltnS ltnW].
move=> j; case: ltngtP=> // [j_i|<-] _.
  case: ifP=> [|_]; last exact: inv.
  rewrite -e=> /ltrW {}iP; apply: ler_trans iP _; exact: inv.
by case: ifP=> //; rewrite -e ltrNge => /negbFE ->.


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.

| Comments GitHub

Contravariance and Recursion

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:

Inductive type :=
| Top (* Any value whatsoever, akin to Object in Java or Ruby *)
| Int
| Arrow (T S : type) (* Functions from T to S *).

Notation "T ⟶ S" := (Arrow T S) (at level 25, right associativity).

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.
Inductive subtype : type -> type -> Prop :=
| STTop T
: T <: Top

| STInt
: Int <: Int

| STArrow T1 T2 S1 S2 of
  T2 <: T1 & S1 <: S2
: T1S1 <: T2S2

where "T <: S" := (subtype T S).

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:

Fail Fixpoint subtypeb T S {struct T} :=
  match T, S with
  | _, Top => true
  | Int, Int => true
  | T1S1, T2S2 => subtypeb T2 T1 && subtypeb S1 S2
  | _, _ => false

Recursive definition of subtypeb is ill-formed.
Recursive call to subtypeb has principal argument equal to "T2"
instead of one of the following variables: "T1" "S1".
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.

Fixpoint subtypeb_gen b T S :=
  match T, S with
  | Top, Top => true
  | Top, _ => ~~ b
  | _ , Top => b
  | Int, Int => true
  | T1S1, T2S2 => subtypeb_gen (~~ b) T1 T2 && subtypeb_gen b S1 S2
  | _, _ => false

Definition subtypeb := subtypeb_gen true.

Notation "T <:? S" := (subtypeb T S) (at level 20, no associativity).

To relate the two definitions of subtyping, we first show that flipping the flag of subtypeb_gen is equivalent to swapping the other arguments.

Lemma subtypeb_genC b T S : subtypeb_gen (~~ b) T S = subtypeb_gen b S T.
by elim: T S b => [| |? IH1 ? IH2] [| |??] //= b; rewrite -?IH1 ?IH2 negbK.

This yields a more convenient equation for subtypeb. (We match on S first to ensure that the RHS is definitionally equal to true when S is Top.)

Lemma subtypebE T S :
  T <:? S =
  match S, T with
  | Top, _ => true
  | Int, Int => true
  | T2S2, T1S1 => T2 <:? T1 && S1 <:? S2
  | _ , _ => false
case: T S=> [| |??] [| |??]; by rewrite /subtypeb //= -(subtypeb_genC false).

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.

Lemma subtypebP T S : reflect (T <: S) (T <:? S).
apply/(iffP idP); last first.
  by elim: T S / => [T| |???? _ IH1 _ IH2] //=; rewrite subtypebE ?IH1 ?IH2.
suffices /(_ true): forall b, subtypeb_gen b T S ->
  subtype (if b then T else S) (if b then S else T) by [].
elim: T S=> [| |T1 IH1 S1 IH2] [| |T2 S2] [] //=;
try case/andP=> /IH1 ? /IH2 ?; by constructor.

Update (August 9, 2019)

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.

Definition body T S := fun subtypeb subtypeb' =>
match T, S with
| _, Top => true
| Int, Int => true
| T1S1, T2S2 => subtypeb' T2 T1 && subtypeb S1 S2
| _, _ => false

Fixpoint subtypeb T S {struct T} := body T S subtypeb subtypeb'
with subtypeb' T S {struct S} := body T S subtypeb' subtypeb.

Notation "T <:? S" := (subtypeb T S) (at level 20, no associativity).

Lemma subtypeb'_subtypeb S T :
(subtypeb' T S = subtypeb T S) * (subtypeb' S T = subtypeb S T).
elim: S T=> [| |Ts IHt Ss IHs] [| | Tt St] //=.
by rewrite !IHt !IHs.

Lemma subtypebP T S : reflect (T <: S) (T <:? S).
apply/(iffP idP); last first.
- by elim: T S / => [[] //| |???? _ IH1 _ IH2] //=; rewrite subtypeb'_subtypeb IH1 IH2.
suffices : (T <:? S -> T <: S) /\ (S <:? T -> S <: T) by case.
elim: S T => [| |T1 IH1 S1 IH2] [| |T2 S2] //=; try by split=>//; constructor.
rewrite !subtypeb'_subtypeb.
split; case/andP.
- by move=> /(proj2 (IH1 _)) subT12 /(proj1 (IH2 _)); constructor.
by move=> /(proj1 (IH1 _)) subT21 /(proj2 (IH2 _)); constructor.