Commit 56301ac8 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Also create a wand when reverting a persistent hypothesis.

This is more consistent with our current consensus of not using
implication. Also, it allows one to reintroduce the persistent
hypothesis into the spatial context.
parent 855014ca
......@@ -578,11 +578,10 @@ Qed.
Lemma tac_revert Δ Δ' i p P Q :
envs_lookup_delete i Δ = Some (p,P,Δ')
(Δ' if p then P Q else P - Q) Δ Q.
(Δ' (if p then P else P) - Q) Δ Q.
intros ? HQ. rewrite envs_lookup_delete_sound //; simpl. destruct p.
- by rewrite HQ -always_and_sep_l impl_elim_r.
- by rewrite HQ wand_elim_r.
intros ? HQ. rewrite envs_lookup_delete_sound //; simpl.
by rewrite HQ /uPred_always_if wand_elim_r.
Lemma tac_revert_ih Δ P Q :
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