ispecialize terms of the form P ∗ Q -∗ R

[markusdemedeiros]

Right now, I don't think we can specialize a hypothesis of the form

∗H : P ∗ Q -∗ R
∗HP : P 
∗HQ : Q 

without exiting proofmode. It would be nice if ispecialize could support this, perhaps by implementing moreIntoWand typeclasses?

[oliversoeser]

This would be achieved by adding the IntoWand instance

instance intoWand_sep_wand (p q : Bool) [BI PROP] (P Q R : PROP) :
    IntoWand p q iprop(P ∗ Q -∗ R) P iprop(Q -∗ R) where
  into_wand := wand_intro <| wand_intro <| sep_assoc.mp.trans <| (sep_mono (intuitionisticallyIf_elim)
  (sep_mono intuitionisticallyIf_elim .rfl)).trans wand_elim_l

however, I don't think that would be the ideal way to go about it. Within MoSeL, the usual way to deal with situations like these is to use specialization patterns (here the $ pattern would apply). I think this would be best dealt by making ispecialize support such patterns to trigger framing, rather than adding instances that apply it indiscriminately during typeclass synthesis.

[lzy0505]

I'm interested in implementing specialization patterns and improving ispecialize. Since @oliversoeser's iapply PR #80 already implements some of the specialization patterns and Proof mode terms, such effort should build on that work. @oliversoeser, do you have plans to extend what you have in the PR?

[oliversoeser]

I do have plans on extending PR #80 further, though probably not with a complete implementation of specialisation patterns. Most important to me is that the parts of iapply dealing with specialisation patterns are doing so by calling helper functions, which can then be reused by ispecialize and others.

[markusdemedeiros]

Cool, I agree that a specialization pattern seems the right way to go about it once those make their way to main