Open meithecatte opened 3 weeks ago
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.
@hackedy could you share your proof? I tried exactly that and it didn't work. Maybe Iris has changed since you did the exercise?
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
Ah, I see, I was trying to do iApply own_dfrac_update.
Following the Recommended Learning Path, by the time one gets to the
hoare_triple_dfrac
exercise inresource_algebra.v
, one will have seeniMod
being used to make use of a lemma exactly once – inpersistently.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 requiresiMod
.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 expectingiApply
to handle the modality for me. It might be a good idea to either insert more exercises requiring the use ofiMod
along the way, to give students the chance to learn it when it is being first introduced, or add a hint to thehoare_triple_dfrac
exercise reminding the student of the existence of theiMod
tactic.