Subterm Selection

When writing tactic proofs, you often need to refer to specific subterms in the current goal — to apply a lemma at a particular site, expand a specific function call, or normalize a particular expression. Subterm selection is a pattern language that lets you pick subterms by shape and location, rather than spelling them out in full.

This is especially useful when:

Terms are complex and writing them out would be verbose and error-prone
The term involves destructor expressions that can't easily be written in surface syntax
You want your proof script to be robust against minor refactors

Basic syntax

Subterm selections are written as [? combinators ] and can be used anywhere a term argument is expected in a tactic:

theorem thm2 a b c =
  a * b + c = 0
[@@by [%use thm1 [? at (_ * _) in concl] ]]

Here, [? at (_ * _) in concl] selects the first subterm matching the pattern _ * _ in the conclusion — in this case, a * b.

Combinators

The selection language has two kinds of combinators: shape matching (what to pick) and focussing (where to look).

Shape matching

Combinator	Description
`at p`	Keep only subterms matching pattern `p` (where `_` is a wildcard)
`index(n)`	Select the `n`-th wildcard in a pattern (1-based; negative indices count from end)
`nth(n)`	Select the `n`-th subterm that satisfies all other combinators
`lhs`	Left-hand side of an equality (equivalent to `at (_ = _) index(1)`)
`rhs`	Right-hand side of an equality (equivalent to `at (_ = _) index(2)`)

Focussing

Combinator	Description
`in concl`	Focus to the conclusions of the goal
`in asm`	Focus to the assumptions (hypotheses) of the goal
`in "name"`	Focus to a named hypothesis or conclusion
`in (pattern)`	Focus to subterms within matching terms

If no in focus is specified, the default is in concl.

How combinators compose

Combinators describe a function composition — they are applied in reverse order (right to left). Each combinator maintains an internal iterator, and all are advanced in composition order until a subterm is found that all combinators agree on.

The algorithm is inspired by Gonthier and Tassi and Noschinski and Traut.

Examples

Given this goal:

theorem thm2 (a : int) (b : int) (c : int) (d : int) =
  ((a + b) * c) + d = g (x + 1)
[@@by [%use thm1 ...] @> ...]

Here's what different selections pick:

Selection	Selected term
`[? in concl]`	`((a + b) * c) + d = g (x + 1)`
`[? at (a + _)]`	`a + b`
`[? at (a + _) in (_ * _)]`	`a + b`
`[? at (_ + d)]`	`((a + b) * c) + d`
`[? at (_ + 1) in concl]`	`x + 1`
`[? at (x + 1) in (g (_))]`	`x + 1`
`[? at ((_ : int)) in (g (_)) index(1)]`	`g (x + 1)`
`[? rhs]`	`g (x + 1)`
`[? lhs]`	`((a + b) * c) + d`
`[? at (_ = _) index(-2)]`	`((a + b) * c) + d`
`[? at (_ * _) lhs]`	`(a + b) * c`
`[? at ((a : int) + _) in (_ + (_ : int))]`	`a + b`

Working with named hypotheses

When hypotheses are named using [@name ...], you can select subterms from a specific hypothesis:

theorem thm3 (x : int) (y : int) =
  f x > 0 [@name xgt0]
  && f y > 0 [@name ygt0]
  ==> g x y > 0
[@@by intros
   @> [%use helper [? at (f (_)) in "xgt0"]]
   @> auto]

This selects f x from the hypothesis named xgt0, and passes it to the helper lemma.

Binding selections

Subterm selections can be bound to variables and reused:

[@@by
  let trm = [? at ((a : int) + _) in (_ + (_ : int))] in
  [%use thm_int trm] @> auto]

Tactics that support subterm selection

Any tactic that takes a term argument can use subterm selection:

use — Select a subterm to pass as an argument to a lemma
cases — Select a subterm to case-split on
expand — Select a function application to expand
normalize — Select a subterm to normalize
replace — Select a term to substitute
generalize — Select a subterm to generalize
subgoal — Select a subterm to use in a cut

Tips

Start simple: Use [? lhs] and [? rhs] for equality goals — they're the most common selections.
Use type annotations: When patterns are ambiguous, add type annotations like (_ : int) to disambiguate.
Layer focussing: Combine at with in to narrow down: at (_ + _) in (_ * _) finds additions inside multiplications.
Debug with nth: If you're getting the wrong match, use nth(2) or nth(3) to step through matches.