Arend Proof Search

Nearly every proof assistant faces a problem with poor discoverability of proven theorems. For instance, try to recall how a lemma describing the commutativity of addition is called in your favorite theorem prover. Is it add_comm? Or +-comm?

IntelliJ Arend provides a possibility to search for functions by the definitions they are talking about. We call this functionality Proof Search. Its closest relatives are the Search vernacular command of Coq and Type Directed Search of Idris.

Overview

Proof search can be invoked by Help > Find Action > Proof Search or via the predefined hotkey Ctrl + Alt + P (⌥ ⌘ P on macOS).

The user interface is clear: you can just type a proof search query in the input field.

Demo of the usage:

Simply put, Proof Search shows all definitions that have a specified pattern as a subexpression of their result type.

-- The following definitions can be found by the pattern `List`:
\func foo : List Nat
\func bar : \Sigma (List Bool) Nat
\func baz {A : \Type} : List A

It is possible to specify an _ as a pattern for an arbitrary term. Also, patterns can be provided in their infix form.

-- The following definitions can be found by the pattern `_ + _ = _ + _`.
\func foo (a b : Nat) : a + b = b + a
\func bar (a b : Int) : a + b = b + a

Apart from displaying the search results, it is possible to show the definition of each entry (by pressing Enter), navigate to the location of the selected definition (F4), and insert the selected definition in the editor (Ctrl + Enter / ⌘ Enter ).

Query Language

Results of the search can be refined by specifying a restrictive query. Proof Search Queries admit the following grammar:

query        ::= (and_pattern '->')* and_pattern
and_pattern  ::= (app_pattern '\and')* app_pattern
app_pattern  ::= atom_pattern+ 
atom_pattern ::= '_' | (IDENTIFIER '.')* IDENTIFIER | '(' app_pattern ')'

IntelliJ Arend provides highlighting for the queries, so syntax errors will be easily discoverable.

Parameters and result type

If there is an -> in a query (i.e. it has several and_patterns), then the rightmost and_pattern will be matched with the codomain of the definition, and the rest patterns delimited by -> will be matched with the domain parameters of the definition.

-- The pattern is `Foo -> Bar`
\func foo (f : Foo) : Bar -- matched
\func bar :    Foo -> Bar -- matched
\func baz :           Bar -- rejected

The order of the left and_patterns is not important.

-- The pattern is `Nat -> Bool -> List Nat`
\func foo (n : Nat)  (b : Bool) : List Nat -- matched
\func bar (b : Bool) (n : Nat)  : List Nat -- matched

Matching multiple patterns in the same term

If there is an \and in an and_pattern (i.e. it has several app_patterns), then the term matches an and_pattern iff it matches all its app_patterns at once. This is useful when you want to find a function that tells something about several definitions, but you don’t remember where they are located precisely.

-- The query is `Nat \and Bool`
\func foo : \Sigma (List Nat) Bool -- matched
\func bar : List Bool = Nat        -- matched

Certainly, it is possible to use \and in patterns for parameters:

-- The query is `Nat \and Bool -> _`
\func foo (e : \Sigma (List Nat) Bool) : 1 = 1 -- matched

There is a difference between Nat -> Bool -> _ and Nat \and Bool -> _: the former will match all definitions that have (not necessarily distinct) parameters mentioning Nat and Bool, while the latter requires the existence of a parameter, that mentions Nat and Bool at the same time.

Restricting namespaces

An app_pattern resembles an application of a function. It can represent a tree of a function call, where subtrees (nested applications) should be surrounded by (). An _ can be specified when an arbitrary term is acceptable here. It is not necessary to consider the exact arity of a function in a pattern.

\func foo (n : Nat) (m : Bool) : \Type
\func bar (n : Nat) : Nat
\func baz : Nat

-- The following matches the queries `foo (bar baz) _`, 
-- `foo (bar baz)`, `foo _`, `foo`
\func f : List (foo (bar baz) true) -- matched

It is possible to specify a subsequence of a module path for the identifier. Also note, that IntelliJ Arend provides code completion for the queries.

\module Foo \where \func foo : Nat
\module Bar \where \func foo : Nat

-- The query is `foo`
\func f : Foo.foo -- matched
\func g : Bar.foo -- matched
\func h : \Sigma (Foo.foo = Bar.foo) -- matched

-- The query is `Foo.foo`
\func f : Foo.foo -- matched
\func g : Bar.foo -- rejected
\func h : \Sigma (Foo.foo = Bar.foo) -- matched

-- The query is `Foo.foo \and Bar.foo`
\func f : Foo.foo -- rejected
\func g : Bar.foo -- rejected
\func h : \Sigma (Foo.foo = Bar.foo) -- matched