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?

I think specially-typed ids of all varieties -- not just eta equalities -- are very common in proof systems. Half the tactics in Coq end up translating into id spelled in an especially exciting way. — Daniel Wagner
Church-encoded Sigma? I want to see this. Where is l from List.length Nat l bound? Instead of eta-reduction you can incorporate eta-expansion in your type checker: an attempt to unify f with \x -> e results in eta-expanding f, so the unification problem becomes (\x -> f x) =?= (\x -> e) and you can proceed further structurally. Ideally this machinery should be type-directed, so e.g. whenever two expressions of type Top are unified, you don't need to unify them structurally and can just conclude that they are the same. — user3237465
@user3237465 all the code is here, I learned how to encode arbitrary GADTs on CoC after a lot of help from Gabriel, András etc. - I was trying to avoid messing with the compiler further, I thought it was really good and elegant that way, which is why this issue quite bothered me ): — MaiaVictor

András Kovács András Kovács · Accepted Answer · 2017-01-28T08:36:47

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.

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

1 Answers