f_equiv: slightly better support for function relations

This makes f_equiv more powerful: with it we can solve goals of the form f x ≡ g x where f, g: X -d> OFE and f ≡ g. We still make no attempt at solving goals where the arguments are different. I think in all cases where this applies, it will finish the proof, so I added a solve.

I also added the testcases from d16ab1aa.

mentioned in merge request !325 (merged)

This breaks a bunch of stuff because more goals get solved.^^ In Iris I don't quite know how; auto does not call f_equiv or does it? iris@d72f8214

In iris/examples it is more expected, there are some repeat f_equiv that now solve the goal entirely.

added 1 commit

• 33a5c8d9 - changelog

Compare with previous version

I added a changelog entry. I propose we merge this, I don't think I have to fix all the fallout upfront.

Please go ahead and merge this. Since more goals are solved, you probably just have to remove some tactics here and there.

added 1 commit

• c00c740b - changelog

Compare with previous version

resolved all threads

enabled an automatic merge when the pipeline for c00c740b succeeds

mentioned in commit 7d5f3593

merged

@iris-users this MR makes f_equiv handle more goals, which can break proof scripts.