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?

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

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

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.

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

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

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