Skip to content

Improved treatment of anonymous hypotheses in the proof mode

Robbert Krebbers requested to merge robbert/proofmode_anon_hyps into master

The proof mode now explicitly keeps track of anonymous hypotheses (i.e. hypotheses that are introduced by the introduction pattern ?). Consider:

Lemma foo {M} (P Q R : uPred M) : P -∗ (Q ∗ R) -∗ Q ∗ P.
Proof. iIntros "? [H ?]". iFrame "H". iFrame. Qed.

After the iIntros, the goal will be:

_ : P
"H" : Q
_ : R
--------------------------------------∗
Q ∗ P

Anonymous hypotheses are displayed in a special way (_ : P). An important property of the new anonymous hypotheses is that it is no longer possible to refer to them by name, whereas before, anonymous hypotheses were given some arbitrary fresh name (typically prefixed by ~), which one could refer to.

Note tactics can still operate on these anonymous hypotheses. For example, both iFrame and iAssumption, as well as the symbolic execution tactics, will use them. The only thing that is not possible is to refer to them yourself, for example, in an introduction, specialization or selection pattern.

Advantages of the new approach:

  • Proofs become more robust as one cannot accidentally refer to anonymous hypotheses by their fresh name.
  • Fresh name generation becomes considerably easier. Since anonymous hypotheses are internally represented by natural numbers (of type N), we can just fold over the hypotheses and take the max plus one. This thus solve issue #101 (closed).

Considering the second point, I also conjecture that this gives a slight performance improvement.

Edited by Robbert Krebbers

Merge request reports