From 79d0d5fdfbc98f71383153f298a6bbb86263a76c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 5 Jul 2016 18:14:16 +0200
Subject: [PATCH] Write some proof mode documentation.
---
ProofMode.md | 390 ++++++++++++++++++++++++---------------------------
README.md | 2 +-
2 files changed, 183 insertions(+), 209 deletions(-)
diff --git a/ProofMode.md b/ProofMode.md
index d08a5408a..5a132163c 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -1,227 +1,201 @@
-The proof mode has the following major features:
+Tactic overview
+===============
+
+Applying hypotheses and lemmas
+------------------------------
+
+- `iExact "H"` : finish the goal if the conclusion matches the hypothesis `H`
+- `iAssumption` : finish the goal if the conclusion matches any hypothesis
+- `iApply trm` : match the conclusion of the current goal against the
+ conclusion of `tetrmrm` and generates goals for the premises of `trm`. See
+ proof mode terms below.
+
+Context management
+------------------
+
+- `iIntros {x1 ... xn} "ipat1 ... ipatn"` : introduce universal quantifiers
+ using Coq introduction patterns `x1 ... xn` and implications/wands using proof
+ mode introduction patterns `ipat1 ... ipatn`.
+- `iClear "H1 ... Hn"` : clear the hypothesis `H1 ... Hn`. The symbol `★` can
+ be used to clear entire spatial context.
+- `iRevert {x1 ... xn} "H1 ... Hn"` : revert the proof mode hypotheses
+ `H1 ... Hn` into wands, as well as the Coq level hypotheses/variables
+ `x1 ... xn` into universal quantifiers. The symbol `★` can be used to revert
+ the entire spatial context.
+- `iRename "H1" into "H2"` : rename the hypothesis `H1` into `H2`.
+- `iSpecialize trm` : instantiate universal quantifiers and eliminate
+ implications/wands of a hypothesis `trm`. See proof mode terms below.
+- `iPoseProof trm as "H"` : put `trm` into the context as a new hypothesis `H`.
+- `iAssert P with "spat" as "ipat"` : create a new goal with conclusion `P` and
+ put `P` in the context of the original goal. The specialization pattern
+ `spat` specifies which hypotheses will be consumed by proving `P` and the
+ introduction pattern `ipat` specifies how to eliminate `P`.
+
+Introduction of logical connectives
+-----------------------------------
+
+- `iPureIntro` : turn a pure goal into a Coq goal. This tactic works for goals
+ of the shape `■φ`, `a ≡ b` on discrete COFEs, and `✓ a` on discrete CMRAs.
+
+- `iLeft` : left introduction of disjunction.
+- `iRight` : right introduction of disjunction.
+
+- `iSplit` : introduction of a conjunction, or separating conjunction provided
+ one of the operands is persistent.
+- `iSplitL "H1 ... Hn"` : introduction of a separating conjunction. The
+ hypotheses `H1 ... Hn` are used for the left conjunct, and the remaining ones
+ for the right conjunct.
+- `iSplitR "H0 ... Hn"` : symmetric version of the above.
+- `iExist t1, .., tn` : introduction of an existential quantifier.
+
+Elimination of logical connectives
+----------------------------------
+
+- `iExFalso` : Ex falso sequitur quod libet.
+- `iDestruct trm as {x1 ... xn} "spat1 ... spatn"` : elimination of existential
+ quantifiers using Coq introduction patterns `x1 ... xn` and elimination of
+ object level connectives using the proof mode introduction patterns
+ `ipat1 ... ipatn`.
+
+Separating logic specific tactics
+---------------------------------
+
+- `iFrame "H0 ... Hn"` : cancel the hypotheses `H0 ... Hn` in the goal.
+- `iCombine "H1" "H2" as "H"` : turns `H1 : P1` and `H2 : P2` into
+ `H : P1 ★ P2`.
+
+The later modality
+------------------
+- `iNext` : introduce a later by stripping laters from all hypotheses.
+- `iLöb {x1 ... xn} as "IH"` : perform Löb induction by generalizing over the
+ Coq level variables `x1 ... xn` and the entire spatial context.
+
+Rewriting
+---------
+
+- `iRewrite trm` : rewrite an equality in the conclusion.
+- `iRewrite trm in "H"` : rewrite an equality in the hypothesis `H`.
+
+Iris
+----
+
+- `iPvsIntro` : introduction of a primitive view shift. Generates a goal if
+ the masks are not syntactically equal.
+- `iPvs trm as {x1 ... xn} "ipat"` : runs a primitive view shift `trm`.
+- `iInv N as {x1 ... xn} "ipat"` : open the invariant `N`.
+- `iInv> N as {x1 ... xn} "ipat"` : open the invariant `N` and establish that
+ it is timeless so no laters have to be added.
+- `iTimeless "H"` : strip a later of a timeless hypotheses `H` in case the
+ conclusion is a primitive view shifts or weakest precondition.
+
+Miscellaneous
+-------------
+
+- The tactic `done` is extended so that it also performs `iAssumption` and
+ introduces pure connectives.
+- The proof mode adds hints to the core `eauto` database so that `eauto`
+ automatically introduces: conjunctions and disjunctions, universal and
+ existential quantifiers, implications and wand, always and later modalities,
+ primitive view shifts, and pure connectives.
+
+Introduction patterns
+=====================
+
+Introduction patterns are used to perform introductions and eliminations of
+multiple connectives on the fly. The proof mode supports the following
+introduction patterns:
+
+- `H` : create a hypothesis named H.
+- `?` : create an anonymous hypothesis.
+- `_` : remove the hypothesis.
+- `$` : frame the hypothesis in the goal.
+- `# ipat` : move the hypothesis to the persistent context.
+- `%` : move the hypothesis to the pure Coq context (anonymously).
+- `[ipat ipat]` : (separating) conjunction elimination.
+- `|ipat|ipat]` : disjunction elimination.
+- `[]` : false elimination.
+
+Apart from this, there are the following introduction patterns that can only
+appear at the top level:
+
+- `!` : introduce a box (provided that the spatial context is empty).
+- `>` : introduce a later (which strips laters from all hypotheses).
+- `{H1 ... Hn}` : clear `H1 ... Hn`.
+- `{$H1 ... $Hn}` : frame `H1 ... Hn` (this pattern can be mixed with the
+ previous pattern, e.g., `{$H1 H2 #H3}`).
+- `/=` : perform `simpl`.
+- `*` : introduce all universal quantifiers.
+- `**` : introduce all universal quantifiers, as well as all arrows and wands.
+
+For example, given:
-=== Intro patterns ===
+ ∀ x, x = 0 ⊢ □ (P → False ∨ □ (Q ∧ ▷ R) -★ P ★ ▷ (R ★ Q ∧ x = pred 2)).
-Similar to Coq's intro tactic, the Iris iIntros tactic can take a list of intro patterns to perform destructions on the fly. Apart from the standard intro patterns (like "?" for creating an anonymous hypothesis, "[p p]" for eliminating a (separating) conjunction, "[p|p]" for eliminating a disjunction, and "[]" for eliminating False, it supports:
+You can write
- # pat : move the hypothesis to the persistent context
- % : move the hypothesis to the pure Coq context
- as an anonymous assumption
- ! : introduce a box (this pattern can only appear at the
- to-level, and can be used only if the spatial context
- is empty)
+ iIntros {x} "% ! $ [[] | #[HQ HR]] /= >".
+
+which results in:
-So, for example, given:
+ x : nat
+ H : x = 0
+ ______________________________________(1/1)
+ ​​"HQ" : Q
+ ​"HR" : R
+ --------------------------------------â–¡
+ R ★ Q ∧ x = 1
- ∀ x, x = 0 → □ (P → □ (Q ∧ ▷ R) -★ ▷ (P ★ R ★ Q ∧ x = 0))
-You can write: iIntros {x} "% ! HP #[HQ HR]", which results in:
+Specialization patterns
+=======================
- H : x = 0
- ______________________________________(1/1)
-​​​ "HQ" : Q
- "HR" : â–· R
- --------------------------------------â–¡
-​​ "HP" : P
- --------------------------------------★
- ▷ (P ★ R ★ Q ∧ x = 0)
+Since we are reasoning in a spatial logic, when eliminating a lemma or
+hypotheses of type ``P_0 -★ ... -★ P_n -★ R`` one has to specify how the
+hypotheses are split between the premises. The proof mode supports the following
+so called specification patterns to express this splitting:
-(Syntax subject to improvements :))
+- `H` : use the hypothesis `H` (it should match the premise exactly). If `H` is
+ spatial, it will be consumed.
+- `[H1 ... Hn]` : generate a goal with the spatial hypotheses `H1 ... Hn` and
+ all persistent hypotheses. The hypotheses `H1 ... Hn` will be consumed.
+- `[-H1 ... Hn]` : negated form of the above pattern
+- `=>[H1 ... Hn]` : same as the above pattern, but can only be used if the goal
+ is a primitive view shift, in which case the view shift will be kept in the
+ goal of the premise too.
+- `[#]` : This pattern can be used when eliminating `P -★ Q` when either `P` or
+ `Q` is persistent. In this case, all hypotheses are available in the goal for
+ the premise as none will be consumed.
+- `[%]` : This pattern can be used when eliminating `P -★ Q` when `P` is pure.
+ It will generate a Coq goal for `P` and does not consume any hypotheses.
+- `*` : instantiate all top-level universal quantifiers with meta variables.
-(Due to limitations of Ltac, introductions for universal quantifiers always have to appear at the beginning and cannot be mixed).
+For example, given:
+ H : □ P -★ P 2 -★ x = 0 -★ Q1 ∗ Q2
-=== Extensibility ===
+You can write:
-The destruction patterns "[p p]" and "[p|p]" do not just work for (separating) conjunctions and disjunctions. For example, when having:
+ iDestruct ("H" with "[#] [H1 H2] [%]") as "[H4 H5]".
- "H" : l ↦{q} v
+Proof mode terms
+================
+
+Many of the proof mode tactics (such as `iDestruct`, `iApply`, `iRewrite`) can
+take both hypotheses and lemmas, and allow one to instantiate universal
+quantifiers and implications/wands of these hypotheses/lemmas on the fly.
-You can write iDestruct "H" as "[H1 H2]" to split the fractional maps to connective into:
+The syntax for the arguments, called _proof mode terms_ of these tactics is:
- "H1" : l ↦{q/2} v
- "H2" : l ↦{q/2} v
+ (H $! t1 ... tn with "spat1 .. spatn")
-The proof mode can be extended using type classes to support all kinds of "destructable" connectives.
+Here, `H` can be both a hypothesis, as well as a Coq lemma whose conclusion is
+of the shape `P ⊢ Q`. In the above, `t1 ... tn` are arbitrary Coq terms used
+for instantiation of universal quantifiers, and `spat1 .. spatn` are
+specialization patterns to eliminate implications and wands.
-I am using type classes for extensibility in many places. The core proof mode thus works for uPred M with any cmra M, and is not tied to the entire Iris logic.
+Proof mode terms can be written down using the following short hands too:
+ (H with "spat1 .. spatn")
+ (H $! t1 ... tn)
+ H
-=== Later ===
-
-The proof mode has a tactic iNext to introduce a later. This tactic will remove a later in the conclusion, and removes laters in all hypotheses. In the above example, when having:
-
-​​​ "HQ" : Q
- "HR" : â–· R
- --------------------------------------â–¡
-​​ "HP" : P
- --------------------------------------★
- ▷ (P ★ R ★ Q ∧ x = 0)
-
-The tactic iNext will remove the later in HR and in the goal. All other hypotheses are left as if. The iNext tactic is extensible; my means of declaring appropriate type class instances you can also make it strip laters below certain connectives (like below ★).
-
-Apart from that, tactics like iDestruct are able to distribute laters. So, when having:
-
- H : ▷ (P ★ Q)
-
-iDestruct will turn it into H1 : â–· P and H2 â–· Q. This can of course be tweaked by declaring type class instances.
-
-
-=== Separating conjunction and framing ===
-
-When proving a separating conjunction P ★ Q, one has to split the spatial hypotheses. The Iris tactics iSplitL and iSplitR take a list of hypotheses that have to be used to prove the conjunct on the left, respectively, the right, the goal for other other conjunct will have all remaining hypotheses.
-
-Apart from that, there is the tactic iFrame which takes a list of hypotheses to frame in the goal. For example, having:
-
- "HQ" : Q
- "HR" : R
- --------------------------------------â–¡
-​​ "HP" : P
- --------------------------------------★
- P ★ R ★ Q ∧ x = 0
-
-The tactic iFrame "HQ HP" will turn the goal into "R ★ x = 0". Note that persistent hypotheses are kept, only spatial hypotheses disappear. So in the example ,"HQ" is kept, but "HP" is gone, after framing.
-
-The iFrame tactic is able to frame under quantifiers and primitive viewshifts. None of this is hard coded, but instead, the tactic can be extended by declaring appropriate type classes, for example, to make it frame under weakest precondition.
-
-
-=== Apply and specialization patterns ===
-
-Given an hypothesis that is an implication:
-
- ​​"H" : P_0 -★ ... -★ P_n -★ R
-
-One cannot just "apply" this hypothesis (as in ordinary Coq) since we are in a spatial logic. So, when applying a lemma you have to specify which hypotheses are used for which premises. For this, Iris has the following, so called, specialization patterns:
-
- H : use hypothesis H (it should match the premise exactly)
- [H1 ... Hn] : use hypotheses H1 ... Hn
- -[H1 ... Hn] : use all hypotheses but H1 ... Hn
- (you can write - instead of -[])
- # : determine that the premise is persistent, in this
- case all hypotheses can be used (and do not
- disappear)
-
-So, in the above you may write:
-
- iApply "H" "[H1 H2] # H3"
-
-This means: create a goal with hypotheses H1 and H2 for the first premise, establish that the second premise is persistent and use all hypotheses for that one, and match the third premise with H3 exactly.
-
-These specialization patterns can be used for many more tactics, for example, you can write:
-
- iDestruct "H" "spec_pattern" as "intro_pattern"
- iSpecialize "H" "spec_pattern"
- iPoseProof "H" "spec_pattern" as "H2"
-
-I noticed that these specialization patterns are not enough, so there are even more. Take the following lemma:
-
- own_valid : ∀ γ a, own γ a ⊢ ✓ a
-
-Given "H" : own γ a you may want to write:
-
- iPoseProof own_valid "H" as "Hvalid"
-
-But in this case "H" will disappear (and you would loose information). So, there are also the following specialization patterns:
-
- H ! : use hypothesis H and establish that the range of
- the applied/specialized hypothesis/lemma is persistent
- - ! : dito, but generate a goal to prove the premise in which
- all hypotheses can be used.
-
-So, in the above you can write:
-
- iPoseProof own_valid "H !" as "Hvalid"
-
-(Yet again, suggestions for improvement of syntax are welcome, as well as a less ad-hoc solution).
-
-Note that many tactics (like iDestruct, iSpecialize, iPoseProof) work for on both hypotheses and lemmas. These may be an entailments, equivalences, arrows, wands, or bi-implications.
-
-
-=== View shifts ===
-
-Many of the Iris tactics (such as iLeft and iRight for introducing disjunctions, iExists for introducing existential quantifiers, and iFrame for framing) work under primitive view shifts.
-
-Next to that, there is the tactic iPvs that can be used to eliminate a primitive view shift (for example, to allocate ghost state or an invariant, or to perform frame preserving updates). The syntax is:
-
- iPvs "hyp" "spec_pattern" as "intro_pattern"
-
-Allocating ghost state is as simple as:
-
- iPvs (own_alloc OneShotPending) as {γ} "Hγ".
-
-Allocating an invariant is as simple as:
-
- iPvs (inv_alloc N _ (one_shot_inv γ l))
- "[Hl Hγ]" as "#HN".
-
-This creates a goal in which you have to prove ▷ one_shot_inv γ l using the hypotheses Hl and Hγ. The as "#HN" moves the allocated invariant to the persistent context.
-
-The iApply tactic also works under primitive viewshifts, so given:
-
- "H" : P -★ Q
-
-The tactic iApply "H" will turn the goal |={E}=> Q into |={E}=> P (and gets rid of "H" depending on whether H is spatial or not).
-
-Apart from that, I have implemented tactics:
-
-+ iTimeless "H": to strip of a later of a timeless hypotheses (type classes are used to establish timelessness)
-+ iPvsAssert P as "intro_pat" with "single_spec_pat": to assert a view shift and then eliminate it
-+ iInv "N" as "intro_pat" : to open the invariant N
-
-All of these tactics also work in case the goal is a weakest precondition. In fact, it works for any connective that is declared as a "frame shifting assertion" (an abstraction that Ralf came up with to characterize connectives around which you can view shift).
-
-
-=== Symbolic execution ===
-
-The proof mode has tactics:
-
- wp_store
- wp_alloc l as "Hl"
- wp_load
- wp_seq
-
-to perform interactive symbolic execution (and similar for many of the programming language connectives). For example, to prove:
-
- WP let: "x" := ref InjL #0 in ... {{ Φ }}
-
-The tactic wp_alloc l as "Hl" will generate a hypotheses "Hl" : l ↦ InjLV #0" and change the goal into:
-
- WP let: "x" := %l in ... {{ Φ }}
-
-Apart from that, it strips laters (since we have performed a step). Next, the tactic wp_let will reduce the let binding (and once more, strip laters when possible).
-
-Most of these tactics are improvements of the tactics that we already had, but are better integrated into the proof mode.
-
-Notably, there is also the tactic:
-
- wp_apply lem "spec_pattern"
-
-Which given a goal WP e {{ Φ }} will look for a redex on which lem matches, and uses the bind rule to apply the lemma. This tactic is very useful to use lemmas corresponding to specifications of earlier proven connectives (see heap_lang/lib/barrier/client.v for example).
-
-
-=== Rewriting ===
-
-We have an internalized equality in the logic (which is defined in the model in terms of the distance relation on COFEs). I have implemented the tactics iRewrite "Heq" and iRewrite "Heq" in "H" to rewrite using the internalized equality. These tactic heavily piggy back on the Coq setoid rewrite machinery to establish non-expansiveness of the connectives involved.
-
-
-=== Error messages ===
-
-I have put some effort in making the tactics of the proof mode generate sensible error messages (instead of just failing with some arbitrary error message from the underlying Coq tactic). This turned out to be pretty difficult due to Ltac's backtracking semantics (and most of all, many of its oddities...)
-
-
-=== Implementation ===
-
-The basic idea of the implementation is surprisingly simple. The proof mode is just syntactic sugar for a judgment:
-
- Δ_persistent ; Δ_spatial ⊢ Q
-
-(See the file proofmode/notation.v. Warning: it uses unicode whitespace characters to make pretty printing work).
-
-The basic forms of all tactics are just Coq lemmas, for example, wand introduction corresponds to the following lemma:
-
- Lemma tac_wand_intro Δ Δ' i P Q :
- envs_app false (Esnoc Enil i P) Δ = Some Δ' →
- Δ' ⊢ Q →
- Δ ⊢ (P -★ Q).
-
-Next to that, I am using Ltac and logic programming with type classes to tie everything together. The proof mode is implemented entirely in Coq and does not involve any OCaml plugins.
diff --git a/README.md b/README.md
index b0e4de15e..f7ea6596a 100644
--- a/README.md
+++ b/README.md
@@ -42,7 +42,7 @@ running:
as described in <http://doi.acm.org/10.1145/2818638>.
* The folder `proofmode` contains the Iris proof mode, which extends Coq with
contexts for persistent and spatial Iris assertions. It also contains tactics
- for interactive proofs in Iris.
+ for interactive proofs in Iris. Documentation can be found in `ProofMode.md`.
* The folder `tests` contains modules we use to test our infrastructure.
Users of the Iris Coq library should *not* depend on these modules; they may
change or disappear without any notice.
--
GitLab