20
$\begingroup$

Agda has a reflection mechanism (not equality reflection or reflexivity, but something related to metaprogramming based on goals and contexts to generate terms) and people have developed some libraries that simulate Coq tactics, for example acata.

However, some people still don't consider Agda to have tactics (for example in Kevin Buzzard's "the future of mathematics" talk, the Q&A section).

On the other hand, Coq and Lean are considered to "have tactics", but what I see is just another syntax for writing reflection code like in Agda. I think it's because I don't understand tactics in these languages good enough. So, what particular feature do they support so that they can be considered to "have tactics"? I have a clear understanding of what reflection is (like in Agda -- the compile time reflection with access to the type-checking monad and bidirectional type checking functions), but I am unsure what do people mean by "tactics".

$\endgroup$
7
  • $\begingroup$ Can Adga’s reflection do the same things that tactics in Lean and Coq can do like rewriting or problem specific decision procedures? If so, maybe it is just a misunderstanding based on the names one uses for things. $\endgroup$
    – Jason Rute
    Commented Mar 19, 2022 at 22:59
  • 1
    $\begingroup$ @JasonRute github.com/agda/agda-stdlib/pull/1658 $\endgroup$
    – ice1000
    Commented Mar 19, 2022 at 23:03
  • 4
    $\begingroup$ My guess is that this partially follows from the conversational convention of using the name of the language to refer to that language plus its standard library. Definitely agda-stdlib does not define enough tactics to allow one to immediately start writing tactic scripts for significant proofs, which is why acata exists. acata is not actively recommended to new users, so it's less part of Agda than agda-stdlib. $\endgroup$
    – James Wood
    Commented Mar 19, 2022 at 23:08
  • 6
    $\begingroup$ The other relevant aspect I can think of is that Agda's interactive editing offers no support for tactic scripts, where one expects to be able to step through them command-by-command. This is more strongly about Agda-as-a-language, though “not having tactics/tactic scripts” is clearly technically too strong a claim. It does, though, probably make tactic scripts unusable in Agda. $\endgroup$
    – James Wood
    Commented Mar 19, 2022 at 23:12
  • 3
    $\begingroup$ Another perspective: while Agda has a collection of individual tactics, it does not have a significant tactic language supporting various modes of composition (“tacticals” in the Isabelle nomenclature) and subgoal management. Or, at least, no-one has implemented such a language. Maybe I should compile these comments into an answer. $\endgroup$
    – James Wood
    Commented Mar 20, 2022 at 0:45

2 Answers 2

20
$\begingroup$

Consider a reasonable type theory $T$ with decidable checking. Think of it as the core type theory implemented in the kernel of a proof assistant, i.e., with fully elaborated and annotated judgements that nobody wants to write with bare hands.

A central task of formalization is inhabitation of a type: given a derivable judgement $\Gamma \vdash A \; \mathsf{type}$ (the goal), the user provides an expression $e$ (the solution), and the kernel checks whether $\Gamma \vdash e : A$ is derivable. How can we do this in a practical way?

It is not practical for the user to write down a fully annotated term $e$. Instead, they write down an expression $c$ in a surface language $V$ (the vernacular) which is elaborated or evaluated by the proof assistant to give a fully annotated expression $e$. In order to account for the possibility of a user error, the proof assistant can be seen as a map $$\textstyle P : \prod_{\Gamma, A} \, (\Gamma \vdash A \; \mathsf{type}) \to V \to \{\mathsf{error}\} + \sum_{e} \, (\Gamma \vdash e : A).$$ We read the above as: given a derivable type $A$ in context $\Gamma$ (the goal) and an expression $c$ of type $V$ (the suggested solution), the proof assistant either recognizes that $c$ evaluates to an expression $e$ such that $\Gamma \vdash e : A$, or it reports an error.

Actually, apart from errors, there could also be other computational effects, such as non-termination, state, user interaction, etc. We thus generalize the above to a suitable computational monad $M$: $$\textstyle P : \prod_{\Gamma, A} \, (\Gamma \vdash A \; \mathsf{type}) \to V \to M(\sum_{e} \, (\Gamma \vdash e : A)).$$

With the general setup explained, we can address the question. What kind of proof assistant one gets depends on the design of the vernacular $V$ and the computational monad $M$. Some possibilities are:

  • Agda: to give the user the impression that they are working with $T$ directly, we design the vernacular $V$ to look like an abridged version of $T$ and call the expressions of $V$ (proof) terms. The computational monad $M$ supports interactive construction of terms through ”holes“ that represent subgoals. (Agda also support meta-programming through which the user can implement proof search and other techniques that people call “tactics”.)

  • Coq and Lean: make the vernacular $V$ look like a command-based programming language. The commands are called tactics. The monad $M$ incorporates the current goal as state that is manipulated by the user through tactics. The command-based language allows general recursion and construction of non-terminating programs.

  • Isabelle/HOL: make the vernacular $V$ look like a meta-level programming language. There is a built-in abstract data type of judgements, which is controlled by a trusted kernel. The user writes programs that evaluate to judgements. There is a library of useful functions for constructing judgements, called tactics. The user is free to implement their own functions, as well as Tetris.

Reflection is the ability for the vernacular $V$ to access the abstract syntax trees of computed judgements. Again, there is more than one way of doing this:

(If someone can provide better descriptions and links to reflection for Lean and Isabelle, that would be grand.)

Reflection is not to be confused with Boolean reflection, which is a proof technique for (ab)using the equality checker as a decision procedure. Please ask a separate question if you'd like to know more.

$\endgroup$
6
$\begingroup$

For what I see reflection and tactics live on different planes: (elaborator) reflection is a lower-level mechanism that opens up a possibility to implement all sorts of things, in particular tactics.

In a paper Sebastian Ullrich and Leonardo de Moura describe how to build a (hygienic) macro system supporting both custom notations and tactics on top of a low-level reflection monad. And indeed that's how tactics are implemented in Lean 4: https://github.com/leanprover/lean4/tree/master/src/Lean/Elab/Tactic

As far as I heard, Idris developers implement tactics on top of elaborator reflection. Basically they pioneered the approach if I understand it correctly. :)

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.