Computations with dependent types often get stuck on rewrites that use opaque lemmas. When the corresponding equality is decidable, these lemmas don't need to be made transparent to unblock computation.
A fairly common occurrence when working with dependent types in Coq is to call Compute on a benign expression and get back a giant, partially-reduced term, like this:
Import EqNotations Vector.VectorNotations.
= matchmatch
Nat.add_1_r 3in (_ = H)
return (Vector.t nat H)
with
| eq_refl => [1; 2; 3; 4]
endas c in (Vector.t _ H)
return
(match
H as c0 return (Vector.t nat c0 -> Type)
with
| 0 =>
fun_ : Vector.t nat 0 =>
False -> forallx1 : Prop, x1 -> x1
| S x => fun_ : Vector.t nat (S x) => nat
end c)
with
| [] =>
funx : False =>
match
x return (forallx0 : Prop, x0 -> x0)
withend
| h :: _ => h
end
: (fun (n : nat) (_ : Vector.t nat (S n)) => nat)
3
(rew [Vector.t nat] Nat.add_1_r 3in
([1; 2; 3] ++ [4]))
This post shows how to work around this issue.
First, a bit of background. In Coq, constants (like theorems and definitions) come in two flavors: unfoldable (also known as transparent), and opaque. This distinction is particularly relevant when performing δ-reduction: transparent constants (introduced using Definition, Fixpoint, Let, etc., or by closing a proof using Defined) can be unfolded, while opaque ones (introduced by closing a proof with Qed) are left untouched (unfolding a constant means replacing its name by its body). In other words, opaque constants are treated very similarly to axioms for computation purposes; according to the manual, …
… this is to keep with the usual mathematical practice of proof irrelevance: what matters in a mathematical development is the sequence of lemma statements, not their actual proofs. This distinguishes lemmas from the usual defined constants, whose actual values are of course relevant in general.
Concretely, here is how the distinction manifests itself:
Definitiontransparent : nat := 1 + 1.
= 2
: nat
1 + 1 = 2
1 + 1 = 2
auto.Qed.
= opaque
: 1 + 1 = 2
This distinction is usually harmless, but it can bite when working with dependent types, which tend to blur the lines between “lemmas” and “defined constants”. Let's look at an example in more detail. Coq's Vector library provides a function Vector.cons: forall {A}, A -> forall {n}, Vector.t A n -> Vector.t A (1 + n) to prepend a single element to a vector, but no corresponding function snoc to append a single element to a vector. There is a function Vector.append: forall {A} {n p}, Vector.t A n -> Vector.t A p -> Vector.t A (n + p) though, so it's almost enough to define snoc as fun v a => v ++ [a]. If we want snoc to have the same type as cons, we'll just have to add a type cast, because the type of v ++ [a] is Vector.t nat (n + 1), and n + 1 and 1 + n are not unifiable. No big deal:
Definitionsnoc {An} (a: A) (v: Vector.t A n)
: Vector.t A (S n) :=
(* [Nat.add_1_r] has type [forall n : nat, n + 1 = S n] *)
rew (Nat.add_1_r n) in (v ++ [a]).
But now look at what happens if I actually try to compute with this function!
= (fix
Ffix (x : nat) (x0 : Vector.t nat x) {struct
x0} : Vector.t nat x :=
match
x0 in (Vector.t _ H)
return (Vector.t nat H)
with
| [] => []
| Vector.cons _ h n x1 =>
(fix Ffix0 (x2 x3 : nat) {struct x2} :
nat :=
match x2 with
| 0 => x3
| S x4 => S (Ffix0 x4 x3)
end) h
((fix
Ffix0 (x2 x3 : nat) {struct x2} :
nat :=
match x2 with
| 0 => x3
| S x4 => S (Ffix0 x4 x3)
end) h 0) :: Ffix n x1
end) 4match
Nat.add_1_r 3in (_ = H)
return (Vector.t nat H)
with
| eq_refl => [1; 2; 3; 4]
end
: Vector.t nat 4
Agh. Could we maybe prove that Vector.map (fun x => 2 * x) (snoc 4 [1; 2; 3]) equals [2; 4; 6; 8], instead of using compute?
The problem is that the proof of Nat.add_1_r is opaque, so cbv can't reduce it. If you look carefully at the large term from earlier, you'll see that it, too, was blocked on (Nat.add_1_r n).
Abort.
The usual fix is to make every proof that might be used in a computation transparent; something like this:
n: nat
n + 1 = S n
n: nat
n + 1 = S n
0 + 1 = 1
n: nat IHn: n + 1 = S n
S n + 1 = S (S n)
0 + 1 = 1
reflexivity.
n: nat IHn: n + 1 = S n
S n + 1 = S (S n)
n: nat IHn: n + 1 = S n
S (n + 1) = S (S n)
n: nat IHn: n + 1 = S n
S (S n) = S (S n)
reflexivity.Defined. (* [Defined] makes the proof transparent *)
Equivalently, we can write the proof as a recursive function, which makes the fact that it always reduces to eq_refl pretty obvious (the second match could also be written as rew [fun y => S n + 1 = S y] (add_1_r_transparent n) in eq_refl):
Fixpointadd_1_r_transparent (n: nat)
: n + 1 = S n :=
match n with
| 0 => eq_refl
| S n =>
match add_1_r_transparent n in (_ = y)
return (S n + 1 = S y) with
| eq_refl => eq_refl
endend.
… and with this, we can get a definition that computes properly:
Definitionsnoc_computational {An} (a: A) (v: Vector.t A n)
: Vector.t A (S n) :=
rew (add_1_r_transparent n) in (v ++ [a]).
= [2; 4; 6; 8]
: Vector.t nat 4
The problem with this approach is that this change needs to be done recursively: you would need to replace Qed with Defined in the definition of all lemmas that you depend on. Not ideal.
Instead, here's a cool trick:
Definitioncomputational_eq {mn} (opaque_eq: m = n) : m = n :=
match Nat.eq_dec m n with
| left transparent_eq => transparent_eq
| _ => opaque_eq (* dead code; could use [False_rect] *)end.
Definitionsnoc' {An} (a: A) (v: Vector.t A n) :=
rew (computational_eq (Nat.add_1_r n)) in (v ++ [a]).
= [2; 4; 6; 8]
: Vector.t nat 4
🎉️. Here is why this works: in the definition of snoc, all that I really need is to have some transparent proof that n + 1 equals 1 + n — I don't really care which one. So, because equality is decidable on nat, I can just ignore the opaque proof returned by Nat.add_1_r, and rebuild a fresh, transparent one using Nat.eq_dec.
More precisely, for any given m and n, one way to construct a proof that m = n is to compare the two numbers, using a recursive comparison function (that's what Nat.eq_dec is, above; importantly, it returns transparent proofs). If the comparison succeeds, it returns a transparent equality proof (eq_refl) that computational_eq returns, allowing computation to proceed.
For arbitrary m and n, values, the comparison could fail. But in computational_eq, it can't: computational_eq takes a proof that its first two arguments are equal, so the second branch of the match is dead code, and the opaque proof isn't computationally relevant anymore.
The key here is that Nat.eq_dec builds a transparent proof, so there's really nothing magical happening — all we're doing is discarding potentially opaque equality proofs on nats and replacing them with a canonical one that we know to be transparent. The big gain is that we only have to define Nat.eq_dec once, instead of having to make all equality proofs transparent.