Commit 2bea47fc authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

`iRevert` of a pure hypotheses generates a wand instead of implication.

parent a3bed7ea
......@@ -170,8 +170,14 @@ Proof.
rewrite -persistent_and_affinely_sep_l. apply pure_elim_l=> ?. by rewrite HQ.
Qed.
Lemma tac_pure_revert Δ φ Q : envs_entails Δ (⌜φ⌝ Q) (φ envs_entails Δ Q).
Proof. rewrite envs_entails_eq. intros HΔ ?. by rewrite HΔ pure_True // left_id. Qed.
Lemma tac_pure_revert Δ φ P Q :
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 *)
Lemma tac_intuitionistic Δ i j p P P' Q :
......
......@@ -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"];
let A := type of x in
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]
end.
......
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