Talk at Petit-dΓ©j Gallinette in Nantes

Jesper Cockx

6 February 2019

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*

`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 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 π

**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 π

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

`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 new command (
- A monad
`Tac`

with support for**goal management**and**backtracking** - A (small but growing)
**library**of basic tactics

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

`Tac`

monadThe 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`

** Tac** implements

`Alternative`

:`empty`

aborts the tactic, backtracking to last choice point`mβ <|> mβ`

first tries`mβ`

, but backtracks to`mβ`

on a failure

`exact`

tacticexact : Term β Tac A exact solution = do hole β getHole unify hole solution qed

`assumption`

tactictryVar : 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

`intro`

tacticintro : 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

`mini-auto`

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

- 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

What else is missing? Let me know!

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

*Go forth and automate thy Agda code*