Library iris.bi.sbi_unfold

The tactic takes a (bi-)entailment of plain propositions and turns it into a a (bi-)implication in the pure step-indexed model. For example, given the goal: x ≼ y ⊣⊢ x.1 ≼ y.1 ∧ x.2 ≼ y.2 The tactic sbi_unfold turns it into ∀ n, x ≼{n} y ↔ x.1 ≼{n} y.1 ∧ x.2 ≼{n} y.2 The tactic sbi_unfold works for goals of the shape ⊢ P, P ⊢ Q, P ⊣⊢ Q. Here, P and Q should be in the "plain" subset of propositions, i.e., ⌜ _ ⌝, <si_pure>, ✓, ≡, ≼, closed under ∧, ∨, →, ∀, ∃, ▷, and match. The separating connectives ∗/-∗ are translated to ∧/→. The tactic attempts to minimize the number of "down closures" ∀ n'. n' ≤ n → .. due to the use of nested implications. For example, given: ⊢ x.1 ≼ y.1 → x.2 ≼ y.2 → x ≼ y The tactic sbi_unfold turns it into ∀ n, x.1 ≼{n} y.1 → x.2 ≼{n} y.2 → x ≼{n} y Instead of (the logically equivalent, but more verbose): ∀ n, ∀ n' ≤ n. x.1 ≼{n'} y.1 → ∀ n'' ≤ n'. x.2 ≼{n''} y.2 → x ≼{n''} y The tactic is implemented using the type class SbiUnfold clo P Pi, which takes a proposition P (which is intended to be plain) as input and produces its interpretation Pi : nat → Prop in the step-indexed model as output, so that the down closure of Pi is equivalent to P. The input indicator clo indicates whether the output Pi should be down closed, i.e., Pi should satisfy Pi n1 → n2 ≤ n1 → Pi n2. In this case there is no need to explicitly down close Pi. We use the clo parameter to avoid needless down closures in the translation of implications (see the example above). In the instance sbi_unfold_impl for P → Q we call SbiUnfold on Q with clo being NotClosed. This optimization is sound because ∀ n' ≤ n, Pi n' → Qi n' and ∀ n' ≤ n, Pi n' → downclose Qi n' are equivalent if Pi is downclosed. Use a Module to avoid polluting the global namespace with the constructor names, one should use sbi_unfold_closure_indicator.NotClosed.

This instance can be applied to any P : siProp so it has cost 100 to make sure it's only used if no other instance can be used.

The top-level lemmas used by the tactic

The instances

The instance for disjunction needs the sub-expressions to be already down closed because ∨ and ∀ do not commute.

The instance for existential needs the sub-expression to be already down closed because ∃ and ∀ do not commute.

We use a Hint Extern to translate match. Intuitively, we want an instance: SbiUnfold (match x with Cj => Pj end) (λ n, match x with Cj => Pij n end) Here, we have SbiUnfold Pj Pij for the branch of each constructor Cj in the match. Actually generating λ n, match x with Cj ⇒ Pij n end is quite fiddly.