Commit 76cbd8d1 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

wp is absorbing.

parent e16d37fa
......@@ -1186,7 +1186,7 @@ Qed.
*)
(* ---------------------------------------------------------------------- *)
(** Proof mode instances *)
(** Proof mode definitions for LambdaSep *)
Module ProofMode.
Export SepBasicTactics.ProofMode.
......@@ -1204,6 +1204,7 @@ Qed.
Instance triple_as_valid t H Q : AsValid (triple t H Q) (H - wp t Q).
Proof. rewrite /AsValid wp_equiv. apply as_valid. Qed.
Instance frame_wp p t R Φ Ψ :
( v, Frame p R (Φ v) (Ψ v)) Frame p R (wp t Φ) (wp t Ψ).
Proof.
......@@ -1211,4 +1212,10 @@ Proof.
iExists (H ?p R)%I. iFrame. iPureIntro. eapply rule_frame_consequence=>//.
iIntros (?) "[??]". iApply HR. iFrame.
Qed.
Instance wp_absorbing t Q : Absorbing (wp t Q).
Proof.
apply wp_equiv. rewrite /bi_absorbingly -htop_True comm.
apply rule_htop_pre. iIntros "$".
Qed.
End ProofMode.
......@@ -2038,6 +2038,12 @@ Proof.
- intros [? Hφ]. apply hpure_intro; [done|].
change ((\[φ] \* \Top%I) h) in Hφ. rewrite hstar_pure in Hφ. naive_solver.
Qed.
Lemma htop_True : \Top = True%I.
Proof.
apply fun_ext_1=>?. apply prop_ext; split=>?.
- rewrite /bi_pure /= /hpure_abs hstar_pure. auto.
- apply htop_intro.
Qed.
Opaque hpure_abs.
(* We need to repeat all these hints appearing in proofmode/tactics.v,
......
Markdown is supported
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