Is it usual to wrap a variable in an useless `id` call to avoid eta-conversion issues on proofs?

Question

Using a language similar to Morte/CoC, I'm trying to prove the simple statement there are lists of arbitrary lengths. For that, I wrote the following type:

∀ n:Nat ->
(ThereIs (List Nat)
  (Equal Nat 
    (List.length Nat l) 
    n)))

ThereIs is the dependent pair (Sigma). All is church-encoded. To prove it, I wrote the following proof:

λ n:Nat ->
(ThereIs.this (List Nat)
  (λ l:(List Nat) -> (Equal Nat (List.length Nat l) n))
  (List.replicate Nat n Nat.Zero)
  (Equal.refl Nat n))

Weirdly, I get a type mismatch error between d (i.e., the free variable of type Nat) and λ c:* -> λ b:(c -> c) -> λ a:c -> (d c b a). But that later term, when eta-reduced, is just d! Since I don't have an eta-reducer ready, I instead made this following "useless identify" function:

λ n: Nat ->

λ Nat:* ->
λ Succ: (Nat -> Nat) ->
λ Zero: Nat ->

(n Nat Succ Zero)

Now, by applying that useless id to every occurence of n, I "un-eta" it, causing the proof to check. I'd like to gain any kind of insight of what is going on here. Is this "useless id" function a known/used pattern on writing proofs? Why isn't the calculus of contructions able to type-check this proof without this little help? Is there any deep reasoning behind this phenomena or is it just how things are for no special reason?

Answer 1

You need to add eta to your conversion checking algorithm. That can be done in several ways, the simplest two are

• Type-directed as in page 22 of Ulf Norell's thesis and used in Agda
• Untyped as used in Coq AFAIK

Untyped eta conversion is complete for functions, and it's also simpler and faster than the typed version (no need to recompute or cache types in neutral applications) in our case. The algorithm goes like this:

We first check the case when both values are lambdas as usual. However, we check two additional cases after that, when only one side is lambda. In these cases, we apply the lambda body to a new generic variable (as usual), and also apply the other term to the same variable, and check equality of the resulting values.

That's all of it! It's actually very simple, and doesn't have much performance cost. Note that we don't need to implement eta reduction, or strong eta normalization, since eta conversion check is easily done on weak-head normal values on the fly.