Commit cc95469a authored by Ike Mulder's avatar Ike Mulder
Browse files

Use nice notation in tutorial examples.

parent 74e5d17e
Pipeline #64297 passed with stage
in 8 minutes and 46 seconds
......@@ -248,14 +248,8 @@ Section verification.
(** Instead of reverting to a manual proof, one can also register a hint for Diaframe.
In this case, this can be done as follows. *)
Instance shoot_hint γ z :
BiAbd (TTl := [tele]) (TTr := [tele]) (* no goal and sidecondition existentials *)
false (* indicates key hypothesis is spatial, not persistent *)
(own γ $ Cinl $ Excl ()) (* key hypothesis *)
(own γ $ Cinr $ to_agree z) (* atomic goal *)
(bupd) (* modality behind which goal can be proven *)
emp%I (* sidecondition / anti-frame *)
(own γ $ Cinr $ to_agree z) (* residue / frame *).
Proof. rewrite /BiAbd /=. iStepS. iApply shoot_update. iStepsS. Qed.
HINT own γ (Cinl $ Excl ()) [- ; emp] [bupd]; own γ (Cinr $ to_agree z) [own γ (Cinr $ to_agree z)].
Proof. iStepS. iApply shoot_update. iStepsS. Qed.
(** Note that we use [bupd] as the modality, instead of [fupd _ _] as in the paper.
Diaframe uses the fact that [|==> P ⊢ |={E,E}=> P] for all [P] and [E] to apply such hints. *)
......@@ -100,20 +100,13 @@ Section verification.
(** Exercise: change the hint to have proper side-conditions and frame, then prove the hint. *)
Global Instance biabd_islist_none xs P :
BiAbd (TTl := [tele]) (TTr := [tele])
false empty_hyp_first
(is_list P xs NONEV)
emp%I (* sidecondition - replace me *)
False%I (* residue - replace me *).
HINT empty_hyp_first [- ; (* replace me *) emp] [id]; is_list P xs NONEV [False (* replace me *)].
rewrite /BiAbd /=.
(** This hint has key hypothesis [empty_hyp_first]. This is another special proposition that is treated
differently by the proof search strategy, like [empty_hyp_last] (ε₁ in the paper). The semantics of
[empty_hyp_first] is just [True], but this hypothesis is always the first hypothesis in every environment Δ.
It can be used for hints to add simplification rules.
(** For this hint, we use [id] as the modality. Diaframe automatically uses the fact that
[id P ⊢ |={E,E}=> P] for all [E] and [P] when applying such hints. *)
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment