Library iris.proofmode.classes

Use this as precondition on "failing" instances of typeclasses that have pure preconditions (such as ElimModal), if you want a nice error to be shown when this instances is picked as part of some proof mode tactic.

FromPure a P φ is used when introducing a pure assertion. It is used by iPureIntro and the [%] specialization pattern. The Boolean a specifies whether introduction of P needs emp in addition to φ. Concretely, for the iPureIntro tactic, this means it specifies whether the spatial context should be empty or not. Note that the Boolean a is not needed for the (dual) IntoPure class, because there we can just ask that P is Affine.

The FromModal φ M sel P Q class is used by the iModIntro tactic to transform a goal P into a modality M and proposition Q, under additional pure assumptions φ. The inputs are P and sel and the outputs are M and Q. The input sel can be used to specify which modality to introduce in case there are multiple choices to turn P into a modality. For example, given ⎡|==> R⎤, sel can be either |==> ?e or ⎡ ?e ⎤, which turn it into an update modality or embedding, respectively. In case there is no need to specify the modality to introduce, sel should be an evar. For modalities N that do not need to augment the proof mode environment, one can define an instance FromModal True modality_id (N P) P. Defining such an instance only imposes the proof obligation P ⊢ N P. Examples of such modalities N are bupd, fupd, except_0, monPred_subjectively and bi_absorbingly.

The FromAffinely P Q class is used to add an <affine> modality to the proposition Q. The input is Q and the output is P.

The IntoAbsorbingly P Q class is used to add an <absorb> modality to the proposition Q. The input is Q and the output is P.

Converting an assumption R into a wand P -∗ Q is done in three stages:

• Strip modalities and universal quantifiers of R until an arrow or a wand has been obtained.
• Balance modalities in the arguments P and Q to match the goal (which used for iApply) or the premise (when used with iSpecialize and a specific hypothesis).
• Instantiate the premise of the wand or implication.

The IntoAnd p P Q1 Q2 class is used to handle some [H1 H2] intro patterns:

• IntoAnd true is used for such patterns in the intuitionistic context
• IntoAnd false is used for such patterns where one of the two sides is discarded (e.g. [_ H]) or where the left-hand side is pure as in [% H] (via an IntoExist fallback).

The inputs are p P and the outputs are Q1 Q2.

The IntoSep P Q1 Q2 class is used to handle [H1 H2] intro patterns in the spatial context, except:

• when one side is _, then IntoAnd is tried first (but IntoSep is used as fallback)
• when the left-hand side is %, then IntoExist is used)

The input is P and the outputs are Q1 Q2.

CombineSepAs, MaybeCombineSepAs and CombineSepGives are all used for the iCombine tactic. These three classes take two hypotheses P and Q as input, and return a (possibly simplified) new hypothesis R. CombineSepAs P Q R means that R may be obtained by deleting both P and Q, and that R is not a trivial combination. MaybeCombineSepAs P Q R progress is like CombineSepAs, but R can be the trivial combination P ∗ Q, and the progress parameter indicates whether this trivial combination is used. CombineSepGives P Q R means that □ R may be obtained 'for free' from P and Q. The result R of CombineSepAs and MaybeCombineSepAs will not contain the observations from CombineSepGives. We deliberately use separate typeclasses CombineSepAs and CombineSepGives. This allows one to (1) combine hypotheses and get additional persistent information, (2) only combine the hypotheses, without the additional persistent information, (3) only get the additional persistent information, while keeping the original hypotheses. A possible alternative would have been something like CombineSepAsGives P1 P2 P R := combine_as_gives : P1 ∗ P2 ⊢ P ∗ □ R, but this was deemed to be harder to use. Specifically, this would force you to always specify both P and R, even though one might only have a good candidate for P, but not R, or the other way around. Note that FromSep and CombineSepAs have nearly the same definition. However, they have different Hint Modes and are used for different tactics. FromSep is used to compute the two new goals obtained after applying iSplitL/iSplitR, taking the current goal as input. CombineSepAs is used to combine two hypotheses into one. In terms of costs, note that the AsFractional instance for CombineSepAs has cost 50. If that instance should take priority over yours, make sure to use a higher cost.

The progress parameter is of the following progress_indicator type:

This aims to make MaybeCombineSepAs instances easier to read than if we had used Booleans. NoProgress indicates that the default instance maybe_combine_sep_as_default below has been used, while MadeProgress indicates that a CombineSepAs instance was used.

We do not have this Maybe construction for CombineSepGives, nor do we provide the trivial CombineSepGives P Q True. This is by design: when the user writes down a 'gives' clause in the iCombine tactic, they intend to receive non-trivial information. If such information cannot be found, we want to produce an error, instead of the trivial hypothesis True.

The ElimModal φ p p' P P' Q Q' class is used by the iMod tactic. The inputs are p, P and Q, and the outputs are φ, p', P' and Q'. The class is used to transform a hypothesis P into a hypothesis P', given a goal Q, which is simultaneously transformed into Q'. The Booleans p and p' indicate whether the original, respectively, updated hypothesis reside in the persistent context (iff true). The proposition φ can be used to express a side-condition that iMod will generate (if not True). An example instance is: ElimModal True p false (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q). This instance expresses that to eliminate |={E1,E2}=> P the goal is transformed from |={E1,E3}=> Q into |={E2,E3}=> Q, and the resulting hypothesis is moved into the spatial context (regardless of where it was originally). A corresponding ElimModal instance for the Iris 1/2-style update modality, would have a side-condition φ on the masks.

We use the classes IsCons and IsApp to make sure that instances such as frame_big_sepL_cons and frame_big_sepL_app cannot be applied repeatedly often when having [∗ list] k ↦ x ∈ ?e, Φ k x with ?e an evar.

IsDisjUnion is similar to IsCons and IsApp but identifies the disj_union operator.

The class IntoEmbed P Q is used to transform hypotheses while introducing embeddings using iModIntro. Input: the proposition P, output: the proposition Q so that P ⊢ ⎡Q⎤.

Accessors. This definition only exists for the purpose of the proof mode; a truly usable and general form would use telescopes and also allow binders for the closing view shift. γ is an option to make it easy for ElimAcc instances to recognize the emp case and make it look nicer.

We make sure that tactics that perform actions on *specific* hypotheses or parts of the goal look through the tc_opaque connective, which is used to make definitions opaque for type class search. For example, when using iDestruct, an explicit hypothesis is affected, and as such, we should look through opaque definitions. However, when using iFrame or iNext, arbitrary hypotheses or parts of the goal are affected, and as such, type class opacity should be respected. This means that there are tc_opaque instances for all proofmode type classes with the exception of:

• FromAssumption used by iAssumption
• Frame and MaybeFrame used by iFrame
• MaybeIntoLaterN and FromLaterN used by iNext
• IntoPersistent used by iIntuitionistic