From iris.algebra Require Export upred.
From iris.algebra Require Import upred_big_op upred_tactics.
From iris.proofmode Require Export environments classes.
From iris.prelude Require Import stringmap hlist.
Import uPred.

Local Notation "Γ !! j" := (env_lookup j Γ).
Local Notation "x ← y ; z" := (match y with Some x ⇒ z | None ⇒ None end).
Local Notation "' ( x1 , x2 ) ← y ; z" :=
  (match y with Some (x1,x2) ⇒ z | None ⇒ None end).
Local Notation "' ( x1 , x2 , x3 ) ← y ; z" :=
  (match y with Some (x1,x2,x3) ⇒ z | None ⇒ None end).

Record envs (M : ucmraT) :=
  Envs { env_relevant : env (uPred M); env_spatial : env (uPred M) }.
Add Printing Constructor envs.
Arguments Envs {_} _ _.
Arguments env_relevant {_} _.
Arguments env_spatial {_} _.

Record envs_wf {M: ucmraT} (Δ : envs M) := {
  env_relevant_valid : env_wf (env_relevant Δ);
  env_spatial_valid : env_wf (env_spatial Δ);
  envs_disjoint i : env_relevant Δ !! i = None ∨ env_spatial Δ !! i = None
}.

Coercion of_envs {M} (Δ : envs M) : uPred M :=
  (⧆■ envs_wf Δ ★ [★] (map (uPred_relevant) (env_relevant Δ)) ★ [★] env_spatial Δ)%I.
Instance: Params (@of_envs) 1.

Section defs.
Context {M: ucmraT}.

Record envs_Forall2 (R : relation (uPred M)) (Δ1 Δ2 : envs M) : Prop := {
  env_relevant_Forall2 : env_Forall2 R (env_relevant Δ1) (env_relevant Δ2);
  env_spatial_Forall2 : env_Forall2 R (env_spatial Δ1) (env_spatial Δ2)
}.

Definition envs_dom {M} (Δ : envs M) : list string :=
  env_dom (env_relevant Δ) ++ env_dom (env_spatial Δ).

Definition envs_lookup (i : string) (Δ : envs M) : option (bool × uPred M) :=
  let (Γp,Γs) := Δ in
  match env_lookup i Γp with
  | Some P ⇒ Some (true, P) | None ⇒ P ← env_lookup i Γs; Some (false, P)
  end.

Definition envs_delete (i : string) (p : bool) (Δ : envs M) : envs M :=
  let (Γp,Γs) := Δ in
  match p with
  | true ⇒ Envs (env_delete i Γp) Γs | false ⇒ Envs Γp (env_delete i Γs)
  end.

Definition envs_lookup_delete (i : string)
    (Δ : envs M) : option (bool × uPred M × envs M) :=
  let (Γp,Γs) := Δ in
  match env_lookup_delete i Γp with
  | Some (P,Γp') ⇒ Some (true, P, Envs Γp' Γs)
  | None ⇒ '(P,Γs') ← env_lookup_delete i Γs; Some (false, P, Envs Γp Γs')
  end.

Definition envs_app (p : bool)
    (Γ : env (uPred M)) (Δ : envs M) : option (envs M) :=
  let (Γp,Γs) := Δ in
  match p with
  | true ⇒ _ ← env_app Γ Γs; Γp' ← env_app Γ Γp; Some (Envs Γp' Γs)
  | false ⇒ _ ← env_app Γ Γp; Γs' ← env_app Γ Γs; Some (Envs Γp Γs')
  end.

Definition envs_simple_replace (i : string) (p : bool) (Γ : env (uPred M))
    (Δ : envs M) : option (envs M) :=
  let (Γp,Γs) := Δ in
  match p with
  | true ⇒ _ ← env_app Γ Γs; Γp' ← env_replace i Γ Γp; Some (Envs Γp' Γs)
  | false ⇒ _ ← env_app Γ Γp; Γs' ← env_replace i Γ Γs; Some (Envs Γp Γs')
  end.

Definition envs_replace (i : string) (p q : bool) (Γ : env (uPred M))
    (Δ : envs M) : option (envs M) :=
  if eqb p q then envs_simple_replace i p Γ Δ
  else envs_app q Γ (envs_delete i p Δ).

Definition envs_split {M}
    (lr : bool) (js : list string) (Δ : envs M) : option (envs M × envs M) :=
  let (Γp,Γs) := Δ in
  '(Γs1,Γs2) ← env_split js Γs;
  match lr with
  | false ⇒ Some (Envs Γp Γs1, Envs Γp Γs2)
  | true ⇒ Some (Envs Γp Γs2, Envs Γp Γs1)
  end.

Definition envs_split'
    (lr : bool) (jr: list string) (js : list string) (Δ : envs M) : option (envs M × envs M) :=
  let (Γp,Γs) := Δ in
  '(Γp1,Γp2) ← env_split jr Γp;
  '(Γs1,Γs2) ← env_split js Γs;
  match lr with
  | false ⇒ Some (Envs Γp1 Γs1, Envs Γp2 Γs2)
  | true ⇒ Some (Envs Γp2 Γs2, Envs Γp1 Γs1)
  end.

Definition envs_relevant (Δ : envs M) :=
  if env_spatial Δ is Enil then true else false.

Definition envs_clear_spatial (Δ : envs M) : envs M :=
  Envs (env_relevant Δ) Enil.

Lemma env_spatial_delete_true Δ i:
  env_spatial (envs_delete i true Δ) = env_spatial Δ.
Proof. by destruct Δ as [??]. Qed.

Lemma env_spatial_delete_false Δ i:
  env_spatial (envs_delete i false Δ) = env_delete i (env_spatial Δ).
Proof. by destruct Δ as [??]. Qed.

Lemma env_relevant_delete_false Δ i:
  env_relevant (envs_delete i false Δ) = env_relevant Δ.
Proof. by destruct Δ as [??]. Qed.

Lemma env_relevant_delete_true Δ i:
  env_relevant (envs_delete i true Δ) = env_delete i (env_relevant Δ).
Proof. by destruct Δ as [??]. Qed.

Lemma env_relevant_lookup_true Δ i P:
  envs_lookup i Δ = Some (true, P) → env_relevant Δ !! i = Some P.
Proof.
  destruct Δ as [??]. rewrite /envs_lookup. case_match.
  - inversion 1; subst; auto.
  - case_match; congruence.
Qed.

Lemma env_spatial_lookup_false Δ i P:
  envs_lookup i Δ = Some (false, P) → env_spatial Δ !! i = Some P.
Proof.
  destruct Δ as [??]. rewrite /envs_lookup. case_match.
  - congruence.
  - case_match; last congruence. inversion 1; subst; auto.
Qed.

End defs.

Section tactics.
Context {M : ucmraT}.
Implicit Types Γ : env (uPred M).
Implicit Types Δ : envs M.
Implicit Types P Q : uPred M.
Lemma of_envs_def Δ :
  of_envs Δ = (⧆■ envs_wf Δ ★
                  [★] (map (uPred_relevant) (env_relevant Δ)) ★
                  [★] 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 Δ.
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 Δ i p P :
  envs_lookup i Δ = Some (p,P) → Δ ⊢ □?p P ★ envs_delete i p Δ.
Proof.
  rewrite /envs_lookup /envs_delete /of_envs=>?; apply pure_elim_sep_l⇒ Hwf.
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
  - rewrite (env_lookup_perm Γp) //=.
    ecancel [[★] _; □ P]%I. ecancel [[★] _]%I.
    rewrite emp_True affine_mono; eauto.
    apply pure_intro.
    destruct Hwf; constructor;
      naive_solver eauto using env_delete_wf, env_delete_fresh.
  - destruct (Γs !! i) eqn:?; simplify_eq/=.
    rewrite (env_lookup_perm Γs) //=.
    ecancel [[★] _; P]%I. ecancel [[★] _]%I.
    rewrite emp_True affine_mono; eauto.
    apply pure_intro.
    destruct Hwf; constructor;
      naive_solver eauto using env_delete_wf, env_delete_fresh.
Qed.

Lemma envs_lookup_delete_different Δ i j p P :
  i ≠ j → envs_lookup i (envs_delete j p Δ) = envs_lookup i Δ.
Proof.
  intros ?. rewrite /envs_lookup /envs_delete.
  destruct p, Δ; rewrite -(env_lookup_delete_different _ i j) //=.
Qed.

Lemma envs_lookup_delete_lookup Δ Δ' Δ'' i j q P1 P2 R Q :
  envs_wf Δ →
  envs_lookup_delete i Δ = Some (false, P1, Δ') →
  envs_lookup j Δ' = Some (q, R) →
  i ≠ j.
Proof.
  rewrite /envs_lookup /envs_lookup_delete /envs_delete /of_envs⇒Hwf Hld.
  case (decide (i = j)); auto; intros →.
  destruct Δ as [Γp Γs], (Γp !! j) eqn:Heq; simplify_eq/=.
  - destruct (env_lookup_delete j Γs) as [(P'&?)|] eqn:Hld'; simplify_eq/=; try congruence.
    rewrite env_lookup_delete_Some in Hld' ×.
    × intros (?&?). exfalso.
      eapply envs_disjoint with _ j in Hwf as [|]; simpl in *; congruence.
    × destruct (env_lookup_delete j Γp) as [(P'&?)|] eqn:Hld''; simplify_eq/=; try congruence.
  - destruct Δ' as [Γp' Γs'], (Γp' !! j) eqn:Heq'.
    × destruct (env_lookup_delete j Γp) as [(P'&?)|] eqn:Hld''; simplify_eq/=.
      destruct (env_lookup_delete j Γs) as [(P'&?)|] eqn:Hld'; simplify_eq/=; try congruence.
    × destruct (env_lookup_delete j Γp) as [(P'&?)|] eqn:Hld''; simplify_eq/=.
      destruct (env_lookup_delete j Γs) as [(P'&?)|] eqn:Hld'; simplify_eq/=; try congruence.
      rewrite env_lookup_delete_Some in Hld' ×.
      intros (?&->).
      rewrite env_delete_fresh_eq; eauto.
      destruct Hwf; eauto.
Qed.

Lemma envs_lookup_sound' Δ i p P :
  envs_lookup i Δ = Some (p,P) → Δ ⊢ (P ★ envs_delete i p Δ).
Proof.
  intros. rewrite envs_lookup_sound //. destruct p; by rewrite //= ?relevant_elim.
Qed.

Lemma envs_wf_elim Δ P: (envs_wf Δ → (Δ ⊢ P)) → Δ ⊢ P.
Proof.
  intros HP. rewrite /of_envs. eapply (pure_elim_spare (envs_wf Δ)); eauto.
Qed.

Lemma envs_lookup_relevant_sound Δ i P :
  envs_lookup i Δ = Some (true,P) → Δ ⊢ (□ P ★ Δ).
Proof.
  intros. rewrite {1}of_envs_def.
  rewrite -(relevant_relevant' (⧆uPred_pure (envs_wf Δ))).
  rewrite relevant_sep_dup'_1.
  rewrite -assoc. rewrite {2}relevant_elim -of_envs_def.
  rewrite {1}envs_lookup_sound //= (of_envs_def Δ).
  rewrite relevant_elim.
  ecancel [⧆_]%I.
  rewrite {1}(relevant_sep_dup'_1 P).
  ecancel [□ P]%I.
  to_front [⧆_]%I.
  rewrite sep_elim_r env_spatial_delete_true.
  ecancel [[★] (env_spatial _)]%I.
  rewrite (env_lookup_perm (env_relevant Δ) i P) //=; last apply env_relevant_lookup_true; auto.
  rewrite env_relevant_delete_true //=.
Qed.
Lemma envs_lookup_relevant_sound' Δ i p P `{RelevantP _ P}:
  envs_lookup i Δ = Some (p,P) → Δ ⊢ (□ P ★ Δ).
Proof.
  destruct p; first apply envs_lookup_relevant_sound.
  intros. rewrite {1}of_envs_def.
  rewrite -(relevant_relevant' (⧆uPred_pure (envs_wf Δ))).
  rewrite relevant_sep_dup'_1.
  rewrite -assoc. rewrite {2}relevant_elim -of_envs_def.
  rewrite {1}envs_lookup_sound //= (of_envs_def Δ).
  rewrite relevant_elim.
  ecancel [⧆_]%I.
  rewrite -{1}(relevant_relevant' P).
  rewrite {1}(relevant_sep_dup'_1 P).
  ecancel [□ P]%I.
  to_front [⧆_]%I.
  rewrite sep_elim_r. rewrite env_relevant_delete_false.
  ecancel [[★] (map uPred_relevant (env_relevant _))]%I.
  rewrite (env_lookup_perm (env_spatial Δ) i P) //=; last apply env_spatial_lookup_false; auto.
  rewrite env_spatial_delete_false //=.
  rewrite relevant_elim.
  auto.
Qed.

Lemma envs_lookup_split Δ i p P :
  envs_lookup i Δ = Some (p,P) → Δ ⊢ □?p P ★ (□?p P -★ Δ).
Proof.
  rewrite /envs_lookup /of_envs=>?; apply pure_elim_sep_l⇒ Hwf.
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
  - rewrite (env_lookup_perm Γp) //=.
    rewrite pure_equiv // -emp_True left_id.
    cancel [□ P]%I. apply wand_intro_l. solve_sep_entails.
  - destruct (Γs !! i) eqn:?; simplify_eq/=.
    rewrite (env_lookup_perm Γs) //=. rewrite pure_equiv // -emp_True left_id.
    cancel [P]. apply wand_intro_l. solve_sep_entails.
Qed.

Lemma envs_lookup_delete_sound Δ Δ' i p P :
  envs_lookup_delete i Δ = Some (p,P,Δ') → Δ ⊢ □?p P ★ Δ'.
Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound. Qed.
Lemma envs_lookup_delete_sound' Δ Δ' i p P :
  envs_lookup_delete i Δ = Some (p,P,Δ') → Δ ⊢ P ★ Δ'.
Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound'. Qed.

Lemma envs_app_sound Δ Δ' p Γ :
  envs_app p Γ Δ = Some Δ' → Δ ⊢ ((if p then [★] (map uPred_relevant Γ) else [★] Γ) -★ Δ').
Proof.
  rewrite /of_envs /envs_app⇒ ?; apply pure_elim_sep_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, sep_intro_Emp_l; [rewrite emp_True; apply affine_mono, 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 map_app big_sep_app; solve_sep_entails.
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_app Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
    apply wand_intro_l, sep_intro_Emp_l; [rewrite emp_True; apply affine_mono, 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_sep_app. solve_sep_entails.
Qed.

Lemma envs_app_sound_affine Δ Δ' p Γ :
  envs_app p Γ Δ = Some Δ' → (Δ ⊢ ⧆ Δ) →
  Δ ⊢ ⧆((if p then [★] (map uPred_relevant Γ) else [★] Γ) -★ Δ').
Proof.
  rewrite /of_envs /envs_app⇒ ? Haff; apply pure_elim_sep_l⇒ Hwf.
  destruct Δ as [Γp Γs], p; simplify_eq/=.
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_app Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
    rewrite pure_equiv //= -?emp_True ?left_id in Haff *=>Haff.
    rewrite Haff.
    apply wand_intro_affine_l, sep_intro_Emp_l; [rewrite emp_True; apply affine_mono, 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 map_app affine_elim big_sep_app; solve_sep_entails.
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_app Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
    rewrite pure_equiv //= -?emp_True ?left_id in Haff *=>Haff.
    rewrite Haff.
    apply wand_intro_affine_l, sep_intro_Emp_l; [rewrite emp_True; apply affine_mono, 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') // affine_elim big_sep_app. solve_sep_entails.
Qed.

Lemma envs_simple_replace_sound' Δ Δ' i p Γ :
  envs_simple_replace i p Γ Δ = Some Δ' →
  envs_delete i p Δ ⊢ ((if p then [★] (map uPred_relevant Γ) else [★] Γ) -★ Δ')%I.
Proof.
  rewrite /envs_simple_replace /envs_delete /of_envs⇒ ?.
  apply pure_elim_sep_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, sep_intro_Emp_l; [rewrite emp_True; apply affine_mono, 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 map_app big_sep_app; solve_sep_entails.
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
    apply wand_intro_l, sep_intro_Emp_l; [rewrite emp_True; apply affine_mono, 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_sep_app. solve_sep_entails.
Qed.

Lemma envs_simple_replace_sound'_affine Δ Δ' i p Γ :
  envs_simple_replace i p Γ Δ = Some Δ' →
  (envs_delete i p Δ ⊢ ⧆ envs_delete i p Δ) →
  envs_delete i p Δ ⊢ ⧆((if p then [★] (map uPred_relevant Γ) else [★] Γ) -★ Δ')%I.
Proof.
  intros Hrep Haff. rewrite Haff. move: Hrep.
  rewrite /envs_simple_replace /envs_delete /of_envs⇒ ?.
  rewrite -sep_affine_3.
  apply pure_elim_sep_l⇒ Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=.
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_replace i Γ Γp) as [Γp'|] eqn:Heqo; simplify_eq/=.
    apply wand_intro_affine_l, sep_intro_Emp_l; [rewrite emp_True; apply affine_mono, 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 map_app big_sep_app. rewrite ?affine_elim. solve_sep_entails.
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
    apply wand_intro_affine_l, sep_intro_Emp_l; [rewrite emp_True; apply affine_mono, 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_sep_app. rewrite affine_elim. solve_sep_entails.
Qed.

Lemma envs_simple_replace_sound Δ Δ' i p P Γ :
  envs_lookup i Δ = Some (p,P) → envs_simple_replace i p Γ Δ = Some Δ' →
  Δ ⊢ ((if p then □ P else P) ★
       ((if p then [★] (map uPred_relevant Γ) else [★] Γ) -★ Δ'))%I.
Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_sound'//. Qed.

Lemma envs_simple_replace_sound_affine Δ Δ' i p P Γ :
  envs_lookup i Δ = Some (p,P) → envs_simple_replace i p Γ Δ = Some Δ' →
  (envs_delete i p Δ ⊢ ⧆ envs_delete i p Δ) →
  Δ ⊢ ((if p then □ P else P) ★
       ⧆((if p then [★] (map uPred_relevant Γ) else [★] Γ) -★ Δ'))%I.
Proof. intros. rewrite envs_lookup_sound // envs_simple_replace_sound'_affine//.
       destruct p; by rewrite //=.
Qed.

Lemma envs_replace_sound' Δ Δ' i p q Γ :
  envs_replace i p q Γ Δ = Some Δ' →
  envs_delete i p Δ ⊢ ((if q then [★] (map uPred_relevant Γ) else [★] Γ) -★ Δ')%I.
Proof.
  rewrite /envs_replace; destruct (eqb _ _) eqn:Hpq.
  - apply eqb_prop in Hpq as →. apply envs_simple_replace_sound'.
  - apply envs_app_sound.
Qed.

Lemma envs_replace_sound'_affine Δ Δ' i p q Γ :
  envs_replace i p q Γ Δ = Some Δ' →
  (envs_delete i p Δ ⊢ ⧆ envs_delete i p Δ) →
  envs_delete i p Δ ⊢ ⧆((if q then [★] (map uPred_relevant Γ) else [★] Γ) -★ Δ')%I.
Proof.
  rewrite /envs_replace; destruct (eqb _ _) eqn:Hpq.
  - apply eqb_prop in Hpq as →. apply envs_simple_replace_sound'_affine.
  - apply envs_app_sound_affine.
Qed.

Lemma envs_replace_sound Δ Δ' i p q P Γ :
  envs_lookup i Δ = Some (p,P) → envs_replace i p q Γ Δ = Some Δ' →
  Δ ⊢ ((if p then □ P else P) ★
       ((if q then [★] (map uPred_relevant Γ) else [★] Γ) -★ Δ'))%I.
Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.

Lemma envs_replace_sound_affine Δ Δ' i p q P Γ :
  envs_lookup i Δ = Some (p,P) → envs_replace i p q Γ Δ = Some Δ' →
  (envs_delete i p Δ ⊢ ⧆ envs_delete i p Δ) →
  Δ ⊢ ((if p then □ P else P) ★
       ⧆((if q then [★] (map uPred_relevant Γ) else [★] Γ) -★ Δ'))%I.
Proof.
  intros. rewrite envs_lookup_sound// envs_replace_sound'_affine//.
  destruct p; rewrite //=.
Qed.

Lemma map_relevant_dup Ps:
  [★] (map uPred_relevant Ps) ⊢
      (([★](map uPred_relevant Ps)) ★ ([★](map uPred_relevant Ps): uPred M))%I.
Proof.
  induction Ps as [| P Ps].
  - rewrite ?right_id //=.
  - rewrite //= {1}(relevant_sep_dup'_1 P) {1}IHPs. solve_sep_entails.
Qed.

Lemma map_relevant_relevant Ps :
  [★] (map uPred_relevant Ps) ⊢□([★](map uPred_relevant Ps): uPred M).
Proof.
  induction Ps as [| P Ps].
  - rewrite ?right_id //=. by rewrite {1}relevant_relevant'.
  - simpl. rewrite {1}IHPs. rewrite -{1}(relevant_relevant' (□P)). rewrite sep_relevant.
    eapply relevant_mono, sep_mono; auto using relevant_elim.
Qed.

Lemma envs_split_sound Δ lr js Δ1 Δ2 :
  envs_split lr js Δ = Some (Δ1,Δ2) → Δ ⊢ Δ1 ★ Δ2.
Proof.
  rewrite /envs_split /of_envs⇒ ?; apply pure_elim_sep_l⇒ Hwf.
  destruct Δ as [Γp Γs], (env_split js _) as [[Γs1 Γs2]|] eqn:?; simplify_eq/=.
  rewrite (env_split_perm Γs) // big_sep_app map_relevant_dup.
  destruct lr; simplify_eq/=;
  cancel [[★] (map uPred_relevant Γp); [★] (map uPred_relevant Γp); [★] Γs1; [★] Γs2]%I;
    destruct Hwf; apply sep_intro_Emp_l; rewrite emp_True; apply affine_mono, pure_intro; constructor;
      naive_solver eauto using env_split_wf_1, env_split_wf_2,
      env_split_fresh_1, env_split_fresh_2.
Qed.

Lemma envs_split'_sound Δ lr jr js Δ1 Δ2 :
  envs_split' lr jr js Δ = Some (Δ1,Δ2) → Δ ⊢ (Δ1 ★ Δ2).
Proof.
  rewrite /envs_split' /of_envs⇒ ?; apply pure_elim_sep_l⇒ Hwf.
  destruct Δ as [Γp Γs].
  destruct (env_split jr _) as [[Γr1 Γr2]|] eqn:?; simplify_eq /=;
  destruct (env_split js _) as [[Γs1 Γs2]|] eqn:?; simplify_eq /=.
  rewrite (env_split_perm Γp) // map_app big_sep_app.
  rewrite (env_split_perm Γs) // big_sep_app.
  destruct lr; simplify_eq/=;
  cancel [[★] (map uPred_relevant Γr1); [★] (map uPred_relevant Γr2); [★] Γs1; [★] Γs2]%I;
    destruct Hwf; apply sep_intro_Emp_l; rewrite emp_True; apply affine_mono, pure_intro;
    constructor;
      naive_solver eauto using env_split_wf_1, env_split_wf_2,
      env_split_fresh_1, env_split_fresh_2.
Qed.

Lemma envs_clear_spatial_sound Δ : Δ ⊢ envs_clear_spatial Δ ★ [★] env_spatial Δ.
Proof.
  rewrite /of_envs /envs_clear_spatial /=; apply pure_elim_sep_l⇒ Hwf.
  rewrite right_id -assoc; apply sep_intro_Emp_l;
  [rewrite emp_True; apply affine_mono, pure_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_Emp|].
  by rewrite IH wand_curry (comm uPred_sep).
Qed.

Lemma envs_relevant_relevant Δ : envs_relevant Δ = true → RelevantP Δ.
Proof.
  intros; destruct Δ as [? []]; simplify_eq/=.
  rewrite /RelevantP of_envs_def. simpl.
  rewrite ?right_id. rewrite {1}map_relevant_relevant.
  rewrite -{1}(relevant_relevant' (⧆_)).
  apply relevant_sep.
Qed.
Hint Immediate envs_relevant_relevant : typeclass_instances.

Global Instance envs_Forall2_refl (R : relation (uPred M)) :
  Reflexive R → Reflexive (envs_Forall2 R).
Proof. by constructor. Qed.
Global Instance envs_Forall2_sym (R : relation (uPred M)) :
  Symmetric R → Symmetric (envs_Forall2 R).
Proof. intros ??? [??]; by constructor. Qed.
Global Instance envs_Forall2_trans (R : relation (uPred M)) :
  Transitive R → Transitive (envs_Forall2 R).
Proof. intros ??? [??] [??] [??]; constructor; etrans; eauto. Qed.
Global Instance envs_Forall2_antisymm (R R' : relation (uPred M)) :
  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 (uPred M)) Δ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 M).
Proof.
  intros [Γp1 Γs1] [Γp2 Γs2] [Hp Hs]; unfold of_envs; simpl in ×.
  apply pure_elim_sep_l⇒Hwf. apply sep_intro_Emp_l.
  - destruct Hwf; rewrite emp_True; apply affine_mono, pure_intro; constructor;
      naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
  - f_equiv; last repeat f_equiv; auto .
    f_equiv. clear -Hp. induction Hp; first econstructor.
    econstructor; auto.
    apply relevant_mono; auto.
Qed.
Global Instance of_envs_proper : Proper (envs_Forall2 (⊣⊢) ==> (⊣⊢)) (@of_envs M).
Proof.
  intros Δ1 Δ2 ?; apply (anti_symm (⊢)); apply of_envs_mono;
    eapply envs_Forall2_impl; [| |symmetry|]; eauto using equiv_entails.
Qed.
Global Instance Envs_mono (R : relation (uPred M)) :
  Proper (env_Forall2 R ==> env_Forall2 R ==> envs_Forall2 R) (@Envs M).
Proof. by constructor. Qed.

Lemma tac_adequate P : (Envs Enil Enil ⊢ P) → Emp ⊢ P.
Proof.
  intros <-. rewrite /of_envs /= !right_id.
  rewrite emp_True; apply affine_mono, pure_intro; repeat constructor.
Qed.

Lemma tac_assumption_empty : Envs Enil Enil ⊢ (Emp: uPred M).
Proof. by rewrite of_envs_def //= sep_elim_r ?right_id. Qed.
Lemma tac_assumption_rel i P : Envs (Esnoc Enil i P) Enil ⊢ □ P.
Proof. rewrite of_envs_def //= ?right_id. apply sep_elim_r. Qed.
Lemma tac_assumption_rel' i P : Envs (Esnoc Enil i P) Enil ⊢ P.
Proof. rewrite of_envs_def //= ?right_id. rewrite relevant_elim. apply sep_elim_r. Qed.
Lemma tac_assumption_rel_affine i P : Envs (Esnoc Enil i (⧆P)) Enil ⊢ P.
Proof. rewrite of_envs_def //= ?left_id ?right_id. transitivity (⧆P)%I;
         last apply affine_elim. rewrite relevant_elim. apply sep_elim_r.
Qed.
Lemma tac_assumption_spatial i P : Envs Enil (Esnoc Enil i P) ⊢ P.
Proof. rewrite of_envs_def //= ?left_id ?right_id. apply sep_elim_r. Qed.
Lemma tac_assumption_spatial_affine i P : Envs Enil (Esnoc Enil i (⧆P)) ⊢ P.
Proof. rewrite of_envs_def //= ?left_id ?right_id. transitivity (⧆P)%I;
         last apply affine_elim. apply sep_elim_r.
Qed.

Lemma tac_assumption Δ Δ' i p P Q :
  envs_lookup_delete i Δ = Some (p,P,Δ') →
  FromAssumption p P Q →
  (Δ' ⊢ ⧆Δ') →
  Δ ⊢ Q.
Proof.
  intros ?? Haff; rewrite envs_lookup_delete_sound //; eauto.
  by rewrite Haff sep_elim_l.
Qed.

Lemma tac_rename Δ Δ' i j p P Q :
  envs_lookup i Δ = Some (p,P) →
  envs_simple_replace i p (Esnoc Enil j P) Δ = Some Δ' →
  (Δ' ⊢ Q) → Δ ⊢ Q.
Proof.
  intros. rewrite envs_simple_replace_sound //.
  destruct p; simpl; by rewrite right_id wand_elim_r.
Qed.

Lemma tac_affine_intro Δ Q :
  (Δ ⊢ ⧆ Δ) → (Δ ⊢ Q) → Δ ⊢ ⧆ Q.
Proof. intros Haff ?. rewrite Haff. by apply affine_mono. Qed.

Lemma tac_clear Δ Δ' i p P Q :
  envs_lookup_delete i Δ = Some (p,P,Δ') → AffineP P → (Δ' ⊢ Q) → Δ ⊢ Q.
Proof.
  intros. rewrite envs_lookup_delete_sound //. destruct p;
  rewrite -(affine_affine P) //= ?relevant_affine sep_elim_r //=.
Qed.

Lemma tac_ex_falso Δ Q : (Δ ⊢ False) → Δ ⊢ Q.
Proof. by rewrite -(False_elim Q). Qed.

Lemma tac_pure_intro Δ Q (φ : Prop) :
  FromPure Q φ →
  (Δ ⊢ ⧆Δ) →
  φ → Δ ⊢ Q.
Proof.
  intros ? Haff ?. rewrite -(from_pure Q) //.
  rewrite Haff emp_True.
  apply affine_mono, True_intro.
Qed.

Lemma tac_pure Δ Δ' i p P φ Q :
  envs_lookup_delete i Δ = Some (p, P, Δ') → IntoPure P φ →
  (φ → Δ' ⊢ Q) → Δ ⊢ Q.
Proof.
  intros ?? HQ. rewrite envs_lookup_delete_sound' //; simpl.
  rewrite (into_pure P). by apply pure_elim_sep_l.
Qed.

Lemma tac_pure_revert Δ φ Q : (Δ ⊢ ■ φ → Q) → (φ → Δ ⊢ Q).
Proof. intros HΔ ?. by rewrite HΔ pure_equiv // left_id. Qed.

Class IntoLaterEnv (Γ1 Γ2 : env (uPred M)) :=
  into_later_env : env_Forall2 IntoLater Γ1 Γ2.
Class IntoLaterEnvs (Δ1 Δ2 : envs M) := {
  into_later_relevant: IntoLaterEnv (env_relevant Δ1) (env_relevant Δ2);
  into_later_spatial: IntoLaterEnv (env_spatial Δ1) (env_spatial Δ2)
}.

Global Instance into_later_env_nil : IntoLaterEnv Enil Enil.
Proof. constructor. Qed.
Global Instance into_later_env_snoc Γ1 Γ2 i P Q :
  IntoLaterEnv Γ1 Γ2 → IntoLater P Q →
  IntoLaterEnv (Esnoc Γ1 i P) (Esnoc Γ2 i Q).
Proof. by constructor. Qed.

Global Instance into_later_envs Γp1 Γp2 Γs1 Γs2 :
  IntoLaterEnv Γp1 Γp2 → IntoLaterEnv Γs1 Γs2 →
  IntoLaterEnvs (Envs Γp1 Γs1) (Envs Γp2 Γs2).
Proof. by split. Qed.

Lemma into_later_env_sound Δ1 Δ2 : IntoLaterEnvs Δ1 Δ2 → Δ1 ⊢ ▷ Δ2.
Proof.
  intros [Hp Hs]; rewrite /of_envs /= !later_sep.
  repeat apply sep_mono; try apply affine_mono; try apply relevant_mono.
  - rewrite -later_intro; apply affine_mono, pure_mono; destruct 1; constructor;
      naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
  - induction Hp; rewrite /= ?later_sep; auto using sep_mono, later_intro.
    apply sep_mono; auto.
    rewrite -(relevant_elim (uPred_later _)) -relevant_relevant_later.
    apply relevant_mono; auto.
  - induction Hs; rewrite /= ?later_sep; auto using sep_mono, later_intro.
Qed.

Lemma tac_next Δ Δ' Q Q' :
  IntoLaterEnvs Δ Δ' → FromLater Q Q' → (Δ' ⊢ Q') → Δ ⊢ Q.
Proof. intros ?? HQ. by rewrite -(from_later Q) into_later_env_sound HQ. Qed.

Lemma tac_löb Δ Δ' i Q:
  envs_relevant Δ = true →
  (Δ ⊢ ⧆ Δ) →
  envs_app true (Esnoc Enil i (⧆▷Q)%I) Δ = Some Δ' →
  (Δ' ⊢ ⧆□ Q) → Δ ⊢ Q.
Proof.
  intros ? Haff ? HQ.
  rewrite -(relevant_elim Q).
  rewrite -(unlimited_löb_1 ( Q)%I).
  rewrite -(relevant_relevant' Δ).
  rewrite -relevant_affine.
  apply relevant_mono.
  rewrite Haff.
  apply affine_mono.
  apply wand_intro_l.
  rewrite envs_app_sound //; simpl.
  rewrite ?right_id.
  rewrite relevant_affine.
  rewrite wand_elim_r //=.
Qed.

Lemma tac_timeless Δ Δ' i P Q :
  TimelessElim Q →
  envs_lookup i Δ = Some (false, ▷ P)%I → TimelessP P →
  envs_simple_replace i false (Esnoc Enil i P) Δ = Some Δ' →
  (Δ' ⊢ Q) → Δ ⊢ Q.
Proof.
  intros ???? HQ. rewrite envs_simple_replace_sound //; simpl.
  by rewrite right_id HQ timeless_elim.
Qed.

Lemma tac_atimeless Δ Δ' i P Q :
  ATimelessElim Q →
  envs_lookup i Δ = Some (false, ⧆▷ P)%I → ATimelessP P →
  envs_simple_replace i false (Esnoc Enil i (⧆P)%I) Δ = Some Δ' →
  (Δ' ⊢ Q) → Δ ⊢ Q.
Proof.
  intros ???? HQ. rewrite envs_simple_replace_sound //; simpl.
  by rewrite right_id HQ atimeless_elim.
Qed.

Lemma tac_relevant_intro Δ Q : envs_relevant Δ = true → (Δ ⊢ Q) → Δ ⊢ □ Q.
Proof. intros. by apply: relevant_intro. Qed.
Lemma tac_relevant Δ Δ' i p P P' Q :
  envs_lookup i Δ = Some (p, P)%I → IntoRelevantP P P' →
  envs_replace i p true (Esnoc Enil i P') Δ = Some Δ' →
  (Δ' ⊢ Q) → Δ ⊢ Q.
Proof.
  intros ??? <-. rewrite envs_replace_sound //; simpl. destruct p.
  - by rewrite right_id (into_relevantP P) relevant_relevant' wand_elim_r.
  - by rewrite right_id (into_relevantP P) wand_elim_r.
Qed.

Lemma tac_impl_intro Δ Δ' i P Q :
  envs_relevant Δ = true →
  envs_app false (Esnoc Enil i P) Δ = Some Δ' →
  (Δ' ⊢ Q) → Δ ⊢ P → Q.
Proof.
  intros ?? HQ. rewrite (relevantP Δ) envs_app_sound //; simpl.
  by rewrite ?right_id relevant_wand_impl_1 relevant_elim HQ.
Qed.
Lemma tac_impl_intro_relevant Δ Δ' i P P' Q :
  IntoRelevantP P P' →
  envs_app true (Esnoc Enil i P') Δ = Some Δ' →
  (Δ' ⊢ Q) → Δ ⊢ P → Q.
Proof.
  intros ?? HQ. rewrite envs_app_sound //; simpl. apply impl_intro_l.
  by rewrite right_id {1}(into_relevantP P) relevant_and_sep_l_1 wand_elim_r.
Qed.
Lemma tac_impl_intro_pure Δ P φ Q : IntoPure P φ → (φ → Δ ⊢ Q) → Δ ⊢ P → Q.
Proof.
  intros. apply impl_intro_l; rewrite (into_pure P).
  by rewrite affine_elim; apply pure_elim_l.
Qed.

Lemma tac_wand_intro Δ Δ' i P Q :
  envs_app false (Esnoc Enil i P) Δ = Some Δ' → (Δ' ⊢ Q) → Δ ⊢ P -★ Q.
Proof.
  intros ? HQ. rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
Qed.
Lemma tac_wand_intro_relevant Δ Δ' i P P' Q :
  IntoRelevantP P P' →
  envs_app true (Esnoc Enil i P') Δ = Some Δ' →
  (Δ' ⊢ Q) → Δ ⊢ P -★ Q.
Proof.
  intros. rewrite envs_app_sound //; simpl.
  rewrite right_id. by apply wand_mono.
Qed.
Lemma tac_wand_intro_pure Δ P φ Q : IntoPure P φ → (φ → Δ ⊢ Q) → Δ ⊢ P -★ Q.
Proof.
  intros. by apply wand_intro_l; rewrite (into_pure P); apply pure_elim_sep_l.
Qed.

Lemma tac_specialize Δ Δ' Δ'' i p j q P1 P2 R Q :
  envs_lookup_delete i Δ = Some (p, P1, Δ') →
  envs_lookup j (if p then Δ else Δ') = Some (q, R) →
  IntoWand R P1 P2 →
  match p with
  | true ⇒ envs_simple_replace j q (Esnoc Enil j P2) Δ
  | false ⇒ envs_replace j q false (Esnoc Enil j P2) Δ'
             
  end = Some Δ'' →
  (Δ'' ⊢ Q) → Δ ⊢ Q.
Proof.
  intros [? ->]%envs_lookup_delete_Some ??? <-. destruct p.
  - rewrite envs_lookup_relevant_sound // envs_simple_replace_sound //; simpl.
    destruct q.
    + by rewrite assoc (into_wand R) relevant_wand_1 wand_elim_r right_id wand_elim_r.
    + by rewrite assoc (into_wand R) relevant_elim wand_elim_r right_id wand_elim_r.
  - rewrite envs_lookup_sound //; simpl.
    rewrite envs_lookup_sound // (envs_replace_sound' _ Δ'') //; simpl.
    destruct q.
    + by rewrite //= right_id assoc (into_wand R) relevant_elim wand_elim_r wand_elim_r.
    + by rewrite //= assoc (into_wand R) wand_elim_r right_id wand_elim_r.
Qed.

Lemma tac_specialize_relevant Δ Δ' Δ'' i p j q P1 P2 R Q :
  envs_lookup_delete i Δ = Some (p, P1, Δ') →
  envs_lookup j (if p then Δ else Δ') = Some (q, R) →
  IntoWand R P1 P2 →
  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'' →
  match p with
    | true ⇒ True
    | false ⇒ AffineP R ∧ RelevantP P2
  end →
  
  (Δ'' ⊢ Q) → Δ ⊢ Q.
Proof.
  intros Hld ??? HR <-. apply envs_wf_elim⇒Hwf.
  destruct p.
  - apply envs_lookup_delete_Some in Hld as [? ->].
    rewrite envs_lookup_relevant_sound // envs_simple_replace_sound //; simpl.
    destruct q.
    + by rewrite assoc (into_wand R) relevant_wand_1 wand_elim_r right_id wand_elim_r.
    + by rewrite assoc (into_wand R) relevant_elim wand_elim_r right_id wand_elim_r.
  - assert (i ≠ j).
    { eapply envs_lookup_delete_lookup; eauto. }
    apply envs_lookup_delete_Some in Hld as [? ->].
    rewrite (envs_lookup_sound _ j) //; last (erewrite <-envs_lookup_delete_different; eauto).
    rewrite envs_lookup_split //; last (rewrite envs_lookup_delete_different; eauto).
    simpl. destruct HR as [? ?].
    assert (□?q P2 ⊣⊢ □ P2) as HP2.
     { destruct q; auto. by rewrite relevant_relevant'. }
     trans (P1 ★ (□?q P2) ★ (P1 -★ envs_delete j q Δ))%I.
     + rewrite assoc -(comm _ P1) assoc. apply sep_mono; last reflexivity.
       trans ((P1 ★ □?q R) ★ □?q P2)%I.
       × rewrite HP2. apply relevant_entails_r'.
         rewrite (into_wand R). rewrite relevant_relevant'.
         by rewrite relevant_if_elim wand_elim_r.
       × rewrite relevant_if_elim affine_sep_elim_l' //.
     + rewrite assoc (comm _ P1) -assoc wand_elim_r.
        rewrite envs_simple_replace_sound' //=; destruct q; by rewrite //= right_id wand_elim_r.
Qed.
Class IntoAssert (P : uPred M) (Q : uPred M) (R : uPred M) :=
  into_assert : R ★ (P -★ Q) ⊢ Q.
Global Arguments into_assert _ _ _ {_}.
Lemma into_assert_default P Q : IntoAssert P Q P.
Proof. by rewrite /IntoAssert wand_elim_r. Qed.

Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q lr js R P1 P2 P1' Q :
  envs_lookup_delete j Δ = Some (q, R, Δ') →
  IntoWand R P1 P2 → IntoAssert P1 Q P1' →
  ('(Δ1,Δ2) ← envs_split lr js Δ';
    Δ2' ← envs_app (envs_relevant Δ1 && q) (Esnoc Enil j P2) Δ2;
    
    Some (Δ1,Δ2')) = Some (Δ1,Δ2') →
  (Δ1 ⊢ P1) → (Δ2' ⊢ Q) → Δ ⊢ Q.
Proof.
  intros [? ->]%envs_lookup_delete_Some ??? HP1 HQ.
  destruct (envs_split _ _ _) as [[? Δ2]|] eqn:?; simplify_eq/=;
    destruct (envs_app _ _ _) eqn:?; simplify_eq/=.
  rewrite envs_lookup_sound // envs_split_sound //.
  rewrite (envs_app_sound Δ2) //; simpl.
  destruct q; rewrite //=; destruct (envs_relevant Δ1) eqn:?; simplify_eq/=.
  - rewrite right_id (into_wand R) (relevantP Δ1) HP1.
    by rewrite assoc relevant_sep wand_elim_l wand_elim_r.
  - by rewrite right_id (into_wand R) relevant_elim assoc HP1 wand_elim_l wand_elim_r.
  - by rewrite right_id (into_wand R) assoc HP1 wand_elim_l wand_elim_r.
  - by rewrite right_id (into_wand R) assoc HP1 wand_elim_l wand_elim_r.
Qed.



Lemma tac_specialize_pure Δ Δ' j q R P1 P2 φ Q :
  envs_lookup j Δ = Some (q, R) →
  IntoWand R P1 P2 → FromPure P1 φ →
  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ' →
  φ → (Δ' ⊢ Q) → Δ ⊢ Q.
Proof.
  intros. rewrite envs_simple_replace_sound //; simpl.
  destruct q; rewrite //=;
  by rewrite right_id (into_wand R) -(from_pure P1) // wand_Emp wand_elim_r.
Qed.


Lemma tac_specialize_relevant_domain Δ Δ' Δ'' j q P1 P2 R Q :
  envs_lookup_delete j Δ = Some (q, R, Δ') →
  IntoWand R P1 P2 →
  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'' →
  (Δ' ⊢ P1) → RelevantP P1 →
  (Δ'' ⊢ Q) → Δ ⊢ Q.
Proof.
  intros [? ->]%envs_lookup_delete_Some ?? HP1 ? <-.
  - rewrite envs_lookup_sound //.
    rewrite -(idemp uPred_and (envs_delete _ _ _)).
    rewrite {1}HP1 (relevantP P1) relevant_and_sep_l_1 assoc.
    rewrite envs_simple_replace_sound' //; simpl.
    destruct q; rewrite //=.
    × rewrite right_id (into_wand R) relevant_wand_1 wand_elim_l.
      by rewrite wand_elim_r.
    × rewrite right_id (into_wand R) relevant_elim wand_elim_l.
      by rewrite wand_elim_r.
Qed.

Lemma tac_specialize_relevant_range Δ Δ' Δ'' j q P1 P2 R Q :
  envs_lookup_delete j Δ = Some (q, R, Δ') →
  IntoWand R P1 P2 →
  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'' →
  (Δ' ⊢ P1) → AffineP R → RelevantP P2 →
  (Δ'' ⊢ Q) → Δ ⊢ Q.
Proof.
  intros [? ->]%envs_lookup_delete_Some ?? HP1 ?? <-.
  - rewrite envs_lookup_sound //=.
    trans (□P2 ★ □?q R ★ envs_delete j q Δ)%I.
    × apply relevant_entails_l'.
      rewrite (into_wand R) HP1.
      destruct q; rewrite //=; first rewrite relevant_elim; rewrite wand_elim_l; eauto.
    × rewrite envs_simple_replace_sound' //=.
      rewrite assoc. rewrite (comm _ (□ P2)%I).
      destruct q; rewrite //= right_id.
      ** rewrite relevant_elim affine_sep_elim_r'; eauto. apply wand_elim_r.
      ** rewrite affine_sep_elim_r'; eauto. by rewrite relevant_elim wand_elim_r.
Qed.


Lemma tac_revert Δ Δ' i p P Q :
  envs_lookup_delete i Δ = Some (p,P,Δ') →
  (Δ' ⊢ if p then □ P -★ Q else P -★ Q) → Δ ⊢ Q.
Proof.
  intros ? HQ. rewrite envs_lookup_delete_sound //; simpl. destruct p.
  - by rewrite HQ wand_elim_r.
  - by rewrite HQ wand_elim_r.
Qed.

Lemma tac_revert_spatial Δ Q :
  (envs_clear_spatial Δ ⊢ env_fold uPred_wand Q (env_spatial Δ)) → Δ ⊢ Q.
Proof.
  intros HΔ. by rewrite envs_clear_spatial_sound HΔ env_fold_wand wand_elim_l.
Qed.

Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P Q R :
  IntoAssert P Q R →
  envs_split lr js Δ = Some (Δ1,Δ2) →
  envs_app (envs_relevant Δ1) (Esnoc Enil j P) Δ2 = Some Δ2' →
  (Δ1 ⊢ P) → (Δ2' ⊢ Q) → Δ ⊢ Q.
Proof.
  intros ??? HP HQ. rewrite envs_split_sound //.
  destruct (envs_relevant Δ1) eqn:?.
  - rewrite (relevantP Δ1) HP envs_app_sound //; simpl.
    by rewrite right_id wand_elim_r.
  - rewrite HP envs_app_sound //; simpl. by rewrite right_id wand_elim_r.
Qed.

Lemma tac_assert_relevant Δ Δ' j P Q :
  RelevantP P →
  envs_app true (Esnoc Enil j P) Δ = Some Δ' →
  (Δ ⊢ P) → (Δ' ⊢ Q) → Δ ⊢ Q.
Proof.
  intros ?? HP ?.
  rewrite -(idemp uPred_and Δ) {1}HP envs_app_sound //; simpl.
  by rewrite right_id {1}(relevantP P) relevant_and_sep_l_1 wand_elim_r.
Qed.


Lemma tac_pose_proof_affine Δ Δ' j P Q :
  (Emp ⊢ P) →
  envs_app true (Esnoc Enil j (⧆P)%I) Δ = Some Δ' →
  (Δ' ⊢ Q) → Δ ⊢ Q.
Proof.
  intros HP ? <-. rewrite envs_app_sound //; simpl.
  assert (Emp ⊢ ⧆ P) as <-.
  { by apply affine_intro; first apply _. }
  rewrite right_id -emp_relevant.
  rewrite wand_Emp //=.
Qed.


Lemma tac_pose_proof_hyp_spare Δ Δ' Δ'' i p j P Q :
  envs_lookup_delete i Δ = Some (p, P, Δ') →
  envs_app p (Esnoc Enil j P) (if p then Δ else Δ') = Some Δ'' →
  (Δ'' ⊢ Q) → Δ ⊢ Q.
Proof.
  intros [? ->]%envs_lookup_delete_Some ? <-. destruct p.
  - rewrite envs_lookup_relevant_sound // envs_app_sound //; simpl.
    by rewrite right_id wand_elim_r.
  - rewrite envs_lookup_sound // envs_app_sound //; simpl.
    by rewrite right_id wand_elim_r.
Qed.

Lemma tac_pose_proof_hyp Δ Δ' Δ'' i p j P Q :
  envs_lookup_delete i Δ = Some (p, P, Δ') →
  envs_app p (Esnoc Enil j P) Δ' = Some Δ'' →
  (Δ'' ⊢ Q) → Δ ⊢ Q.
Proof.
  intros [? ->]%envs_lookup_delete_Some ? <-. destruct p.
  - rewrite envs_lookup_sound // envs_app_sound //; simpl.
    by rewrite right_id wand_elim_r.
  - rewrite envs_lookup_sound // envs_app_sound //; simpl.
    by rewrite right_id wand_elim_r.
Qed.

Lemma tac_apply Δ Δ' i p R P1 P2 :
  envs_lookup_delete i Δ = Some (p, R, Δ') → IntoWand R P1 P2 →
  (Δ' ⊢ P1) → Δ ⊢ P2.
Proof.
  intros ?? HP1. rewrite envs_lookup_delete_sound' //.
  by rewrite (into_wand R) HP1 wand_elim_l.
Qed.