Commit e17ac4ad authored by Robbert Krebbers's avatar Robbert Krebbers

Fix issue #98.

We used to normalize the goal, and then checked whether it was of
a certain shape. Since `uPred_valid P` normalized to `True ⊢ P`,
there was no way of making a distinction between the two, hence
`True ⊢ P` was treated as `uPred_valid P`.

In this commit, I use type classes to check whether the goal is of
a certain shape. Since we declared `uPred_valid` as `Typeclasses
Opaque`, we can now make a distinction between `True ⊢ P` and
`uPred_valid P`.
parent 36322106
...@@ -51,7 +51,7 @@ Proof. ...@@ -51,7 +51,7 @@ Proof.
Qed. Qed.
Lemma inv_alloc_open N E P : Lemma inv_alloc_open N E P :
N E True ={E, E∖↑N}= inv N P (P ={E∖↑N, E}= True). N E (|={E, E∖↑N}=> inv N P (P ={E∖↑N, E}= True))%I.
Proof. Proof.
rewrite inv_eq /inv_def fupd_eq /fupd_def. iIntros (Sub) "[Hw HE]". rewrite inv_eq /inv_def fupd_eq /fupd_def. iIntros (Sub) "[Hw HE]".
iMod (ownI_alloc_open ( (N : coPset)) P with "Hw") iMod (ownI_alloc_open ( (N : coPset)) P with "Hw")
......
...@@ -190,6 +190,8 @@ Notation "P ==∗ Q" := (P -∗ |==> Q)%I ...@@ -190,6 +190,8 @@ Notation "P ==∗ Q" := (P -∗ |==> Q)%I
(at level 99, Q at level 200, format "P ==∗ Q") : uPred_scope. (at level 99, Q at level 200, format "P ==∗ Q") : uPred_scope.
Coercion uPred_valid {M} (P : uPred M) : Prop := True%I P. Coercion uPred_valid {M} (P : uPred M) : Prop := True%I P.
Typeclasses Opaque uPred_valid.
Notation "P -∗ Q" := (P Q) Notation "P -∗ Q" := (P Q)
(at level 99, Q at level 200, right associativity) : C_scope. (at level 99, Q at level 200, right associativity) : C_scope.
......
...@@ -15,7 +15,7 @@ Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ. ...@@ -15,7 +15,7 @@ Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
Proof. solve_inG. Qed. Proof. solve_inG. Qed.
Definition heap_adequacy Σ `{heapPreG Σ} e σ φ : Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
( `{heapG Σ}, True WP e {{ v, ⌜φ v }}) ( `{heapG Σ}, WP e {{ v, ⌜φ v }}%I)
adequate e σ φ. adequate e σ φ.
Proof. Proof.
intros Hwp; eapply (wp_adequacy _ _); iIntros (?) "". intros Hwp; eapply (wp_adequacy _ _); iIntros (?) "".
......
...@@ -91,7 +91,7 @@ Qed. ...@@ -91,7 +91,7 @@ Qed.
Lemma newbarrier_spec (P : iProp Σ) : Lemma newbarrier_spec (P : iProp Σ) :
{{{ True }}} newbarrier #() {{{ l, RET #l; recv l P send l P }}}. {{{ True }}} newbarrier #() {{{ l, RET #l; recv l P send l P }}}.
Proof. Proof.
iIntros (Φ) "HΦ". iIntros (Φ) "_ HΦ".
rewrite -wp_fupd /newbarrier /=. wp_seq. wp_alloc l as "Hl". rewrite -wp_fupd /newbarrier /=. wp_seq. wp_alloc l as "Hl".
iApply ("HΦ" with "[> -]"). iApply ("HΦ" with "[> -]").
iMod (saved_prop_alloc (F:=idCF) P) as (γ) "#?". iMod (saved_prop_alloc (F:=idCF) P) as (γ) "#?".
......
...@@ -35,7 +35,7 @@ Section mono_proof. ...@@ -35,7 +35,7 @@ Section mono_proof.
Lemma newcounter_mono_spec (R : iProp Σ) : Lemma newcounter_mono_spec (R : iProp Σ) :
{{{ True }}} newcounter #() {{{ l, RET #l; mcounter l 0 }}}. {{{ True }}} newcounter #() {{{ l, RET #l; mcounter l 0 }}}.
Proof. Proof.
iIntros (Φ) "HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl". iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
iMod (own_alloc ( (O:mnat) (O:mnat))) as (γ) "[Hγ Hγ']"; first done. iMod (own_alloc ( (O:mnat) (O:mnat))) as (γ) "[Hγ Hγ']"; first done.
iMod (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]"). iMod (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]").
{ iNext. iExists 0%nat. by iFrame. } { iNext. iExists 0%nat. by iFrame. }
...@@ -111,7 +111,7 @@ Section contrib_spec. ...@@ -111,7 +111,7 @@ Section contrib_spec.
{{{ True }}} newcounter #() {{{ True }}} newcounter #()
{{{ γ l, RET #l; ccounter_ctx γ l ccounter γ 1 0 }}}. {{{ γ l, RET #l; ccounter_ctx γ l ccounter γ 1 0 }}}.
Proof. Proof.
iIntros (Φ) "HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl". iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
iMod (own_alloc (! O%nat ! 0%nat)) as (γ) "[Hγ Hγ']"; first done. iMod (own_alloc (! O%nat ! 0%nat)) as (γ) "[Hγ Hγ']"; first done.
iMod (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]"). iMod (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]").
{ iNext. iExists 0%nat. by iFrame. } { iNext. iExists 0%nat. by iFrame. }
......
...@@ -166,7 +166,7 @@ Lemma wp_alloc E e v : ...@@ -166,7 +166,7 @@ Lemma wp_alloc E e v :
to_val e = Some v to_val e = Some v
{{{ True }}} Alloc e @ E {{{ l, RET LitV (LitLoc l); l v }}}. {{{ True }}} Alloc e @ E {{{ l, RET LitV (LitLoc l); l v }}}.
Proof. Proof.
iIntros (<-%of_to_val Φ) "HΦ". iApply wp_lift_atomic_head_step_no_fork; auto. iIntros (<-%of_to_val Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1) "Hσ !>"; iSplit; first by auto. iIntros (σ1) "Hσ !>"; iSplit; first by auto.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done. iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
......
...@@ -164,9 +164,9 @@ End adequacy. ...@@ -164,9 +164,9 @@ End adequacy.
Theorem wp_adequacy Σ Λ `{invPreG Σ} e σ φ : Theorem wp_adequacy Σ Λ `{invPreG Σ} e σ φ :
( `{Hinv : invG Σ}, ( `{Hinv : invG Σ},
True ={}= stateI : state Λ iProp Σ, (|={}=> stateI : state Λ iProp Σ,
let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
stateI σ WP e {{ v, ⌜φ v }}) stateI σ WP e {{ v, ⌜φ v }})%I)
adequate e σ φ. adequate e σ φ.
Proof. Proof.
intros Hwp; split. intros Hwp; split.
...@@ -188,9 +188,9 @@ Qed. ...@@ -188,9 +188,9 @@ Qed.
Theorem wp_invariance Σ Λ `{invPreG Σ} e σ1 t2 σ2 φ : Theorem wp_invariance Σ Λ `{invPreG Σ} e σ1 t2 σ2 φ :
( `{Hinv : invG Σ}, ( `{Hinv : invG Σ},
True ={}= stateI : state Λ iProp Σ, (|={}=> stateI : state Λ iProp Σ,
let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
stateI σ1 WP e {{ _, True }} (stateI σ2 ={,}= ⌜φ⌝)) stateI σ1 WP e {{ _, True }} (stateI σ2 ={,}= ⌜φ⌝))%I)
rtc step ([e], σ1) (t2, σ2) rtc step ([e], σ1) (t2, σ2)
φ. φ.
Proof. Proof.
......
...@@ -50,19 +50,25 @@ Tactic Notation "iMatchHyp" tactic1(tac) := ...@@ -50,19 +50,25 @@ Tactic Notation "iMatchHyp" tactic1(tac) :=
| |- context[ environments.Esnoc _ ?x ?P ] => tac x P | |- context[ environments.Esnoc _ ?x ?P ] => tac x P
end. end.
Class AsValid {M} (φ : Prop) (P : uPred M) := as_entails : φ P.
Arguments AsValid {_} _%type _%I.
Instance as_valid_valid {M} (P : uPred M) : AsValid (uPred_valid P) P | 0.
Proof. by rewrite /AsValid. Qed.
Instance as_valid_entails {M} (P Q : uPred M) : AsValid (P Q) (P - Q) | 1.
Proof. split. apply uPred.entails_wand. apply uPred.wand_entails. Qed.
Instance as_valid_equiv {M} (P Q : uPred M) : AsValid (P Q) (P Q).
Proof. split. apply uPred.equiv_iff. apply uPred.iff_equiv. Qed.
(** * Start a proof *) (** * Start a proof *)
Ltac iStartProof := Ltac iStartProof :=
lazymatch goal with lazymatch goal with
| |- of_envs _ _ => idtac | |- of_envs _ _ => idtac
| |- ?P => | |- ?P =>
lazymatch eval hnf in P with apply (proj2 (_ : AsValid P _)), tac_adequate
(* need to use the unfolded version of [uPred_valid] due to the hnf *) || fail "iStartProof: not a uPred"
| True _ => apply tac_adequate
| _ _ => apply uPred.wand_entails, tac_adequate
(* need to use the unfolded version of [⊣⊢] due to the hnf *)
| uPred_equiv' _ _ => apply uPred.iff_equiv, tac_adequate
| _ => fail "iStartProof: not a uPred"
end
end. end.
(** * Context manipulation *) (** * Context manipulation *)
...@@ -529,18 +535,16 @@ a goal [P] for non-dependent arguments [x_i : P]. *) ...@@ -529,18 +535,16 @@ a goal [P] for non-dependent arguments [x_i : P]. *)
Tactic Notation "iIntoValid" open_constr(t) := Tactic Notation "iIntoValid" open_constr(t) :=
let rec go t := let rec go t :=
let tT := type of t in let tT := type of t in
lazymatch eval hnf in tT with first
| True _ => apply t [apply (proj1 (_ : AsValid tT _) t)
| _ _ => apply (uPred.entails_wand _ _ t) |lazymatch eval hnf in tT with
(* need to use the unfolded version of [⊣⊢] due to the hnf *) | ?P ?Q => let H := fresh in assert P as H; [|go uconstr:(t H); clear H]
| uPred_equiv' _ _ => apply (uPred.equiv_iff _ _ t) | _ : ?T, _ =>
| ?P ?Q => let H := fresh in assert P as H; [|go uconstr:(t H); clear H] (* Put [T] inside an [id] to avoid TC inference from being invoked. *)
| _ : ?T, _ => (* This is a workarround for Coq bug #4969. *)
(* Put [T] inside an [id] to avoid TC inference from being invoked. *) let e := fresh in evar (e:id T);
(* This is a workarround for Coq bug #4969. *) let e' := eval unfold e in e in clear e; go (t e')
let e := fresh in evar (e:id T); end] in
let e' := eval unfold e in e in clear e; go (t e')
end in
go t. go t.
(* The tactic [tac] is called with a temporary fresh name [H]. The argument (* The tactic [tac] is called with a temporary fresh name [H]. The argument
......
...@@ -40,7 +40,7 @@ Section client. ...@@ -40,7 +40,7 @@ Section client.
Lemma client_safe : WP client {{ _, True }}%I. Lemma client_safe : WP client {{ _, True }}%I.
Proof. Proof.
iIntros ""; rewrite /client. wp_alloc y as "Hy". wp_let. iIntros ""; rewrite /client. wp_alloc y as "Hy". wp_let.
wp_apply (newbarrier_spec N (y_inv 1 y)). wp_apply (newbarrier_spec N (y_inv 1 y) with "[//]").
iIntros (l) "[Hr Hs]". wp_let. iIntros (l) "[Hr Hs]". wp_let.
iApply (wp_par (λ _, True%I) (λ _, True%I) with "[Hy Hs] [Hr]"); last auto. iApply (wp_par (λ _, True%I) (λ _, True%I) with "[Hy Hs] [Hr]"); last auto.
- (* The original thread, the sender. *) - (* The original thread, the sender. *)
......
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