5 ntac: The New Tactic System

8.12

5 ntac: The New Tactic System🔗ℹ

William J. Bowman <wjb@williamjbowman.com>

Paul Wang

As Coq has shown, tactics have proven useful for doing complex proofs. In Cur, tactics are not built-in or provided by the language. However, any user can use meta-programming to add tactics to Cur. In fact, a user did. Cur originally shipped with a proof-of-concept tactic system, but the system did not scale well. So Jay designed and prototyped a new one over a weekend in 200 lines of code. Now it’s the default system.

5.1 The ntac system🔗ℹ

(require cur/ntac/base)

package: cur-lib

A tactic is used at the top-level of a proof script. A tactic is a Racket function that satisfies the contact (r:-> nttz? nttz?) (where r:-> is the Racket function contract normally written ->; we use r:-> since Cur redefined ->). Tactics easily compose, may navigate the proof tree, resolve multiple holes, and be called recursively.

A tactical is used to manipulate the focus of proof tree, such as to resolve a single hole. A tactical satisfies the contract (r:-> dict? ntt?) We will conflate tacticals with functions that produce tacticals from addition arguments. I.e. we also call functions that satisfy (r:-> syntax? ... (r:-> dict? ntt?)) tacticals. Tacticals receive additional arguments as Cur syntax; for technical reasons these need to be processed by ntac-syntax before being used in a tactical. Tacticals are usually used by the fill tactic, which simply applies a tactical to the current focus of the proof tree zipper. We usually provide macros for the surface syntax of tacticals so that users need not deal with syntax objects directly, or explicitly use the fill tactic. These macros follow the naming convention by-_tactical.

5.1.1 Usage🔗ℹ

syntax
(ntac type tactic ...)

Run the ntac tactic ... to produce a term inhabiting type.

Examples:

> ((ntac (forall (x : Nat) Nat)
    by-intro by-assumption)
   z)
(z)
> ((ntac (forall (x : Nat) Nat)
   interactive)
  z)
(z)

syntax
(define-theorem name ty ps ...)

Short hand for (define name (ntac ty ps ...))

Example:

> (define-theorem nat-id (forall (x : Nat) Nat)
by-intro by-assumption)

5.1.2 Base Tactics🔗ℹ

These tactics are used in the tactic system API, while other other tactics are defined outside the base system.

value
next : tactic?

Move the focus to the next hole.

5.1.3 Proof Trees🔗ℹ

TODO: The internal details of the tactic system should be de-emphasized, and the tactics that programmers actually want to use should be more prominent. These next few subsections should probably be moved to the end of the documentation.

The ntac proof tree datatype ntt represents a Cur term with holes. Specifically, the proof tree contains nodes for a hole, an exact term, a combination of subterms, and a context manipulation.

struct
(struct ntt (contains-hole? goal)
    #:transparent)
  contains-hole? : boolean?
  goal : syntax?

An ntac proof tree. Records the current goal, as syntax representing a Cur type, and whether or not there is a hole.

struct
(struct ntt-hole ntt (contains-hole? goal)
    #:transparent)
  contains-hole? : boolean?
  goal : syntax?

A node in an ntac proof tree representing a hole to be filled.

procedure
(make-ntt-hole goal) → ntt?
goal : syntax?

Create a new ntt-hole? node whose hole is goal?. The resulting ntt? does contains-hole?.

struct
(struct ntt-exact ntt (contains-hole? goal term)
    #:transparent)
  contains-hole? : boolean?
  goal : syntax?
  term : syntax?

A node in an ntac proof tree holding a Cur term, as syntax?, satisfying goal.

procedure
(make-ntt-exact goal term) → ntt?
goal : syntax?
term : syntax?

Create a new ntt-exact? node that proves goal via the Cur term term. The resulting ntt? does not contains-hole?.

struct
(struct ntt-context ntt ( contains-hole?
goal
env-transformer
subtree)
    #:transparent)
  contains-hole? : boolean?
  goal : syntax?
  env-transformer : (r:-> dict? dict?)
  subtree : ntt?

A node in an ntac proof tree that records information about the local environment, by manipulating the context of the subtree using env-transformer.

procedure
(make-ntt-context env-transformer subtree) → ntt?
env-transformer : (r:-> dict? dict?)
subtree : ntt?

Create a new ntt-context? node that manipulates the subtree according to env-transformer. The resulting ntt? inherits the goal from subtree and only contains-hole? if subtree does.

struct
(struct ntt-apply ntt (contains-hole? goal subtrees f)
    #:transparent)
  contains-hole? : boolean?
  goal : syntax?
  subtrees : (listof ntt?)
  f : (r:-> syntax? ... syntax?)

A node in an ntac proof tree that proves goal by using f to combine the terms that result from subtrees into a single Cur term.

procedure
(make-ntt-apply goal subtrees f) → ntt?
  goal : syntax?
  subtrees : (listof ntt)
  f : (r:-> syntax? ... syntax?)

Create a new ntt-apply? node that uses f to build a proof tree out of subtrees, with goal remaining to be proved. The resulting ntt? contains-hole? if any subtrees do.

struct
(struct ntt-done ntt (contains-hole? goal subtree)
    #:transparent)
  contains-hole? : boolean?
  goal : syntax?
  subtree : ntt?

A node in an ntac proof tree that asserts that the subtree is complete.

procedure
(make-ntt-done subtree) → ntt?
subtree : ntt?

Create a new ntt-done? node with subtree. Results in an error if subtree contains-hole?.

5.1.4 Proof Tree Zipper🔗ℹ

To navigate the proof tree, we define the ntac tree zipper.

TODO: Actually, these dicts need to be ordered-dicts or envs. Also, right now they’re hashes TODO: Should we hide the details of this struct?

struct
(struct nttz (context focus prev))
  context : dict?
  focus : ntt?
  prev : (r:-> ntt? nttz?)

An ntac tree zipper. Contains the local environment for the focus of the proof tree, context, the subtree being focused on focus, and a function that navigates up the tree once the focused subtree is complete prev.

procedure
(nttz-up nttz) → nttz?
nttz : nttz?

Navigate up the proof tree.

procedure
(nttz-down-context nttz) → nttz?
nttz : nttz?

Navigate down when the proof tree when the focus is a context node.

procedure
(nttz-down-apply nttz) → nttz?
nttz : nttz?

Navigate down when the proof tree when the focus is an apply node.

procedure
(nttz-done? nttz) → boolean?
nttz : nttz?

Returns #t when the focus is complete, and #f otherwise.

5.1.5 Tactic System API🔗ℹ

procedure
(new-proof-tree goal) → ntt?
goal : syntax?

Create a new proof tree with goal.

procedure
(proof-tree->complete-term pt [err-stx]) → syntax?
pt : ntt?
err-stx : syntax? = #f

Run a the proof tree pt to produce a Cur term, as syntax. Raise an error if the proof tree contains-hole?, using err-stx for error location.

procedure
(eval-proof-step ptz pstep) → nttz?
ptz : nttz?
pstep : syntax?

Evaluate the tactic represented by pstep on ptz, performing error handling.

procedure
(eval-proof-script pt psteps [err-stx]) → ntt?
  pt : ntt?
  psteps : (listof syntax?)
  err-stx : syntax? = #f

Evaluate the tactic script represented by psteps on the proof tree pt, checking that the resulting proof is valid for the goal of pt and producing an error otherwise, using err-stx for error location.

procedure
(ntac-proc goal ps) → syntax?
goal : syntax?
ps : (listof syntax?)

A procedure version of ntac. Runs the proof script represented by ps to produce a Cur term of type represented by goal.

procedure
(ntac-syntax stx) → syntax?
stx : syntax?

For technical reasons, top-level syntax objects representing Cur terms need to be processed before being used in a tactical. This function performs that processing. Usually, this function is used in a macro that provides surface syntax for a tactical.

5.1.6 theorem-info🔗ℹ

struct
(struct theorem-info identifier-info (name orig))
name : identifier?
orig : syntax?

Representation for theorems defined with define-theorem. Needed because the actual binding may have normalized the original theorem.

5.2 Standard Tactics and Tacticals🔗ℹ

(require cur/ntac/standard)

package: cur-lib

struct
(struct exn:fail:ntac exn:fail ())

A phase 1 value; an exception representing an ntac failure.

struct
(struct exn:fail:ntac:goal exn:fail:ntac ())

A phase 1 value; an exception representing an failure for an ntac tactic or tactical to match against the current goal.

procedure
(raise-ntac-goal-exception msgf arg ...) → any
msgf : string?
arg : string?

A phase 1 procedure; raises exn:fail:ntac:goal, using the format string msgf with arguments args to format the error message.

syntax
(ntac-match goal [pattern branch] ...)

A phase 0 form; like cur-match, but implicitly raises exn:fail:ntac:goal if none of the patterns match.

TODO: Create deftactic and deftactical?

value
nop : tactic?

The no-op tactic; does nothing.

procedure
(exact e) → tactical?
e : syntax?

Fills the current hole with exactly e, using ntt-exact.

value
display-focus : tactic?

Print the focus of the proof tree, and its local environment.

Example:

> ((ntac (forall (x : Nat) Nat)
display-focus by-intro display-focus by-assumption)
z)
--------------------------------
(Π (x : Nat) Nat)
x : Nat
--------------------------------
Nat
(z)

procedure
(try t) → tactic?
t : tactic?

Runs the tactic t on the proof tree, but ignore any exn:fail:ntac:goals and return the proof tree unchanged if such an exception is raised.

Examples:

> ((ntac (forall (x : Nat) Nat)
    by-assumption)
   z)
could not find matching assumption for goal #<syntax:/home/r
oot/user/.local/share/racket/8.12/pkgs/cur-lib/cur/curnel/co
c.rkt:61:39 (#%app Π-- (#%plain-app Nat) (lambda (x)
(#%plain-app Nat)))>
> ((ntac (forall (x : Nat) Nat)
    (try by-assumption))
   z)
eval:6:0: qed: Proof incomplete.
  in: ((try by-assumption))

procedure
(fill t) → tactic?
t : tactical?

Runs the tactical t on the focus of the proof tree.

Example:

> ((ntac (forall (x : Nat) Nat)
(fill (intro)) by-assumption)
z)
(z)

procedure
(intro [name]) → tactical?
name : identifier? = #f

Matches when the current goal has the form (forall (id : type-expr) body-expr), introducing the assumption name : type-expr into the local environment, using id if no name is provided. Raises exn:fail:ntac:goal if the goal does not have the this form.

Examples:

> ((ntac (forall (x : Nat) Nat)
    (fill (intro)) by-assumption)
   z)
(z)
> ((ntac (forall (x : Nat) Nat)
    (fill (intro (ntac-syntax #'x))) by-assumption)
   z)
ntac-syntax: undefined;
cannot reference an identifier before its definition
  in module: 'anonymous-module

syntax
(by-intro id)
by-intro

Short hand for (fill (intro #'id)) and (fill (intro)), respectively.

Example:

> ((ntac (forall (x : Nat) Nat)
by-intro by-assumption)
z)
(z)

syntax
(by-intros id ...)

Shorthand for (by-intro id) ....

value
assumption : tactical?

Solves the goal by looking for a matching assumption in the local environment. Raises exn:fail:ntac:goal if not assumption matches the goal.

Example:

> ((ntac (forall (x : Nat) Nat)
by-intro (fill assumption))
z)
(z)

TODO: Maybe just define the macro by that expands to (fill (tactical rest ...))

syntax
by-assumption

Short hand for (fill (assumption))

Example:

> ((ntac (forall (x : Nat) Nat)
by-intro by-assumption)
z)
(z)

value
obvious : tactical?

Attempts to solve a goal by doing the obvious thing.

Example:

> ((ntac (forall (x : Nat) Nat)
(fill obvious) (fill obvious))
z)
(z)

TODO: This breaks the naming convention; probably should have obvious-step and obvious

value
by-obvious : tactic?

Try to solve all the holes by doing the obvious thing.

Example:

> ((ntac (forall (x : Nat) Nat)
by-obvious)
z)
(z)

syntax
(by-assert name thm)

Short hand for (fill (assert #'name #'thm)).

Example:

> ((ntac
    (∀ [x : Nat] [y : Nat]
       (-> (== Nat x y)
           (== Nat y x)))
    (by-intros x y x=y)
    ; define local thm named y=x
    (by-assert y=x (== Nat y x))
    ; prove y=x
    display-focus
    (by-rewriteR x=y)
    display-focus
    reflexivity
    ; prove original goal using y=x
    display-focus
    (by-assumption y=x))
   1 1 (refl Nat 1))
y: unbound identifier in module

procedure
(assert name thm) → tactical?
name : identifier?
thm : syntax?

Shifts the goal to defining thm. When thm is proven, shifts the goal to the original goal, but with name bound to thm in the context.

value
simpl : tactic?

Simplifies the current goal by evaluating it.

Example:

> (define-theorem plus_1_l
    (∀ [n : Nat] (== Nat (plus 1 n) (s n)))
    by-intro
    display-focus
    simpl
    display-focus
    reflexivity)
n : Nat
--------------------------------
(== Nat (s n) (s n))
n : Nat
--------------------------------
(== Nat (s n) (s n))

syntax
(by-destruct name)
(by-destruct name #:as param-namess)

Short hand for (fill (destruct #'x)) or (fill (destruct #'x #'param-namess)).

Examples:

> (define-theorem plus-1-neq-0
    (∀ [n : Nat] (== Bool (nat-equal? (plus 1 n) 0) false))
    (by-intro n)
    display-focus
    (by-destruct n #:as [() (n-1)])
    ; zero case
    display-focus
    simpl
    display-focus
    reflexivity
    ; succ case
    display-focus
    simpl
    display-focus
    reflexivity)
n : Nat
--------------------------------
(== Bool false false)
--------------------------------
(== Bool false false)
--------------------------------
(== Bool false false)
n-1 : Nat
--------------------------------
(== Bool false false)
n-1 : Nat
--------------------------------
(== Bool false false)
> (plus-1-neq-0 0)
(refl (Bool) (false))
> (plus-1-neq-0 1)
(refl (Bool) (false))

procedure
(destruct name [param-namess]) → tactical?
name : identifier?
param-namess : syntax? = #f

Splits the goal into n subgoals, where n is the number of possible cases for name.

The resulting proof term uses match.

param-namess should be a list of list of identifiers, which are used as the binders in each clause. If not specified, the original binder names from the data declaration are used. Does not include induction hypotheses for recursive arguments.

syntax
(by-induction name #:as param-namess)

Short hand for (fill (induction #'x #'param-namess)).

Example:

> (define-theorem plus-n-0
    (∀ [n : Nat] (== Nat n (plus n z)))
    (by-intro n)
    simpl
    (by-induction n #:as [() (n-1 IH)])
    ; zero case
    display-focus
    reflexivity
    ; succ case
    display-focus
    simpl
    display-focus
    (by-rewriteL IH)
    display-focus
    reflexivity)
--------------------------------
(== Nat z z)
n-1 : Nat
IH : (== Nat n-1 (plus n-1 z))
--------------------------------
(== Nat (s n-1) (s (plus n-1 z)))
n-1 : Nat
IH : (== Nat n-1 (plus n-1 z))
--------------------------------
(== Nat (s n-1) (s (plus n-1 z)))
n-1 : Nat
IH : (== Nat n-1 (plus n-1 z))
--------------------------------
(== Nat (s n-1) (s n-1))

procedure
(induction name param-namess) → tactical?
name : identifier?
param-namess : syntax?

Splits the goal into n subgoals, where n is the number of possible cases for name.

Unlike destruct, induction binds an induction hypothesis for recursive arguments in each case.

The resulting proof term uses new-elim.

param-namess should be a list of list of identifiers, which are used as the binders in each clause. If not specified, the original binder names from the data declaration are used.

5.2.1 Interactive Tactic🔗ℹ

In Cur, interactivity is just a user-defined tactic.

value
interactive : tactic?

Starts a REPL that prints the proof state, reads a tactic (as ntac would), evaluates the tactic, and repeats. Exits when the proof is finished. Handles exn:fail:ntac:goal by printing the message and continuing the REPL.

Example:

> ((ntac (forall (x : Nat) Nat)
interactive)
z)
(z)

5.3 Auto-related Tactics🔗ℹ

(require cur/ntac/auto)

package: cur-lib

Ntac provides an automatic proof solving tactic that generates proof steps using pairs of tactic presets and identifiers from the current context and a user-defined hints database.

value
auto : tactic?

The Cur implementation of Coq’s auto.

We first try by-obvious for trivial goals. If this fails, we then introduce each variable to context and exhaustively attempt pairings of preset tactics and identifiers.

The tactic returns when either the goal has been completed or the maximum number of tactic applications specified by current-max-auto-depth has been reached.

Example:

> (define-theorem plus-n-0
(∀ [n : Nat] (== Nat n (plus n 0)))
auto)

value
current-max-auto-depth : parameter?

A phase 1 parameter for defining the maximum search depth for auto. By default, up to 4 tactics are applied to the initial tree zipper state before failure.

value
current-hints : parameter?

A phase 1 parameter denoting the current hints database used by auto. By default, this parameter is empty.

Uses a guard to ensure that values are ordered and unique. The ordering of the hints determines the order of tactic application.

value
display-hints : tactic?

Print the local hints database.

syntax
(define-theorem #:hints (hint ...) name ty ps ...)

Short hand for (define name (ntac ty ps ...)).

Optionally allows for specification of a hints database scoped to the theorem.

Examples:

> (define-theorem pred-example-1
    (∀ [p : Bool]
       (== (and p p) p))
    (by-intros p)
    (by-destruct p)
    reflexivity
    reflexivity)
p: unbound identifier in module
> (define-theorem pred-example-2
    #:hints (pred-example-1)
    (∀ [p : Bool] [q : Bool]
       (-> (== p q)
           (== p true)
           (== (and p q) true)))
    display-hints
    auto)
(pred-example-1)

syntax
(hints hint ...)

Create a new hints database closure extending current-hints while prepending the specified list of hints.

Examples:

> (define-theorem pred-example-1
    (∀ [p : Bool]
       (== (and p p) p))
    (by-intros p)
    (by-destruct p)
    reflexivity
    reflexivity)
p: unbound identifier in module
> (define-theorem pred-example-2
    #:hints (pred-example-1)
    (∀ [p : Bool] [q : Bool]
       (-> (== p q)
           (== p true)
           (== (and p q) true)))
    display-hints
    (hints (pred-example-2) display-hints)
    display-hints
    auto)
(pred-example-1)
(pred-example-2 pred-example-1)
(pred-example-1)

struct
(struct tactic-preset (proc id no-name-arg?)
    #:transparent)
  proc : tactic?
  id : syntax?
  no-name-arg? : boolean?

A preset definition of a tactic. Includes metadata for the desired identifier and whether the tactic consumes an identifier when invoked.

value
current-auto-tactics : parameter?

A phase 1 parameter for denoting the list of tactic-preset to try for auto.

The ordering of the presets determines execution order, so it is recommended to arrange base cases first (e.g. by-assumption).

5.4 Rewrite-related Tactics🔗ℹ

(require cur/ntac/rewrite)

package: cur-lib

Ntac includes two libraries of rewrite tactics: one (the above) for "standard" Paulin-Mohring equality (ie, ==), and another (cur/ntac/ML-rewrite) for Martin-Lof equality (i.e., ML-=).

Each library provides versions of the following bindings.

value
reflexivity : tactic?

For a goal (== A a b), shorthand for (fill (exact #'(refl A a))).

syntax
(by-rewrite name . es)

Rewrites the current goal with name, instantiating with es if necessary.

Rewrites from right-to-left (equivalent to Coq’s ->), i.e., for a theorem (== A x y), x is replaced with y.

Short hand for (fill (rewrite #'name #:es #'es)).

Equivalent to by-rewriteR.

Example:

> (define-theorem identity-fn-applied-twice
    (∀ [f : (-> Bool Bool)]
       (-> (∀ [x : Bool] (== Bool (f x) x))
           (∀ [b : Bool] (== Bool (f (f b)) b))))
    (by-intros f H b)
    display-focus
    (by-rewrite H b)
    display-focus
    (by-rewrite H b)
    display-focus
    reflexivity)
f : (→ Bool Bool)
H : (Π (x : Bool) (== Bool (f x) x))
b : Bool
--------------------------------
(== Bool (f (f b)) b)
b: unbound identifier in module

syntax
(by-rewriteR name . es)

Rewrites the current goal with name, instantiating with es if necessary.

Rewrites from right-to-left (equivalent to Coq’s ->), i.e., for a theorem (== A x y), x is replaced with y.

Short hand for (fill (rewrite #'name #:es #'es)).

Equivalent to by-rewrite.

syntax
(by-rewriteL name . es)

Rewrites the current goal with name, instantiating with es if necessary.

Short hand for (fill (rewrite #'name #:es #'es #:left? #t)).

Rewrites from left-to-right (equivalent to Coq’s <-), i.e., for a theorem (== A x y), y is replaced with x.

procedure
(rewrite name
[ #:left? left?
#:es es
#:thm-name thm-name
#:thm thm]) → tactical?
  name : identifier?
  left? : boolean? = #f
  es : syntax? = #'()
  thm-name : identifier? = #f
  thm : syntax? = #f

Rewrites the current goal with name, instantiating with es if necessary.

By default, rewrites from right-to-left (equivalent to Coq’s ->), i.e., for a theorem (== A x y), x is replaced with y. If left? is #t, rewrites from left-to-right instead (Coq’s <-).

syntax
(by-replace ty from to)

Shorthand for (fill (replace #'ty #'from #'to)).

Replaces instances of from in the goal, which has type ty, with to. Adds ty as a subgoal.

Examples:

> (define-theorem plus-n-Sm
      (∀ [n : Nat] [m : Nat]
         (== Nat (s (plus n m)) (plus n (s m))))
      (by-intro n)
      (by-intro m)
      simpl
      (by-induction n #:as [() (n-1 IH)])

      simpl
      reflexivity

      simpl
      (by-rewrite IH)
      reflexivity)
> (define-theorem plus_comm
      (∀ [n : Nat] [m : Nat]
         (== Nat (plus n m) (plus m n)))
      (by-intro n)
      (by-intro m)
      simpl
      (by-induction n #:as [() (n-1 IH)])

      simpl
      display-focus
      (by-rewriteL plus-n-0 m)
      display-focus
      reflexivity

      simpl
      (by-rewriteL plus-n-Sm m n-1)
      (by-rewrite IH)
      reflexivity)
m : Nat
--------------------------------
(== Nat m (plus m z))
m : Nat
--------------------------------
(== Nat m m)
> (define-theorem plus-assoc
    (∀ [n : Nat] [m : Nat] [p : Nat]
       (== Nat (plus n (plus m p)) (plus (plus n m) p)))
    (by-intros n m p)
    simpl
    (by-induction n #:as [() (n-1 IH)])
    ; zero case
    reflexivity
    ; succ case
    simpl
    (by-rewrite IH)
    reflexivity)
n: unbound identifier in module
> (define-theorem plus-swap
    (∀ [n : Nat] [m : Nat] [p : Nat]
       (== Nat (plus n (plus m p))
                 (plus m (plus n p))))
    (by-intros n m p)
    (by-rewrite plus-assoc n m p)
    display-focus
    (by-replace Nat (plus n m) (plus m n))
    display-focus
    (by-rewriteL plus-assoc m n p)
    reflexivity
    ; proof of by-replace theorem
    display-focus
    (by-rewrite plus_comm m n)
    display-focus
    reflexivity)
plus-assoc: unbound identifier in module

procedure
(replace ty from to) → tactical?
  ty : syntax?
  from : syntax?
  to : syntax?

Replaces instances of from in the goal, which has type ty, with to.

1	Curnel Forms
2	Reflection
3	Standard Library
4	Olly: Ott-like Librar Y
5	ntac: The New Tactic System

5.1	The ntac system
5.2	Standard Tactics and Tacticals
5.3	Auto-related Tactics
5.4	Rewrite-related Tactics