Library zoo.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.

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.

Basic rules

Lemma tac_eval Δ Q Q' :
  (Q' ⊢ Q) →
  envs_entails Δ Q' → envs_entails Δ Q.

Lemma tac_eval_in Δ i p P P' Q :
  envs_lookup i Δ = Some (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.

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

Global Instance affine_env_bi `(!BiAffine PROP) Γ : AffineEnv Γ | 0.

Local Instance affine_env_spatial Δ :
  AffineEnv (env_spatial Δ) → Affine ([∗] env_spatial Δ).

Lemma tac_emp_intro Δ : AffineEnv (env_spatial Δ) → envs_entails Δ emp.

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.

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.

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.

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.

False

Lemma tac_ex_falso Δ Q : envs_entails Δ False → envs_entails Δ Q.

Lemma tac_false_destruct Δ i p P Q :
  envs_lookup i Δ = Some (p ,P ) →
  P = False%I →
  envs_entails Δ Q.

Pure

Lemma tac_pure_intro Δ Q φ a :
  FromPure a Q φ →
  (if a then AffineEnv (env_spatial Δ) else TCTrue) →
  φ →
  envs_entails Δ Q.

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.

Lemma tac_pure_revert Δ φ P Q :
  MakeAffinely ⌜ φ ⌝ P →
  envs_entails Δ (P -∗ Q) →
  (φ → envs_entails Δ Q).

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.

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.

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

Lemma tac_revert_ih Δ P Q {φ : Prop} (H φ : φ) :
  IntoIH φ Δ P →
  env_spatial_is_nil Δ = true →
  envs_entails Δ (<pers > P → Q) →
  envs_entails Δ Q.

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.

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 DirectionIntoEmpValid φ P → IntoEmpValid φ P.
Lemma into_emp_valid_impl (φ ψ : Type) P :
  φ → IntoEmpValid ψ P → IntoEmpValid (φ → ψ) P.
Lemma into_emp_valid_forall {A} (φ : A → Type) P x :
  IntoEmpValid (φ x) P → IntoEmpValid (∀ x : A, φ x) P.
Lemma into_emp_valid_tforall {TT : tele} (φ : TT → Prop) P x :
  IntoEmpValid (φ x) P → IntoEmpValid (∀.. x : TT , φ x) P.
Lemma into_emp_valid_proj φ P : IntoEmpValid φ P → φ → ⊢ P.

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.

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.

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.

Conjunction splitting

Lemma tac_and_split Δ P Q1 Q2 :
FromAnd P Q1 Q2 → envs_entails Δ Q1 → envs_entails Δ Q2 → envs_entails Δ P.

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.

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 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.
Global Instance combine_seps_as_gives_singleton P :
  CombineSepsAsGives [P] P True | 1.
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..}.

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

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.

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.

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.

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.

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.

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.

Framing

Lemma tac_frame_pure Δ (φ : Prop) P Q :
  φ → Frame true ⌜φ ⌝ P Q → envs_entails Δ Q → envs_entails Δ P.

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.

Disjunction

Lemma tac_or_l Δ P Q1 Q2 :
  FromOr P Q1 Q2 → envs_entails Δ Q1 → envs_entails Δ P.
Lemma tac_or_r Δ P Q1 Q2 :
  FromOr P Q1 Q2 → envs_entails Δ Q2 → envs_entails Δ P.

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.

Forall

Lemma tac_forall_intro {A} Δ (Φ : A → PROP) Q name :
  FromForall Q Φ name →
  (
   let _ := name in
   ∀ a, envs_entails Δ (Φ a)) →
  envs_entails Δ Q.

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.

Lemma tac_forall_revert {A} Δ (Φ : A → PROP) :
  envs_entails Δ (∀ a , Φ a) → ∀ a, envs_entails Δ (Φ a).

Existential

Lemma tac_exist {A} Δ P (Φ : A → PROP) :
  FromExist P Φ → (∃ a, envs_entails Δ (Φ a)) → envs_entails Δ P.

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.

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.

Accumulate hypotheses

Lemma tac_accu Δ P :
env_to_prop (env_spatial Δ) = P →
envs_entails Δ P.

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.

Rewriting

Lemma tac_rewrite `{!Sbi 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.

Lemma tac_rewrite_in `{!Sbi 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.

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.
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'.
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).

Lemma into_laterN_env_sound {PROP : bi} n (Δ1 Δ2 : envs PROP) :
  MaybeIntoLaterNEnvs n Δ1 Δ2 → of_envs Δ1 ⊢ ▷^n (of_envs Δ2 ).