Factor out solve_proper_prepare

This helps when debugging solve_proper_core failures.

added 2 commits

• 461bc9c9 - f_equiv: comments
• b8ba5d8a - factor out solve_proper preparation into a separate tactic

Compare with previous version

Why don't we let f_equiv also perform:

repeat lazymatch goal with
  | |- (_ ==> _)%signature _ _ => intros ???
  | |- pointwise_relation _ _ _ _ => intros ?
  | |- ?R ?f _ => try let f' := constr:(λ x, f x) in intros ?
  end

That should solve the issue in https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/76

I did not want to do that in the f_equiv loop. Certainly, the %signature stuff is preparation-only, isn't it? Also, I don't think it would solve the issue. It does an intros ? when the goal is a function, but doing that without the progress simpl I added leads to loops.

added 1 commit

• e1c92aa2 - remove a useless try

Compare with previous version

I updated this to remove a useless try.

Any objections left?

No objections.

FWIW: I started some experiments to implement a more sensible f_equiv that works for functions of arbitrary arity, performs less backtracking, and takes Params instances into account. However, this MR is not in the way of that, so feel free to merge.

mentioned in commit 572581f1

merged