phanerozoic/Coq-Iris huggingface dataset:
(* iris/proofmode/environments.v *)
Ltac simplify
:=
  repeat match goal with
  | _ => progress simplify_eq/=
  | H : context [ident_beq ?s1 ?s2] |- _ => destruct (ident_beq_reflect s1 s2)
  | |- context [ident_beq ?s1 ?s2] => destruct (ident_beq_reflect s1 s2)
  | H : context [pm_option_bind _ ?x] |- _ => destruct x eqn:?
  | |- context [pm_option_bind _ ?x] => destruct x eqn:?
  | _ => case_match
  end.
(* iris/proofmode/environments.v *)
Lemma env_lookup_perm Γ i x : Γ !! i = Some x → Γ ≡ₚ x :: env_delete i Γ.
Proof.
  induction Γ; intros; simplify; rewrite 1?Permutation_swap; f_equiv; eauto.
Qed.
(* iris/proofmode/environments.v *)
Lemma env_lookup_snoc Γ i P : env_lookup i (Esnoc Γ i P) = Some P.
Proof. induction Γ; simplify; auto. Qed.
(* iris/proofmode/environments.v *)
Lemma env_lookup_snoc_ne Γ i j P :
  i ≠ j → env_lookup i (Esnoc Γ j P) = env_lookup i Γ.
Proof. induction Γ=> ?; simplify; auto. Qed.
(* iris/proofmode/environments.v *)
Lemma env_app_perm Γ Γapp Γ' :
  env_app Γapp Γ = Some Γ' → env_to_list Γ' ≡ₚ Γapp ++ Γ.
Proof. revert Γ'; induction Γapp; intros; simplify; f_equal; auto. Qed.
(* iris/proofmode/environments.v *)
Lemma env_app_fresh Γ Γapp Γ' i :
  env_app Γapp Γ = Some Γ' → Γapp !! i = None → Γ !! i = None → Γ' !! i = None.
Proof. revert Γ'. induction Γapp; intros; simplify; eauto. Qed.
(* iris/proofmode/environments.v *)
Lemma env_app_fresh_1 Γ Γapp Γ' i x :
  env_app Γapp Γ = Some Γ' → Γ' !! i = None → Γ !! i = None.
Proof. revert Γ'. induction Γapp; intros; simplify; eauto. Qed.
(* iris/proofmode/environments.v *)
Lemma env_app_disjoint Γ Γapp Γ' i :
  env_app Γapp Γ = Some Γ' → Γapp !! i = None ∨ Γ !! i = None.
Proof.
  revert Γ'.
  induction Γapp; intros; simplify; naive_solver eauto using env_app_fresh_1.
Qed.
(* iris/proofmode/environments.v *)
Lemma env_app_wf Γ Γapp Γ' : env_app Γapp Γ = Some Γ' → env_wf Γ → env_wf Γ'.
Proof. revert Γ'. induction Γapp; intros; simplify; eauto. Qed.
(* iris/proofmode/environments.v *)
Lemma env_replace_fresh Γ Γj Γ' i j :
  env_replace j Γj Γ = Some Γ' →
  Γj !! i = None → env_delete j Γ !! i = None → Γ' !! i = None.
Proof. revert Γ'. induction Γ; intros; simplify; eauto using env_app_fresh. Qed.
(* iris/proofmode/environments.v *)
Lemma env_replace_wf Γ Γi Γ' i :
  env_replace i Γi Γ = Some Γ' → env_wf (env_delete i Γ) → env_wf Γ'.
Proof.
  revert Γ'. induction Γ; intros ??; simplify; [|inversion_clear 1];
    eauto using env_app_wf, env_replace_fresh.
Qed.
(* iris/proofmode/environments.v *)
Lemma env_replace_lookup Γ Γi Γ' i :
  env_replace i Γi Γ = Some Γ' → is_Some (Γ !! i).
Proof. revert Γ'. induction Γ; intros; simplify; eauto. Qed.
(* iris/proofmode/environments.v *)
Lemma env_replace_perm Γ Γi Γ' i :
  env_replace i Γi Γ = Some Γ' → Γ' ≡ₚ Γi ++ env_delete i Γ.
Proof.
  revert Γ'. induction Γ as [|Γ IH j y]=>Γ' ?; simplify; auto using env_app_perm.
  rewrite -Permutation_middle -IH //.
Qed.
(* iris/proofmode/environments.v *)
Lemma env_lookup_delete_correct Γ i :
  env_lookup_delete i Γ = (x ← Γ !! i; Some (x,env_delete i Γ)).
Proof. induction Γ; intros; simplify; eauto. Qed.
(* iris/proofmode/environments.v *)
Lemma env_lookup_delete_Some Γ Γ' i x :
  env_lookup_delete i Γ = Some (x,Γ') ↔ Γ !! i = Some x ∧ Γ' = env_delete i Γ.
Proof. rewrite env_lookup_delete_correct; simplify; naive_solver. Qed.
(* iris/proofmode/environments.v *)
Lemma env_lookup_env_delete Γ j : env_wf Γ → env_delete j Γ !! j = None.
Proof. induction 1; intros; simplify; eauto. Qed.
(* iris/proofmode/environments.v *)
Lemma env_lookup_env_delete_ne Γ i j : i ≠ j → env_delete j Γ !! i = Γ !! i.
Proof. induction Γ; intros; simplify; eauto. Qed.
(* iris/proofmode/environments.v *)
Lemma env_delete_fresh Γ i j : Γ !! i = None → env_delete j Γ !! i = None.
Proof. induction Γ; intros; simplify; eauto. Qed.
(* iris/proofmode/environments.v *)
Lemma env_delete_wf Γ j : env_wf Γ → env_wf (env_delete j Γ).
Proof. induction 1; simplify; eauto using env_delete_fresh. Qed.
(* iris/proofmode/environments.v *)
Instance env_Forall2_refl (P : relation A) :
  Reflexive P → Reflexive (env_Forall2 P).
Proof. intros ? Γ. induction Γ; constructor; auto. Qed.
(* iris/proofmode/environments.v *)
Instance env_Forall2_sym (P : relation A) :
  Symmetric P → Symmetric (env_Forall2 P).
Proof. induction 2; constructor; auto. Qed.
(* iris/proofmode/environments.v *)
Instance env_Forall2_trans (P : relation A) :
  Transitive P → Transitive (env_Forall2 P).
Proof.
  intros ? Γ1 Γ2 Γ3 HΓ; revert Γ3.
  induction HΓ; inversion_clear 1; constructor; eauto.
Qed.
(* iris/proofmode/environments.v *)
Instance env_Forall2_antisymm (P Q : relation A) :
  AntiSymm P Q → AntiSymm (env_Forall2 P) (env_Forall2 Q).
Proof. induction 2; inversion_clear 1; constructor; auto. Qed.
(* iris/proofmode/environments.v *)
Lemma env_Forall2_impl {B} (P Q : A → B → Prop) Γ Σ :
  env_Forall2 P Γ Σ → (∀ x y, P x y → Q x y) → env_Forall2 Q Γ Σ.
Proof. induction 1; constructor; eauto. Qed.
(* iris/proofmode/environments.v *)
Instance Esnoc_proper (P : relation A) :
  Proper (env_Forall2 P ==> (=) ==> P ==> env_Forall2 P) Esnoc.
Proof. intros Γ1 Γ2 HΓ i ? <-; by constructor. Qed.
(* iris/proofmode/environments.v *)
Instance env_to_list_proper (P : relation A) :
  Proper (env_Forall2 P ==> Forall2 P) env_to_list.
Proof. induction 1; constructor; auto. Qed.
(* iris/proofmode/environments.v *)
Lemma env_Forall2_fresh {B} (P : A → B → Prop) Γ Σ i :
  env_Forall2 P Γ Σ → Γ !! i = None → Σ !! i = None.
Proof. by induction 1; simplify. Qed.
(* iris/proofmode/environments.v *)
Lemma env_Forall2_wf {B} (P : A → B → Prop) Γ Σ :
  env_Forall2 P Γ Σ → env_wf Γ → env_wf Σ.
Proof. induction 1; inversion_clear 1; eauto using env_Forall2_fresh. Qed.
(* iris/proofmode/environments.v *)
Lemma env_subenv_fresh Γ Σ i : env_subenv Γ Σ → Σ !! i = None → Γ !! i = None.
Proof. by induction 1; simplify. Qed.
(* iris/proofmode/environments.v *)
Lemma env_subenv_wf Γ Σ : env_subenv Γ Σ → env_wf Σ → env_wf Γ.
Proof. induction 1; inversion_clear 1; eauto using env_subenv_fresh. Qed.
(* iris/proofmode/environments.v *)
Instance env_to_list_subenv_proper :
  Proper (env_subenv ==> sublist) (@env_to_list A).
Proof. induction 1; simpl; constructor; auto. Qed.
(* iris/proofmode/environments.v *)
Record envs (PROP : bi)
:= Envs {
  env_intuitionistic : env PROP;
  env_spatial : env PROP;
  env_counter : positive (** A counter to generate fresh hypothesis names *)
}.
(* iris/proofmode/environments.v *)
(* We now define the judgment [envs_entails Δ Q] for proof mode entailments.
This judgment expresses that [Q] can be proved under the proof mode environment
[Δ]. To improve performance and to encapsulate the internals of the proof mode
(i.e. to ensure that tactics like [intro] cannot accidentally unfold the
entailment), we seal off [envs_entails].

The way the the definitions below are setup involves some trickery so we can
implement the [iFresh] tactic, which increases the counter [env_counter], in
an efficient way. Concretely, we made sure that [envs_entails (Envs Γp Γs c) Q]
and [envs_entails (Envs Γp Γs c') Q] are convertible for any [c] and [c']. This
way, [iFresh] can simply be implemented by changing the goal from
[envs_entails (Envs Γp Γs c) Q] into [envs_entails (Envs Γp Γs (Pos_succ c)) Q]
using the tactic [change_no_check]. This way, the generated proof term
contains no additional steps for changing the counter.

We first define a version [pre_envs_entails] that takes the two contexts
[env_intuitionistic] and [env_spatial] as its arguments. We seal this definition
and then lift it to take the whole proof mode context [Δ : envs PROP]. This is
crucial to make sure that the counter [env_counter] is not part of the seal. *)
Record envs_wf' {PROP : bi} (Γp Γs : env PROP)
:= {
  env_intuitionistic_valid : env_wf Γp;
  env_spatial_valid : env_wf Γs;
  envs_disjoint i : Γp !! i = None ∨ Γs !! i = None
}.
(* iris/proofmode/environments.v *)
Definition envs_wf {PROP : bi} (Δ : envs PROP)
:=
  envs_wf' (env_intuitionistic Δ) (env_spatial Δ).
(* iris/proofmode/environments.v *)
Notation env_and_persistently Γ
:= ([∧ list] P ∈ env_to_list Γ, <pers> P)%I.
(* iris/proofmode/environments.v *)
Definition of_envs' {PROP : bi} (Γp Γs : env PROP) : PROP
:=
  (⌜envs_wf' Γp Γs⌝ ∧ env_and_persistently Γp ∧ [∗] Γs)%I.
(* iris/proofmode/environments.v *)
Instance : Params (@of_envs') 1
:= {}.
(* iris/proofmode/environments.v *)
Definition of_envs {PROP : bi} (Δ : envs PROP) : PROP
:=
  of_envs' (env_intuitionistic Δ) (env_spatial Δ).
(* iris/proofmode/environments.v *)
Instance : Params (@of_envs) 1
:= {}.
(* iris/proofmode/environments.v *)
Definition pre_envs_entails_def {PROP : bi} (Γp Γs : env PROP) (Q : PROP)
:=
  of_envs' Γp Γs ⊢ Q.
(* iris/proofmode/environments.v *)
Definition pre_envs_entails_aux : seal (@pre_envs_entails_def).
Proof. by eexists. Qed.
(* iris/proofmode/environments.v *)
Definition pre_envs_entails
:= pre_envs_entails_aux.(unseal).
(* iris/proofmode/environments.v *)
Definition pre_envs_entails_unseal :
  @pre_envs_entails = @pre_envs_entails_def
:= pre_envs_entails_aux.(seal_eq).
(* iris/proofmode/environments.v *)
Definition envs_entails {PROP : bi} (Δ : envs PROP) (Q : PROP) : Prop
:=
  pre_envs_entails  PROP (env_intuitionistic Δ) (env_spatial Δ) Q.
(* iris/proofmode/environments.v *)
Definition envs_entails_unseal :
  @envs_entails = λ PROP (Δ : envs PROP) Q, (of_envs Δ ⊢ Q).
Proof. by rewrite /envs_entails pre_envs_entails_unseal. Qed.
(* iris/proofmode/environments.v *)
Instance : Params (@envs_entails) 1
:= {}.
(* iris/proofmode/environments.v *)
Record envs_Forall2 {PROP : bi} (R : relation PROP) (Δ1 Δ2 : envs PROP)
:= {
  env_intuitionistic_Forall2 : env_Forall2 R (env_intuitionistic Δ1) (env_intuitionistic Δ2);
  env_spatial_Forall2 : env_Forall2 R (env_spatial Δ1) (env_spatial Δ2)
}.
(* iris/proofmode/environments.v *)
Definition envs_dom {PROP} (Δ : envs PROP) : list ident
:=
  env_dom (env_intuitionistic Δ) ++ env_dom (env_spatial Δ).
(* iris/proofmode/environments.v *)
Definition envs_lookup {PROP} (i : ident) (Δ : envs PROP) : option (bool * PROP)
:=
  let (Γp,Γs,n) := Δ in
  match env_lookup i Γp with
  | Some P => Some (true, P)
  | None => P ← env_lookup i Γs; Some (false, P)
  end.
(* iris/proofmode/environments.v *)
Definition envs_delete {PROP} (remove_intuitionistic : bool)
    (i : ident) (p : bool) (Δ : envs PROP) : envs PROP
:=
  let (Γp,Γs,n) := Δ in
  match p with
  | true => Envs (if remove_intuitionistic then env_delete i Γp else Γp) Γs n
  | false => Envs Γp (env_delete i Γs) n
  end.
(* iris/proofmode/environments.v *)
Definition envs_lookup_delete {PROP} (remove_intuitionistic : bool)
    (i : ident) (Δ : envs PROP) : option (bool * PROP * envs PROP)
:=
  let (Γp,Γs,n) := Δ in
  match env_lookup_delete i Γp with
  | Some (P,Γp') => Some (true, P, Envs (if remove_intuitionistic then Γp' else Γp) Γs n)
  | None => '(P,Γs') ← env_lookup_delete i Γs; Some (false, P, Envs Γp Γs' n)
  end.
(* iris/proofmode/environments.v *)
Fixpoint envs_lookup_delete_list {PROP} (remove_intuitionistic : bool)
    (js : list ident) (Δ : envs PROP) : option (bool * list PROP * envs PROP)
:=
  match js with
  | [] => Some (true, [], Δ)
  | j :: js =>
     '(p,P,Δ') ← envs_lookup_delete remove_intuitionistic j Δ;
     '(q,Ps,Δ'') ← envs_lookup_delete_list remove_intuitionistic js Δ';
     Some ((p:bool) &&& q, P :: Ps, Δ'')
  end.
(* iris/proofmode/environments.v *)
Definition envs_snoc {PROP} (Δ : envs PROP)
    (p : bool) (j : ident) (P : PROP) : envs PROP
:=
  let (Γp,Γs,n) := Δ in
  if p then Envs (Esnoc Γp j P) Γs n else Envs Γp (Esnoc Γs j P) n.
(* iris/proofmode/environments.v *)
Definition envs_app {PROP : bi} (p : bool)
    (Γ : env PROP) (Δ : envs PROP) : option (envs PROP)
:=
  let (Γp,Γs,n) := Δ in
  match p with
  | true => _ ← env_app Γ Γs; Γp' ← env_app Γ Γp; Some (Envs Γp' Γs n)
  | false => _ ← env_app Γ Γp; Γs' ← env_app Γ Γs; Some (Envs Γp Γs' n)
  end.
(* iris/proofmode/environments.v *)
Definition envs_simple_replace {PROP : bi} (i : ident) (p : bool)
    (Γ : env PROP) (Δ : envs PROP) : option (envs PROP)
:=
  let (Γp,Γs,n) := Δ in
  match p with
  | true => _ ← env_app Γ Γs; Γp' ← env_replace i Γ Γp; Some (Envs Γp' Γs n)
  | false => _ ← env_app Γ Γp; Γs' ← env_replace i Γ Γs; Some (Envs Γp Γs' n)
  end.
(* iris/proofmode/environments.v *)
Definition envs_replace {PROP : bi} (i : ident) (p q : bool)
    (Γ : env PROP) (Δ : envs PROP) : option (envs PROP)
:=
  if beq p q then envs_simple_replace i p Γ Δ
  else envs_app q Γ (envs_delete true i p Δ).
(* iris/proofmode/environments.v *)
Definition env_spatial_is_nil {PROP} (Δ : envs PROP) : bool
:=
  if env_spatial Δ is Enil then true else false.
(* iris/proofmode/environments.v *)
Definition envs_clear_spatial {PROP} (Δ : envs PROP) : envs PROP
:=
  Envs (env_intuitionistic Δ) Enil (env_counter Δ).
(* iris/proofmode/environments.v *)
Definition envs_clear_intuitionistic {PROP} (Δ : envs PROP) : envs PROP
:=
  Envs Enil (env_spatial Δ) (env_counter Δ).
(* iris/proofmode/environments.v *)
Definition envs_incr_counter {PROP} (Δ : envs PROP) : envs PROP
:=
  Envs (env_intuitionistic Δ) (env_spatial Δ) (Pos_succ (env_counter Δ)).
(* iris/proofmode/environments.v *)
Fixpoint envs_split_go {PROP}
    (js : list ident) (Δ1 Δ2 : envs PROP) : option (envs PROP * envs PROP)
:=
  match js with
  | [] => Some (Δ1, Δ2)
  | j :: js =>
     '(p,P,Δ1') ← envs_lookup_delete true j Δ1;
     if p : bool then envs_split_go js Δ1 Δ2 else
     envs_split_go js Δ1' (envs_snoc Δ2 false j P)
  end.
(* iris/proofmode/environments.v *)
(* if [d = Right] then [result = (remaining hyps, hyps named js)] and
   if [d = Left] then [result = (hyps named js, remaining hyps)] *)
Definition envs_split {PROP} (d : direction)
    (js : list ident) (Δ : envs PROP) : option (envs PROP * envs PROP)
:=
  '(Δ1,Δ2) ← envs_split_go js Δ (envs_clear_spatial Δ);
  if d is Right then Some (Δ1,Δ2) else Some (Δ2,Δ1).
(* iris/proofmode/environments.v *)
Fixpoint env_to_prop_go {PROP : bi} (acc : PROP) (Γ : env PROP) : PROP
:=
  match Γ with Enil => acc | Esnoc Γ _ P => env_to_prop_go (P ∗ acc)%I Γ end.
(* iris/proofmode/environments.v *)
Definition env_to_prop {PROP : bi} (Γ : env PROP) : PROP
:=
  match Γ with Enil => emp%I | Esnoc Γ _ P => env_to_prop_go P Γ end.
(* iris/proofmode/environments.v *)
Fixpoint env_to_prop_and_go {PROP : bi} (acc : PROP) (Γ : env PROP) : PROP
:=
  match Γ with Enil => acc | Esnoc Γ _ P => env_to_prop_and_go (P ∧ acc)%I Γ end.
(* iris/proofmode/environments.v *)
Definition env_to_prop_and {PROP : bi} (Γ : env PROP) : PROP
:=
  match Γ with Enil => True%I | Esnoc Γ _ P => env_to_prop_and_go P Γ end.
(* iris/proofmode/environments.v *)
Lemma of_envs_eq Δ :
  of_envs Δ =
  (⌜envs_wf Δ⌝ ∧
    env_and_persistently (env_intuitionistic Δ) ∧
    [∗] env_spatial Δ)%I.
Proof. done. Qed.
(* iris/proofmode/environments.v *)
Lemma of_envs'_alt Γp Γs :
  of_envs' Γp Γs ⊣⊢ ⌜envs_wf' Γp Γs⌝ ∧ □ [∧] Γp ∗ [∗] Γs.
Proof.
  rewrite /of_envs'. f_equiv.
  rewrite -persistent_and_affinely_sep_l. f_equiv.
  clear. induction Γp as [|Γp IH ? Q]; simpl.
  { apply (anti_symm (⊢)); last by apply True_intro.
    by rewrite persistently_True. }
  rewrite IH persistently_and. done.
Qed.
(* iris/proofmode/environments.v *)
Lemma of_envs_alt Δ :
  of_envs Δ ⊣⊢ ⌜envs_wf Δ⌝ ∧ □ [∧] env_intuitionistic Δ ∗ [∗] env_spatial Δ.
Proof. rewrite /of_envs of_envs'_alt //. Qed.
(* iris/proofmode/environments.v *)
Instance envs_Forall2_refl (R : relation PROP) :
  Reflexive R → Reflexive (envs_Forall2 R).
Proof. by constructor. Qed.
(* iris/proofmode/environments.v *)
Instance envs_Forall2_sym (R : relation PROP) :
  Symmetric R → Symmetric (envs_Forall2 R).
Proof. intros ??? [??]; by constructor. Qed.
(* iris/proofmode/environments.v *)
Instance envs_Forall2_trans (R : relation PROP) :
  Transitive R → Transitive (envs_Forall2 R).
Proof. intros ??? [??] [??] [??]; constructor; etrans; eauto. Qed.
(* iris/proofmode/environments.v *)
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.
(* iris/proofmode/environments.v *)
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.
(* iris/proofmode/environments.v *)
Instance env_intuitionistic_mono :
  Proper (envs_Forall2 (⊢) ==> env_Forall2 (⊢)) (@env_intuitionistic PROP).
Proof. solve_proper. Qed.
(* iris/proofmode/environments.v *)
Instance env_intuitionistic_flip_mono :
  Proper (flip (envs_Forall2 (⊢)) ==> flip (env_Forall2 (⊢))) (@env_intuitionistic PROP).
Proof. solve_proper. Qed.
(* iris/proofmode/environments.v *)
Instance env_intuitionistic_proper :
  Proper (envs_Forall2 (⊣⊢) ==> env_Forall2 (⊣⊢)) (@env_intuitionistic PROP).
Proof. solve_proper. Qed.
(* iris/proofmode/environments.v *)
Instance env_spatial_mono :
  Proper (envs_Forall2 (⊢) ==> env_Forall2 (⊢)) (@env_spatial PROP).
Proof. solve_proper. Qed.
(* iris/proofmode/environments.v *)
Instance env_spatial_flip_mono :
  Proper (flip (envs_Forall2 (⊢)) ==> flip (env_Forall2 (⊢))) (@env_spatial PROP).
Proof. solve_proper. Qed.
(* iris/proofmode/environments.v *)
Instance env_spatial_proper :
  Proper (envs_Forall2 (⊣⊢) ==> env_Forall2 (⊣⊢)) (@env_spatial PROP).
Proof. solve_proper. Qed.
(* iris/proofmode/environments.v *)
Instance of_envs_mono' :
  Proper (env_Forall2 (⊢) ==> env_Forall2 (⊢) ==> (⊢)) (@of_envs' PROP).
Proof.
  intros Γp1 Γp2 Hp Γs1 Γs2 Hs; apply and_mono; simpl in *.
  - apply pure_mono=> -[???]. constructor;
      naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
  - f_equiv; [|by repeat f_equiv].
    induction Hp; simpl; repeat (done || f_equiv).
Qed.
(* iris/proofmode/environments.v *)
Instance of_envs_proper' :
  Proper (env_Forall2 (⊣⊢) ==> env_Forall2 (⊣⊢) ==> (⊣⊢)) (@of_envs' PROP).
Proof.
  intros Γp1 Γp2 Hp Γs1 Γs2 Hs; apply (anti_symm (⊢)); apply of_envs_mono';
    eapply (env_Forall2_impl (⊣⊢)); by eauto using equiv_entails_1_1.
Qed.
(* iris/proofmode/environments.v *)
Instance of_envs_mono : Proper (envs_Forall2 (⊢) ==> (⊢)) (@of_envs PROP).
Proof. solve_proper. Qed.
(* iris/proofmode/environments.v *)
Instance of_envs_proper : Proper (envs_Forall2 (⊣⊢) ==> (⊣⊢)) (@of_envs PROP).
Proof. solve_proper. Qed.
(* iris/proofmode/environments.v *)
Instance Envs_proper (R : relation PROP) :
  Proper (env_Forall2 R ==> env_Forall2 R ==> eq ==> envs_Forall2 R) (@Envs PROP).
Proof. by constructor. Qed.
(* iris/proofmode/environments.v *)
Instance envs_entails_proper :
  Proper (envs_Forall2 (⊣⊢) ==> (⊣⊢) ==> iff) (@envs_entails PROP).
Proof. rewrite envs_entails_unseal. solve_proper. Qed.
(* iris/proofmode/environments.v *)
Instance envs_entails_mono :
  Proper (flip (envs_Forall2 (⊢)) ==> (⊢) ==> impl) (@envs_entails PROP).
Proof. rewrite envs_entails_unseal=> Δ1 Δ2 ? P1 P2 <- <-. by f_equiv. Qed.
(* iris/proofmode/environments.v *)
Instance envs_entails_flip_mono :
  Proper (envs_Forall2 (⊢) ==> flip (⊢) ==> flip impl) (@envs_entails PROP).
Proof. rewrite envs_entails_unseal=> Δ1 Δ2 ? P1 P2 <- <-. by f_equiv. Qed.
(* iris/proofmode/environments.v *)
Lemma envs_delete_intuitionistic Δ i : envs_delete false i true Δ = Δ.
Proof. by destruct Δ. Qed.
(* iris/proofmode/environments.v *)
Lemma envs_delete_spatial Δ i :
  envs_delete false i false Δ = envs_delete true i false Δ.
Proof. by destruct Δ. Qed.
(* iris/proofmode/environments.v *)
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.
(* iris/proofmode/environments.v *)
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_eq=>?.
  apply pure_elim_l=> Hwf.
  destruct Δ as [Γp Γs], (Γp !! i) eqn:Heqo; simplify_eq/=.
  - rewrite pure_True ?left_id; last (destruct Hwf, rp; constructor;
      naive_solver eauto using env_delete_wf, env_delete_fresh).
    rewrite -persistently_and_intuitionistically_sep_l assoc.
    apply and_mono; last done. apply and_intro.
    + rewrite (env_lookup_perm Γp) //= and_elim_l //.
    + destruct rp; last done.
      rewrite (env_lookup_perm Γp) //= and_elim_r //.
  - 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) //=.
    rewrite ![(P ∗ _)%I]comm.
    rewrite persistent_and_sep_assoc. done.
Qed.
(* iris/proofmode/environments.v *)
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.
(* iris/proofmode/environments.v *)
Lemma envs_lookup_intuitionistic_sound Δ i P :
  envs_lookup i Δ = Some (true,P) → of_envs Δ ⊢ □ P ∗ of_envs Δ.
Proof. intros ?%(envs_lookup_sound' _ false). by destruct Δ. Qed.
(* iris/proofmode/environments.v *)
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_eq=>Hwf ?.
  rewrite [⌜envs_wf Δ⌝%I]pure_True // left_id.
  destruct Δ as [Γp Γs], (Γp !! i) eqn:Heqo; simplify_eq/=.
  - rewrite -persistently_and_intuitionistically_sep_l.
    rewrite (env_lookup_perm Γp) //= [(⌜_⌝ ∧ _)%I]and_elim_r !assoc //.
  - destruct (Γs !! i) eqn:?; simplify_eq/=.
    rewrite (env_lookup_perm Γs) //=.
    rewrite [(⌜_⌝ ∧ _)%I]and_elim_r.
    rewrite (comm _ P) -persistent_and_sep_assoc.
    apply and_mono; first done. rewrite comm //.
Qed.
(* iris/proofmode/environments.v *)
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.
(* iris/proofmode/environments.v *)
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.
(* iris/proofmode/environments.v *)
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.
(* iris/proofmode/environments.v *)
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.
(* iris/proofmode/environments.v *)
Lemma envs_lookup_delete_list_nil Δ rp :
  envs_lookup_delete_list rp [] Δ = Some (true, [], Δ).
Proof. done. Qed.
(* iris/proofmode/environments.v *)
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.
(* iris/proofmode/environments.v *)
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.