Commit 2285a577 authored by Robbert Krebbers's avatar Robbert Krebbers

Make iApply more powerful and uniform.

It not behaves more consistently with iExact and thus also works in the
case H : P -★ □^n Q |- Q.
parent 7b5cf8fe
Pipeline #2559 passed with stage
in 3 minutes and 57 seconds
...@@ -99,7 +99,7 @@ Lemma newbarrier_spec (P : iProp) (Φ : val → iProp) : ...@@ -99,7 +99,7 @@ Lemma newbarrier_spec (P : iProp) (Φ : val → iProp) :
Proof. Proof.
iIntros (HN) "[#? HΦ]". iIntros (HN) "[#? HΦ]".
rewrite /newbarrier. wp_seq. wp_alloc l as "Hl". rewrite /newbarrier. wp_seq. wp_alloc l as "Hl".
iApply "HΦ". iApply ("HΦ" with "|==>[-]").
iPvs (saved_prop_alloc (F:=idCF) _ P) as (γ) "#?". iPvs (saved_prop_alloc (F:=idCF) _ P) as (γ) "#?".
iPvs (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]") iPvs (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]")
as (γ') "[#? Hγ']"; eauto. as (γ') "[#? Hγ']"; eauto.
......
...@@ -7,66 +7,51 @@ From iris.proofmode Require Import tactics. ...@@ -7,66 +7,51 @@ From iris.proofmode Require Import tactics.
Section savedprop. Section savedprop.
Context (M : ucmraT). Context (M : ucmraT).
Notation iProp := (uPred M). Notation iProp := (uPred M).
Notation "¬ P" := ((P False))%I : uPred_scope. Notation "¬ P" := ( (P False))%I : uPred_scope.
Implicit Types P : iProp.
(* Saved Propositions and view shifts. *) (* Saved Propositions and view shifts. *)
Context (sprop : Type) (saved : sprop iProp iProp) (pvs : iProp iProp). Context (sprop : Type) (saved : sprop iProp iProp) (pvs : iProp iProp).
Hypothesis pvs_mono : forall P Q, (P Q) pvs P pvs Q. Hypothesis pvs_mono : P Q, (P Q) pvs P pvs Q.
Hypothesis sprop_persistent : forall i P, PersistentP (saved i P). Hypothesis sprop_persistent : i P, PersistentP (saved i P).
Hypothesis sprop_alloc_dep : Hypothesis sprop_alloc_dep :
forall (P : sprop iProp), True pvs ( i, saved i (P i)). (P : sprop iProp), True pvs ( i, saved i (P i)).
Hypothesis sprop_agree : Hypothesis sprop_agree : i P Q, saved i P saved i Q P Q.
forall i P Q, saved i P saved i Q P Q.
(* Self-contradicting assertions are inconsistent *) (* Self-contradicting assertions are inconsistent *)
Lemma no_self_contradiction (P : iProp) `{!PersistentP P} : Lemma no_self_contradiction P `{!PersistentP P} : (P ¬ P) False.
(P ¬ P) False.
Proof. (* FIXME: Cannot destruct the <-> as two implications. iApply with <-> also does not work. *) Proof. (* FIXME: Cannot destruct the <-> as two implications. iApply with <-> also does not work. *)
rewrite /uPred_iff. iIntros "#[H1 H2]". (* FIXME: Cannot iApply "H1". *) rewrite /uPred_iff. iIntros "#[H1 H2]".
iAssert P as "#HP". iAssert P as "#HP".
{ iApply "H2". iIntros "!#HP". by iApply ("H1" with "HP"). } { iApply "H2". iIntros "! #HP". by iApply ("H1" with "[#]"). }
by iApply ("H1" with "HP HP"). by iApply ("H1" with "[#]").
Qed. Qed.
(* "Assertion with name [i]" is equivalent to any assertion P s.t. [saved i P] *) (* "Assertion with name [i]" is equivalent to any assertion P s.t. [saved i P] *)
Definition A (i : sprop) : iProp := P, saved i P P. Definition A (i : sprop) : iProp := P, saved i P P.
Lemma saved_is_A i P `{!PersistentP P} : saved i P (A i P). Lemma saved_is_A i P `{!PersistentP P} : saved i P (A i P).
Proof. Proof.
rewrite /uPred_iff. iIntros "#HS !". iSplit. rewrite /uPred_iff. iIntros "#HS !". iSplit.
- iIntros "H". iDestruct "H" as (Q) "[#HSQ HQ]". - iDestruct 1 as (Q) "[#HSQ HQ]".
iPoseProof (sprop_agree i P Q with "[]") as "Heq"; first by eauto. iApply (sprop_agree i P Q with "[]"); eauto.
rewrite /uPred_iff. by iApply "Heq".
- iIntros "#HP". iExists P. by iSplit. - iIntros "#HP". iExists P. by iSplit.
Qed. Qed.
(* Define [Q i] to be "negated assertion with name [i]". Show that this (* Define [Q i] to be "negated assertion with name [i]". Show that this
implies that assertion with name [i] is equivalent to its own negation. *) implies that assertion with name [i] is equivalent to its own negation. *)
Definition Q i := saved i (¬ A i). Definition Q i := saved i (¬ A i).
Lemma Q_self_contradiction i : Lemma Q_self_contradiction i : Q i (A i ¬ A i).
Q i (A i ¬ A i). Proof. iIntros "#HQ !". by iApply (saved_is_A i (¬A i)). Qed.
Proof.
iIntros "#HQ". iApply (@saved_is_A i (¬ A i)%I _). (* FIXME: If we already introduced the box, this iApply does not work. *)
done.
Qed.
(* We can obtain such a [Q i]. *) (* We can obtain such a [Q i]. *)
Lemma make_Q : Lemma make_Q : True pvs ( i, Q i).
True pvs ( i, Q i). Proof. apply sprop_alloc_dep. Qed.
Proof.
apply sprop_alloc_dep.
Qed.
(* Put together all the pieces to derive a contradiction. *) (* Put together all the pieces to derive a contradiction. *)
(* TODO: Have a lemma in upred.v that says that we cannot view shift to False. *) (* TODO: Have a lemma in upred.v that says that we cannot view shift to False. *)
Lemma contradiction : True pvs False. Lemma contradiction : True pvs False.
Proof. Proof.
rewrite make_Q. apply pvs_mono. rewrite make_Q. apply pvs_mono. iDestruct 1 as (i) "HQ".
iIntros "HQ". iDestruct "HQ" as (i) "HQ". iApply (no_self_contradiction (A i)). by iApply Q_self_contradiction.
iApply (@no_self_contradiction (A i) _).
by iApply Q_self_contradiction.
Qed. Qed.
End savedprop. End savedprop.
...@@ -87,10 +87,12 @@ Global Instance from_later_sep P1 P2 Q1 Q2 : ...@@ -87,10 +87,12 @@ Global Instance from_later_sep P1 P2 Q1 Q2 :
Proof. intros ??; red. by rewrite later_sep; apply sep_mono. Qed. Proof. intros ??; red. by rewrite later_sep; apply sep_mono. Qed.
(* IntoWand *) (* IntoWand *)
Global Instance into_wand_wand P Q : IntoWand (P - Q) P Q. Global Instance into_wand_wand P Q Q' :
Proof. done. Qed. FromAssumption false Q Q' IntoWand (P - Q) P Q'.
Global Instance into_wand_impl P Q : IntoWand (P Q) P Q. Proof. by rewrite /FromAssumption /IntoWand /= => ->. Qed.
Proof. apply impl_wand. Qed. Global Instance into_wand_impl P Q Q' :
FromAssumption false Q Q' IntoWand (P Q) P Q'.
Proof. rewrite /FromAssumption /IntoWand /= => ->. by rewrite impl_wand. Qed.
Global Instance into_wand_iff_l P Q : IntoWand (P Q) P Q. Global Instance into_wand_iff_l P Q : IntoWand (P Q) P Q.
Proof. by apply and_elim_l', impl_wand. Qed. Proof. by apply and_elim_l', impl_wand. Qed.
Global Instance into_wand_iff_r P Q : IntoWand (P Q) Q P. Global Instance into_wand_iff_r P Q : IntoWand (P Q) Q P.
......
...@@ -12,6 +12,10 @@ Proof. intros ??. by rewrite -pvs_intro (from_pure P). Qed. ...@@ -12,6 +12,10 @@ Proof. intros ??. by rewrite -pvs_intro (from_pure P). Qed.
Global Instance from_assumption_pvs E p P Q : Global Instance from_assumption_pvs E p P Q :
FromAssumption p P Q FromAssumption p P (|={E}=> Q)%I. FromAssumption p P Q FromAssumption p P (|={E}=> Q)%I.
Proof. rewrite /FromAssumption=>->. apply pvs_intro. Qed. Proof. rewrite /FromAssumption=>->. apply pvs_intro. Qed.
Global Instance into_wand_pvs E1 E2 R P Q :
IntoWand R P Q IntoWand R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 100.
Proof. rewrite /IntoWand=>->. apply wand_intro_l. by rewrite pvs_wand_r. Qed.
Global Instance from_sep_pvs E P Q1 Q2 : Global Instance from_sep_pvs E P Q1 Q2 :
FromSep P Q1 Q2 FromSep (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2). FromSep P Q1 Q2 FromSep (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2).
Proof. rewrite /FromSep=><-. apply pvs_sep. Qed. Proof. rewrite /FromSep=><-. apply pvs_sep. Qed.
...@@ -26,9 +30,6 @@ Qed. ...@@ -26,9 +30,6 @@ Qed.
Global Instance frame_pvs E1 E2 R P Q : Global Instance frame_pvs E1 E2 R P Q :
Frame R P Q Frame R (|={E1,E2}=> P) (|={E1,E2}=> Q). Frame R P Q Frame R (|={E1,E2}=> P) (|={E1,E2}=> Q).
Proof. rewrite /Frame=><-. by rewrite pvs_frame_l. Qed. Proof. rewrite /Frame=><-. by rewrite pvs_frame_l. Qed.
Global Instance into_wand_pvs E1 E2 R P Q :
IntoWand R P Q IntoWand R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 100.
Proof. rewrite /IntoWand=>->. apply wand_intro_l. by rewrite pvs_wand_r. Qed.
Global Instance timeless_elim_pvs E1 E2 Q : TimelessElim (|={E1,E2}=> Q). Global Instance timeless_elim_pvs E1 E2 Q : TimelessElim (|={E1,E2}=> Q).
Proof. Proof.
......
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