# 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
end.

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

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.
Proof.
by elim: T S b => [| |? IH1 ? IH2] [| |??] //= b; rewrite -?IH1 ?IH2 negbK.
Qed.

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
end.
Proof.
case: T S=> [| |??] [| |??]; by rewrite /subtypeb //= -(subtypeb_genC false).
Qed.

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

### 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
end.

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).
Proof.
elim: S T=> [| |Ts IHt Ss IHs] [| | Tt St] //=.
by rewrite !IHt !IHs.
Qed.

Lemma subtypebP T S : reflect (T <: S) (T <:? S).
Proof.
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.
Qed.

| Comments # Checking for Constructors

When writing tactics, there are situations where it would be useful to know whether a term begins with a constructor. One possibility is to extract the head of the term and use the is_constructor tactic.

Ltac head t :=
match t with
| ?t' _ => head t'
| _ => t
end.

Ltac head_constructor t :=
let t' := head t in is_constructor t'.

Goal True.
(* These calls succeed *)
head_constructor 0.
head_constructor 1.
(* ...but this one fails *)
Fail head_constructor (1 + 1).
(*
The command has indeed failed with message:
In nested Ltac calls to "head_constructor" and "is_constructor", last call failed.
Tactic failure: not a constructor.
*)

Abort.

As of version 8.8, the is_constructor tactic is undocumented, but this should hopefully be fixed soon. Interestingly, we can achieve almost the same effect without is_constructor, by observing that Coq does not reduce a fixpoint unless it is applied to a term that begins with a constructor.

Reset head_constructor.
Ltac head_constructor t :=
match type of t with
| ?T =>
let r := eval cbn in ((fix loop (t' : T) {struct t'} := tt) t) in
match r with tt => idtac end
end.

Goal True.
(* Succeed *)
head_constructor 0.
head_constructor 1.
Abort.

Unlike the previous version, this one reduces the term using cbn before testing it. Thus, the following test succeeds, while the analogous one before failed:

Goal True.
(* Succeeds *)
head_constructor (1 + 1).
Abort.

Update Anton Trunov pointed out that we can emulate the behavior of the first tactic with a fixpoint by adding a flag in the call to eval:

Reset head_constructor.
Ltac head_constructor t :=
match type of t with
| ?T =>
let r := eval cbn fix in ((fix loop (t' : T) {struct t'} := tt) t) in
match r with tt => idtac end
end.

Now, only the outer fixpoint is reduced.

Goal True.
Fail head_constructor (1 + 1).
Abort.

| Comments # Equality in Coq

Coq views truth through the lens of provability. The hypotheses it manipulates are not mere assertions of truth, but formal proofs of the corresponding statements ─ data structures that can be inspected to build other proofs. It is not a coincidence that function types and logical implication use the same notation, A -> B, because proofs of implication in Coq are functions: they take proofs of the precondition as inputs and return a proof of the consequent as the output. Such proofs are written with the same language we use for programming in Coq; tactics are but scripts that build such programs for us. A proof that implication is transitive, for example, amounts to function composition.

Definition implication_is_transitive (A B C : Prop) :
(A -> B) -> (B -> C) -> (A -> C) :=
fun HAB HBC HA => HBC (HAB HA).

Similarly, inductive propositions in Coq behave just like algebraic data types in typical functional programming languages. With pattern matching, we can check which constructor was used in a proof and act accordingly.

Definition or_false_r (A : Prop) : A \/ False -> A :=
fun (H : A \/ False) =>
match H with
| or_introl HA => HA
| or_intror contra => match contra with end
end.

Disjunction \/ is an inductive proposition with two constructors, or_introl and or_intror, whose arguments are proofs of its left and right sides. In other words, a proof of A \/ B is either a proof of A or a proof of B. Falsehood, on the other hand, is an inductive proposition with no constructors. Matching on a proof of False does not require us to consider any cases, thus allowing the expression to have any type we please. This corresponds to the so-called principle of explosion, which asserts that from a contradiction, anything follows.
The idea of viewing proofs as programs is known as the Curry-Howard correspondence. It has been a fruitful source of inspiration for the design of many other logics and programming languages beyond Coq, other noteworthy examples including Agda and Nuprl. I will discuss a particular facet of this correspondence in Coq: the meaning of a proof of equality.

## Defining equality

The Coq standard library defines equality as an indexed inductive proposition. (The familiar x = y syntax is provided by the standard library using Coq's notation mechanism.)

Inductive eq (T : Type) (x : T) : T -> Prop :=
| eq_refl : eq T x x.

This declaration says that the most basic way of showing x = y is when x and y are the "same" term ─ not in the strict sense of syntactic equality, but in the more lenient sense of equality "up to computation" used in Coq's theory. For instance, we can use eq_refl to show that 1 + 1 = 2, because Coq can simplify the left-hand side using the definition of + and arrive at the right-hand side.
To prove interesting facts about equality, we generally use the rewrite tactic, which in turn is implemented by pattern matching. Matching on proofs of equality is more complicated than for typical data types because it is a non-uniform indexed proposition ─ that is, the value of its last argument is not fixed for the whole declaration, but depends on the constructor used. (This non-uniformity is what allows us to put two occurrences of x on the type of eq_refl.)
Concretely, suppose that we have elements x and y of a type T, and a predicate P : T -> Prop. We want to prove that P y holds assuming that x = y and P x hold. This can be done with the following program:

Definition rewriting
(T : Type) (P : T -> Prop) (x y : T) (p : x = y) (H : P x) : P y :=
match p in _ = z return P z with
| eq_refl => H
end.

Compared to common match expressions, this one has two extra clauses. The first, in _ = z, allows us to provide a name to the non-uniform argument of the type of p. The second, return P z, allows us to declare what the return type of the match expression is as a function of z. At the top level, z corresponds to y, which means that the whole match has type P y. When checking each individual branch, however, Coq requires proofs of P z using values of z that correspond to the constructors of that branch. Inside the eq_refl branch, z corresponds to x, which means that we have to provide a proof of P x. This is why the use of H there is valid.
To illustrate, here are proofs of two basic facts about equality: transitivity and symmetry.

Definition etrans {T} {x y z : T} (p : x = y) (q : y = z) : x = z :=
match p in _ = w return w = z -> x = z with
| eq_refl => fun q' : x = z => q'
end q.

Definition esym {T} {x y : T} (p : x = y) : y = x :=
match p in _ = z return z = x with
| eq_refl => eq_refl
end.

Notice the return clause in the first proof, which uses a function type. We cannot use w = z alone, as the final type of the expression would be y = z. The other reasonable guess, x = z, wouldn't work either, since we would have nothing of that type to return in the branch ─ q has type y = z, and Coq does not automatically change it to x = z just because we know that x and y ought to be equal inside the branch. The practice of returning a function is so common when matching on dependent types that it even has its own name: the convoy pattern, a term coined by Adam Chlipala in his CDPT book.
In addition to functions, pretty much any type expression can go in the return clause of a match. This flexibility allows us to derive many basic reasoning principles ─ for instance, the fact that constructors are disjoint and injective.

Definition eq_Sn_m (n m : nat) (p : S n = m) :=
match p in _ = k return match k with
| 0 => False
| S m' => n = m'
end with
| eq_refl => eq_refl
end.

Definition succ_not_zero n : S n <> 0 :=
eq_Sn_m n 0.

Definition succ_inj n m : S n = S m -> n = m :=
eq_Sn_m n (S m).

In the eq_refl branch, we know that k is of the form S n. By substituting this value in the return type, we find that the result of the branch must have type n = n, which is why eq_refl is accepted. Since this is only value of k we have to handle, it doesn't matter that False appears in the return type of the match: that branch will never be used. The more familiar lemmas succ_not_zero and succ_inj simply correspond to special cases of eq_Sn_m. A similar trick can be used for many other inductive types, such as booleans, lists, and so on.

## Mixing proofs and computation

Proofs can be used not only to build other proofs, but also in more conventional programs. If we know that a list is not empty, for example, we can write a function that extracts its first element.

From mathcomp Require Import seq.

Definition first {T} (s : seq T) (Hs : s <> [::]) : T :=
match s return s <> [::] -> T with
| [::] => fun Hs : [::] <> [::] => match Hs eq_refl with end
| x :: _ => fun _ => x
end Hs.

Here we see a slightly different use of dependent pattern matching: the return type depends on the analyzed value s, not just on the indices of its type. The rules for checking that this expression is valid are the same: we substitute the pattern of each branch for s in the return type, and ensure that it is compatible with the result it produces. On the first branch, this gives a contradictory hypothesis [::] <> [::], which we can discard by pattern matching as we did earlier. On the second branch, we can just return the first element of the list.
Proofs can also be stored in regular data structures. Consider for instance the subset type {x : T | P x}, which restricts the elements of the type T to those that satisfy the predicate P. Elements of this type are of the form exist x H, where x is an element of T and H is a proof of P x. Here is an alternative version of first, which expects the arguments s and Hs packed as an element of a subset type.

Definition first' {T} (s : {s : seq T | s <> [::]}) : T :=
match s with
| exist s Hs => first s Hs
end.

While powerful, this idiom comes with a price: when reasoning about a term that mentions proofs, the proofs must be explicitly taken into account. For instance, we cannot show that two elements exist x H1 and exist x H2 are equal just by reflexivity; we must explicitly argue that the proofs H1 and H2 are equal. Unfortunately, there are many cases in which this is not possible ─ for example, two proofs of a disjunction A \/ B need to use the same constructor to be considered equal.
The situation is not as bad as it might sound, because Coq was designed to allow a proof irrelevance axiom without compromising its soundness. This axiom says that any two proofs of the same proposition are equal.

Axiom proof_irrelevance : forall (P : Prop) (p q : P), p = q.

If we are willing to extend the theory with this axiom, much of the pain of mixing proofs and computation goes away; nevertheless, it is a bit upsetting that we need an extra axiom to make the use of proofs in computation practical. Fortunately, much of this convenience is already built into Coq's theory, thanks to the structure of proofs of equality.

## Proof irrelevance and equality

A classical result of type theory says that equalities between elements of a type T are proof irrelevant provided that T has decidable equality. Many useful properties can be expressed in this way; in particular, any boolean function f : S -> bool can be seen as a predicate S -> Prop defined as fun x : S => f x = true. Thus, if we restrict subset types to computable predicates, we do not need to worry about the proofs that appear in its elements.
You might wonder why any assumptions are needed in this result ─ after all, the definition of equality only had a single constructor; how could two proofs be different? Let us begin by trying to show the result without relying on any extra assumptions. We can show that general proof irrelevance can be reduced to irrelevance of "reflexive equality": all proofs of x = x are equal to eq_refl x.

Section Irrelevance.

Variable T : Type.
Implicit Types x y : T.

Definition almost_irrelevance :
(forall x (p : x = x), p = eq_refl x) ->
(forall x y (p q : x = y), p = q) :=
fun H x y p q =>
match q in _ = z return forall p' : x = z, p' = q with
| eq_refl => fun p' => H x p'
end p.

This proof uses the extended form of dependent pattern matching we have seen in the definition of first: the return type mentions q, the very element we are matching on. It also uses the convoy pattern to "update" the type of p with the extra information gained by matching on q.
The almost_irrelevance lemma may look like progress, but it does not actually get us anywhere, because there is no way of proving its premise without assumptions. Here is a failed attempt.

Fail Definition irrelevance x (p : x = x) : p = eq_refl x :=
match p in _ = y return p = eq_refl x with
| eq_refl => eq_refl
end.

Coq complains that the return clause is ill-typed: its right-hand side has type x = x, but its left-hand side has type x = y. That is because when checking the return type, Coq does not use the original type of p, but the one obtained by generalizing the index of its type according to the in clause.
It took many years to understand that, even though the inductive definition of equality only mentions one constructor, it is possible to extend the type theory to allow for provably different proofs of equality between two elements. Homotopy type theory, for example, introduced a univalence principle that says that proofs of equality between two types correspond to isomorphisms between them. Since there are often many different isomorphisms between two types, irrelevance cannot hold in full generality.
To obtain an irrelevance result, we must assume that T has decidable equality.

Hypothesis eq_dec : forall x y, x = y \/ x <> y.

The argument roughly proceeds as follows. We use decidable equality to define a normalization procedure that takes a proof of equality as input and produces a canonical proof of equality of the same type as output. Crucially, the output of the procedure does not depend on its input. We then show that the normalization procedure has an inverse, allowing us to conclude ─ all proofs must be equal to the canonical one.
Here is the normalization procedure.

Definition normalize {x y} (p : x = y) : x = y :=
match eq_dec x y with
| or_introl e => e
| or_intror _ => p
end.

If x = y holds, eq_dec x y must return something of the form or_introl e, the other branch being contradictory. This implies that normalize is constant.

Lemma normalize_const {x y} (p q : x = y) : normalize p = normalize q.
Proof. by rewrite /normalize; case: (eq_dec x y). Qed.

The inverse of normalize is defined by combining transitivity and symmetry of equality.

Notation "p * q" := (etrans p q).

Notation "p ^-1" := (esym p)
(at level 3, left associativity, format "p ^-1").

Definition denormalize {x y} (p : x = y) := p * (normalize (eq_refl y))^-1.

As the above notation suggests, we can show that esym is the inverse of etrans, in the following sense.

Definition etransK x y (p : x = y) : p * p^-1 = eq_refl x :=
match p in _ = y return p * p^-1 = eq_refl x with
| eq_refl => eq_refl (eq_refl x)
end.

This proof avoids the problem that we encountered in our failed proof of irrelevance, resulting from generalizing the right-hand side of p. In this return type, p * p^-1 has type x = x, which matches the one of eq_refl x. Notice why the result of the eq_refl branch is valid: we must produce something of type eq_refl x * (eq_refl x)^-1 = eq_refl x, but by the definitions of etrans and esym, the left-hand side computes precisely to eq_refl x.
Armed with etransK, we can now relate normalize to its inverse, and conclude the proof of irrelevance.

Definition normalizeK x y (p : x = y) :
normalize p * (normalize (eq_refl y))^-1 = p :=
match p in _ = y return normalize p * (normalize (eq_refl y))^-1 = p with
| eq_refl => etransK x x (normalize (eq_refl x))
end.

Lemma irrelevance x y (p q : x = y) : p = q.
Proof.
by rewrite -[LHS]normalizeK -[RHS]normalizeK (normalize_const p q).
Qed.

End Irrelevance.

## Irrelevance of equality in practice

The Mathematical Components library provides excellent support for types with decidable equality in its eqtype module, including a generic result of proof irrelevance like the one I gave above (eq_irrelevance). The class structure used by eqtype makes it easy for Coq to infer proofs of decidable equality, which considerably simplifies the use of this and other lemmas. The Coq standard library also provides a proof of this lemma (eq_proofs_unicity_on), though it is a bit harder to use, since it does not make use of any mechanisms for inferring results of decidable equality.