<figure><img src="image_1.png" /></figure>

HAL
open science

# Proof by Pointing Revisited

Laurent Théry

► To cite this version:

Laurent Théry. Proof by Pointing Revisited. Inria & Université Cote d'Azur, Sophia Antipolis, France. 2025. hal-05337440v2

HAL Id: hal-05337440

https://hal.science/hal-05337440v2

Submitted on 5 Nov 2025 (v2), last revised 26 Nov 2025 (v3)

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.
# Proof by Pointing Revisited

Laurent Théry

STAMP TEAM - INRIA

Laurent.Thery@inria.fr

October 2025

## 1 Introduction

Proof by Pointing was proposed in [1] as a direct way to guide the process of building a proof tree. The decision to revisit it was motivated by two events. First, I had the pleasure of being a member of Pablo Donato's PhD jury. In his thesis [2], Pablo proposes some very nice extensions of Proof by Pointing. Second, Enrico Tassi gave me his habilitation thesis [3] to proof-read. He presents his language Elpi (a variant of λ-Prolog) and an extension Rocq-Elpi that provides a framework for interacting with the Rocq prover. In the following, we present our re-implementation of Proof by Pointing and one of its extensions, Proof by Linking, using Rocq-Elpi.

## 2 Proof by Pointing Rules

The idea of Proof by Pointing is to indicate with the pointer a sub-formula of interest in order to trigger some proof steps. These steps aim to make the selected sub-formula the top formula of one of the generated subgoals. Let us take a simple example with the following formula:

$$ (A \land B) \lor C $$

Suppose that we point to B :

$$ (A \land \boxed{B}) \lor C $$

B is on the right of a conjunction that is on the left of a disjunction. To bring it to the surface, we first apply the ∨-introduction-left rule to reach the conjunction, and then the ∧-introduction rule to extract B .

$$ \frac{\frac{A \qquad \boxed{B}}{A \land \boxed{B}}}{(A \land \boxed{B}) \lor C} $$

The idea is simple. Each application of a rule makes the selected formula one step closer to the surface. This recursive behaviour can be highlighted by explicitly showing the nested nature of the selection

$$ (A \land \boxed{B}) \lor C $$
Now we can show how the introduction rules propagate the selected term. For example, we have two rules for disjunction

$$ \frac{\boxed{A}}{\boxed{A} \lor \boxed{B}} $$

$$ \frac{\boxed{B}}{\boxed{A} \lor \boxed{B}} $$

and two rules for conjunction

$$ \frac{\boxed{A} \quad \boxed{B}}{\boxed{A} \land \boxed{B}} $$

$$ \frac{\boxed{B} \quad \boxed{A}}{\boxed{A} \land \boxed{B}} $$

Note that, with respect to our example, we swap the subgoals produced by the rule when the right conjunct is selected. The application of Proof by Pointing can generate multiple goals. Performing this swapping ensures that the subgoal containing the selected formula is always the leftmost subgoal. Provers like Rocq manipulate subgoals as a stack. Thus, the selected formula will always become the conclusion of the goal that is on top of the stack. We call this subgoal, the *active subgoal*.

The introduction rule for the implication is the one that deals with assumptions. A goal *G* is associated with a context, typically a list of assumptions *H*₁, *H*₂ ... *H*₂. This is written

$$ H_1, H_2...H_n \vdash G $$

So the natural rules for the $\Rightarrow$-introduction are the following

$$ \frac{\Gamma, \boxed{A} \vdash B}{\Gamma \vdash \boxed{A} \Rightarrow B} $$

$$ \frac{\Gamma, A \vdash \boxed{B}}{\Gamma \vdash A \Rightarrow \boxed{B}} $$

These were the rules given in the original paper [1]. We depart from them. While performing the recursive process of Proof by Pointing, we have already seen that there is a notion of the active subgoal. There is also the notion of *active assumption*, which arises when dealing with elimination rules. For example, one of the original rules for the disjunction elimination was the following

$$ \frac{\Gamma, \boxed{A} \vdash G \quad \Gamma, B \vdash G}{\Gamma, \boxed{A} \lor B \vdash G} $$

It created two subgoals. The first one contains the active assumption. Let us explain our alternative for handling this active assumption. First, we retain only the right-introduction rule for implication:

$$ \frac{\dots, A \vdash \boxed{B}}{A \Rightarrow \boxed{B}} $$

Thus, the context is mentioned explicitly only when we add an element (*A*). Second, we use the left-hand side of the implication to identify which assumption in the context we are working with. Thus, the $\lor$-elimination rules become
$$ \frac{\boxed{A} \Rightarrow G \quad \dots B \vdash G}{\boxed{A} \lor B \Rightarrow G} $$

$$ \frac{\boxed{B} \Rightarrow G \quad \dots, A \vdash G}{A \lor \boxed{B} \Rightarrow G} $$

Similarly, the $\land$-elimination rules become

$$ \frac{\dots B \vdash \boxed{A} \Rightarrow G}{\boxed{A} \land B \Rightarrow G} $$

$$ \frac{\dots, A \vdash \boxed{B} \Rightarrow G}{A \land \boxed{B} \Rightarrow G} $$

We are left with the $\Rightarrow$-elimination rules

$$ \frac{\boxed{A} \quad \dots, B \vdash G}{(\boxed{A} \Rightarrow B) \Rightarrow G} $$

$$ \frac{\boxed{B} \Rightarrow G \quad A}{(A \Rightarrow \boxed{B}) \Rightarrow G} $$

For completeness we can also give the rule for the negation in an intuitionistic setting

$$ \frac{\boxed{A}}{\neg \boxed{A} \Rightarrow G} $$

$$ \frac{\boxed{A} \Rightarrow \perp}{\neg \boxed{A}} $$

Note that we also add a default rule that deactivates the assumption once it has reached the surface.

$$ \frac{\dots, A \vdash G}{\boxed{A} \Rightarrow G} $$

A reasonable companion rule is one that closes an obvious goal.

$$ \boxed{A} \Rightarrow \overline{A} $$

Figure 1 summarises all the rules
<figure><img src="image_2.png" /><figcaption>Figure 1: Proof by Pointing rules</figcaption></figure>

## 3 The Tactic

Proof by Pointing lets the user build proofs by direct mouse manipulation. Nevertheless, we need to integrate it into a state-of-the-art interactive prover. In a tactic-based prover such as Hol [4] or Rocq, this means we must record in the script a dedicated tactic that encodes the selection of a term. For example, the version for the Hol theorem prover [4], called FINGER_TAC, used a notion of occurrence borrowed from the CONVERT library developed by David Shepherd. An occurrence was a sequence of letters a, b and f where

* f meant going down to the left part of an application (the function)

* a meant going down to the right part of an application (the argument)

* b meant going inside the body of a λ abstraction.

If we take our initial example

$$ (A \wedge \mathbf{B}) \vee C $$

this term is represented by the Hol term
COMB (COMB (CONST 'OR') (COMB (COMB 'AND' (VAR 'A')) (VAR 'B')) (VAR 'C'))

thus the occurrence for *B* is *fa*, and it is represented in the script by the tactic

FINGER_TAC (GOAL_OCC 'fa').

This kind of occurrence is easy to generate but difficult to read. This means that the resulting script will be difficult to maintain. Fortunately, Rocq and its SSREFLECT extension [5] provide a very expressive language for denoting patterns. It can be used to improve greatly the legibility of a Proof by Pointing tactic. A pattern is simply a term in which placeholders _ may appear anywhere to denote arbitrary subterms. For example, a pattern that is matching our previous term is the following

$$(_ \wedge B) \vee _$$

This is not ideal since *B* could still be an arbitrary large term. To improve readability further, we can use a binding construction to indicate it is the location of *B* and not its value we are interested in here.

$$[X \text{ in } (_ \wedge X) \vee_]$$

We believe that this produces a very concise and legible tactic:

$$\text{pbb } [X \text{ in } (_ \wedge X) \vee _].$$

We can go a step further if we look at the implication introduction rule

$$\frac{\boxed{A} \quad \dots, B \vdash G}{(\boxed{A} \Rightarrow B) \Rightarrow G}$$

provers like Rocq name assumptions explicitly. A good naming convention makes the scripts more robust and easier to maintain. So the actual rule is

$$\frac{\boxed{A} \quad \dots, H : B \vdash G}{(\boxed{A} \Rightarrow B) \Rightarrow G}$$

The question now is how we generate the name. If we look at a command that could generate such assumption, it may look like

$$\text{pbb } [X \text{ in } (X \Rightarrow \_ ) \Rightarrow _].$$

The *B* that is introduced corresponds to the first placeholder _ . In fact, Rocq provides named placeholder ?name. It is used to represent non-linear pattern. In our case, we can make use the name to explicitly name the assumption that is introduced.

$$\text{pbb } [X \text{ in } (X \Rightarrow ?H) \Rightarrow _].$$

Another rule generates a new assumption when the active assumption reaches the surface
$$ \frac{\dots, A \vdash G}{A \Rightarrow G} $$

In that case, we use the name X given by the binder in the pattern to generate the name

$$ \frac{\dots, X : A \vdash G}{A \Rightarrow G} $$

# 4 The Implementation

We now describe the implementation of Proof by Pointing, following the presentation above. It is written with Elpi. Each rule we described maps directly to one Elpi rule from a predicate pbp_builtin. This predicate takes the current goal and the pattern and returns a partial proof term.

pred pbp_build i:term, i:term, o:term.

Let us explain the rule for $\wedge$-introduction. In Rocq, a proof of a conjunction is built using the conj constructor.

conj : :forall A B : Prop, A -> B -> A /\ B.

it takes a proof of A and a proof of B to construct a proof of $A \wedge B$. So the rule

$$ \frac{A \quad B}{A \wedge B} $$

corresponds to the Elpi rule

pbp_build {{ lp:P /\ _ }} {{ lp:P1 /\ lp:uvar }} {{ conj lp:R1 _ }} :- pbp_build P P1 R1.

If the pattern contains a place holder on the right (this is the uvar), we construct a conj whose first argument is built from the recursive call with the left argument P and P1. To keep the active goal at the top of the stack, we first define a variant of conj that swaps its arguments.

Definition conjR {A B : Prop} (X : A) (Y : B) := conj Y X.

so the other $\wedge$-introduction rule is coded as

pbp_build {{ _ /\ lp:P }} {{ lp:uvar /\ lp:P1 }} {{ conjR lp:R1 _ }} :- pbp_build P P1 R1.

For the $\wedge$-elimination rules, we need the following two Rocq lemmas:

Lemma andlimp {A B C : Prop} (H : B -> A -> C) : A /\ B -> C.

Proof. by move=> [H1 H2]; apply: H. Qed.

Lemma and2imp {A B C : Prop} (H : A -> B -> C) : A /\ B -> C.

Proof. by move=> [H1 H2]; apply: H. Qed.

and the two rules
$$ \frac{\dots H : B \vdash [A] \Rightarrow G}{[A] \wedge B \Rightarrow G} $$

$$ \frac{\dots, H : A \vdash [B] \Rightarrow G}{A \wedge [B] \Rightarrow G} $$

are encoded as

pbp_build {{lp:P /\ _ -> lp:S }} {{lp:P1 /\ lp:X -> lp:uvar}} {{and1imp lp:R}} :-
get_name X H, !,
pbp_build {{lp:P -> lp:S }} {{lp:P1 -> _ }} R1,
R = fun H _ (x\ R1).
pbp_build {{_ /\ lp:P -> lp:S }} {{lp:X /\ lp:P1 -> lp:uvar}} {{and2imp lp:R}} :-
get_name X H, !,
pbp_build {{lp:P -> lp:S }} {{lp:P1 -> _ }} R1,
R = fun H _ (x\ R1).

These rules deserve some explanation. The representation of Rocq functions in Rocq-Elpi. A function `fun x : type => body` is represented in Elpi as `fun "x" bype' (\x. body')`. The name of the binder is explicitly given as the first arguments. Here we use a predicate `get_name` to retrieve the name of a fun. Its declaration is the following

pred get_name i: term o: name.
get_name uvar `pbp`.

with a default clause that generates the name pbp for an anonymous placeholder. Listing 1 together with Listing 2 list all the rules corresponding to Figure 1.

We are almost done. What remains to be explained is how we link the Proof by Pointing to a Rocq tactic that is calling our `pbp_build` set of rules.

Elpi Tactic pbp_tac.
Elpi Accumulate Db pbp_build.db.
Elpi Accumulate lp:{{
  solve (goal Ty [open-trm N F] as G) GL :-
    pbp_scan N F Ty G GL.
}}.

Notation "[ X 'in' Z ]" := (fun X => Z).
Tactic Notation "pbp" uconstr(t) :=
elpi pbp_tac ltac_open_term:(t).

Let us try to explain what is happening when calling the tactic

$$ \text{pbb } [X \text{ in } (X \Rightarrow ?H) \Rightarrow \_]. $$

Unfortunately, the current version of Coq-Elpi causes Elpi to lose the names of named placeholders. In order to preserve the capability to name assumptions, a quick fix is to use *open terms* :

$$ \text{pbb } [X \text{ in } (X \Rightarrow H) \Rightarrow \_]. $$

When we move to the Elpi world (open-trm N F), F is a closed term to which the necessary abstractions have been added to capture all free variables. In our example, this term F corresponds to

$$ \text{fun } H \Rightarrow \text{fun } X \Rightarrow (X \Rightarrow H) \Rightarrow \_. $$
```
pred pbp_build i:term, i:term, o:term.
pbp_build {{ lp:P /\ _ }} {{ lp:P1 /\ lp:uvar }} {{ conj lp:R1 _ }} :-
pbp_build P P1 R1.
pbp_build {{ _ /\ lp:P }} {{ lp:uvar /\ lp:P1 }} {{ conjR lp:R1 _ }} :-
pbp_build P P1 R1.
pbp_build {{ lp:P /\ _ }} {{ lp:P1 /\ lp:uvar }} {{ or_introl lp:R1 }} :- !,
pbp_build P P1 R1.
pbp_build {{ _ /\ lp:P }} {{ lp:uvar /\ lp:P1 }} {{ or_intror lp:R1 }} :- !,
pbp_build P P1 R1.
pbp_build {{ _ -> lp:P }} {{ lp:X -> lp:P1 }} R :-
    get_name X H, !, pbp_build P P1 R1, R = fun H _ (x\ R1).
pbp_build {{lp:P /\ _ -> lp:S }} {{lp:P1 /\ lp:X -> lp:uvar}} {{andlimp lp:R}} :-
    get_name X H, !, pbp_build {{lp:P -> lp:S}} {{lp:P1 -> _}} R1,
    R = fun H _ (x\ R1).
pbp_build {{_ /\ lp:P -> lp:S }} {{lp:X /\ lp:P1 -> lp:uvar}} {{and2imp lp:R}} :-
    get_name X H, !, pbp_build {{lp:P -> lp:S}} {{lp:P1 -> _}} R1,
    R = fun H _ (x\ R1).
pbp_build {{lp:P /\ _ -> lp:S }} {{lp:P1 /\ lp:X -> lp:uvar}} {{orlimp lp:R1
    lp:Z}} :-
    get_name X H, !, !, pbp_build {{lp:P -> lp:S}} {{lp:P1 -> _}} R1,
    Z = fun H _ (x\ _).
pbp_build {{_ /\ lp:P -> lp:S }} {{lp:X /\ lp:P1 -> lp:uvar}} {{or2imp lp:R1
    lp:Z}} :-
    get_name X H, !, pbp_build {{lp:P -> lp:S}} {{lp:P1 -> _}} R1,
    Z = fun H _ (x\ _).
pbp_build {{(lp:P ->_) -> _}} {{(lp:P1 -> lp:X) -> lp:uvar}} {{implimp lp:T
    lp:T1}} :-
    get_name X H, !, pbp_build P P1 T, T1 = fun H _ (x\ _).
pbp_build {{(_ -> lp:P) -> lp:R}} {{(lp:uvar -> lp:P1) -> lp:uvar}} {{imp2imp lp:T
    _}} :-
pbp_build {{lp:P -> lp:R}} {{lp:P1 -> _}} T.
pbp_build {{~ lp:P }} {{~ lp:P1 }} R :-
pbp_build {{lp:P -> False}} {{ lp:P1 -> _ }} R.
pbp_build {{(~ lp:P) -> _}} {{~ lp:P1 -> lp:uvar }} R :-
pbp_build P P1 R1, R = {{negimp lp:R1}}.
```

<caption>Listing 1: pbp_builtin predicate</caption>

```
Lemma andlimp {A B C : Prop} (H : B -> A -> C) : A /\ B -> C.
Proof. by move=> [H1 H2]; apply: H. Qed.
Lemma and2imp {A B C : Prop} (H : A -> B -> C) : A /\ B -> C.
Proof. by move=> [H1 H2]; apply: H. Qed.
Lemma orlimp {A B C : Prop} (H : A -> C) (H1 : B -> C) : A /\ B -> C.
Proof. by move=> [H2|H2]; [apply/H/H2 | apply/H1/H2]. Qed.
Lemma or2imp {A B C : Prop} (H : B -> C) (H1 : A -> C) : A /\ B -> C.
Proof. by move=> [H2|H2]; [apply/H1/H2 | apply/H/H2]. Qed.
Lemma implimp {A B C : Prop} (H : A) (H1 : B -> C) (H2 : A -> B) : C.
Proof. by apply/H1/H2. Qed.
Lemma imp2imp {A B C : Prop} (H1 : B -> C) (H : A) (H2 : A -> B) : C.
Proof. by apply/H1/H2. Qed.
Lemma negimp {A B : Prop} (H : A) (H1 : ~ A) : B.
Proof. by case: H1. Qed.
Definition conjR {A B : Prop} (X : A) (Y : B) := conj Y X.
```

<caption>Listing 2: Rocq constructors</caption>
The variable *N* is set to the number of abstractions that were needed to close the term. In our example, *N* is equal to 1 : the abstraction *t* was needed to close the free variable *H*. The only remaining step is to define the *pbp_scan* predicate, that first adds a new clause *get_name* for all the free variables and then add the closing clauses before calling *pbp_build* and using a *refine* command to apply the proof term that has been computed.

pred pbp_scan i:int, i:term o:term o:goal o: list sealed-goal.
pbp_scan 0 (fun N _ S) Ty G GL :- !,
pi x \
  pbp_build _ x _ =>
  pbp_build {{ _ -> _ }} {{lp:x -> lp:uvar}} (fun N _ ) =>
  pbp_build {{lp:X -> lp:X}} {{lp:x -> lp:uvar}} (fun N _ (x\x)) =>
  (pbp_build Ty (S x) R,
   coq.elaborate-skeleton R Ty T ok,
   refine.no_check T G GL).
pbp_scan N (fun Na _ S) Ty G GL :- !,
N1 is N - 1,
pi x \ get_name x Na =>
  pbp_scan N1 (S x) Ty G GL.
}}.

## 5 An Extension to Proof by Linking

A natural extension of Proof by Pointing is to allow two selections instead of one. This is called Proof by Linking in [2]. One elementary example that illustrates it is the following :

$$A \Rightarrow (A \Rightarrow B) \Rightarrow B$$

We can link the *Bs*. This corresponds to the usual back-chaining.

$$A \Rightarrow (A \Rightarrow \boxed{B}) \Rightarrow \boxed{B}$$

We can link the *As*. This time, it corresponds to forward-chaining.

$$\boxed{A} \Rightarrow (\boxed{A}) \Rightarrow B) \Rightarrow B$$

To extend the tactic syntax, we use a double binder.

$$\text{pbb } [XY \text{ in } X \Rightarrow (Y \Rightarrow _ ) \Rightarrow _ ].$$

Even though we do not exploit it here, it clearly indicates a source *X* and a target *Y*. An alternative would be to use multiple occurrences of *X*.

$$\text{pbb } [X \text{ in } X \Rightarrow (X \Rightarrow _ ) \Rightarrow _ ].$$

Now we can present the new rules. They handle two selected terms. First, note that the previous rules are still valid. They can be seen as the processing of the common part of the two selections. When these selections diverge, either one selection is inside an active assumption and the other one in the goal, or the two selections are in two active assumptions. There is one exception, namely the following rule:
$$ \frac{\boxed{A} \Rightarrow \boxed{B} \Rightarrow C}{\boxed{A} \wedge \boxed{B} \Rightarrow C} $$

It turns one active assumption into two active assumptions. Figure 2 gives the rules that manipulate only one active assumption (and an active goal with only one exception : the previous rule). Figure 3 gives the rules that manipulate two active assumptions.

$$ \frac{\boxed{A} \Rightarrow \boxed{B} \quad A \vdash C}{\boxed{A} \Rightarrow \boxed{B} \wedge C} $$

$$ \frac{\text{....B} \vdash \boxed{A} \Rightarrow \boxed{C}}{\boxed{A} \wedge \boxed{B} \Rightarrow \boxed{C}} $$

$$ \frac{\boxed{A} \Rightarrow \boxed{B} \Rightarrow C}{\boxed{A} \wedge \boxed{B} \Rightarrow C} $$

$$ \frac{\boxed{A} \Rightarrow \boxed{B}}{\boxed{A} \Rightarrow \boxed{B} \vee C} $$

$$ \frac{\boxed{A} \Rightarrow \boxed{C} \quad \text{....B} \vdash C}{\boxed{A} \vee \boxed{B} \Rightarrow \boxed{C}} $$

$$ \frac{\text{...., B} \vdash \boxed{A} \Rightarrow \boxed{C}}{\boxed{A} \Rightarrow \boxed{B} \Rightarrow \boxed{C}} $$

$$ \frac{\boxed{A} \Rightarrow \boxed{B} \Rightarrow \bot}{\boxed{A} \Rightarrow \neg \boxed{B}} $$

$$ \boxed{A} \Rightarrow \boxed{A} $$

$$ \frac{\boxed{A} \Rightarrow \boxed{C} \quad A \vdash B}{\boxed{A} \Rightarrow B \wedge \boxed{C}} $$

$$ \frac{\text{...., } A \vdash \boxed{B} \Rightarrow \boxed{C}}{A \wedge \boxed{B} \Rightarrow \boxed{C}} $$

$$ \frac{\boxed{A} \Rightarrow \boxed{C}}{\boxed{A} \Rightarrow B \vee \boxed{C}} $$

$$ \frac{\boxed{B} \Rightarrow \boxed{C} \quad \text{...., } A \vdash C}{A \vee \boxed{B} \Rightarrow \boxed{C}} $$

$$ \frac{\boxed{B} \Rightarrow \boxed{C} \quad A}{(A \Rightarrow \boxed{B}) \Rightarrow \boxed{C}} $$

<caption>**Figure 2:** Proof by Linking rules : one active assumption</caption>
<figure><img src="image_3.png" /><figcaption>**Figure 3:** Proof by Linking rules : two active assumptions</figcaption></figure>

# 6 Conclusion

Revisiting Proof by Pointing has been a lot of fun. First, we borrowed some ideas coming from the SSREFLECT extension. The use of a pattern to denote the selected terms gives a more robust way to generate scripts. Moreover, treating the goal as a stack and introducing the notion of an active assumption simplifies the implementation. Second, using Elpi has been surprisingly smooth. The main reason is that it is a rule-based language, which fits perfectly with our objective. The complete code is available here.

https://github.com/thery/coq_tmp/blob/main/pbp.v

# Bibliography

[1] Y. Bertot, G. Kahn, and L. Théry, “Proof by pointing,” in TACS, Springer, 1994, pp. 141–160.

[2] P. Donato, “Deep Inference for Graphical Theorem Proving,” Phd thesis, Institut Polytechnique de Paris, 2024.

[3] E. Tassi, “Elpi: rule-based extension language,” Hdr thesis, Université Côte d’Azur, 2025.

[4] M. J. C. Gordon and T. F. Melham, *Introduction to HOL: a theorem proving environment for higher order logic*. Cambridge University Press, 1993.

[5] G. Gonthier, A. Mahboubi, and E. Tassi, “A Small Scale Reflection Extension for the Coq system,” Research Report RR-6455, 2016. [Online]. Available: https://inria.hal.science/inria-00258384