Edit-time tactics for Agda

Talk at Petit-dΓ©j Gallinette in Nantes

Jesper Cockx

6 February 2019

Introduction

Wait, what’s Agda again?

Agda is a functional programming language like Haskell, except:

  • Agda is strongly typed
  • Agda has no side effects

It is also a proof assistant like Coq, except:

  • It supports indexed datatypes
  • It has readable proof terms

Interactive commands in Agda

  • C-c C-SPC: give a term
  • C-c C-r: refine the goal
  • C-c C-c: case split on a variable
  • C-c C-a: automatically fill the goal

these are hard-coded into Agda 😞

Tactic languages

Tactic languages such as Ltac allow the user to define their own tactics:

Theorem plus_1_neq_0 : βˆ€ n : nat,
  beq_nat (n + 1) 0 = false.
Proof.
  intros n. destruct n as [| n'].
  - reflexivity.
  - reflexivity. Qed.

it’s another language to learn 😞

we cannot see the result at edit-time 😞

Reflection

Elaborator reflection (Idris, Agda, Lean) exposes typechecker to the reflection API

myTerm : Term
myTerm = con (quote suc) [ vArg (var 0 []) ]

macro
  myMacro : Term β†’ TC ⊀
  myMacro hole = TC.unify hole myTerm

test : Nat β†’ Nat
test x = myMacro -- == suc x

no support for subgoals or backtracking 😞

Edit-time tactics in Idris

Joomy Korkut 2018, Edit-Time Tactics in Idris (master thesis at Wesleyan)

  • Tactics are written using elaborator reflection: it’s just Idris code
  • Tactics can be run edit-time: resulting term is pasted into the code

Presenting: ataca

An implementation in three parts:

  • Two small additions to Agda
    • A new command (C-c C-m) for running a macro at edit-time
    • A new backtracking primitive runSpeculative
  • A monad Tac with support for goal management and backtracking
  • A (small but growing) library of basic tactics

Demo time!

Follow the demo on https://github.com/jespercockx/ataca/blob/master/src/Ataca/Demo.agda

Under the hood

The Tac monad

The core of ataca is the Tac monad:

  • tac : Tac A is a tactic that either fails or solves the goal, creating a bunch of subgoals with some A for each subgoal
  • liftTC : TC A β†’ Tac A runs a primitive TC action as a tactic
  • m >>= f first runs m and then runs f on all subgoals created by m

Backtracking primitives

Tac implements Alternative:

  • empty aborts the tactic, backtracking to last choice point
  • m₁ <|> mβ‚‚ first tries m₁, but backtracks to mβ‚‚ on a failure

Example: exact tactic

exact : Term β†’ Tac A
exact solution = do
  hole ← getHole
  unify hole solution
  qed

Example: assumption tactic

tryVar : Nat β†’ Tac A
tryVar i = exact (var i [])

assumption : Tac A
assumption = do
  ctx ← getContext
  let xs = from 0 for (length ctx)
  choice $ map tryVar xs

Example: intro tactic

intro : Tac ⊀
intro = do
  hole , type ← getHoleWithType
  pi a b ← reduce type
    where t β†’ empty
  body ← newMetaCtx (a ∷ []) $ unAbs b
  let v = getVisibility a
  unify hole (lam v (body <$ b))
  addCtx a >> setHole body

Example: mini-auto tactic

mini-auto : Tac ⊀
mini-auto = repeat 10 $
  assumption       <|>
  intro            <|>
  introAbsurd      <|>
  introConstructor

Conclusions

Future work

  • Improve the efficiency
    • Agda side: only reflect parts of the term we actually need!
    • Ataca side: new primitives for controlling backtracking
  • Expand the tactics library
  • Add well-scoped and well-typed syntax representations

Questions?

What else is missing? Let me know!

Follow my progress on https://github.com/jespercockx/ataca

Go forth and automate thy Agda code