Introduction

Wait, what’s Agda again?

Agda is a functional programming language like Haskell, except:

• Agda is strongly typed
• Agda has no side effects

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  []) ]

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  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  $
  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