Bullet Proof-General

This is a proof general extension inserts bullets (aka goal selectors) and Qed. automatiacally if they missing, after C-c C-n or C-c C-entrer command.

Installation

From sources

mkdir -p ~/.emacs.d
cd ~/.emacs.d
git clone https://github.com/yaitskov/proof-general-bullet.git

Append following lines to ~/.emacs.d/init.el file:

(add-to-list 'load-path "~/.emacs.d/proof-general-bullet/lisp")
(require 'bullet-proof-general)

Features overview

Feature effect appears after C-c C-n or C-c C-enter.

Automatic bullet insertion

Use case 0

Snippet before completion:

  split.(* cursor is here *)

Snippet after completion:

  split.
  - (* cursor is here *)

Use case 1

Snippet before completion:

  split.
  - auto.(* cursor is here *)

Snippet after completion:

  split.
  - auto.
  - (* cursor is here *)

Use case 2

Snippet before completion:

  split.
  - inducion x.
    + auto.
    + auto.(* cursor is here *)

Snippet after completion:

  split.
  - inducion x.
    + auto.
    + auto.
  - (* cursor is here *)

Automatic Qed. insertion

Snippet before completion:

Lemma x : True.
Proof.
  reflexivity.(* cursor is here *)

Snippet after completion:

Lemma x : True.
Proof.
  reflexivity.
Qed.
(* cursor is here *)

Bulk bullet indentation

Functions bpg-indent-right and bpg-indent-right rewrite bullets with their siblings in the hierarchy, so a big snippet with bullets can be quickly moved into a subgoal or vice versa. For example you want to move split tactic, used at very beginning of the proof, into a subgoals generated by induction tactic:

  split.
  - induction x.
    + auto.
    + auto.
      * induciton y.
        -- auto.
        -- auto.
    + reflexivity.

The proof of split subgoal bubbles up:

  induction x.
  - auto.
  - auto.
    + induciton y.
      * auto.
      * auto.
  - reflexivity.

Bullet sync by indentation

Function bpg-sync-bullets-by-indent rewrite bullets in the region with bullets which correspond to indentation in the line.

Before:

  + idtac "x".
    split.
    * auto.
    * auto.
  + idtac "y".

After:

  - idtac "x".
    split.
    + auto.
    * auto.
  + idtac "y".