Subterm Selection

Some ImandraX tactics that take a term as an argument (like use or cases) can be cumbersome to use with complex argument terms. In some cases it may even be impossible to state the exact terms (e.g. destructor terms). For these reasons, ImandraX supports subterm selection, which allows us to pick a subterm from a (sub-) goal instead of having to spell it out.

For example, in

theorem thm1 x = ...

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

the instruction [? at (_ * _) in concl] means that ImandraX will pick the first term that matches the pattern (_ * _) in the conclusion of the goal (where _ are wildcards). In this example, that is a * b.

The selection instructions are a sequence of combinators (like at ... and in ...) that describe how to traverse the goal to find the right term. Essentially they fall into two classes:

focussing (where to look), and
shape matching (what to pick).

The complete list of combinators is as follows:

Combinator	Meaning
`at` `p`	Keep only subterms that match the pattern `p` (a pattern term, usually containing wildcards).
`in` `f`	Focus the selection to terms appearing within the focus `f` (as described below).
`index(n)`	Select the `n`-th wildcard in a pattern (1-based, negative indices count from the end).
`nth(n)`	Select the `n`-th subterm that agrees with all other combinators.
`lhs`	The left-hand side of the goal (if the goal is an equality). Equivalent to `at (_ = _) index(1)`.
`rhs`	The right-hand side of the goal (if the goal is an equality). Equivalent to `at (_ = _) index(2)`.

The focus expressions for in are as follows:

Focus	Meaning
`concl`	The conclusions of the goal
`asm`	The assumptions (hypotheses) of the goal
`n`	A named hypothesis or conclusion with name `n` (a string)
`t`	A pattern term

Combinators describe a function composition (as in (f ∘ g)(x) = f(g(x))) and some may find that they need to be read “backwards” to their intuition. For each combinator, an iterator is kept internally and they are advanced in composition order until a subterm is found that all combinators agree with.

If no focus is set by the use of an in instruction, the default is to select from the conclusion (in concl).

The selection algorithm is inspired by and adapted from Gonthier and Tassi and Noschinksi and Traut, with the subterm iteration order and combinator composition close to the latter.

Examples

For the following examples, consider the goal

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

We would like to select various subterms of the goal for application of thm1 (which we assume depends on a single int).

Sometimes we may want to select the entire conclusion and [? in concl] indeed selects ((a + b) * c) + d = g (x + 1). The following table lists a number of examples with their corresponding selections on this particular goal:

Selection pattern	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)`
`[? at (_ = _) index(-2)]`	`((a + b) * c) + d`
`[? at (_ * _) lhs ]`	`(a + b) * c`
`[? at ((a : int) + _) in (_ + (_ : int)) ]`	`a + b`