Commit 6b0f250f by Robbert Krebbers

### Move theorems about `envs_` to `environments.v` where also these operations are defined.

parent 85425d47
 ... ... @@ -5,8 +5,6 @@ Set Default Proof Using "Type". Import bi. Import env_notations. Local Notation "b1 && b2" := (if b1 then b2 else false) : bool_scope. (* Coq versions of the tactics *) Section bi_tactics. Context {PROP : bi}. ... ... @@ -14,366 +12,6 @@ Implicit Types Γ : env PROP. Implicit Types Δ : envs PROP. Implicit Types P Q : PROP. Lemma of_envs_eq Δ : of_envs Δ = (⌜envs_wf Δ⌝ ∧ □ [∧] env_intuitionistic Δ ∗ [∗] env_spatial Δ)%I. Proof. done. Qed. (** An environment is a ∗ of something intuitionistic and the spatial environment. TODO: Can we define it as such? *) Lemma of_envs_eq' Δ : of_envs Δ ⊣⊢ (⌜envs_wf Δ⌝ ∧ □ [∧] env_intuitionistic Δ) ∗ [∗] env_spatial Δ. Proof. rewrite of_envs_eq persistent_and_sep_assoc //. Qed. Lemma envs_delete_persistent Δ i : envs_delete false i true Δ = Δ. Proof. by destruct Δ. Qed. Lemma envs_delete_spatial Δ i : envs_delete false i false Δ = envs_delete true i false Δ. Proof. by destruct Δ. Qed. Lemma envs_lookup_delete_Some Δ Δ' rp i p P : envs_lookup_delete rp i Δ = Some (p,P,Δ') ↔ envs_lookup i Δ = Some (p,P) ∧ Δ' = envs_delete rp i p Δ. Proof. rewrite /envs_lookup /envs_delete /envs_lookup_delete. destruct Δ as [Γp Γs]; rewrite /= !env_lookup_delete_correct. destruct (Γp !! i), (Γs !! i); naive_solver. Qed. Lemma envs_lookup_sound' Δ rp i p P : envs_lookup i Δ = Some (p,P) → of_envs Δ ⊢ □?p P ∗ of_envs (envs_delete rp i p Δ). Proof. rewrite /envs_lookup /envs_delete /of_envs=>?. apply pure_elim_l=> Hwf. destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=. - rewrite pure_True ?left_id; last (destruct Hwf, rp; constructor; naive_solver eauto using env_delete_wf, env_delete_fresh). destruct rp. + rewrite (env_lookup_perm Γp) //= intuitionistically_and. by rewrite and_sep_intuitionistically -assoc. + rewrite {1}intuitionistically_sep_dup {1}(env_lookup_perm Γp) //=. by rewrite intuitionistically_and and_elim_l -assoc. - destruct (Γs !! i) eqn:?; simplify_eq/=. rewrite pure_True ?left_id; last (destruct Hwf; constructor; naive_solver eauto using env_delete_wf, env_delete_fresh). rewrite (env_lookup_perm Γs) //=. by rewrite !assoc -(comm _ P). Qed. Lemma envs_lookup_sound Δ i p P : envs_lookup i Δ = Some (p,P) → of_envs Δ ⊢ □?p P ∗ of_envs (envs_delete true i p Δ). Proof. apply envs_lookup_sound'. Qed. Lemma envs_lookup_persistent_sound Δ i P : envs_lookup i Δ = Some (true,P) → of_envs Δ ⊢ □ P ∗ of_envs Δ. Proof. intros ?%(envs_lookup_sound' _ false). by destruct Δ. Qed. Lemma envs_lookup_sound_2 Δ i p P : envs_wf Δ → envs_lookup i Δ = Some (p,P) → □?p P ∗ of_envs (envs_delete true i p Δ) ⊢ of_envs Δ. Proof. rewrite /envs_lookup /of_envs=>Hwf ?. rewrite [⌜envs_wf Δ⌝%I]pure_True // left_id. destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=. - rewrite (env_lookup_perm Γp) //= intuitionistically_and and_sep_intuitionistically and_elim_r. cancel [□ P]%I. solve_sep_entails. - destruct (Γs !! i) eqn:?; simplify_eq/=. rewrite (env_lookup_perm Γs) //= and_elim_r. cancel [P]. solve_sep_entails. Qed. Lemma envs_lookup_split Δ i p P : envs_lookup i Δ = Some (p,P) → of_envs Δ ⊢ □?p P ∗ (□?p P -∗ of_envs Δ). Proof. intros. apply pure_elim with (envs_wf Δ). { rewrite of_envs_eq. apply and_elim_l. } intros. rewrite {1}envs_lookup_sound//. apply sep_mono_r. apply wand_intro_l, envs_lookup_sound_2; done. Qed. Lemma envs_lookup_delete_sound Δ Δ' rp i p P : envs_lookup_delete rp i Δ = Some (p,P,Δ') → of_envs Δ ⊢ □?p P ∗ of_envs Δ'. Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound'. Qed. Lemma envs_lookup_delete_list_sound Δ Δ' rp js p Ps : envs_lookup_delete_list rp js Δ = Some (p,Ps,Δ') → of_envs Δ ⊢ □?p [∗] Ps ∗ of_envs Δ'. Proof. revert Δ Δ' p Ps. induction js as [|j js IH]=> Δ Δ'' p Ps ?; simplify_eq/=. { by rewrite intuitionistically_emp left_id. } destruct (envs_lookup_delete rp j Δ) as [[[q1 P] Δ']|] eqn:Hj; simplify_eq/=. apply envs_lookup_delete_Some in Hj as [Hj ->]. destruct (envs_lookup_delete_list _ js _) as [[[q2 Ps'] ?]|] eqn:?; simplify_eq/=. rewrite -intuitionistically_if_sep_2 -assoc. rewrite envs_lookup_sound' //; rewrite IH //. repeat apply sep_mono=>//; apply intuitionistically_if_flag_mono; by destruct q1. Qed. Lemma envs_lookup_delete_list_cons Δ Δ' Δ'' rp j js p1 p2 P Ps : envs_lookup_delete rp j Δ = Some (p1, P, Δ') → envs_lookup_delete_list rp js Δ' = Some (p2, Ps, Δ'') → envs_lookup_delete_list rp (j :: js) Δ = Some (p1 && p2, (P :: Ps), Δ''). Proof. rewrite //= => -> //= -> //=. Qed. Lemma envs_lookup_delete_list_nil Δ rp : envs_lookup_delete_list rp [] Δ = Some (true, [], Δ). Proof. done. Qed. Lemma envs_lookup_snoc Δ i p P : envs_lookup i Δ = None → envs_lookup i (envs_snoc Δ p i P) = Some (p, P). Proof. rewrite /envs_lookup /envs_snoc=> ?. destruct Δ as [Γp Γs], p, (Γp !! i); simplify_eq; by rewrite env_lookup_snoc. Qed. Lemma envs_lookup_snoc_ne Δ i j p P : i ≠ j → envs_lookup i (envs_snoc Δ p j P) = envs_lookup i Δ. Proof. rewrite /envs_lookup /envs_snoc=> ?. destruct Δ as [Γp Γs], p; simplify_eq; by rewrite env_lookup_snoc_ne. Qed. Lemma envs_snoc_sound Δ p i P : envs_lookup i Δ = None → of_envs Δ ⊢ □?p P -∗ of_envs (envs_snoc Δ p i P). Proof. rewrite /envs_lookup /envs_snoc /of_envs=> ?; apply pure_elim_l=> Hwf. destruct Δ as [Γp Γs], (Γp !! i) eqn:?, (Γs !! i) eqn:?; simplify_eq/=. apply wand_intro_l; destruct p; simpl. - apply and_intro; [apply pure_intro|]. + destruct Hwf; constructor; simpl; eauto using Esnoc_wf. intros j; destruct (ident_beq_reflect j i); naive_solver. + by rewrite intuitionistically_and and_sep_intuitionistically assoc. - apply and_intro; [apply pure_intro|]. + destruct Hwf; constructor; simpl; eauto using Esnoc_wf. intros j; destruct (ident_beq_reflect j i); naive_solver. + solve_sep_entails. Qed. Lemma envs_app_sound Δ Δ' p Γ : envs_app p Γ Δ = Some Δ' → of_envs Δ ⊢ (if p then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ'. Proof. rewrite /of_envs /envs_app=> ?; apply pure_elim_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=. - destruct (env_app Γ Γs) eqn:Happ, (env_app Γ Γp) as [Γp'|] eqn:?; simplify_eq/=. apply wand_intro_l, and_intro; [apply pure_intro|]. + destruct Hwf; constructor; simpl; eauto using env_app_wf. intros j. apply (env_app_disjoint _ _ _ j) in Happ. naive_solver eauto using env_app_fresh. + rewrite (env_app_perm _ _ Γp') //. rewrite big_opL_app intuitionistically_and and_sep_intuitionistically. solve_sep_entails. - destruct (env_app Γ Γp) eqn:Happ, (env_app Γ Γs) as [Γs'|] eqn:?; simplify_eq/=. apply wand_intro_l, and_intro; [apply pure_intro|]. + destruct Hwf; constructor; simpl; eauto using env_app_wf. intros j. apply (env_app_disjoint _ _ _ j) in Happ. naive_solver eauto using env_app_fresh. + rewrite (env_app_perm _ _ Γs') // big_opL_app. solve_sep_entails. Qed. Lemma envs_app_singleton_sound Δ Δ' p j Q : envs_app p (Esnoc Enil j Q) Δ = Some Δ' → of_envs Δ ⊢ □?p Q -∗ of_envs Δ'. Proof. move=> /envs_app_sound. destruct p; by rewrite /= right_id. Qed. Lemma envs_simple_replace_sound' Δ Δ' i p Γ : envs_simple_replace i p Γ Δ = Some Δ' → of_envs (envs_delete true i p Δ) ⊢ (if p then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ'. Proof. rewrite /envs_simple_replace /envs_delete /of_envs=> ?. apply pure_elim_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=. - destruct (env_app Γ Γs) eqn:Happ, (env_replace i Γ Γp) as [Γp'|] eqn:?; simplify_eq/=. apply wand_intro_l, and_intro; [apply pure_intro|]. + destruct Hwf; constructor; simpl; eauto using env_replace_wf. intros j. apply (env_app_disjoint _ _ _ j) in Happ. destruct (decide (i = j)); try naive_solver eauto using env_replace_fresh. + rewrite (env_replace_perm _ _ Γp') //. rewrite big_opL_app intuitionistically_and and_sep_intuitionistically. solve_sep_entails. - destruct (env_app Γ Γp) eqn:Happ, (env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=. apply wand_intro_l, and_intro; [apply pure_intro|]. + destruct Hwf; constructor; simpl; eauto using env_replace_wf. intros j. apply (env_app_disjoint _ _ _ j) in Happ. destruct (decide (i = j)); try naive_solver eauto using env_replace_fresh. + rewrite (env_replace_perm _ _ Γs') // big_opL_app. solve_sep_entails. Qed. Lemma envs_simple_replace_singleton_sound' Δ Δ' i p j Q : envs_simple_replace i p (Esnoc Enil j Q) Δ = Some Δ' → of_envs (envs_delete true i p Δ) ⊢ □?p Q -∗ of_envs Δ'. Proof. move=> /envs_simple_replace_sound'. destruct p; by rewrite /= right_id. Qed. Lemma envs_simple_replace_sound Δ Δ' i p P Γ : envs_lookup i Δ = Some (p,P) → envs_simple_replace i p Γ Δ = Some Δ' → of_envs Δ ⊢ □?p P ∗ ((if p then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ'). Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_sound'//. Qed. Lemma envs_simple_replace_maybe_sound Δ Δ' i p P Γ : envs_lookup i Δ = Some (p,P) → envs_simple_replace i p Γ Δ = Some Δ' → of_envs Δ ⊢ □?p P ∗ (((if p then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ') ∧ (□?p P -∗ of_envs Δ)). Proof. intros. apply pure_elim with (envs_wf Δ). { rewrite of_envs_eq. apply and_elim_l. } intros. rewrite {1}envs_lookup_sound//. apply sep_mono_r, and_intro. - rewrite envs_simple_replace_sound'//. - apply wand_intro_l, envs_lookup_sound_2; done. Qed. Lemma envs_simple_replace_singleton_sound Δ Δ' i p P j Q : envs_lookup i Δ = Some (p,P) → envs_simple_replace i p (Esnoc Enil j Q) Δ = Some Δ' → of_envs Δ ⊢ □?p P ∗ (□?p Q -∗ of_envs Δ'). Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_singleton_sound'//. Qed. Lemma envs_replace_sound' Δ Δ' i p q Γ : envs_replace i p q Γ Δ = Some Δ' → of_envs (envs_delete true i p Δ) ⊢ (if q then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ'. Proof. rewrite /envs_replace; destruct (beq _ _) eqn:Hpq. - apply eqb_prop in Hpq as ->. apply envs_simple_replace_sound'. - apply envs_app_sound. Qed. Lemma envs_replace_singleton_sound' Δ Δ' i p q j Q : envs_replace i p q (Esnoc Enil j Q) Δ = Some Δ' → of_envs (envs_delete true i p Δ) ⊢ □?q Q -∗ of_envs Δ'. Proof. move=> /envs_replace_sound'. destruct q; by rewrite /= ?right_id. Qed. Lemma envs_replace_sound Δ Δ' i p q P Γ : envs_lookup i Δ = Some (p,P) → envs_replace i p q Γ Δ = Some Δ' → of_envs Δ ⊢ □?p P ∗ ((if q then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ'). Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed. Lemma envs_replace_singleton_sound Δ Δ' i p q P j Q : envs_lookup i Δ = Some (p,P) → envs_replace i p q (Esnoc Enil j Q) Δ = Some Δ' → of_envs Δ ⊢ □?p P ∗ (□?q Q -∗ of_envs Δ'). Proof. intros. by rewrite envs_lookup_sound// envs_replace_singleton_sound'//. Qed. Lemma envs_lookup_envs_clear_spatial Δ j : envs_lookup j (envs_clear_spatial Δ) = ''(p,P) ← envs_lookup j Δ; if p : bool then Some (p,P) else None. Proof. rewrite /envs_lookup /envs_clear_spatial. destruct Δ as [Γp Γs]; simpl; destruct (Γp !! j) eqn:?; simplify_eq/=; auto. by destruct (Γs !! j). Qed. Lemma envs_clear_spatial_sound Δ : of_envs Δ ⊢ of_envs (envs_clear_spatial Δ) ∗ [∗] env_spatial Δ. Proof. rewrite /of_envs /envs_clear_spatial /=. apply pure_elim_l=> Hwf. rewrite right_id -persistent_and_sep_assoc. apply and_intro; [|done]. apply pure_intro. destruct Hwf; constructor; simpl; auto using Enil_wf. Qed. Lemma env_spatial_is_nil_intuitionistically Δ : env_spatial_is_nil Δ = true → of_envs Δ ⊢ □ of_envs Δ. Proof. intros. unfold of_envs; destruct Δ as [? []]; simplify_eq/=. rewrite !right_id /bi_intuitionistically {1}affinely_and_r persistently_and. by rewrite persistently_affinely_elim persistently_idemp persistently_pure. Qed. Lemma envs_lookup_envs_delete Δ i p P : envs_wf Δ → envs_lookup i Δ = Some (p,P) → envs_lookup i (envs_delete true i p Δ) = None. Proof. rewrite /envs_lookup /envs_delete=> -[?? Hdisj] Hlookup. destruct Δ as [Γp Γs], p; simplify_eq/=. - rewrite env_lookup_env_delete //. revert Hlookup. destruct (Hdisj i) as [->| ->]; [|done]. by destruct (Γs !! _). - rewrite env_lookup_env_delete //. by destruct (Γp !! _). Qed. Lemma envs_lookup_envs_delete_ne Δ rp i j p : i ≠ j → envs_lookup i (envs_delete rp j p Δ) = envs_lookup i Δ. Proof. rewrite /envs_lookup /envs_delete=> ?. destruct Δ as [Γp Γs],p; simplify_eq/=. - destruct rp=> //. by rewrite env_lookup_env_delete_ne. - destruct (Γp !! i); simplify_eq/=; by rewrite ?env_lookup_env_delete_ne. Qed. Lemma envs_split_go_sound js Δ1 Δ2 Δ1' Δ2' : (∀ j P, envs_lookup j Δ1 = Some (false, P) → envs_lookup j Δ2 = None) → envs_split_go js Δ1 Δ2 = Some (Δ1',Δ2') → of_envs Δ1 ∗ of_envs Δ2 ⊢ of_envs Δ1' ∗ of_envs Δ2'. Proof. revert Δ1 Δ2. induction js as [|j js IH]=> Δ1 Δ2 Hlookup HΔ; simplify_eq/=; [done|]. apply pure_elim with (envs_wf Δ1)=> [|Hwf]. { by rewrite /of_envs !and_elim_l sep_elim_l. } destruct (envs_lookup_delete _ j Δ1) as [[[[] P] Δ1'']|] eqn:Hdel; simplify_eq/=; auto. apply envs_lookup_delete_Some in Hdel as [??]; subst. rewrite envs_lookup_sound //; rewrite /= (comm _ P) -assoc. rewrite -(IH _ _ _ HΔ); last first. { intros j' P'; destruct (decide (j = j')) as [->|]. - by rewrite (envs_lookup_envs_delete _ _ _ P). - rewrite envs_lookup_envs_delete_ne // envs_lookup_snoc_ne //. eauto. } rewrite (envs_snoc_sound Δ2 false j P) /= ?wand_elim_r; eauto. Qed. Lemma envs_split_sound Δ d js Δ1 Δ2 : envs_split d js Δ = Some (Δ1,Δ2) → of_envs Δ ⊢ of_envs Δ1 ∗ of_envs Δ2. Proof. rewrite /envs_split=> ?. rewrite -(idemp bi_and (of_envs Δ)). rewrite {2}envs_clear_spatial_sound. rewrite (env_spatial_is_nil_intuitionistically (envs_clear_spatial _)) //. rewrite -persistently_and_intuitionistically_sep_l. rewrite (and_elim_l ( _)%I) persistently_and_intuitionistically_sep_r intuitionistically_elim. destruct (envs_split_go _ _) as [[Δ1' Δ2']|] eqn:HΔ; [|done]. apply envs_split_go_sound in HΔ as ->; last first. { intros j P. by rewrite envs_lookup_envs_clear_spatial=> ->. } destruct d; simplify_eq/=; solve_sep_entails. Qed. Lemma prop_of_env_sound Γ : prop_of_env Γ ⊣⊢ [∗] Γ. Proof. destruct Γ as [|Γ ? P]; simpl; first done. revert P. induction Γ as [|Γ IH ? Q]=>P; simpl. - by rewrite right_id. - rewrite /= IH (comm _ Q _) assoc. done. Qed. Global Instance envs_Forall2_refl (R : relation PROP) : Reflexive R → Reflexive (envs_Forall2 R). Proof. by constructor. Qed. Global Instance envs_Forall2_sym (R : relation PROP) : Symmetric R → Symmetric (envs_Forall2 R). Proof. intros ??? [??]; by constructor. Qed. Global Instance envs_Forall2_trans (R : relation PROP) : Transitive R → Transitive (envs_Forall2 R). Proof. intros ??? [??] [??] [??]; constructor; etrans; eauto. Qed. Global Instance envs_Forall2_antisymm (R R' : relation PROP) : AntiSymm R R' → AntiSymm (envs_Forall2 R) (envs_Forall2 R'). Proof. intros ??? [??] [??]; constructor; by eapply (anti_symm _). Qed. Lemma envs_Forall2_impl (R R' : relation PROP) Δ1 Δ2 : envs_Forall2 R Δ1 Δ2 → (∀ P Q, R P Q → R' P Q) → envs_Forall2 R' Δ1 Δ2. Proof. intros [??] ?; constructor; eauto using env_Forall2_impl. Qed. Global Instance of_envs_mono : Proper (envs_Forall2 (⊢) ==> (⊢)) (@of_envs PROP). Proof. intros [Γp1 Γs1] [Γp2 Γs2] [Hp Hs]; apply and_mono; simpl in *. - apply pure_mono=> -[???]. constructor; naive_solver eauto using env_Forall2_wf, env_Forall2_fresh. - by repeat f_equiv. Qed. Global Instance of_envs_proper : Proper (envs_Forall2 (⊣⊢) ==> (⊣⊢)) (@of_envs PROP). Proof. intros Δ1 Δ2 HΔ; apply (anti_symm (⊢)); apply of_envs_mono; eapply (envs_Forall2_impl (⊣⊢)); [| |symmetry|]; eauto using equiv_entails. Qed. Global Instance Envs_proper (R : relation PROP) : Proper (env_Forall2 R ==> env_Forall2 R ==> eq ==> envs_Forall2 R) (@Envs PROP). Proof. by constructor. Qed. Global Instance envs_entails_proper : Proper (envs_Forall2 (⊣⊢) ==> (⊣⊢) ==> iff) (@envs_entails PROP). Proof. rewrite envs_entails_eq. solve_proper. Qed. Global Instance envs_entails_flip_mono : Proper (envs_Forall2 (⊢) ==> flip (⊢) ==> flip impl) (@envs_entails PROP). Proof. rewrite envs_entails_eq=> Δ1 Δ2 ? P1 P2 <- <-. by f_equiv. Qed. (** * Adequacy *) Lemma tac_adequate P : envs_entails (Envs Enil Enil 1) P → P. Proof. ... ...
 From iris.proofmode Require Import base. From iris.algebra Require Export base. From iris.bi Require Export bi. From iris.bi Require Import tactics. Set Default Proof Using "Type". Import bi. Inductive env (A : Type) : Type := | Enil : env A ... ... @@ -22,6 +24,9 @@ Module env_notations. Notation "x ← y ; z" := (y ≫= λ x, z). Notation "' x1 .. xn ← y ; z" := (y ≫= (λ x1, .. (λ xn, z) .. )). Notation "Γ !! j" := (env_lookup j Γ). (* andb will not be simplified by pm_reduce *) Notation "b1 && b2" := (if b1 then b2 else false) : bool_scope. End env_notations. Import env_notations. ... ... @@ -335,3 +340,370 @@ Definition prop_of_env {PROP : bi} (Γ : env PROP) : PROP := match Γ with Enil => acc | Esnoc Γ _ P => aux Γ (P ∗ acc)%I end in match Γ with Enil => emp%I | Esnoc Γ _ P => aux Γ P end. Section envs. Context {PROP : bi}. Implicit Types Γ : env PROP. Implicit Types Δ : envs PROP. Implicit Types P Q : PROP. Lemma of_envs_eq Δ : of_envs Δ = (⌜envs_wf Δ⌝ ∧ □ [∧] env_intuitionistic Δ ∗ [∗] env_spatial Δ)%I. Proof. done. Qed. (** An environment is a ∗ of something intuitionistic and the spatial environment. TODO: Can we define it as such? *) Lemma of_envs_eq' Δ : of_envs Δ ⊣⊢ (⌜envs_wf Δ⌝ ∧ □ [∧] env_intuitionistic Δ) ∗ [∗] env_spatial Δ. Proof. rewrite of_envs_eq persistent_and_sep_assoc //. Qed. Lemma envs_delete_persistent Δ i : envs_delete false i true Δ = Δ. Proof. by destruct Δ. Qed. Lemma envs_delete_spatial Δ i : envs_delete false i false Δ = envs_delete true i false Δ. Proof. by destruct Δ. Qed. Lemma envs_lookup_delete_Some Δ Δ' rp i p P : envs_lookup_delete rp i Δ = Some (p,P,Δ') ↔ envs_lookup i Δ = Some (p,P) ∧ Δ' = envs_delete rp i p Δ. Proof. rewrite /envs_lookup /envs_delete /envs_lookup_delete. destruct Δ as [Γp Γs]; rewrite /= !env_lookup_delete_correct. destruct (Γp !! i), (Γs !! i); naive_solver. Qed. Lemma envs_lookup_sound' Δ rp i p P : envs_lookup i Δ = Some (p,P) → of_envs Δ ⊢ □?p P ∗ of_envs (envs_delete rp i p Δ). Proof. rewrite /envs_lookup /envs_delete /of_envs=>?. apply pure_elim_l=> Hwf. destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=. - rewrite pure_True ?left_id; last (destruct Hwf, rp; constructor; naive_solver eauto using env_delete_wf, env_delete_fresh). destruct rp. + rewrite (env_lookup_perm Γp) //= intuitionistically_and. by rewrite and_sep_intuitionistically -assoc. + rewrite {1}intuitionistically_sep_dup {1}(env_lookup_perm Γp) //=. by rewrite intuitionistically_and and_elim_l -assoc. - destruct (Γs !! i) eqn:?; simplify_eq/=. rewrite pure_True ?left_id; last (destruct Hwf; constructor; naive_solver eauto using env_delete_wf, env_delete_fresh). rewrite (env_lookup_perm Γs) //=. by rewrite !assoc -(comm _ P). Qed. Lemma envs_lookup_sound Δ i p P : envs_lookup i Δ = Some (p,P) → of_envs Δ ⊢ □?p P ∗ of_envs (envs_delete true i p Δ). Proof. apply envs_lookup_sound'. Qed. Lemma envs_lookup_persistent_sound Δ i P : envs_lookup i Δ = Some (true,P) → of_envs Δ ⊢ □ P ∗ of_envs Δ. Proof. intros ?%(envs_lookup_sound' _ false). by destruct Δ. Qed. Lemma envs_lookup_sound_2 Δ i p P : envs_wf Δ → envs_lookup i Δ = Some (p,P) → □?p P ∗ of_envs (envs_delete true i p Δ) ⊢ of_envs Δ. Proof. rewrite /envs_lookup /of_envs=>Hwf ?. rewrite [⌜envs_wf Δ⌝%I]pure_True // left_id. destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=. - rewrite (env_lookup_perm Γp) //= intuitionistically_and and_sep_intuitionistically and_elim_r. cancel [□ P]%I. solve_sep_entails. - destruct (Γs !! i) eqn:?; simplify_eq/=. rewrite (env_lookup_perm Γs) //= and_elim_r. cancel [P]. solve_sep_entails. Qed. Lemma envs_lookup_split Δ i p P : envs_lookup i Δ = Some (p,P) → of_envs Δ ⊢ □?p P ∗ (□?p P -∗ of_envs Δ). Proof. intros. apply pure_elim with (envs_wf Δ). { rewrite of_envs_eq. apply and_elim_l. } intros. rewrite {1}envs_lookup_sound//. apply sep_mono_r. apply wand_intro_l, envs_lookup_sound_2; done. Qed. Lemma envs_lookup_delete_sound Δ Δ' rp i p P : envs_lookup_delete rp i Δ = Some (p,P,Δ') → of_envs Δ ⊢ □?p P ∗ of_envs Δ'. Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound'. Qed. Lemma envs_lookup_delete_list_sound Δ Δ' rp js p Ps : envs_lookup_delete_list rp js Δ = Some (p,Ps,Δ') → of_envs Δ ⊢ □?p [∗] Ps ∗ of_envs Δ'. Proof. revert Δ Δ' p Ps. induction js as [|j js IH]=> Δ Δ'' p Ps ?; simplify_eq/=. { by rewrite intuitionistically_emp left_id. } destruct (envs_lookup_delete rp j Δ) as [[[q1 P] Δ']|] eqn:Hj; simplify_eq/=. apply envs_lookup_delete_Some in Hj as [Hj ->]. destruct (envs_lookup_delete_list _ js _) as [[[q2 Ps'] ?]|] eqn:?; simplify_eq/=. rewrite -intuitionistically_if_sep_2 -assoc. rewrite envs_lookup_sound' //; rewrite IH //. repeat apply sep_mono=>//; apply intuitionistically_if_flag_mono; by destruct q1. Qed. Lemma envs_lookup_delete_list_cons Δ Δ' Δ'' rp j js p1 p2 P Ps : envs_lookup_delete rp j Δ = Some (p1, P, Δ') → envs_lookup_delete_list rp js Δ' = Some (p2, Ps, Δ'') → envs_lookup_delete_list rp (j :: js) Δ = Some (p1 && p2, (P :: Ps), Δ''). Proof. rewrite //= => -> //= -> //=. Qed. Lemma envs_lookup_delete_list_nil Δ rp : envs_lookup_delete_list rp [] Δ = Some (true, [], Δ). Proof. done. Qed. Lemma envs_lookup_snoc Δ i p P : envs_lookup i Δ = None → envs_lookup i (envs_snoc Δ p i P) = Some (p, P). Proof. rewrite /envs_lookup /envs_snoc=> ?. destruct Δ as [Γp Γs], p, (Γp !! i); simplify_eq; by rewrite env_lookup_snoc. Qed. Lemma envs_lookup_snoc_ne Δ i j p P : i ≠ j → envs_lookup i (envs_snoc Δ p j P) = envs_lookup i Δ. Proof. rewrite /envs_lookup /envs_snoc=> ?. destruct Δ as [Γp Γs], p; simplify_eq; by rewrite env_lookup_snoc_ne. Qed. Lemma envs_snoc_sound Δ p i P : envs_lookup i Δ = None → of_envs Δ ⊢ □?p P -∗ of_envs (envs_snoc Δ p i P).