Framing: Make* classes lead to suboptimal results
Framing uses Make*
classes to turn terms into a certain form, e.g. a leading ▷^n
. However, those classes require the original term to be equivalent with the converted one. This leads to situations such as
Lemma test_iFrame_later_rel (P : PROP) :
▷ P -∗ (▷ (P ∧ P)).
Proof. iIntros "?". iFrame.
(* Now the goal is [▷ emp] *)
I would expect the goal to become emp
(and hence iFrame
closing the goal), and indeed that would be sound (emp
implies ▷ emp
) but it doesn't happen.