Stream: Coq devs & plugin devs

Topic: TC and eta for functions


view this post on Zulip Janno (Feb 14 2024 at 10:01):

I am looking at the dnet code (https://github.com/coq/coq/blob/master/tactics/btermdn.ml) and I am a little surprised by the fact that eta_reduce (and eta_reduce_pat) are not used for recursive calls to decomp (in constr_val_discr and constr_val_pat). I am not sure if I am reading the code correctly but it seems to me that (fun x => f x) y is going to be treated as matching everything while (fun x => f x) would be treated as matching exactly f (assuming f is hint opaque). Am I missing something in the code?

view this post on Zulip Pierre-Marie Pédrot (Feb 14 2024 at 10:20):

This looks OK w.r.t. to the spec, which only mandates an approximation.

view this post on Zulip Janno (Feb 14 2024 at 10:32):

Oh, sure. But is there a point in not making the approximating more exact?

view this post on Zulip Enrico Tassi (Feb 14 2024 at 10:38):

According to our tests, TC resolution in Coq and eta for function are not best friends. If the eta expansion is in an instance, then Coq does not like it. If the eta expansion is in the goal, then it finds the instance.

view this post on Zulip Pierre-Marie Pédrot (Feb 14 2024 at 10:40):

@Enrico Tassi this looks like a bug, did you investigate why this failed in the first case?

view this post on Zulip Enrico Tassi (Feb 14 2024 at 10:47):

nope. Since I don't know the spec I don't even know what I should expect. The TC solver we are developing with @Davide F should quotient over eta since our "unification may introduce eta expansions" in different places...

view this post on Zulip Janno (Feb 14 2024 at 10:47):

I was also under the impression that TC and eta was not a solved problem at all (both in correctness and in performance) and I am worried about it particularly because of the planned removal of compatibility constants which will probably generate more eta expansions of primitive projections


Last updated: Oct 13 2024 at 01:02 UTC