Stream: Equations devs & users

Topic: apply_funelim vs funelim


view this post on Zulip Théo Winterhalter (Dec 24 2020 at 09:50):

Is it to be expected that sometimes apply_funelim will fail when funelim will succeed? I have an example where this is the case, but don't know how to minimise yet.

view this post on Zulip Matthieu Sozeau (Jan 04 2021 at 12:41):

Yes, it might fail because the unification problem is too hard to resolve

view this post on Zulip Théo Winterhalter (Jan 04 2021 at 12:49):

Oh ok. I thought funelim was supposed to be apply_funelim plus some automation.

view this post on Zulip Matthieu Sozeau (Jan 04 2021 at 13:11):

It is, in a way. However funelim makes a goal of the form forall args, P args (f args) where P has some equalities to remember the actual arguments of the function, that is trivial to unify with the eliminators conclusion. apply_funelim does no massaging of the goal in comparison and just launches the (heuristic) higher-order matching in the hope to find a solution.

view this post on Zulip Théo Winterhalter (Jan 04 2021 at 13:13):

I see. Thanks. :)


Last updated: Jan 29 2023 at 15:02 UTC