phanerozoic/Coq-Iris huggingface dataset:
(* iris/proofmode/coq_tactics.v *)
Lemma tac_impl_intro_drop Δ P Q R :
  FromImpl R P Q → envs_entails Δ Q → envs_entails Δ R.
Proof.
  rewrite /FromImpl envs_entails_unseal => <- ?. apply impl_intro_l. by rewrite and_elim_r.
Qed.
(* iris/proofmode/coq_tactics.v *)
Lemma tac_wand_intro Δ i P Q R :
  FromWand R P Q →
  match envs_app false (Esnoc Enil i P) Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end →
  envs_entails Δ R.
Proof.
  destruct (envs_app _ _ _) as [Δ'|] eqn:Hrep; last done.
  rewrite /FromWand envs_entails_unseal => <- HQ.
  rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
Qed.
(* iris/proofmode/coq_tactics.v *)
Lemma tac_wand_intro_intuitionistic Δ i P P' Q R :
  FromWand R P Q →
  IntoPersistent false P P' →
  TCOr (Affine P) (Absorbing Q) →
  match envs_app true (Esnoc Enil i P') Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end →
  envs_entails Δ R.
Proof.
  destruct (envs_app _ _ _) as [Δ'|] eqn:Hrep; last done.
  rewrite /FromWand envs_entails_unseal => <- ? HPQ HQ.
  rewrite envs_app_singleton_sound //=. apply wand_intro_l. destruct HPQ.
  - rewrite -(affine_affinely P) (_ : P = <pers>?false P)%I //
            (into_persistent _ P) wand_elim_r //.
  - rewrite (_ : P = <pers>?false P)%I // (into_persistent _ P).
    by rewrite -{1}absorbingly_intuitionistically_into_persistently
      absorbingly_sep_l wand_elim_r HQ.
Qed.
(* iris/proofmode/coq_tactics.v *)
Lemma tac_wand_intro_drop Δ P Q R :
  FromWand R P Q →
  TCOr (Affine P) (Absorbing Q) →
  envs_entails Δ Q →
  envs_entails Δ R.
Proof.
  rewrite envs_entails_unseal /FromWand => <- HPQ ->. apply wand_intro_l. by rewrite sep_elim_r.
Qed.
(* iris/proofmode/coq_tactics.v *)
(* This is pretty much [tac_specialize_assert] with [js:=[j]] and [tac_exact],
but it is doing some work to keep the order of hypotheses preserved. *)
Lemma tac_specialize remove_intuitionistic Δ i p j q P1 P2 R Q :
  envs_lookup i Δ = Some (p, P1) →
  let Δ' := envs_delete remove_intuitionistic i p Δ in
  envs_lookup j Δ' = Some (q, R) →
  IntoWand q p R P1 P2 →
  match envs_replace j q (p &&& q) (Esnoc Enil j P2) Δ' with
  | Some Δ'' => envs_entails Δ'' Q
  | None => False
  end → envs_entails Δ Q.
Proof.
  rewrite envs_entails_unseal /IntoWand. intros ?? HR ?.
  destruct (envs_replace _ _ _ _ _) as [Δ''|] eqn:?; last done.
  rewrite (envs_lookup_sound' _ remove_intuitionistic) //.
  rewrite envs_replace_singleton_sound //. destruct p; simpl in *.
  - rewrite -{1}intuitionistically_idemp -{1}intuitionistically_if_idemp.
    rewrite {1}(intuitionistically_intuitionistically_if q).
    by rewrite HR assoc intuitionistically_if_sep_2 !wand_elim_r.
  - by rewrite HR assoc !wand_elim_r.
Qed.
(* iris/proofmode/coq_tactics.v *)
Lemma tac_specialize_assert Δ j (q am neg : bool) js R P1 P2 P1' Q :
  envs_lookup j Δ = Some (q, R) →
  IntoWand q false R P1 P2 →
  (if am then AddModal P1' P1 Q else TCEq P1' P1) →
  match
    '(Δ1,Δ2) ← envs_split (if neg is true then Right else Left)
                          js (envs_delete true j q Δ);
    Δ2' ← envs_app (negb am &&& q &&& env_spatial_is_nil Δ1) (Esnoc Enil j P2) Δ2;
    Some (Δ1,Δ2') (* does not preserve position of [j] *)
  with
  | Some (Δ1,Δ2') =>
     (* The constructor [conj] of [∧] still stores the contexts [Δ1] and [Δ2'] *)
     envs_entails Δ1 P1' ∧ envs_entails Δ2' Q
  | None => False
  end → envs_entails Δ Q.
Proof.
  rewrite envs_entails_unseal. intros ?? Hmod HQ.
  destruct (_ ≫= _) as [[Δ1 Δ2']|] eqn:?; last done.
  destruct HQ as [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_singleton_sound Δ2) //; simpl.
  rewrite -intuitionistically_if_idemp (into_wand q false) /=.
  destruct (negb am &&& q &&& env_spatial_is_nil Δ1) eqn:Hp; simpl.
  - move: Hp. rewrite !lazy_andb_true negb_true. intros [[-> ->] ?]; simpl.
    destruct Hmod. rewrite env_spatial_is_nil_intuitionistically // HP1.
    by rewrite assoc intuitionistically_sep_2 wand_elim_l wand_elim_r HQ.
  - rewrite intuitionistically_if_elim HP1. destruct am; last destruct Hmod.
    + by rewrite assoc -(comm _ P1') -assoc wand_trans HQ.
    + by rewrite assoc wand_elim_l wand_elim_r HQ.
Qed.
(* iris/proofmode/coq_tactics.v *)
Lemma tac_unlock_emp Δ Q : envs_entails Δ Q → envs_entails Δ (emp ∗ locked Q).
Proof. rewrite envs_entails_unseal=> ->. by rewrite -lock left_id. Qed.
(* iris/proofmode/coq_tactics.v *)
Lemma tac_unlock_True Δ Q : envs_entails Δ Q → envs_entails Δ (True ∗ locked Q).
Proof. rewrite envs_entails_unseal=> ->. by rewrite -lock -True_sep_2. Qed.
(* iris/proofmode/coq_tactics.v *)
Lemma tac_unlock Δ Q : envs_entails Δ Q → envs_entails Δ (locked Q).
Proof. by unlock. Qed.
(* iris/proofmode/coq_tactics.v *)
Lemma tac_specialize_frame Δ j (q am : bool) R P1 P2 P1' Q Q' :
  envs_lookup j Δ = Some (q, R) →
  IntoWand q false R P1 P2 →
  (if am then AddModal P1' P1 Q else TCEq P1' P1) →
  envs_entails (envs_delete true j q Δ) (P1' ∗ locked Q') →
  Q' = (P2 -∗ Q)%I →
  envs_entails Δ Q.
Proof.
  rewrite envs_entails_unseal. intros ?? Hmod HPQ ->.
  rewrite envs_lookup_sound //. rewrite HPQ -lock.
  rewrite (into_wand q false) /= assoc -(comm _ P1') -assoc wand_trans.
  destruct am; [done|destruct Hmod]. by rewrite wand_elim_r.
Qed.
(* iris/proofmode/coq_tactics.v *)
Lemma tac_specialize_assert_pure Δ j q a R P1 P2 φ Q :
  envs_lookup j Δ = Some (q, R) →
  IntoWand q false R P1 P2 →
  FromPure a P1 φ →
  φ →
  match envs_simple_replace j q (Esnoc Enil j P2) Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end →
  envs_entails Δ Q.
Proof.
  destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:?; last done.
  rewrite envs_entails_unseal=> ?????. rewrite envs_simple_replace_singleton_sound //=.
  rewrite -intuitionistically_if_idemp (into_wand q false) /=.
  rewrite -(from_pure a P1) pure_True //.
  rewrite -affinely_affinely_if affinely_True_emp.
  by rewrite left_id wand_elim_r.
Qed.
(* iris/proofmode/coq_tactics.v *)
Lemma tac_specialize_assert_intuitionistic Δ j q P1 P1' P2 R Q :
  envs_lookup j Δ = Some (q, R) →
  IntoWand q true R P1 P2 →
  Persistent P1 →
  IntoAbsorbingly P1' P1 →
  envs_entails (envs_delete true j q Δ) P1' →
  match envs_simple_replace j q (Esnoc Enil j P2) Δ with
  | Some Δ'' => envs_entails Δ'' Q
  | None => False
  end → envs_entails Δ Q.
Proof.
  rewrite envs_entails_unseal => ???? HP1 HQ.
  destruct (envs_simple_replace _ _ _ _) as [Δ''|] eqn:?; last done.
  rewrite -HQ envs_lookup_sound //.
  rewrite -(idemp bi_and (of_envs (envs_delete _ _ _ _))).
  rewrite {2}envs_simple_replace_singleton_sound' //; simpl.
  rewrite {1}HP1 (into_absorbingly P1' P1) (persistent_persistently_2 P1).
  rewrite absorbingly_elim_persistently persistently_and_intuitionistically_sep_l assoc.
  rewrite -intuitionistically_if_idemp -intuitionistically_idemp.
  rewrite (intuitionistically_intuitionistically_if q).
  by rewrite intuitionistically_if_sep_2 (into_wand q true) wand_elim_l wand_elim_r.
Qed.
(* iris/proofmode/coq_tactics.v *)
Lemma tac_specialize_intuitionistic_helper Δ j q P R R' Q :
  envs_lookup j Δ = Some (q,P) →
  (if q then TCTrue else BiAffine PROP) →
  envs_entails Δ (<absorb> R) →
  IntoPersistent false R R' →
  match envs_replace j q true (Esnoc Enil j R') Δ with
  | Some Δ'' => envs_entails Δ'' Q
  | None => False
  end → envs_entails Δ Q.
Proof.
  rewrite envs_entails_unseal => ?? HR ??.
  destruct (envs_replace _ _ _ _ _) as [Δ'|] eqn:?; last done.
  rewrite -(idemp bi_and (of_envs Δ)) {1}HR.
  rewrite envs_replace_singleton_sound //; destruct q; simpl.
  - by rewrite (_ : R = <pers>?false R)%I // (into_persistent _ R)
      absorbingly_elim_persistently sep_elim_r
      persistently_and_intuitionistically_sep_l wand_elim_r.
  - by rewrite (absorbing_absorbingly R) (_ : R = <pers>?false R)%I //
      (into_persistent _ R) sep_elim_r
      persistently_and_intuitionistically_sep_l wand_elim_r.
Qed.
(* iris/proofmode/coq_tactics.v *)
(* A special version of [tac_assumption] that does not do any of the
[FromAssumption] magic. *)
Lemma tac_specialize_intuitionistic_helper_done Δ i q P :
  envs_lookup i Δ = Some (q,P) →
  envs_entails Δ (<absorb> P).
Proof.
  rewrite envs_entails_unseal /bi_absorbingly=> /envs_lookup_sound=> ->.
  rewrite intuitionistically_if_elim comm. f_equiv; auto using pure_intro.
Qed.
(* iris/proofmode/coq_tactics.v *)
Lemma tac_revert Δ i Q :
  match envs_lookup_delete true i Δ with
  | Some (p,P,Δ') => envs_entails Δ' ((if p then □ P else P)%I -∗ Q)
  | None => False
  end →
  envs_entails Δ Q.
Proof.
  rewrite envs_entails_unseal => HQ.
  destruct (envs_lookup_delete _ _ _) as [[[p P] Δ']|] eqn:?; last done.
  rewrite envs_lookup_delete_sound //=.
  rewrite HQ. destruct p; simpl; auto using wand_elim_r.
Qed.
(* iris/proofmode/coq_tactics.v *)
Class IntoIH (φ : Prop) (Δ : envs PROP) (Q : PROP)
:=
  into_ih : φ → □ of_envs Δ ⊢ Q.
(* iris/proofmode/coq_tactics.v *)
Instance into_ih_entails Δ Q : IntoIH (envs_entails Δ Q) Δ Q.
Proof. by rewrite envs_entails_unseal /IntoIH bi.intuitionistically_elim. Qed.
(* iris/proofmode/coq_tactics.v *)
Instance into_ih_forall {A} (φ : A → Prop) Δ Φ :
  (∀ x, IntoIH (φ x) Δ (Φ x)) → IntoIH (∀ x, φ x) Δ (∀ x, Φ x) | 2.
Proof. rewrite /IntoIH=> HΔ ?. apply forall_intro=> x. by rewrite (HΔ x). Qed.
(* iris/proofmode/coq_tactics.v *)
Instance into_ih_impl (φ ψ : Prop) Δ P Q :
  MakeAffinely ⌜ φ ⌝ P →
  IntoIH ψ Δ Q → IntoIH (φ → ψ) Δ (P -∗ Q) | 1.
Proof.
  rewrite /IntoIH /MakeAffinely=> <- HΔ ?.
  rewrite -persistent_impl_wand_affinely. apply impl_intro_l, pure_elim_l. auto.
Qed.
(* iris/proofmode/coq_tactics.v *)
(* The instances [into_ih_Forall] and [into_ih_Forall2] are used to support
induction principles for mutual inductive types such as finitely branching trees:

  Inductive ntree := Tree : list ntree → ntree.

  Lemma ntree_ind (P : ntree → Prop) :
    (∀ l, Forall P l → P (Tree l)) → ∀ t, P t.

Note 1: We need an [IntoIH] instance for any predicate transformer (like
[Forall]) that is used in induction principles. However, since nested induction
with lists is most common, we currently only support [Forall] and [Forall2].

Note 2: We could also write the instance [into_ih_Forall] using the big operator
for conjunction, or using the forall quantifier. We use the big operator
because that corresponds most closely to [Forall], and we use the version with
separating conjunction because we do not have a binary version of the big
operator for conjunctions, and want to treat [Forall] and [Forall2]
consistently. *)
Instance into_ih_Forall {A} (φ : A → Prop) l Δ Φ :
  (∀ x, IntoIH (φ x) Δ (Φ x)) →
  IntoIH (Forall φ l) Δ ([∗ list] x ∈ l, □ Φ x) | 2.
Proof.
  rewrite /IntoIH=> HΔ. induction 1 as [|x l ? IH]; simpl.
  { apply (affine _). }
  rewrite {1}intuitionistically_sep_dup. f_equiv; [|done].
  apply intuitionistically_intro', HΔ; auto.
Qed.
(* iris/proofmode/coq_tactics.v *)
Instance into_ih_Forall2 {A B} (φ : A → B → Prop) l1 l2 Δ Φ :
  (∀ x1 x2, IntoIH (φ x1 x2) Δ (Φ x1 x2)) →
  IntoIH (Forall2 φ l1 l2) Δ ([∗ list] x1;x2 ∈ l1;l2, □ Φ x1 x2) | 2.
Proof.
  rewrite /IntoIH=> HΔ. induction 1 as [|x1 x2 l1 l2 ? IH]; simpl.
  { apply (affine _). }
  rewrite {1}intuitionistically_sep_dup. f_equiv; [|done].
  apply intuitionistically_intro', HΔ; auto.
Qed.
(* iris/proofmode/coq_tactics.v *)
Lemma tac_revert_ih Δ P Q {φ : Prop} (Hφ : φ) :
  IntoIH φ Δ P →
  env_spatial_is_nil Δ = true →
  envs_entails Δ (<pers> P → Q) →
  envs_entails Δ Q.
Proof.
  rewrite /IntoIH envs_entails_unseal. intros HP ? HPQ.
  rewrite (env_spatial_is_nil_intuitionistically Δ) //.
  rewrite -(idemp bi_and (□ (of_envs Δ))%I).
  rewrite -{1}intuitionistically_idemp {1}intuitionistically_into_persistently_1.
  by rewrite {1}HP // intuitionistically_elim HPQ impl_elim_r.
Qed.
(* iris/proofmode/coq_tactics.v *)
Lemma tac_assert Δ j P Q :
  match envs_app true (Esnoc Enil j (P -∗ P)%I) Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end → envs_entails Δ Q.
Proof.
  destruct (envs_app _ _ _) as [Δ'|] eqn:?; last done.
  rewrite envs_entails_unseal=> ?. rewrite (envs_app_singleton_sound Δ) //; simpl.
  by rewrite -(entails_wand P) // intuitionistically_emp emp_wand.
Qed.
(* iris/proofmode/coq_tactics.v *)
Definition IntoEmpValid (φ : Type) (P : PROP)
:= φ → ⊢ P.
(* iris/proofmode/coq_tactics.v *)
(* These lemmas are [Defined] because the guardedness checker must see
through them. See https://gitlab.mpi-sws.org/iris/iris/issues/274. For the
same reason, their bodies use as little automation as possible. *)
Lemma into_emp_valid_here φ P : AsEmpValid DirectionIntoEmpValid φ P → IntoEmpValid φ P.
Proof. rewrite /IntoEmpValid. intros [Hi1 ?]. apply Hi1, eq_refl. Defined.
(* iris/proofmode/coq_tactics.v *)
Lemma into_emp_valid_impl (φ ψ : Type) P :
  φ → IntoEmpValid ψ P → IntoEmpValid (φ → ψ) P.
Proof. rewrite /IntoEmpValid => Hφ Hi1 Hi2. apply Hi1, Hi2, Hφ. Defined.
(* iris/proofmode/coq_tactics.v *)
Lemma into_emp_valid_forall {A} (φ : A → Type) P x :
  IntoEmpValid (φ x) P → IntoEmpValid (∀ x : A, φ x) P.
Proof. rewrite /IntoEmpValid => Hi1 Hi2. apply Hi1, Hi2. Defined.
(* iris/proofmode/coq_tactics.v *)
Lemma into_emp_valid_tforall {TT : tele} (φ : TT → Prop) P x :
  IntoEmpValid (φ x) P → IntoEmpValid (∀.. x : TT, φ x) P.
Proof. rewrite /IntoEmpValid tforall_forall=> Hi1 Hi2. apply Hi1, Hi2. Defined.
(* iris/proofmode/coq_tactics.v *)
Lemma into_emp_valid_proj φ P : IntoEmpValid φ P → φ → ⊢ P.
Proof. intros HP. apply HP. Defined.
(* iris/proofmode/coq_tactics.v *)
(* When called by the proof mode, the proof of [P] is produced by calling
[into_emp_valid_proj]. That call must be transparent to the guardedness
checker, per https://gitlab.mpi-sws.org/iris/iris/issues/274; hence, it must
be done _outside_ [tac_pose_proof], so the latter can remain opaque. *)
Lemma tac_pose_proof Δ j P Q :
  (⊢ P) →
  match envs_app true (Esnoc Enil j P) Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end →
  envs_entails Δ Q.
Proof.
  destruct (envs_app _ _ _) as [Δ'|] eqn:?; last done.
  rewrite envs_entails_unseal => HP <-. rewrite envs_app_singleton_sound //=.
  by rewrite -HP /= intuitionistically_emp emp_wand.
Qed.
(* iris/proofmode/coq_tactics.v *)
Lemma tac_pose_proof_hyp Δ i j Q :
  match envs_lookup_delete false i Δ with
  | None => False
  | Some (p, P, Δ') =>
    match envs_app p (Esnoc Enil j P) Δ' with
    | None => False
    | Some Δ'' => envs_entails Δ'' Q
    end
  end →
  envs_entails Δ Q.
Proof.
  destruct (envs_lookup_delete _ _ _) as [((p&P)&Δ')|] eqn:Hlookup; last done.
  destruct (envs_app _ _ _) as [Δ''|] eqn:?; last done.
  rewrite envs_entails_unseal. move: Hlookup. rewrite envs_lookup_delete_Some.
  intros [? ->] <-.
  rewrite envs_lookup_sound' // envs_app_singleton_sound //=.
  by rewrite wand_elim_r.
Qed.
(* iris/proofmode/coq_tactics.v *)
Lemma tac_apply Δ i p R P1 P2 :
  envs_lookup i Δ = Some (p, R) →
  IntoWand p false R P1 P2 →
  envs_entails (envs_delete true i p Δ) P1 → envs_entails Δ P2.
Proof.
  rewrite envs_entails_unseal => ?? HP1. rewrite envs_lookup_sound //.
  by rewrite (into_wand p false) /= HP1 wand_elim_l.
Qed.
(* iris/proofmode/coq_tactics.v *)
(* * Conjunction splitting *)
Lemma tac_and_split Δ P Q1 Q2 :
  FromAnd P Q1 Q2 → envs_entails Δ Q1 → envs_entails Δ Q2 → envs_entails Δ P.
Proof. rewrite envs_entails_unseal. intros. rewrite -(from_and P). by apply and_intro. Qed.
(* iris/proofmode/coq_tactics.v *)
(* * Separating conjunction splitting *)
Lemma tac_sep_split Δ d js P Q1 Q2 :
  FromSep P Q1 Q2 →
  match envs_split d js Δ with
  | None => False
  | Some (Δ1,Δ2) => envs_entails Δ1 Q1 ∧ envs_entails Δ2 Q2
  end → envs_entails Δ P.
Proof.
  destruct (envs_split _ _ _) as [(Δ1&Δ2)|] eqn:?; last done.
  rewrite envs_entails_unseal=>? [HQ1 HQ2].
  rewrite envs_split_sound //. by rewrite HQ1 HQ2.
Qed.
(* iris/proofmode/coq_tactics.v *)
(* * Combining
For the [iCombine] tactic, users provide a [Ps : list PROP] which should be
combined to a single [PROP]. The (public) classes currently available,
[MaybeCombineSepAs] and [CombineSepGives], can combine two given [PROP]s. The
following [CombineSepsAs] and [CombineSepsAsGives] typeclasses are an
implementation detail of [iCombine], lifting the combining operation to
one on [list PROP].

Computing the 'gives' clause for a list of hypotheses is somewhat involved.
We cannot just fold [CombineSepGives] over the list, since the output of the
first [CombineSepGives] is not suitable as the input for the next iteration. For
example, one might have [CombineSepGives (own γ a) (own γ b) (✓ (a ⋅ b))]. This
does not directly allow us to combine [[own γ a; own γ b; own γ c]] to
[✓ (a ⋅ b ⋅ c)], since [CombineSepGives (✓ (b ⋅ c)) (own γ a) ?] does not work.
We need to first compute the 'as' clause of the tail to proceed: that is, use
the fact that the 'as' clause of [[own γ b; own γ c]] is [own γ (b ⋅ c)].
We could let [CombineSepsAs] compute the 'as' clause of the tail separately, but
this results in quadratic complexity. We therefore bundle both clauses
in the [CombineSepsAsGives] typeclass given below.

Note that an alternative would be to compute pairwise 'gives' clauses of the
head of the list with every element in the tail, and [∧]-ing that with the
'gives' clause of the tail. In the example above, this would result in
[✓ (a ⋅ b) ∧ ✓ (a ⋅ c) ∧ ✓ (b ⋅ c)]. This approach is not strong enough:
it does not allow us to conclude [✓ (a ⋅ b ⋅ c)]. *)
Class CombineSepsAsGives {PROP : bi} (Ps : list PROP) (Q R : PROP)
:= {
  combine_seps_as_gives_as : [∗] Ps ⊢ Q;
  combine_seps_as_gives_gives : [∗] Ps ⊢ <pers> R;
}.
(* iris/proofmode/coq_tactics.v *)
Instance combine_seps_as_gives_nil : @CombineSepsAsGives PROP [] emp True.
Proof.
  split; first done. rewrite persistently_True.
  by apply pure_intro.
Qed.
(* iris/proofmode/coq_tactics.v *)
Instance combine_seps_as_gives_singleton P :
  CombineSepsAsGives [P] P True | 1.
Proof.
  split; first by rewrite /= right_id. rewrite persistently_True.
  by apply pure_intro.
Qed.
(* iris/proofmode/coq_tactics.v *)
Instance combine_seps_gives_cons P Ps Q R Q' progress R' R'':
  CombineSepsAsGives Ps Q R → (* [Q] and [R] are result from combining tail *)
  MaybeCombineSepAs P Q Q' progress → (* [Q'] is [P] and [Q] combined *)
  CombineSepGives P Q R' → (* [R'] is obtained for free from [P] and [Q] *)
  MakeAnd R R' R'' → (* [R''] is nicely and-ing [R] and [R'] *)
  CombineSepsAsGives (P :: Ps) Q' R'' | 2.
(** By and-ing [R] and [R'], the resulting 'gives' clause [R''] will contain
redundant information in some cases. However, this is necessary in other cases.

For example, if we take [Ps = [own γ q1; own γ q2; own γ q3]] with [fracR] as
the cmra, we get [R'' = (q2 + q3 ≤ 1) ∧ (q1 + q2 + q3 ≤ 1)]. Here, the first
conjunct [R] follows from the second [R'], so there is redundancy.

However, if we take
[Ps = [own γ (CoPset E1); own γ (CoPset E2); own γ (CoPset E3)]] with
[coPset_disjR] as the cmra, we get [R'' = (E2 ## E3) ∧ (E1 ## (E2 ∪ E3))], where
the first conjunct does not follow from the second conjunct. Similarly for
[Ps = [l ↦{q1} v1; l ↦{q2} v2; l ↦ {q3} v3]], where
[R'' = (v1 = v2) ∧ (v2 = v3) ∧ {..other info about qs..}]. *)
Proof.
  case => HPsQ.
  rewrite /CombineSepGives /MakeAnd => HPsR HQ' HR' HR''.
  split; first by rewrite /= HPsQ HQ'.
  rewrite -HR'' /=.
  rewrite persistently_and. apply and_intro.
  - by rewrite HPsR sep_elim_r.
  - by rewrite HPsQ.
Qed.
(* iris/proofmode/coq_tactics.v *)
(* If just the 'as' clause is needed, we will instead look for instances of
the following [CombineSepsAs] typeclass. *)
Class CombineSepsAs {PROP : bi} (Ps : list PROP) (Q : PROP)
:=
  combine_seps_as : [∗] Ps ⊢ Q.
(* iris/proofmode/coq_tactics.v *)
(* To ensure consistency of the output [Q] with that of [CombineSepsAsGives],
the only instance of [CombineSepsAs] is constructed with an instance of
[CombineSepsAsGives]. The one thing we need to keep in mind here is that
instances of [CombineSepsAsGives] can only be found if [CombineSepGives]
instances exist. Unlike for the 'as' clause, there is no trivial 'gives'
combination --- if the user writes a 'gives' clause, they intend to receive
non-trivial information, and should receive an error if this cannot be found.

To still allow trivial combining with an 'as' clause, we add a trivial
[CombineSepGives] instance _only_ during the typeclass search of [CombineSepsAs]
via [CombineSepsAsGives]. This means we both get consistent output [Q] from
[CombineSepsAsGives] and [CombineSepsAs], while [iCombine "H1 H2" gives "H"]
still fails if "H1" and "H2" are unrelated *)
Instance combine_seps_as_from_as_gives Ps Q R :
  ((∀ P P', CombineSepGives P P' True%I) → CombineSepsAsGives Ps Q R) →
  CombineSepsAs Ps Q.
Proof.
  move => HPsQ. apply HPsQ. move => P P'. rewrite /CombineSepGives.
  rewrite persistently_True. by apply pure_intro.
Qed.
(* iris/proofmode/coq_tactics.v *)
Lemma tac_combine_as Δ1 Δ2 Δ3 js p Ps j P Q :
  envs_lookup_delete_list false js Δ1 = Some (p, Ps, Δ2) →
  CombineSepsAs Ps P →
  envs_app p (Esnoc Enil j P) Δ2 = Some Δ3 →
  envs_entails Δ3 Q → envs_entails Δ1 Q.
Proof.
  rewrite envs_entails_unseal => ??? <-. rewrite envs_lookup_delete_list_sound //.
  rewrite combine_seps_as. rewrite envs_app_singleton_sound //=.
  by rewrite wand_elim_r.
Qed.
(* iris/proofmode/coq_tactics.v *)
Lemma combine_seps_gives_of_envs Δ1 Δ2 js p Ps P R :
  envs_lookup_delete_list false js Δ1 = Some (p, Ps, Δ2) →
  CombineSepsAsGives Ps P R →
  of_envs Δ1 ⊢ of_envs Δ1 ∗ □ R.
Proof.
  move => ??.
  assert (of_envs Δ1 ⊢ of_envs Δ1 ∧ <pers> R) as H.
  { apply and_intro; first done.
    rewrite envs_lookup_delete_list_sound //.
    by rewrite combine_seps_as_gives_gives
        intuitionistically_if_elim sep_elim_l. }
  by rewrite {1}H persistently_and_intuitionistically_sep_r.
Qed.
(* iris/proofmode/coq_tactics.v *)
Lemma tac_combine_gives Δ1 Δ2 Δ3 js p Ps j P Q R :
  envs_lookup_delete_list false js Δ1 = Some (p, Ps, Δ2) →
  CombineSepsAsGives Ps P R →
  envs_app true (Esnoc Enil j R) Δ1 = Some Δ3 →
  envs_entails Δ3 Q → envs_entails Δ1 Q.
Proof.
  rewrite envs_entails_unseal => ??? <-.
  erewrite combine_seps_gives_of_envs => //.
  rewrite envs_app_singleton_sound //=.
  by apply wand_elim_l'.
Qed.
(* iris/proofmode/coq_tactics.v *)
Lemma tac_combine_as_gives Δ1 Δ2 Δ3 js p Ps j k P R Q :
  envs_lookup_delete_list false js Δ1 = Some (p, Ps, Δ2) →
  CombineSepsAsGives Ps P R →
    (* this □ is okay, since we will call iDestructHyp anyway *)
  envs_app p (Esnoc (Esnoc Enil j P) k (□ R)%I) Δ2 = Some Δ3 →
  envs_entails Δ3 Q → envs_entails Δ1 Q.
Proof.
  rewrite envs_entails_unseal => ??? <-.
  rewrite (combine_seps_gives_of_envs _ _ _ _ Ps) //.
  rewrite envs_lookup_delete_list_sound //.
  rewrite combine_seps_as_gives_as envs_app_sound //.
  destruct p => /=.
  - rewrite right_id affinely_and -!intuitionistically_def.
    rewrite intuitionistically_idemp and_sep_intuitionistically.
    by rewrite -(comm _ (□ R)%I) assoc wand_elim_r.
  - by rewrite right_id -(comm _ (□ R)%I) assoc wand_elim_r.
Qed.
(* iris/proofmode/coq_tactics.v *)
(* * Conjunction/separating conjunction elimination *)
Lemma tac_and_destruct Δ i p j1 j2 P P1 P2 Q :
  envs_lookup i Δ = Some (p, P) →
  (if p then IntoAnd true P P1 P2 else IntoSep P P1 P2) →
  match envs_simple_replace i p (Esnoc (Esnoc Enil j1 P1) j2 P2) Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end →
  envs_entails Δ Q.
Proof.
  destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
  rewrite envs_entails_unseal. intros. rewrite envs_simple_replace_sound //=. destruct p.
  - rewrite (into_and _ P) /= right_id (comm _ P1).
    rewrite -persistently_and wand_elim_r //.
  - by rewrite /= (into_sep P) right_id -(comm _ P1) wand_elim_r.
Qed.