Skip to content
GitLab

Make `wp_apply` perform `wp_pure` in small steps until the lemma matches the goal.

Merged Robbert Krebbers requested to merge robbert/wp_apply_pure into master

Currently wp_apply first performs wp_pures, which might cause the goal to be normalized too far.

We experienced this issue in Actris, see https://gitlab.mpi-sws.org/iris/actris/-/blob/master/theories/examples/basics.v#L358, where we had to carefully call wp_pure for a certain number of times, and then iApply the lemma.

This MR fixes this issue by letting adding a new variant wp_smart_apply that performs wp_pure step-by-step. The old wp_apply now performs no reduction whatsoever.

Edited by Ralf Jung

Merge request reports