Make iApply "with" specialization lazier
For example, the [$]
specialization pattern for frame inference is too eager. In the example below, it would like to be able to prove the premises of swap_spec
by framing. However, this does not quite work because wp_apply
first tries to prove the premises of the lemma by framing, and then tries to match the goal. Since framing is performed first, it instantiates evars in the wrong way. If it would first try to match the goal, and then frame, the evars would already be instantiated when framing is performed.
From iris.heap_lang Require Import proofmode notation.
Parameter swap : val.
Definition rotate_r : val := λ: "x" "y" "z",
swap "y" "z";; swap "x" "y".
Section proof.
Context `{!heapG Σ}.
Lemma swap_spec x y v1 v2 :
{{{ x ↦ v1 ∗ y ↦ v2 }}} swap #x #y {{{ RET #(); x ↦ v2 ∗ y ↦ v1 }}}.
Proof. Admitted.
Lemma rotate_r_spec x y z v1 v2 v3 :
{{{ x ↦ v1 ∗ y ↦ v2 ∗ z ↦ v3 }}}
rotate_r #x #y #z
{{{ RET #(); x ↦ v3 ∗ y ↦ v1 ∗ z ↦ v2 }}}.
Proof.
iIntros (Φ) "(Hx & Hy & Hz) Post". do 3 wp_lam.
Fail wp_apply (swap_spec with "[$]").
wp_apply (swap_spec y z with "[$]").
Admitted.
End proof.
It's probably easy to come up with a simpler example, but I ran into this one while preparing the Iris tutorial.
Another example:
Lemma test_apply_unification_order {A : Type}
(Φ : (A → PROP) → PROP)
(HΦ : forall f x, f x -∗ Φ f) f x :
id (f x) -∗ Φ f.
Proof. iIntros "Hf". iApply (HΦ with "Hf"). Qed.