Exercise requires iMod without much previous exposure to the tactic

[meithecatte]

Following the Recommended Learning Path, by the time one gets to the hoare_triple_dfrac exercise in resource_algebra.v, one will have seen iMod being used to make use of a lemma exactly once – in persistently.v, quite a while ago.

Moreover, at that point one doesn't have much practical experience doing that themselves. hoare_triple_dfrac is the first exercise that requires iMod.

This might make it quite hard to remember that iMod is how one is supposed to eliminate the update modality. Indeed, I myself got stuck expecting iApply to handle the modality for me. It might be a good idea to either insert more exercises requiring the use of iMod along the way, to give students the chance to learn it when it is being first introduced, or add a hint to the hoare_triple_dfrac exercise reminding the student of the existence of the iMod tactic.

[hackedy]

For what it's worth, I did hoare_triple_dfrac using only iApply, which I guess is willing to eliminate the |==> in a hypothesis if it's being applied to a goal that has a (fancy) update modality.

[meithecatte]

@hackedy could you share your proof? I tried exactly that and it didn't work. Maybe Iris has changed since you did the exercise?

[hackedy]

Hi Maja, here's my proof

Lemma hoare_triple_dfrac (γ : gname):
  {{{ own γ (DfracOwn 1) }}} #1 + #1 {{{v , RET v; own γ DfracDiscarded }}}.
Proof.
  iIntros "* Hown Hpost".
  rewrite own_dfrac_update.
  wp_pures.
  iApply "Hpost".
  iApply "Hown".
Qed.

Here's the versions of everything

% opam list
# Packages matching: installed
# Name                # Installed # Synopsis
base-bigarray         base
base-domains          base
base-nnp              base        Naked pointers prohibited in the OCaml heap
base-threads          base
base-unix             base
conf-gmp              4           Virtual package relying on a GMP lib system install
conf-pkg-config       3           Check if pkg-config is installed and create an opam
coq                   8.19.2      The Coq Proof Assistant
coq-core              8.19.2      The Coq Proof Assistant -- Core Binaries and Tools
coq-iris              4.2.0       A Higher-Order Concurrent Separation Logic Framewor
coq-iris-heap-lang    4.2.0       The canonical example language for Iris
coq-stdlib            8.19.2      The Coq Proof Assistant -- Standard Library
coq-stdpp             1.10.0      An extended "Standard Library" for Coq
coqide-server         8.19.2      The Coq Proof Assistant, XML protocol server
dune                  3.16.0      Fast, portable, and opinionated build system
host-arch-arm64       1           OCaml on AArch64 (64-bit)
host-system-other     1           OCaml on an unidentified system
ocaml                 5.2.0       The OCaml compiler (virtual package)
ocaml-base-compiler   5.2.0       Official release 5.2.0
ocaml-config          3           OCaml Switch Configuration
ocaml-options-vanilla 1           Ensure that OCaml is compiled with no special optio
ocamlfind             1.9.6       A library manager for OCaml
zarith                1.14        Implements arithmetic and logical operations over a

[meithecatte]

Ah, I see, I was trying to do iApply own_dfrac_update.