From a4ca0c56718be0c0614b661aa913de5b973fd6b7 Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Wed, 23 Sep 2015 16:20:37 -0400 Subject: [PATCH] Documentation for tactics complete --- scribblings/stdlib/tactics.scrbl | 139 ++++++++++++++++++++++++++++++- 1 file changed, 137 insertions(+), 2 deletions(-) diff --git a/scribblings/stdlib/tactics.scrbl b/scribblings/stdlib/tactics.scrbl index e64a682..ef840d4 100644 --- a/scribblings/stdlib/tactics.scrbl +++ b/scribblings/stdlib/tactics.scrbl @@ -8,8 +8,15 @@ built-in or provided by the language. However, any user can use meta-programming Cur. A tactic system ships in the standard library, written entirely in user-land code. @section{Proof State and Defining Tactics} -In Cur, a @deftech{tactic} is a Racket function from @tech{proof state} to @tech{proof state} that -runs at @gtech{phase} 1. +@defmodule[cur/stdlib/tactics/base] + +@defform*[((define-tactic (name id ... id-ps)) + (define-tactic name procedure-expr))]{ +Defines a new @tech{tactic}, at @gtech{phase} 1. A @deftech{tactic} is a Racket function from +@tech{proof state} to @tech{proof state} that runs at @gtech{phase} 1. A @tech{tactic} takes any +number of arguments, plus the @tech{proof state}. The @tech{proof state} must be the final argument of +the tactic. +} @defproc[(proof? [p any/c]) boolean?]{ @@ -58,8 +65,136 @@ Returns @racket[#t] is the proof of the @racket[proof-state?] @racket[ps] is a @racket[complete-proof?], and @racket[#f] otherwise. } +@defproc[(proof-state-goal-ref [ps proof-sate?] [i natural-number/c]) + syntax?]{ +Returns the @racket[i]th @tech{goal} from the proof state @racket[ps]. +} + +@defproc[(proof-state-current-goal-ref [ps proof-state?]) + syntax?]{ +Returns the @tech{goal} using the index from +@racket[(proof-state-current-goal ps)]. +} + +@defproc[(proof-state-env-ref [ps proof-state?] [name symbol?]) + syntax?]{ +Returns the type of the assumption @racket[name] in the local +environment of @racket[ps]. +} + +@defproc[(proof-state-env-ref-by-type [ps proof-state?] [type syntax?]) + (or/c symbol? #f)]{ +Returns the name of the assumption of type @racket[type] from the local +environment of @racket[ps], or @racket[#f] is no +assumption with @racket[type] exists. +} + +@defproc[(proof-state-extend-env [ps proof-state?] + [name (or/c symbol? identifier?)] + [type syntax?]) + proof-state?]{ +Returns a proof state with the local environment of +@racket[ps] updated to include the assumption @racket[name] of type +@racket[type]. +} + +@defproc[(proof-state-current-goal-set [ps proof-state?] + [goal syntax?]) + proof-state?]{ +Returns a proof state with the current goal in the goals list of +@racket[ps] changed to @racket[goal]. +} + +@defproc[(proof-state-fill-proof-hole [ps proof-state?] [pf proof?]) + proof-state?]{ +Returns a proof state with the current holes of the proof filled with +@racket[pf]. +} + +@defproc[(proof-state-extend-proof-context [ps proof-state?] + [ctxt procedure?]) + proof-state?]{ +Updates the proof in @racket[ps] by playing the current proof inside the +holes of @racket[ctxt]. +} + +@defproc[(print-proof-state [ps proof-state?]) + void?]{ +Pretty-prints @racket[ps] to the @racket[current-output-port]. +} + +@defproc[(lookup-tactic [name (or/c symbol? identifier?)]) + procedure?]{ +Returns the tactic defined with name @racket[name]. Only works when the +tactic is defined and a theorem has been defined but not proved. +} + +@defform[(define-theorem name prop)]{ +Defines a new theorem. +} + +@defform[(proof (tactic args ...) ...)]{ +Proves the theorem previously defined with @racket[define-theorem]. Currently, this proof is not +saved anywhere, only checked against the most recent theorem defined via @racket[define-theorem]. + +Note that the proof state is implicitly given to each call by @racket[proof] and should not appear as +an explicit argument. +} + +@todo{Examples, better documentation (e.g. don't say "returns a proof state"; the signature says so)} + @section{Standard Tactics} +The tactic system includes several standard tactics. + +@defmodule[cur/stdlib/tactics/standard] + +@defproc[(intro [name identifier?] [ps proof-state?]) + proof-state?]{ +Matches when the current goal has the form @racket[(forall (id : type-expr) body-expr)], introducing +the assumption @racket[id : type-expr] into the local environment of @racket[ps]. +} + +@defproc[(by-assumption [ps proof-state?]) + proof-state?]{ +Matches with the current goal has a type that matches an assumption in the local environment of +@racket[ps]. Completes the goal. +} + +@defproc[(obvious [ps proof-state?]) + proof-state?]{ +Attempts to prove the current goal by doing the obvious thing. +} + +@defproc[(restart [ps proof-state?]) + proof-state?]{ +Resets @racket[ps] to its state when the proof began. Clears the proof and goals, reinitializing the +goals to the original theorem. +} + +@defproc[(print [ps proof-state?]) + proof-state?]{ +Prints @racket[ps], returning it unmodified. +} + +@defproc[(forget [x identifier?] [ps proof-state?]) + proof-state?]{ +Removes the assumption @racket[x] from the local environment of @racket[ps]. +} @section{Interactive Tactic} +In Cur, interactivity is just a user-defined tactic. + +@defproc[(interactive [ps proof-state?]) + proof-state?]{ +Starts a REPL that prints @racket[ps], reads a tactic (as @racket[proof] would), evaluates the +tactic, and repeats. To quit, use @racket[(quit)]. +} @section{SarTactic (Sarcastic Tactics)} +@defmodule[cur/stdlib/tactics/sartactic] + +The SarTactic library provides amusing wrappers around the standard tactics. This library exists +mostly for the author's own amusement, and to ensure the extensibility of the tactic system. + +It defines the same tactics as @racketmodname[cur/stdlib/tactics/standard], but each tactics will +insult the user, and will only work some of the time.