Commit 5fa30a35 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'robbert/iRevert_pure' into 'master'

Let `iRevert` of a pure hypotheses generate a wand instead of implication.

See merge request !789
parents e785e4a0 83256c1d
Pipeline #65348 passed with stage
in 11 minutes and 20 seconds
...@@ -21,6 +21,8 @@ lemma. ...@@ -21,6 +21,8 @@ lemma.
the conclusion. The old behavior can be emulated with`iExFalso. iExact "H".` the conclusion. The old behavior can be emulated with`iExFalso. iExact "H".`
* In `iInduction`, support induction schemes that involve `Forall` and * In `iInduction`, support induction schemes that involve `Forall` and
`Forall2` (for example, for trees with finite branching). `Forall2` (for example, for trees with finite branching).
* Change `iRevert` of a pure hypothesis to generate a magic wand instead of an
implication.
**Changes in `base_logic`:** **Changes in `base_logic`:**
......
...@@ -170,8 +170,14 @@ Proof. ...@@ -170,8 +170,14 @@ Proof.
rewrite -persistent_and_affinely_sep_l. apply pure_elim_l=> ?. by rewrite HQ. rewrite -persistent_and_affinely_sep_l. apply pure_elim_l=> ?. by rewrite HQ.
Qed. Qed.
Lemma tac_pure_revert Δ φ Q : envs_entails Δ (⌜φ⌝ Q) (φ envs_entails Δ Q). Lemma tac_pure_revert Δ φ P Q :
Proof. rewrite envs_entails_eq. intros HΔ ?. by rewrite HΔ pure_True // left_id. Qed. FromAffinely P φ
envs_entails Δ (P - Q)
(φ envs_entails Δ Q).
Proof.
rewrite /FromAffinely envs_entails_eq. intros <- -> ?.
by rewrite pure_True // affinely_True_emp affinely_emp left_id.
Qed.
(** * Intuitionistic *) (** * Intuitionistic *)
Lemma tac_intuitionistic Δ i j p P P' Q : Lemma tac_intuitionistic Δ i j p P P' Q :
......
...@@ -651,7 +651,10 @@ Local Tactic Notation "iForallRevert" ident(x) := ...@@ -651,7 +651,10 @@ Local Tactic Notation "iForallRevert" ident(x) :=
first [let A := type of x in idtac|fail 1 "iRevert:" x "not in scope"]; first [let A := type of x in idtac|fail 1 "iRevert:" x "not in scope"];
let A := type of x in let A := type of x in
lazymatch type of A with lazymatch type of A with
| Prop => revert x; first [apply tac_pure_revert|err x] | Prop =>
revert x; first
[eapply tac_pure_revert; [iSolveTC (* [FromAffinely], should never fail *)|]
|err x]
| _ => revert x; first [apply tac_forall_revert|err x] | _ => revert x; first [apply tac_forall_revert|err x]
end. end.
......
...@@ -408,6 +408,29 @@ No applicable tactic. ...@@ -408,6 +408,29 @@ No applicable tactic.
"HQ" : Q "HQ" : Q
--------------------------------------∗ --------------------------------------∗
▷ P ∗ Q ▷ P ∗ Q
"test_iRevert_pure"
: string
1 goal
PROP : bi
φ : Prop
P : PROP
============================
"H" : <affine> ⌜φ⌝ -∗ P
--------------------------------------∗
<affine> ⌜φ⌝ -∗ P
"test_iRevert_pure_affine"
: string
1 goal
PROP : bi
BiAffine0 : BiAffine PROP
φ : Prop
P : PROP
============================
"H" : ⌜φ⌝ -∗ P
--------------------------------------∗
⌜φ⌝ -∗ P
"elim_mod_accessor" "elim_mod_accessor"
: string : string
1 goal 1 goal
......
...@@ -1157,6 +1157,22 @@ Proof. ...@@ -1157,6 +1157,22 @@ Proof.
iIntros (?) "HP HQ". iModIntro. Show. by iFrame. iIntros (?) "HP HQ". iModIntro. Show. by iFrame.
Qed. Qed.
Check "test_iRevert_pure".
Lemma test_iRevert_pure (φ : Prop) P :
φ (<affine> φ - P) - P.
Proof.
(* Check that iRevert creates a wand instead of an implication *)
iIntros (Hφ) "H". iRevert (Hφ). Show. done.
Qed.
Check "test_iRevert_pure_affine".
Lemma test_iRevert_pure_affine `{!BiAffine PROP} (φ : Prop) P :
φ ( φ - P) - P.
Proof.
(* If the BI is affine, no affine modality should be added *)
iIntros (Hφ) "H". iRevert (Hφ). Show. done.
Qed.
End tests. End tests.
Section parsing_tests. Section parsing_tests.
......
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