Commit 29ee3a0f authored by Robbert Krebbers's avatar Robbert Krebbers

Revert "Let iLöb automatically revert and introduce spatial hypotheses."

This reverts commit 3cc38ff6.

The reverted pure hypotheses and variables appear in the wrong order.
parent 3cc38ff6
Pipeline #450 passed with stage
......@@ -796,12 +796,6 @@ Proof.
Qed.
Lemma entails_wand P Q : (P Q) True (P - Q).
Proof. auto using wand_intro_l. Qed.
Lemma wand_curry P Q R : (P - Q - R) (P Q - R).
Proof.
apply (anti_symm _).
- apply wand_intro_l. by rewrite (comm _ P) -assoc !wand_elim_r.
- do 2 apply wand_intro_l. by rewrite assoc (comm _ Q) wand_elim_r.
Qed.
Lemma sep_and P Q : (P Q) (P Q).
Proof. auto. Qed.
......
......@@ -140,7 +140,7 @@ Lemma wait_spec l P (Φ : val → iProp) :
Proof.
rename P into R; rewrite /recv /barrier_ctx.
iIntros "[Hr HΦ]"; iDestruct "Hr" as {γ P Q i} "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
iLöb as "IH". wp_rec. wp_focus (! _)%E.
iLöb "Hγ HQR HΦ" as "IH". wp_rec. wp_focus (! _)%E.
iSts γ as [p I]; iDestruct "Hγ" as "[Hl Hr]".
wp_load. destruct p.
- (* a Low state. The comparison fails, and we recurse. *)
......
......@@ -75,7 +75,7 @@ Lemma join_spec (Ψ : val → iProp) l (Φ : val → iProp) :
(join_handle l Ψ v, Ψ v - Φ v) WP join (%l) {{ Φ }}.
Proof.
rewrite /join_handle; iIntros "[[% H] Hv]"; iDestruct "H" as {γ} "(#?&Hγ&#?)".
iLöb as "IH". wp_rec. wp_focus (! _)%E.
iLöb "Hγ Hv" as "IH". wp_rec. wp_focus (! _)%E.
iInv N as "Hinv"; iDestruct "Hinv" as {v} "[Hl Hinv]".
wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
- iSplitL "Hl"; [iNext; iExists _; iFrame "Hl"; by iLeft|].
......
......@@ -85,9 +85,6 @@ Definition envs_split {M}
Definition envs_persistent {M} (Δ : envs M) :=
if env_spatial Δ is Enil then true else false.
Definition envs_clear_spatial {M} (Δ : envs M) : envs M :=
Envs (env_persistent Δ) Enil.
(* Coq versions of the tactics *)
Section tactics.
Context {M : cmraT}.
......@@ -95,10 +92,6 @@ Implicit Types Γ : env (uPred M).
Implicit Types Δ : envs M.
Implicit Types P Q : uPred M.
Lemma of_envs_def Δ :
of_envs Δ = ( envs_wf Δ Π env_persistent Δ Π★ env_spatial Δ)%I.
Proof. done. Qed.
Lemma envs_lookup_delete_Some Δ Δ' i p P :
envs_lookup_delete i Δ = Some (p,P,Δ')
envs_lookup i Δ = Some (p,P) Δ' = envs_delete i p Δ.
......@@ -234,23 +227,9 @@ Proof.
env_split_fresh_1, env_split_fresh_2.
Qed.
Lemma envs_clear_spatial_sound Δ :
Δ (envs_clear_spatial Δ Π★ env_spatial Δ)%I.
Proof.
rewrite /of_envs /envs_clear_spatial /=; apply const_elim_sep_l=> Hwf.
rewrite right_id -assoc; apply sep_intro_True_l; [apply const_intro|done].
destruct Hwf; constructor; simpl; auto using Enil_wf.
Qed.
Lemma env_fold_wand Γ Q : env_fold uPred_wand Q Γ (Π★ Γ - Q).
Proof.
revert Q; induction Γ as [|Γ IH i P]=> Q /=; [by rewrite wand_True|].
by rewrite IH wand_curry (comm uPred_sep).
Qed.
Lemma envs_persistent_persistent Δ : envs_persistent Δ = true PersistentP Δ.
Lemma env_special_nil_persistent Δ : envs_persistent Δ = true PersistentP Δ.
Proof. intros; destruct Δ as [? []]; simplify_eq/=; apply _. Qed.
Hint Immediate envs_persistent_persistent : typeclass_instances.
Hint Immediate env_special_nil_persistent : typeclass_instances.
(** * Adequacy *)
Lemma tac_adequate P : Envs Enil Enil P True P.
......@@ -274,9 +253,9 @@ Qed.
Lemma tac_clear Δ Δ' i p P Q :
envs_lookup_delete i Δ = Some (p,P,Δ') Δ' Q Δ Q.
Proof. intros. by rewrite envs_lookup_delete_sound // sep_elim_r. Qed.
Lemma tac_clear_spatial Δ Δ' Q :
envs_clear_spatial Δ = Δ' Δ' Q Δ Q.
Proof. intros <- ?. by rewrite envs_clear_spatial_sound // sep_elim_l. Qed.
Lemma tac_clear_spatial Δ Δ1 Δ2 Q :
envs_split true [] Δ = Some (Δ1,Δ2) Δ1 Q Δ Q.
Proof. intros. by rewrite envs_split_sound // sep_elim_l. Qed.
Lemma tac_duplicate Δ Δ' i p j P Q :
envs_lookup i Δ = Some (p, P)
......@@ -350,16 +329,14 @@ Lemma tac_next Δ Δ' Q Q' :
Proof. intros ?? HQ. by rewrite -(strip_later_l Q) strip_later_env_sound HQ. Qed.
Lemma tac_löb Δ Δ' i Q :
envs_app true (Esnoc Enil i
( env_fold uPred_wand Q (env_spatial Δ)))%I Δ = Some Δ'
envs_persistent Δ = true
envs_app true (Esnoc Enil i ( Q)%I) Δ = Some Δ'
Δ' Q Δ Q.
Proof.
intros ? HQ. rewrite /of_envs assoc. apply wand_elim_l'.
rewrite -(always_elim (_ - Q))%I -(löb ( (_ - _)))%I; apply impl_intro_l.
apply (always_intro _ _), wand_intro_r.
rewrite always_and_sep_l -(assoc _ ( _))%I -(assoc _ ( _))%I -of_envs_def.
rewrite envs_app_sound //; simpl; rewrite right_id env_fold_wand HQ.
by rewrite -always_later wand_elim_r.
intros ?? HQ. rewrite (persistentP Δ) envs_app_sound //; simpl.
rewrite right_id -{2}(always_elim Q) -(löb ( Q)); apply impl_intro_l.
rewrite -always_later -{1}(always_always ( ( Q))) always_and_sep_l'.
by rewrite -always_sep wand_elim_r HQ.
Qed.
(** * Always *)
......
......@@ -32,12 +32,6 @@ Instance env_dom {A} : Dom (env A) stringset :=
fix go Γ := let _ : Dom _ _ := @go in
match Γ with Enil => | Esnoc Γ i _ => {[ i ]} dom stringset Γ end.
Fixpoint env_fold {A B} (f : B A A) (x : A) (Γ : env B) : A :=
match Γ with
| Enil => x
| Esnoc Γ _ y => env_fold f (f y x) Γ
end.
Fixpoint env_app {A} (Γapp : env A) (Γ : env A) : option (env A) :=
match Γapp with
| Enil => Some Γ
......
......@@ -81,6 +81,7 @@ Proof.
eauto using tac_pvs_timeless.
Qed.
Hint Immediate env_special_nil_persistent : typeclass_instances.
Lemma tac_pvs_assert {A} (fsa : FSA Λ Σ A) fsaV Δ Δ1 Δ2 Δ2' E lr js j P Q Φ :
FSASplit Q E fsa fsaV Φ
envs_split lr js Δ = Some (Δ1,Δ2)
......
......@@ -4,7 +4,7 @@ From iris.proofmode Require Export notation.
From iris.prelude Require Import stringmap.
Declare Reduction env_cbv := cbv [
env_lookup env_fold env_lookup_delete env_delete env_app
env_lookup env_lookup_delete env_delete env_app
env_replace env_split_go env_split
decide (* operational classes *)
sumbool_rec sumbool_rect (* sumbool *)
......@@ -755,7 +755,8 @@ Tactic Notation "iNext":=
Tactic Notation "iLöb" "as" constr (H) :=
eapply tac_löb with _ H;
[env_cbv; reflexivity || fail "iLöb:" H "not fresh"|].
[reflexivity || fail "iLöb: non-empty spatial context"
|env_cbv; reflexivity || fail "iLöb:" H "not fresh"|].
Tactic Notation "iLöb" "{" ident(x1) "}" "as" constr (H) :=
iRevert { x1 }; iLöb as H; iIntros { x1 }.
......
......@@ -42,7 +42,7 @@ Section LiftingTests.
n1 < n2
Φ #(n2 - 1) WP FindPred #n2 #n1 @ E {{ Φ }}.
Proof.
iIntros {Hn} "HΦ". iLöb {n1 Hn} as "IH".
iIntros {Hn} "HΦ". iLöb {n1 Hn} "HΦ" as "IH".
wp_rec. wp_let. wp_op. wp_let. wp_op=> ?; wp_if.
- iApply "IH" "% HΦ". omega.
- iPvsIntro. by assert (n1 = n2 - 1) as -> by omega.
......
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