5 ntac: The New Tactic System

7.7

top ← prev up next →

5 ntac: The New Tactic System

William J. Bowman <wjb@williamjbowman.com>

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:eval:5:0 (real-Π (x : Nat) 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)
(z)

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))
x : Nat
y : Nat
x=y : (== Nat x y)
--------------------------------
(== Nat y x)
x : Nat
y : Nat
x=y : (== Nat x y)
--------------------------------
(== Nat y y)
x : Nat
y : Nat
x=y : (== Nat x y)
y=x : (== Nat y x)
--------------------------------
(== Nat y x)
(PM-refl (Nat) (s (z)))

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 (plus 1 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 (nat-equal? (plus 1 n) 0) false)
n : Nat
--------------------------------
(== Bool (nat-equal? (plus 1 z) 0) false)
n : Nat
--------------------------------
(== Bool false false)
n : Nat
n-1 : Nat
--------------------------------
(== Bool (nat-equal? (plus 1 (s n-1)) 0) false)
n : Nat
n-1 : Nat
--------------------------------
(== Bool false false)
> (plus-1-neq-0 0)
(PM-refl (Bool) (false))
> (plus-1-neq-0 1)
(PM-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-destruct/elim name)
(by-destruct/elim name #:as param-namess)

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

Examples:

> (define negb
    (λ [b : Bool]
      (new-elim b (λ [b : Bool] Bool) false true)))
> (negb true)
(false)
> (negb false)
(true)
> (negb (negb true))
(true)
> (negb (negb false))
(false)
> (define-theorem negb-invol
    (forall [b : Bool] (== Bool (negb (negb b)) b))
    (by-intro b)
    (by-destruct/elim b)
    ; true case
    display-focus
    simpl
    display-focus
    reflexivity
    ; false case
    display-focus
    simpl
    display-focus
    reflexivity)
--------------------------------
(== Bool (negb (negb true)) true)
--------------------------------
(== Bool true true)
--------------------------------
(== Bool (negb (negb false)) false)
--------------------------------
(== Bool false false)

procedure
(destruct/elim 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 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.

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 (new-elim z (λ (anon : Nat) Nat) z (λ (x : Nat) (λ (ih-x : Nat) (s ih-x)))))
n-1 : Nat
IH : (== Nat n-1 (new-elim n-1 (λ (anon : Nat) Nat) z (λ (x : Nat) (λ (ih-x : Nat) (s ih-x)))))
--------------------------------
(== Nat (s n-1) (new-elim (s n-1) (λ (anon : Nat) Nat) z (λ (x : Nat) (λ (ih-x : Nat) (s ih-x)))))
n-1 : Nat
IH : (== Nat n-1 (new-elim n-1 (λ (anon : Nat) Nat) z (λ (x : Nat) (λ (ih-x : Nat) (s ih-x)))))
--------------------------------
(== Nat (s n-1) (s (new-elim n-1 (λ (anon : Nat) Nat) z (λ (x : Nat) (λ (ih-x : Nat) (s ih-x))))))
n-1 : Nat
IH : (== Nat n-1 (new-elim n-1 (λ (anon : Nat) Nat) z (λ (x : Nat) (λ (ih-x : Nat) (s ih-x)))))
--------------------------------
(== 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 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)
f : (-> Bool Bool)
H : (∀ (x : Bool) (== Bool (f x) x))
b : Bool
--------------------------------
(== Bool (f b) b)
f : (-> Bool Bool)
H : (∀ (x : Bool) (== Bool (f x) x))
b : Bool
--------------------------------
(== Bool b b)

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.

syntax
(by-rewrite/thm thm . es)

Rewrites the current goal with thm, where thm is a theorem defined with define-theorem, 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

(let ([thm-info (syntax-local-eval #'thm)])
  (fill (rewrite #'thm
                 #:thm-name (theorem-info-name thm-info)
                 #:thm (theorem-info-orig thm-info)
                 #:es #'es)))

Examples:

> (define-theorem negb-invol
    (forall [b : Bool] (== Bool (not (not b)) b))
    (by-intro b)
    (by-destruct/elim b)
    simpl
    reflexivity
    simpl
    reflexivity)
> (define-theorem not-applied-twice
    (∀ [f : (-> Bool Bool)]
       (-> (∀ [x : Bool] (== Bool (f x) (not x)))
           (∀ [b : Bool] (== Bool (f (f b)) b))))
    (by-intros f H b)
    display-focus
    (by-rewrite H b)
    display-focus
    (by-rewrite H (not b))
    display-focus
    (by-rewrite/thm negb-invol b)
    display-focus
    reflexivity)
f : (-> Bool Bool)
H : (∀ (x : Bool) (== Bool (f x) (not x)))
b : Bool
--------------------------------
(== Bool (f (f b)) b)
f : (-> Bool Bool)
H : (∀ (x : Bool) (== Bool (f x) (not x)))
b : Bool
--------------------------------
(== Bool (f (not b)) b)
f : (-> Bool Bool)
H : (∀ (x : Bool) (== Bool (f x) (not x)))
b : Bool
--------------------------------
(== Bool (not (not b)) b)
f : (-> Bool Bool)
H : (∀ (x : Bool) (== Bool (f x) (not x)))
b : Bool
--------------------------------
(== Bool b b)

syntax
(by-rewriteR/thm thm . es)

Same as (by-rewrite/thm thm . es).

syntax
(by-rewriteL/thm thm . es)

Rewrites the current goal with thm, where thm is a theorem defined with define-theorem, instantiating with es if necessary.

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

Short hand for

(let ([thm-info (syntax-local-eval #'thm)])
  (fill (rewrite #'thm
                 #:thm-name (theorem-info-name thm-info)
                 #:thm (theorem-info-orig thm-info)
                 #:left? #t
                 #:es #'es)))

syntax
(by-rewrite/thm/normalized thm . es)

Rewrites the current goal with the normalized version of thm, where thm is a theorem defined with define-theorem, 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

(let ([thm-info (syntax-local-eval #'thm)])
  (fill (rewrite #'thm
                 #:thm-name (theorem-info-name thm-info)
                 #:thm (cur-reflect (identifier-info-type thm-info))
                 #:es #'es)))

Examples:

> (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
    reflexivity
    ; succ case
    simpl
    (by-rewriteL IH)
    reflexivity)
> (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)])
    ; zero case
    simpl
    reflexivity
    ; succ case
    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)])
    ; zero case
    simpl
    display-focus
    (by-rewriteL/thm/normalized plus-n-0 m)
    display-focus
    reflexivity
    ; succ case
    simpl
    (by-rewriteL/thm/normalized plus-n-Sm m n-1)
    (by-rewrite IH)
    reflexivity)
m : Nat
--------------------------------
(== Nat m (new-elim m (λ (anon : Nat) Nat) z (λ (x : Nat) (λ (ih-x : Nat) (s ih-x)))))
m : Nat
--------------------------------
(== Nat m m)

syntax
(by-rewriteR/thm/normalized thm . es)

Same as (by-rewrite/thm/normalized thm . es).

syntax
(by-rewriteL/thm/normalized thm . es)

Rewrites the current goal with the normalized version of thm, where thm is a theorem defined with define-theorem, instantiating with es if necessary.

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

Short hand for

(let ([thm-info (syntax-local-eval #'thm)])
  (fill (rewrite #'thm
                 #:thm-name (theorem-info-name thm-info)
                 #:thm (cur-reflect (identifier-info-type thm-info))
                 #:left? #t
                 #:es #'es)))

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-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)
> (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/thm plus-assoc n m p)
    display-focus
    (by-replace Nat (plus n m) (plus m n))
    display-focus
    (by-rewriteL/thm plus-assoc m n p)
    reflexivity
    ; proof of by-replace theorem
    display-focus
    (by-rewrite/thm plus_comm m n)
    display-focus
    reflexivity)
n : Nat
m : Nat
p : Nat
--------------------------------
(== Nat (plus (plus n m) p) (plus m (plus n p)))
n : Nat
m : Nat
p : Nat
--------------------------------
(== Nat (plus (plus m n) p) (plus m (plus n p)))
n : Nat
m : Nat
p : Nat
--------------------------------
(== Nat (plus m n) (plus n m))
n : Nat
m : Nat
p : Nat
--------------------------------
(== Nat (plus n m) (plus n m))
with-limit: out of time

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.

top ← prev up next →

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	Rewrite-related Tactics