GitLab

The current proofs for some HeapLang tactics use a bunch of separation logic theorems manually, like this proof:

Lemma tac_wp_free Δ Δ' s E i K l v Φ :
  MaybeIntoLaterNEnvs 1 Δ Δ' →
  envs_lookup i Δ' = Some (false, l ↦ v)%I →
  (let Δ'' := envs_delete false i false Δ' in
   envs_entails Δ'' (WP fill K (Val $ LitV LitUnit) @ s; E {{ Φ }})) →
  envs_entails Δ (WP fill K (Free (LitV l)) @ s; E {{ Φ }}).
Proof.
  rewrite envs_entails_eq=> ? Hlk Hfin.
  rewrite -wp_bind. eapply wand_apply; first exact: wp_free.
  rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
  rewrite -Hfin wand_elim_r (envs_lookup_sound' _ _ _ _ _ Hlk).
  apply later_mono, sep_mono_r, wand_intro_r. rewrite right_id //.
Qed.

It would be much nicer to use the proof mode to do these proofs, which is also nicely circular because we're extending the proof mode using the proof mode. For example, the above proof can be written:

  rewrite envs_entails_eq=> ? Hlk Hfin.
  rewrite into_laterN_env_sound.
  iIntros "HΔ'".
  iApply wp_bind.
  pose proof (envs_lookup_sound' _ false _ _ _ Hlk) as HΔ'split.
  set (Δ'':=envs_delete false i false Δ') in *.
  iDestruct (HΔ'split with "HΔ'") as "[Hl HΔ'']".
  iApply (wp_free with "Hl").
  iNext. iIntros "_".
  iApply (Hfin with "HΔ''").

This proof isn't shorter but you can figure out how to write such a proof using only the proof mode rather than convoluted uses of theorems like sep_mono_r and wand_intro_r. This particular case become slightly messier because if you do iDestruct envs_lookup_sound with "HΔ'" then the proof mode reduces envs_delete and the result is horrendous.

I don't think we need to re-do all of the proofs; I'm thinking having a few such examples would go a long way as examples that demonstrate how to extend the IPM in a nice way. We couldn't port all of the theorems anyway since of course some of these theorems are actually used to implement the IPM.