Library iris.proofmode.coq_tactics

From iris.bi Require Export bi telescopes.
From iris.proofmode Require Export base environments classes classes_make
modality_instances.
From iris.prelude Require Import options.
Import bi.
Import env_notations.

Local Open Scope lazy_bool_scope.

Section tactics.
Context {PROP : bi}.
Implicit Types Γ : env PROP.
Implicit Types Δ : envs PROP.
Implicit Types P Q : PROP.

Starting and stopping the proof mode

Lemma tac_start P : envs_entails (Envs Enil Enil 1) P → ⊢ P.
Proof.
  rewrite envs_entails_unseal !of_envs_eq /=.
  rewrite left_id=><-.
  apply and_intro⇒ //. apply pure_intro; repeat constructor.
Qed.

Lemma tac_stop Δ P :
  (match env_intuitionistic Δ, env_spatial Δ with
   | Enil, Γs ⇒ env_to_prop Γs
   | Γp, Enil ⇒ □ env_to_prop_and Γp
   | Γp, Γs ⇒ □ env_to_prop_and Γp ∗ env_to_prop Γs
   end ⊢ P ) →
  envs_entails Δ P.
Proof.
  rewrite envs_entails_unseal !of_envs_eq. intros <-. rewrite and_elim_r.
  destruct (env_intuitionistic Δ).
  { rewrite env_to_prop_sound and_elim_r //. }
  cbv zeta. destruct (env_spatial Δ).
  - rewrite env_to_prop_and_pers_sound. rewrite comm. done.
  - rewrite env_to_prop_and_pers_sound env_to_prop_sound.
    rewrite /bi_affinely [(emp ∧ _)%I]comm -persistent_and_sep_assoc left_id //.
Qed.

Basic rules

Lemma tac_eval Δ Q Q' :
  (∀ (Q'':=Q'), Q'' ⊢ Q ) →
  envs_entails Δ Q' → envs_entails Δ Q.
Proof. by intros <-. Qed.

Lemma tac_eval_in Δ i p P P' Q :
  envs_lookup i Δ = Some (p , P ) →
  (∀ (P'':=P'), P ⊢ P') →
  match envs_simple_replace i p (Esnoc Enil i P') Δ 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 ? HP ?.
  rewrite envs_simple_replace_singleton_sound //; simpl.
  by rewrite HP wand_elim_r.
Qed.

Class AffineEnv (Γ : env PROP) := affine_env : Forall Affine Γ.
Global Instance affine_env_nil : AffineEnv Enil.
Proof. constructor. Qed.
Global Instance affine_env_snoc Γ i P :
  Affine P → AffineEnv Γ → AffineEnv (Esnoc Γ i P).
Proof. by constructor. Qed.

Global Instance affine_env_bi `(!BiAffine PROP) Γ : AffineEnv Γ | 0.
Proof. induction Γ; apply _. Qed.

Local Instance affine_env_spatial Δ :
  AffineEnv (env_spatial Δ) → Affine ([∗] env_spatial Δ).
Proof. intros H. induction H; simpl; apply _. Qed.

Lemma tac_emp_intro Δ : AffineEnv (env_spatial Δ) → envs_entails Δ emp.
Proof. intros. by rewrite envs_entails_unseal (affine (of_envs Δ)). Qed.

Lemma tac_assumption Δ i p P Q :
  envs_lookup i Δ = Some (p ,P ) →
  FromAssumption p P Q →
  (let Δ' := envs_delete true i p Δ in
   if env_spatial_is_nil Δ' then TCTrue
   else TCOr (Absorbing Q) (AffineEnv (env_spatial Δ'))) →
  envs_entails Δ Q.
Proof.
  intros ?? H. rewrite envs_entails_unseal envs_lookup_sound //.
  simpl in ×. destruct (env_spatial_is_nil _) eqn:?.
  - by rewrite (env_spatial_is_nil_intuitionistically _) // sep_elim_l.
  - rewrite from_assumption. destruct H; by rewrite sep_elim_l.
Qed.

Lemma tac_assumption_coq Δ P Q :
  (⊢ P ) →
  FromAssumption false P Q →
  (if env_spatial_is_nil Δ then TCTrue
   else TCOr (Absorbing Q) (AffineEnv (env_spatial Δ))) →
  envs_entails Δ Q.
Proof.
  rewrite /FromAssumption /bi_emp_valid /= ⇒ HP HPQ H.
  rewrite envs_entails_unseal -(left_id emp%I bi_sep (of_envs Δ)).
  rewrite HP HPQ.
  destruct (env_spatial_is_nil _) eqn:?.
  - by rewrite (env_spatial_is_nil_intuitionistically _) // sep_elim_l.
  - destruct H; by rewrite sep_elim_l.
Qed.

Lemma tac_rename Δ i j p P Q :
  envs_lookup i Δ = Some (p ,P ) →
  match envs_simple_replace i p (Esnoc Enil j P) Δ 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⇒ ??. rewrite envs_simple_replace_singleton_sound //.
  by rewrite wand_elim_r.
Qed.

Lemma tac_clear Δ i p P Q :
  envs_lookup i Δ = Some (p ,P ) →
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) →
  envs_entails (envs_delete true i p Δ) Q →
  envs_entails Δ Q.
Proof.
  rewrite envs_entails_unseal⇒ ?? HQ. rewrite envs_lookup_sound //. rewrite HQ.
  by destruct p; rewrite /= sep_elim_r.
Qed.

False

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

Lemma tac_false_destruct Δ i p P Q :
  envs_lookup i Δ = Some (p ,P ) →
  P = False%I →
  envs_entails Δ Q.
Proof.
  rewrite envs_entails_unseal ⇒ ??. subst. rewrite envs_lookup_sound //; simpl.
  by rewrite intuitionistically_if_elim sep_elim_l False_elim.
Qed.

Pure

Lemma tac_pure_intro Δ Q φ a :
  FromPure a Q φ →
  (if a then AffineEnv (env_spatial Δ) else TCTrue ) →
  φ →
  envs_entails Δ Q.
Proof.
  intros ???. rewrite envs_entails_unseal -(from_pure a Q). destruct a; simpl.
  - by rewrite (affine (of_envs Δ)) pure_True // affinely_True_emp.
  - by apply pure_intro.
Qed.

Lemma tac_pure Δ i p P φ Q :
  envs_lookup i Δ = Some (p , P ) →
  IntoPure P φ →
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) →
  (φ → envs_entails (envs_delete true i p Δ) Q ) → envs_entails Δ Q.
Proof.
  rewrite envs_entails_unseal⇒ ?? HPQ HQ.
  rewrite envs_lookup_sound //; simpl. destruct p; simpl.
  - rewrite (into_pure P) -persistently_and_intuitionistically_sep_l persistently_pure.
    by apply pure_elim_l.
  - destruct HPQ.
    + rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_l.
      by apply pure_elim_l.
    + rewrite (into_pure P) -(persistent_absorbingly_affinely ⌜ _ ⌝) absorbingly_sep_lr.
      rewrite -persistent_and_affinely_sep_l. apply pure_elim_l⇒ ?. by rewrite HQ.
Qed.

Lemma tac_pure_revert Δ φ P Q :
  MakeAffinely ⌜ φ ⌝ P →
  envs_entails Δ (P -∗ Q) →
  (φ → envs_entails Δ Q ).
Proof.
  rewrite /MakeAffinely envs_entails_unseal. intros <- → ?.
  by rewrite pure_True // affinely_True_emp left_id.
Qed.

Intuitionistic

Lemma tac_intuitionistic Δ i j p P P' Q :
  envs_lookup i Δ = Some (p , P ) →
  IntoPersistent p P P' →
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) →
  match envs_replace i p true (Esnoc Enil j P') Δ with
  | None ⇒ False
  | Some Δ' ⇒ envs_entails Δ' Q
  end →
  envs_entails Δ Q.
Proof.
  destruct (envs_replace _ _ _ _ _) as [Δ'|] eqn:Hrep; last done.
  rewrite envs_entails_unseal=>?? HPQ HQ. rewrite envs_replace_singleton_sound //=.
  destruct p; simpl; rewrite /bi_intuitionistically.
  - by rewrite -(into_persistent true P) /= wand_elim_r.
  - 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.

Lemma tac_spatial Δ i j p P P' Q :
  envs_lookup i Δ = Some (p , P ) →
  (if p then FromAffinely P' P else TCEq P' P ) →
  match envs_replace i p false (Esnoc Enil j P') Δ with
  | None ⇒ False
  | Some Δ' ⇒ envs_entails Δ' Q
  end →
  envs_entails Δ Q.
Proof.
  intros ? HP. destruct (envs_replace _ _ _ _ _) as [Δ'|] eqn:Hrep; last done.
  rewrite envs_entails_unseal⇒ <-. rewrite envs_replace_singleton_sound //; simpl.
  destruct p; simpl; last destruct HP.
  - by rewrite intuitionistically_affinely (from_affinely P' P) wand_elim_r.
  - by rewrite wand_elim_r.
Qed.

Implication and wand

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.

Global 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.
Global 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.

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.

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.

Definition IntoEmpValid (φ : Type) (P : PROP) := φ → ⊢ P.

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 φ P → IntoEmpValid φ P.
Proof. by intros [??]. Defined.
Lemma into_emp_valid_impl (φ ψ : Type) P :
  φ → IntoEmpValid ψ P → IntoEmpValid (φ → ψ) P.
Proof. rewrite /IntoEmpValid ⇒ Hφ Hi1 Hi2. apply Hi1, Hi2, Hφ. Defined.
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.
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.
Lemma into_emp_valid_proj φ P : IntoEmpValid φ P → φ → ⊢ P.
Proof. intros HP. apply HP. Defined.

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.

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.

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.

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.

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.

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 PROPs. 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;
}.
Global Hint Mode CombineSepsAsGives + ! - - : typeclass_instances.
Global Arguments CombineSepsAsGives {_} _%_I _%_I _%_I.
Global Arguments combine_seps_as_gives_as {_} _%_I _%_I _%_I {_}.
Global Arguments combine_seps_as_gives_gives {_} _%_I _%_I _%_I {_}.

Global Instance combine_seps_as_gives_nil : @CombineSepsAsGives PROP [] emp True.
Proof.
  split; first done. rewrite persistently_True.
  by apply pure_intro.
Qed.
Global 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.
Global Instance combine_seps_gives_cons P Ps Q R Q' progress R' R'':
  CombineSepsAsGives Ps Q R →
  MaybeCombineSepAs P Q Q' progress →
  CombineSepGives P Q R' →
  MakeAnd R R' 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.

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.
Global Hint Mode CombineSepsAs + ! - : typeclass_instances.
Global Arguments CombineSepsAs {_} _%_I _%_I.
Global Arguments combine_seps_as {_} _%_I _%_I {_}.

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

Global 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.

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.

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.

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.

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 →

  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.

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.

Lemma tac_and_destruct_choice Δ i p d j P P1 P2 Q :
  envs_lookup i Δ = Some (p , P ) →
  (if p then IntoAnd p P P1 P2 : Type else
    TCOr (IntoAnd p P P1 P2) (TCAnd (IntoSep P P1 P2)
      (if d is Left then TCOr (Affine P2) (Absorbing Q)
       else TCOr (Affine P1) (Absorbing Q)))) →
  match envs_simple_replace i p (Esnoc Enil j (if d is Left then P1 else 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 ⇒ ? HP HQ.
  rewrite envs_simple_replace_singleton_sound //=. destruct p.
  { rewrite (into_and _ P) HQ. destruct d; simpl.
    - by rewrite and_elim_l wand_elim_r.
    - by rewrite and_elim_r wand_elim_r. }
  destruct HP as [?|[??]].
  { rewrite (into_and _ P) HQ. destruct d; simpl.
    - by rewrite and_elim_l wand_elim_r.
    - by rewrite and_elim_r wand_elim_r. }
  rewrite (into_sep P) HQ. destruct d; simpl.
  - by rewrite (comm _ P1) -assoc wand_elim_r sep_elim_r.
  - by rewrite -assoc wand_elim_r sep_elim_r.
Qed.

Framing

Lemma tac_frame_pure Δ (φ : Prop) P Q :
  φ → Frame true ⌜φ ⌝ P Q → envs_entails Δ Q → envs_entails Δ P.
Proof.
  rewrite envs_entails_unseal ⇒ ? Hframe →. rewrite -Hframe /=.
  rewrite -persistently_and_intuitionistically_sep_l persistently_pure.
  auto using and_intro, pure_intro.
Qed.

Lemma tac_frame Δ i p R P Q :
  envs_lookup i Δ = Some (p , R ) →
  Frame p R P Q →
  envs_entails (envs_delete false i p Δ) Q → envs_entails Δ P.
Proof.
  rewrite envs_entails_unseal. intros ? Hframe HQ.
  rewrite (envs_lookup_sound' _ false) //. by rewrite -Hframe HQ.
Qed.

Disjunction

Lemma tac_or_l Δ P Q1 Q2 :
  FromOr P Q1 Q2 → envs_entails Δ Q1 → envs_entails Δ P.
Proof.
  rewrite envs_entails_unseal⇒ ? →. rewrite -(from_or P). by apply or_intro_l'.
Qed.
Lemma tac_or_r Δ P Q1 Q2 :
  FromOr P Q1 Q2 → envs_entails Δ Q2 → envs_entails Δ P.
Proof.
  rewrite envs_entails_unseal⇒ ? →. rewrite -(from_or P). by apply or_intro_r'.
Qed.

Lemma tac_or_destruct Δ i p j1 j2 P P1 P2 Q :
  envs_lookup i Δ = Some (p , P ) → IntoOr P P1 P2 →
  match envs_simple_replace i p (Esnoc Enil j1 P1) Δ,
        envs_simple_replace i p (Esnoc Enil j2 P2) Δ with
  | Some Δ1, Some Δ2 ⇒ envs_entails Δ1 Q ∧ envs_entails Δ2 Q
  | _, _ ⇒ False
  end →
  envs_entails Δ Q.
Proof.
  destruct (envs_simple_replace i p (Esnoc Enil j1 P1)) as [Δ1|] eqn:?; last done.
  destruct (envs_simple_replace i p (Esnoc Enil j2 P2)) as [Δ2|] eqn:?; last done.
  rewrite envs_entails_unseal. intros ?? (HP1&HP2). rewrite envs_lookup_sound //.
  rewrite (into_or P) intuitionistically_if_or sep_or_r; apply or_elim.
  - rewrite (envs_simple_replace_singleton_sound' _ Δ1) //.
    by rewrite wand_elim_r.
  - rewrite (envs_simple_replace_singleton_sound' _ Δ2) //.
    by rewrite wand_elim_r.
Qed.

Forall

Lemma tac_forall_intro {A} Δ (Φ : A → PROP) Q name :
  FromForall Q Φ name →
  (
   let _ := name in
   ∀ a , envs_entails Δ (Φ a)) →
  envs_entails Δ Q.
Proof. rewrite envs_entails_unseal /FromForall⇒ <-. apply forall_intro. Qed.

Lemma tac_forall_specialize {A} Δ i p P (Φ : A → PROP) Q :
  envs_lookup i Δ = Some (p , P ) → IntoForall P Φ →
  (∃ x : A ,
      match envs_simple_replace i p (Esnoc Enil i (Φ x)) Δ with
      | None ⇒ False
      | Some Δ' ⇒ envs_entails Δ' Q
      end) →
  envs_entails Δ Q.
Proof.
  rewrite envs_entails_unseal. intros ?? (x&?).
  destruct (envs_simple_replace) as [Δ'|] eqn:?; last done.
  rewrite envs_simple_replace_singleton_sound //; simpl.
  by rewrite (into_forall P) (forall_elim x) wand_elim_r.
Qed.

Lemma tac_forall_revert {A} Δ (Φ : A → PROP) :
  envs_entails Δ (∀ a , Φ a) → ∀ a , envs_entails Δ (Φ a).
Proof. rewrite envs_entails_unseal ⇒ HΔ a. by rewrite HΔ (forall_elim a). Qed.

Existential

Lemma tac_exist {A} Δ P (Φ : A → PROP) :
  FromExist P Φ → (∃ a , envs_entails Δ (Φ a)) → envs_entails Δ P.
Proof.
  rewrite envs_entails_unseal ⇒ ? [a ?].
  rewrite -(from_exist P). eauto using exist_intro'.
Qed.

Lemma tac_exist_destruct {A} Δ i p j P (Φ : A → PROP) (name: ident_name) Q :
  envs_lookup i Δ = Some (p , P ) → IntoExist P Φ name →
  (
    let _ := name in
    ∀ a ,
     match envs_simple_replace i p (Esnoc Enil j (Φ a)) Δ with
     | Some Δ' ⇒ envs_entails Δ' Q
     | None ⇒ False
     end) →
  envs_entails Δ Q.
Proof.
  rewrite envs_entails_unseal ⇒ ?? HΦ. rewrite envs_lookup_sound //.
  rewrite (into_exist P) intuitionistically_if_exist sep_exist_r.
  apply exist_elim⇒ a; specialize (HΦ a) as Hmatch.
  destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
  rewrite envs_simple_replace_singleton_sound' //; simpl. by rewrite wand_elim_r.
Qed.

Modalities

Lemma tac_modal_elim Δ i j p p' φ P' P Q Q' :
  envs_lookup i Δ = Some (p , P ) →
  ElimModal φ p p' P P' Q Q' →
  φ →
  match envs_replace i p p' (Esnoc Enil j P') Δ with
  | None ⇒ False
  | Some Δ' ⇒ envs_entails Δ' Q'
  end →
  envs_entails Δ Q.
Proof.
  destruct (envs_replace _ _ _ _ _) as [Δ'|] eqn:?; last done.
  rewrite envs_entails_unseal ⇒ ??? HΔ. rewrite envs_replace_singleton_sound //=.
  rewrite HΔ. by eapply elim_modal.
Qed.

Accumulate hypotheses

Lemma tac_accu Δ P :
  env_to_prop (env_spatial Δ) = P →
  envs_entails Δ P.
Proof.
  rewrite envs_entails_unseal=><-.
  rewrite env_to_prop_sound !of_envs_eq and_elim_r and_elim_r //.
Qed.

Invariants

Lemma tac_inv_elim {X : Type} Δ i j φ p Pinv Pin Pout (Pclose : option (X → PROP))
      Q (Q' : X → PROP) :
  envs_lookup i Δ = Some (p , Pinv ) →
  ElimInv φ Pinv Pin Pout Pclose Q Q' →
  φ →
  (∀ R ,
    match envs_app false (Esnoc Enil j
      (Pin -∗
       (∀ x , Pout x -∗ pm_option_fun Pclose x -∗? Q' x ) -∗
       R
      )%I) (envs_delete false i p Δ)
    with Some Δ'' ⇒ envs_entails Δ'' R | None ⇒ False end) →
  envs_entails Δ Q.
Proof.
  rewrite envs_entails_unseal⇒ ? Hinv ? /(_ Q) Hmatch.
  destruct (envs_app _ _ _) eqn:?; last done.
  rewrite -Hmatch (envs_lookup_sound' _ false) // envs_app_singleton_sound //; simpl.
  apply wand_elim_r', wand_mono; last done. apply wand_intro_r, wand_intro_r.
  rewrite intuitionistically_if_elim -assoc. destruct Pclose; simpl in ×.
  - setoid_rewrite wand_curry. auto.
  - setoid_rewrite <-(right_id emp%I _ (Pout _)). auto.
Qed.

Rewriting

Lemma tac_rewrite `{!BiInternalEq PROP} Δ i p Pxy d Q :
  envs_lookup i Δ = Some (p , Pxy ) →
  ∀ {A : ofe} (x y : A) (Φ : A → PROP ),
    IntoInternalEq Pxy x y →
    (Q ⊣⊢ Φ (if d is Left then y else x)) →
    NonExpansive Φ →
    envs_entails Δ (Φ (if d is Left then x else y)) → envs_entails Δ Q.
Proof.
  intros ? A x y ? HPxy → ?. rewrite envs_entails_unseal.
  apply internal_eq_rewrite'; auto. rewrite {1}envs_lookup_sound //.
  rewrite (into_internal_eq Pxy x y) intuitionistically_if_elim sep_elim_l.
  destruct d; auto using internal_eq_sym.
Qed.

Lemma tac_rewrite_in `{!BiInternalEq PROP} Δ i p Pxy j q P d Q :
  envs_lookup i Δ = Some (p , Pxy ) →
  envs_lookup j Δ = Some (q , P ) →
  ∀ {A : ofe} (x y : A) (Φ : A → PROP ),
    IntoInternalEq Pxy x y →
    (P ⊣⊢ Φ (if d is Left then y else x)) →
    NonExpansive Φ →
    match envs_simple_replace j q (Esnoc Enil j (Φ (if d is Left then x else y))) Δ with
    | None ⇒ False
    | Some Δ' ⇒ envs_entails Δ' Q
    end →
    envs_entails Δ Q.
Proof.
  rewrite envs_entails_unseal /IntoInternalEq ⇒ ?? A x y Φ HPxy HP ? Hentails.
  destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:?; last done. rewrite -Hentails.
  rewrite -(idemp bi_and (of_envs Δ)) {2}(envs_lookup_sound _ i) //.
  rewrite (envs_simple_replace_singleton_sound _ _ j) //=.
  rewrite HP HPxy (intuitionistically_if_elim _ (_ ≡ _)) sep_elim_l.
  rewrite persistent_and_affinely_sep_r -assoc. apply wand_elim_r'.
  rewrite -persistent_and_affinely_sep_r. apply impl_elim_r'. destruct d.
  - apply (internal_eq_rewrite x y (λ y , □?q Φ y -∗ of_envs Δ')%I). solve_proper.
  - rewrite internal_eq_sym.
    eapply (internal_eq_rewrite y x (λ y , □?q Φ y -∗ of_envs Δ')%I). solve_proper.
Qed.

Löb

Lemma tac_löb Δ i Q :
  BiLöb PROP →
  env_spatial_is_nil Δ = true →
  match envs_app true (Esnoc Enil i (▷ Q)%I) Δ with
  | None ⇒ False
  | Some Δ' ⇒ envs_entails Δ' Q
  end →
  envs_entails Δ Q.
Proof.
  destruct (envs_app _ _ _) as [Δ'|] eqn:?; last done.
  rewrite envs_entails_unseal ⇒ ?? HQ.
  rewrite (env_spatial_is_nil_intuitionistically Δ) //.
  rewrite envs_app_singleton_sound //; simpl. rewrite HQ.
  apply löb_wand_intuitionistically.
Qed.
End tactics.

Introduction of modalities

The following private classes are used internally by tac_modal_intro / iModIntro to transform the proofmode environments when introducing a modality.

The class TransformIntuitionisticEnv M C Γin Γout is used to transform the intuitionistic environment using a type class C.

Inputs:

Γin : the original environment.
M : the modality that the environment should be transformed into.
C : PROP → PROP → Prop : a type class that is used to transform the individual hypotheses. The first parameter is the input and the second parameter is the output.

Outputs:

Γout : the resulting environment.

The actual introduction tactic

  Lemma tac_modal_intro {A} φ (sel : A) Γp Γs n Γp' Γs' Q Q' fi :
    FromModal φ M sel Q' Q →
    IntoModalIntuitionisticEnv M Γp Γp' (modality_intuitionistic_action M) →
    IntoModalSpatialEnv M Γs Γs' (modality_spatial_action M) fi →
    (if fi then Absorbing Q' else TCTrue ) →
    φ →
    envs_entails (Envs Γp' Γs' n) Q → envs_entails (Envs Γp Γs n) Q'.
  Proof.
    rewrite envs_entails_unseal /FromModal !of_envs_eq ⇒ HQ' HΓp HΓs ? Hφ HQ.
    apply pure_elim_l⇒ -[???]. assert (envs_wf (Envs Γp' Γs' n)) as Hwf.
    { split; simpl in ×.
      - destruct HΓp as [| |????? []| |]; eauto using Enil_wf.
      - destruct HΓs as [| |?????? []| |]; eauto using Enil_wf.
      - assert (∀ i , Γp !! i = None → Γp' !! i = None).
        { destruct HΓp as [| |????? []| |]; eauto. }
        assert (∀ i , Γs !! i = None → Γs' !! i = None).
        { destruct HΓs as [| |?????? []| |]; eauto. }
        naive_solver. }
    trans (<absorb >?fi Q')%I; last first.
    { destruct fi; last done. apply: absorbing. }
    simpl. rewrite -(HQ' Hφ). rewrite -HQ pure_True // left_id. clear HQ' HQ.
    rewrite !persistent_and_affinely_sep_l.
    rewrite -modality_sep absorbingly_if_sep. f_equiv.
    - rewrite -absorbingly_if_intro.
      remember (modality_intuitionistic_action M).
      destruct HΓp as [? M|M C Γp ?%TCForall_Forall|? M C Γp Γp' []|? M Γp|M Γp]; simpl.
      + rewrite !affinely_True_emp. apply modality_emp.
      + eauto using modality_intuitionistic_forall_big_and.
      + eauto using modality_intuitionistic_transform,
          modality_and_transform.
      + by rewrite {1}affinely_elim_emp affinely_True_emp (modality_emp M).
      + eauto using modality_intuitionistic_id_big_and.
    - remember (modality_spatial_action M).
      destruct HΓs as [? M|M C Γs ?%TCForall_Forall|? M C Γs Γs' fi []|? M Γs|M Γs]; simpl.
      + by rewrite modality_emp.
      + rewrite {1}(modality_spatial_forall_big_sep _ _ Γs) //.
      + destruct fi.
        × rewrite /= /bi_absorbingly (comm _ True%I).
          eauto using modality_spatial_transform.
        × rewrite /= -(right_id emp%I bi_sep (M _)).
          eauto using modality_spatial_transform.
      + rewrite -{1}(modality_spatial_clear M) // -modality_emp.
        rewrite absorbingly_emp_True. apply True_intro.
      + rewrite {1}(modality_spatial_id M ([∗] Γs)) //.
  Qed.
End tac_modal_intro.

The class MaybeIntoLaterNEnvs is used by tactics that need to introduce laters, e.g., the symbolic execution tactics.

Class MaybeIntoLaterNEnvs {PROP : bi} (n : nat) (Δ1 Δ2 : envs PROP) := {
  into_later_intuitionistic :
    TransformIntuitionisticEnv (modality_laterN n) (MaybeIntoLaterN false n)
      (env_intuitionistic Δ1) (env_intuitionistic Δ2);
  into_later_spatial :
    TransformSpatialEnv (modality_laterN n)
      (MaybeIntoLaterN false n) (env_spatial Δ1) (env_spatial Δ2) false
}.

Global Instance into_laterN_envs {PROP : bi} n (Γp1 Γp2 Γs1 Γs2 : env PROP) m :
  TransformIntuitionisticEnv (modality_laterN n) (MaybeIntoLaterN false n) Γp1 Γp2 →
  TransformSpatialEnv (modality_laterN n) (MaybeIntoLaterN false n) Γs1 Γs2 false →
  MaybeIntoLaterNEnvs n (Envs Γp1 Γs1 m) (Envs Γp2 Γs2 m).
Proof. by split. Qed.

Lemma into_laterN_env_sound {PROP : bi} n (Δ1 Δ2 : envs PROP) :
  MaybeIntoLaterNEnvs n Δ1 Δ2 → of_envs Δ1 ⊢ ▷^n (of_envs Δ2 ).
Proof.
  intros [[Hp ??] [Hs ??]]; rewrite !of_envs_eq.
  rewrite ![(env_and_persistently _ ∧ _)%I]persistent_and_affinely_sep_l.
  rewrite !laterN_and !laterN_sep.
  rewrite -{1}laterN_intro. apply and_mono, sep_mono.
  - apply pure_mono; destruct 1; constructor; naive_solver.
  - apply Hp; rewrite /= /MaybeIntoLaterN.
    + intros P Q →. by rewrite laterN_intuitionistically_2.
    + intros P Q. by rewrite laterN_and.
  - by rewrite Hs //= right_id.
Qed.