Yarrow started off as an implementation of a typing algorithm for PTSs. Over the time it evolved into a simple proof-assistant. Its main features are:
This program has some disadvantages compared to other proof-assistants:
This program was developed by Jan Zwanenburg. Questions and remarks will be gratefully received and answered. You can reach the author at the following address.
Jan Zwanenburg
Computing Science Department
University of Nijmegen
Postbus 9010
650 Gl Nijmegen
The Netherlands
e-mail: janz@cs.kun.nl
Homepage:
http://www.cs.kun.nl/~janz/
Yarrow homepage:
http://www.cs.kun.nl/~janz/yarrow/index.html
Yarrow is an implementation of Pure Type Systems (see [Bar92]) with several extensions. In Yarrow you can experiment with various pure type systems, with emphasis on using a type system as a logic. A basic knowledge on type systems and the Curry-Howard-de Bruijn isomorphism is required. Experience with proof-assistants is useful for proving theorems.
There are three extensions of PTSs implemented in Yarrow.
First, we have definitions. Definitions are
indispensable for any practical use of PTSs.
Pure Type Systems with definitions (DPTs) are defined in
[SP93];
the most important property of these systems is that apart from
GLOBAL definitions definitions in the context, also LOCAL
definitions within terms are admitted.
Second, we have subtyping. Subtyping makes the type system more flexible.
In particular, it can be used with records to allow formalization of
Object-Oriented Programming to a certain degree.
Pure Type Systems with Subtyping are defined in
[Zwa99].
Third, we have records. Records are useful for defining programs in a PTS,
in particular Object-Oriented programs.
Yarrow has two modes. It starts in the MAIN-mode, where you can get the type of a term, reduce terms and extend the context. From the main-mode you can get to the PROVE-mode by the 'prove'- command. In the prove-mode a term for a certain type is interactively constructed with tactics. When this is done, the program returns to the main-mode.
The next section describes the syntax used in Yarrow. The other two chapters describe the main-mode and prove-mode in more detail.
Happy typing!
References:
The syntax is quite close to the standard syntax of the typed lambda calculus. We write
\x:T.e @x:T.e let x:=e:T.f f e (e)
Precedence goes from lowest to highest, so \x:T.x x means
\x:T.(x x) and not (\x:T.x) x.
The lambda, pi and let terms do extend to right as far as possible.
We use the following shorthands:
\x1,x2,..xn:T.e @x1,x2,..xn:T.e T->U @x:T.U if x does not occur
in U (the -> is right-associative)
let x:=e.f
Variables and sorts can consists of the following characters:
a..z A..Z 0..9 * # ' _
They may not start with a digit, underline or apostroph however.
The words let, then, else,
in and on are keywords (independent of case).
Variables can also be used infix, see
infix-notation.
In the name of commands, the case of the letters is ignored. Two dash signes '--' signal the rest of the line is comment.
There is a restricted to split terms over several lines: If a line ends with '.' '->' ':' ',' ':=' or an operator, the term may be completed on the following line. This works also if not enough closing parentheses ')' have been seen.
Example:
Var complicated : @a,b,c,d:Nat. @f:Nat->Nat->Nat.
@P,Q:*.@R:Nat->*. (P->Q) \/
R (
f a (f (f b c) d))
Variables can also be notated as OPERATORS, consisting of a sequence of the
following characters:
+ < > / \ & ! $ % ^ ~ | @ ; = [ ] - _ ' 0..9
They may not start with a digit, underline or apostroph either.
The single backslash '\', the arrow '->', the single bar '|'
and the single at '@' are reserved.
So '->@' is scanned as one infix operator, and not as the
symbols arrow and at!
An operator must be used infix. Sometimes you wish to use it in
a prefix-way, or without two arguments. Then you have to enclose
the operator in parentheses. Some examples:
Var (+) : Nat -> Nat -> Nat
Def double := \x:Nat. x+x
Def S := (+) one
An infix operator binds weaker than application, but stronger
than ->. For information concerning associativity and precedence
between operators see
Infix,
InfixL and
InfixR.
This infix system is quite similar to that
used in the functional programming languages Gofer and Haskell.
In Yarrow certain extensions to Pure Type Systems may be selected.
These extensions are not automatically active; they have to be selected
with the command System.
At the moment we have the following extensions:
System (*,#),(*:#),((*,*),(#,*)),(#),((#,*))
for the second order lambda calculus with subtyping and
bounded quantification.
\x <: t : T. e@x <: t : T. e\x <: t. e as shorthand for
\x <: t : T. e if t : T. This shorthand is
also available for bounded quantifications.
Check term <: term
checks if the first term is a subtype of the second term.
Var var-list <:
term : term declares a bounded
variable.
Type gives a minimal type, and
Intro and Apply work also for bounded
quantifications.
->records
in the command System. E.g.System (*->records,#),(*:#),((*,*), (#,*))*, and record-values
will have as sort *. Records may only be activated for
one sort.
{|l1:T1, .. ln:Tn|}{l1=t1, .. ln=tn} t`ln may be zero.{|l1:T1, .. ln:Tn|} : ss is the sort for which records are activated
and all labels are different
{l1=t1, .. ln=tn} : {|l1:T1, .. ln:Tn|}i we have ti : Ti
and all labels are different
t`li : Tit : {|l1:T1, .. ln:Tn|}
{l1=t1, .. ln=tn}`li reduces to ti
{l= one, m= true} and {m= true, l= one} are
not considered syntactically equal terms. (But they have identical
reduction behaviour.)
When both records and subtyping are selected there is subtyping on
records. The subtyping rule for records is:
{|l1:T1 .. ln:Tn|} <: {|k1:U1 .. km : Um|} if for every
j <= m there
is an i with li=kj and Ti <: Uj.
For example:
System (*->records,#),(*:#),((*,*), (#,*)), (#), ((#,*))
gives the usual second order lambda calculus with records and subtyping.
A term in this calculus is
(\X <: {|id:Int|}. \x:X. x`id) {|id:Int, n:S|} {id=two, n=h}
assuming proper declarations for Int, S, two, h have been
made.
In the main-mode of Yarrow you can extend the context, get the type of terms, reduce terms and enter the prove-mode with a certain goal. The commands available here fall in 5 categories:
The following commands extend or examine the context.
Var var-list : term
Var var-list <: term
: term
: term'
is optional.
Var Nat : *
Var mult,(+) : Nat->Nat->Nat
Def,
subtyping
Def var := term
Def var := term
: term2
Def Bool := @A:*.A->A->A
Def true := \A:*.\a1:A.\a2:A.a1 : Bool
Var
Context [: sort-list] [On filename]
Context "modulename" [: sort-list]
[On filename]
Context var .. var
[: sort-list] [On filename]
Context var
[: sort-list] [On filename]
This command displays the global context. With option s set, also all corresponding sorts are shown. The piece of the context defined in modules is only indicated by the first and last name of each module.
The second variant displays the part of a context as defined in the named module.
The third variant displays only the variables in the indicated range, and the fourth variant displays only the given variable.
The optional sort-list indicates the sorts for which all definitions will be printed in full. Defining terms belonging to other sorts are abbreviated to ".." .
Optionally, a filename may be given, to which the output is redirected.
Option
Reset var
Clear
Print var
Prove var : term
Task.
Def,
Task
Deduction var num
The following commands implement miscellaneous typing and reduction routines.
Type term
Check term : term
Check term :=: term
Check term <: term
subtyping
bRed term
bdRed,
dRed
dRed term
bdRed,
bRed
bdRed term
dRed,
bRed
Some of these commands allow you to set parameters of the system, and others implement auxilary functions.
Quit
Help
Help command
Help list
System sys
System
Changes the type system used to sys. The context is
cleared, unless the old system is a part of sys.
If sys can be mapped to \C it is terminating,
and if \U- can be mapped to sys it is non-terminating.
This is verified by this program and a corresponding
message is issued. If the system is not terminating,
typing may not terminate, so this program can hang or
crash. On top of that, if the type system is considered as
a logic, it is inconsistent.
sys consists of the list of sorts, the list of
axioms and the list of rules, all seperated by a
comma, and enclosed by parentheses. Every list
consists of a number of items seperated by commas.
A sort is a just an identifier.
An axiom consists of two sorts seperated by
a colon.
A rule consists of a triple of sorts seperated by
commas, and is enclosed by parentheses. The third sort
may be omitted, in which case it is assumed to be
equal to the second sort.
The System command is also used to select
extensions of Pure Type Systems available in Yarrow, e.g. subtyping.
See 'extensions'.
The second variant displays the current type system.
System (Set,Type),(Set:Type),((Set,Set),(Set,Type))
for \P.System (*,#,##),(*:#,#:##),((*,*),(*,#,##))extensions
Read "filename"
Path
Option +opt
Option -opt
Option
bdRed, bRed, dRed
There are three mechanisms for keeping terms readable. The first is infix-notation, the second is permitting arguments to be implicit in some circumstances and the third is declaring certain variables as binders.
Infix num var
Infix 2 (=)
Infix 5 (+)
InfixR,
InfixL,
infix-notation
InfixL num var
InfixL 5 (-)x-y-z will be interpreted as
(x-y)-z
Infix,
InfixR,
infix-notation
InfixR num var
InfixR 7 (^)x^y^z will be interpreted as
x^(y^z).
Infix,
InfixL,
infix-notation
Implicit num var
Often a number of type-arguments are superfluous, in the sense that they can be derived from the context. Yarrow has a simple way of suppressing most useless arguments. Arguments to a variable can be suppressed in Yarrow, if they can be derived by inspecting following arguments. In most cases, this is good enough. Internally, always all parameters are represented.
This command is only allowed if var has been defined. It expresses that you want to suppress the first num arguments of var. After this command, the first num arguments may be all left out, but this is not compulsory; otherwise all of them must be given. In order to be able to decide whether or not some arguments are implicit, the restriction is made that the first argument of var has an other sort than the num+1th argument.
If option i is turned off, implicit arguments are no longer admitted, and all arguments are printed. Turning this option on again will re-allow implicit arguments in exactly the same way as before.
id : @A:*.A->A
comp : @A,B,C:*. (B->C) -> (A->B) -> (A->C)
(=) : @A:*. A->A->Prop
Then the following commands define these
variables to have the usual number of
implicit arguments:Implicit 1 id
Implicit 3 comp
Implicit 1 (=)id O (means id Nat O)comp not even
(means comp Nat Bool Bool not even)O=O (means (=) Nat O O)
Option
Binder var
Ex : (Nat->*) -> *
and Ex is declared as a binder:Binder ExEx x:Nat. x=x stands for
Ex (\x:Nat. x=x).Ex to P is now written as
(Ex) P.
Implicit
Yarrow has a module system that allows pieces of contexts to be loaded without repeating type-checking. A module is a file, consisting of:
A module is created by the command Save
name. In this module all new variables are saved; new variables
are not contained in a loaded module.
In a following session, all definitions and declarations in the module can be
regained quickly by the command Load
name.
A module m can depend on other modules. This is automatically registered when saving: all modules loaded on that moment form the import list of module m. When m is loaded, any imported modules are also loaded. If any of the imported modules has changed since it was included in the import-list of m, the context defined in m is type-checked again. In this way consistency is guaranteed.
Yarrow always keeps the context ordered in such a way, that it can be split
in two pieces. The first piece corresponds to loaded modules, and the
second piece contains new variables. The Save command will only
save the second piece, and Load will insert the
new variables between the two pieces.
The Clear command makes Yarrow forget
that it has loaded the last module. This is necessary if modules have to be
concatenated in a bigger module or if some definitions have to be deleted
from a module.
We illustrate the use of modules with an example. We assume the user
wants to build a theory of natural numbers, and already has defined some
logical primitives in "logic". A first session typically looks
like this:
system ..
load "logic"
var natural := ..
(some more definitions and lemmas)
save "natural"
Now a module natural is created, with
logic in the import list, but the logic primitives themselves
are not included in natural.
On the next session, the user wants to extend natural
with more theory:
system ..
load "natural"
prove mult_symmetric : ..
(still more definitions and lemmas)
save "natural"
The module logic has been loaded automatically, since it is
in the import list of natural. Now this module is
extended with still more definitions. The user discovers that he needs
another logical theorem. He shouldn't prove it right away, since then
it is impossible to get them in the logic module. The course he should take
is:
clear
reset natural
prove another_logical_theorem : ..
save "logic"
load "natural"
Module natural is type-checked again to see if it is still
valid.
Now he can continue his quest for a formal proof of Fermat's theorem, and
we conclude the example here.
Now we describe the commands for modules in more detail.
Save "filename"
.yc. The type system used,
the import list and infix and implicit declarations are also stored.
The import list for this module is the list of all modules currently
loaded.Save "integer"
Load,
Clear
Load "filename"
Load
Loads module with name filename.yc, and all
modules on the import list of this module.
It is checked that the module is valid in the current type system.
(If the context is empty, the type system is changed to the type system
of the module).
Furthermore, if any of the imported modules are changed,
filename is type-checked again to ensure consistency.
The declarations of the module are inserted in the context just after
the last declaration of the last module.
The second variant gives a list of all modules currently loaded, with the first and last variable that every module contains.
Load "integer"
Save,
Clear,
Read,
Path
Clear
Load "int1"
Load "int2"
Clear
Clear
Save "int1and2"int1and2 contains all declarations of both
int1 and int2. Without the clear
commands, int1and2 would be empty.
Load,
Save
Path "pathname"
Path
Adds filename to the current path. This means that
every Load and Read operation will also look
in this directory for files. On start-up only the current directory
is in the path. Note that modules are always saved in the
current directory.
You can use both / and \ as separation
between directory names, this is automatically corrected for the
platform, if necessary. Use .. for the parent directory,
and . for the current directory.
The second variant displays all paths.
Path "theories/lists"
Load,
Read
In the prove-mode a term of a given type is interactively constructed.
You enter the prove-mode with the prove
command from the main-mode. Tactics are the commands that direct the
construction process, but sometimes also some commands are needed
that don't contribute to the proof-term, e.g. to undo some tactics, to
leave the prove-mode or to get some information. The distinction between
tactics and other commands is important, since only tactics can be combined
or undone.
This chapter is divided into three sections. The first section describes
all tactics, the second section describes the
other commands available in prove-mode,
and the last section describes the matching
procedure we use (this is used in the common apply-tactic).
In the prove-mode a term of a given type is interactively constructed. Tactics are the commands that direct this process. We call the term that is being constructed the proof-term.
More specifically, at every moment during the construction, the proof-term
is a lambda-term with some holes in it. Every hole has a type,
which is called the goal.
At the beginning, the proof-term is just one hole, and its type is the
type given in the prove-command.
By tactics this hole is gradually filled in, refining the corresponding goal.
Typically, new holes are constructed during this process. The proof-term
is complete when there are no holes left. Then the prove-mode can be exited
and the constructed term is included as a definition in the context.
A hole can occur inside a lambda-abstraction. This means that every hole has a local context, listing the abstracted variables with their types. In the prove-mode the first goal is shown under its local context, seperated by a line. The other goals are shown without their context. An example:
2 goals
P : *
Q : *
R : *
H : P->Q->R
H1 : Q
H2 : P
--------------------------------------------------
P
2) Q
This shows two goals, P and Q, and the local
context of the first goal. Holes themselves are not shown, unless the
corresponding option is turned on. Then the whole process of constructing
proof-term is made explicit
(see Option).
Normally tactics work on the first goal. Another goal can be selected with
the Focus tactic.
What follows is a list of tactics. They are divided into 4 categories:
These tactics are shown in order of frequency of use.
Intro var-list
Intro
@-type or a let-type, this tactic
introduces one variable or definition. In variant 1
the given variable name is used, otherwise a name will
be chosen (usually the name already occurring in the
type).
Intro A,x,H1,H2
Intros
Intros
Intros num
Intro as often as possible.
The second variant repeats Intro num times.
Intro,
Repeat
Apply term
Apply term On
term-list
Find an inhabitant of the current goal by applying term to some other terms. Some of these arguments can be inferred, the others become new goals.
This tactic tries first to apply term to zero arguments,
then to apply to one argument, then to two, and so on.
For n arguments, this means that the type of term
should be of the form @x1:T1.@x2:T2. ... @xn:Tn. U
(after unfolding of definitions, if neccesary).
The type U is then matched against the current goal
to determine the type of the arguments. If the matching
fails, or some type
Ti cannot be determined, this number of
arguments fails. Otherwise it succeeds, and all types
corresponding to arguments that cannot be determined
become new goals.
H : @x:Nat. P x -> Q x Q zeroApply H succeeds with as
new goalP zeroH is applied to two arguments. The first
is zero and is determined by matching. The
second argument is of type P zero and could
not be determined by matching, so becomes a new hole.
The second variant is a combination of the Forward tactic and the Apply 1 tactic.
lem : @x,y,z : Int. x<y -> y<z -> x<zH : b<c---------a<cApply lem On H results in the goal---------a<bExact term
Assumption
Assumption
Exact
Cut term
First
First term
Cut is the order of the
generated subgoals. Indeed, it is the same as Cut
followed by Focus 2.
Cut,
Focus
Forward term
Forward term On
term-list
Introduce a variable with the same type as term.
Suppose term is of type T.
Then this tactic is a shortcut for the consecutive tactics
First T
Exact term
Intro
So First uses the cut-rule, and immediately solves
one of the goals by the proof-term term.
In practice, this tactic is used to support forward-reasoning, i.e. combine the propositions we already have in a new proposition, without referring to the goal.
H2 : @x:Nat. P x -> Q xH3 : P y ---------RForward H2 y H3 results inH2 : @x:Nat. P x -> Q xH3 : P y H4 : Q y ---------R
The disadvantage of Forward 1 is that often big applications have
to be typed in, with many arguments that are clear from the context.
In example 1 above, the argument y of H2 is clear from the context.
The second variant of Forward solves this problem; in the example
above we can just type
Forward H2 On H3
which gives the same effect.
The second variant of Forward tries to make a proof-term of the
form
term .. term1 .. term2 .. etc. ..
termn
where on each place with dots zero or more terms are inserted, to
make the term well-typed. The terms that are inserted are either
found by matching, or become new goals.
In this way, forward reasoning is much easier.
If term is a local variable v,
and we use only 'arrow-elimination' to obtain the new assumption,
this variable v is hidden.
lem : @x,y,z : Int. x<y -> y<z -> x<zH1 : a<bH2 : b<c---------RForward lem On H1, H2 results in a new
assumptionH3 : a<cFirst,
Exact,
Intro,
Hide
Let var := term
Let var := term
: term2
These tactics do not change the goal or the local context, but only change the way the local context is printed.
Hide var-list
Unhide
Unhide var-list
Unhide
Hide
These tactics convert the goal (or sometimes, a hypothesis), into a beta-delta convertible one.
Unfold var
Unfold num-list var
Unfold var In var2
Unfold num-list var In var2
Unfold 1,3 pluspaths).
Implicit,
Infix,
Simplify,
Convert
Simplify
Convert,
Unfold,
Pattern
Convert term
Unfold,
Simplify,
Pattern
Pattern term
Pattern num-list term
paths).
Convert
Tactics that are useful only in conjunction with certain lemmas are
called special. Currently we have special tactics for propositional and
predicate logic,
and for dealing with Leibniz-equality. All these tactics work independent
of the name of the connectives. E.g. "and", "/\" or "PRODUCT" may be all
used as the name for conjunction. However, the user has to indicate which
lemmas have to be used for each special tactic. This is done with the
command use.
Use tacticname var
Use
AndI,
AndEL,
AndER,
OrIL,
OrIR,
OrE,
NotI,
NotE,
FalseE,
ExistsI,
ExistsE,
Rewrite,
Lewrite,
Refl
AndI
@P,Q:s. P -> Q -> and P Q
Use
AndEL term
AndEL term On
term-list
@P,Q:s. and P Q -> P
Forward,
AndER,
AndE,
Use
AndER term
AndER term On
term-list
@P,Q:s. and P Q -> Q
Forward,
AndEL,
AndE,
Use
AndE term
AndE term On
term-list
Forward,
AndEL,
AndER,
Use,
Hide
OrIL
@P,Q:s. P -> or P Q
Use
OrIR
@P,Q:s. Q -> or P Q
Use
OrE term
OrE term On
term-list
@P,Q:s1. @R:s2. or P Q -> (P->R) -> (Q->R) -> R
Forward,
Use,
Hide
NotI
@P:s. (P -> False) -> Not P
Use
NotE term
NotE term On
term-list
Not P,
and the goal should be False.
This tactic replaces the goal by P.
The second variant is a combination of 'Forward' and 'NotE 1'.@P:s. Not P -> P -> False
Forward,
Use
FalseE
use:@P:s. False -> P
Use
ExistsI term
@x1:t1. ... @xn:tn. @x:t. @P:t->s. P x -> Ex x1 .. xn P
Use
ExistsE term
ExistsE term On
term-list
@x1:t1. ... @xn:tn. @P:t->s1. @R:s2. Ex x1 .. xn P ->
(@x:t. P x -> R) -> R
Forward,
Use,
Hide
Rewrite [num] term
[On term-list] [In var]
On clause are a combination
of 'Forward' and 'Rewrite' without On clause.
Finally, it is also possible to rewrite in an assumption,
using the In clause.@x1:t1. .. @xn:tn.@x,y:t. @P:t->sort. eq x1 .. xn x y -> P y -> P xy and x! Var eq : @A:*. A -> A -> *
Var eq_elim_l : { as above }
Use Rewrite eq_elim_l
Var lemma : @x:Nat. eq Nat x (minus x zero)Q two -> R Rewrite lemma will yield as new goalQ (minus two zero) -> R
paths).
Forward,
Lewrite,
Use
Lewrite [num] term
[On term-list] [In var]
@x1:t1. .. @xn:tn.@x,y:t. @P:t->sort. eq x1 .. xn x y -> P x -> P yy and x! paths).
Rewrite,
Use
Refl
eq A x x', where
x and x' are bd-convertible.
This tactic proofs the goal by using the corresponding reflexivity
lemma. This lemma should be of the following form:@x1:t1. .. @xn:tn. @x:t. eq x1 .. xn x xUse
Tacticals are ways of composing tactics and can be useful to reduce the number of commands the user has to give to reach the goal.
Then ( tactic1
| tactic2 | ...
| tacticn )
Then tactic1
The tactical first performs tactic and then tactic1 on the first of the generated subgoals, tactic2 on the second of the generated subgoals, etc. If there are more new subgoals than tactics, the last tactic in the list is applied to the rest of the subgoals. If there are fewer new subgoals than tactics, the rest of the tactics is ignored. If any application of a tactic fails, the combination fails as a whole, meaning it has no effect.
The second variant is just an instance of the first variant, where n equals one, and the parentheses have been left out. So tactic1 is performed on all generated subgoals.
Try,
Repeat,
Else
Try tactic
Apply H Then Try Assumption
This example shows how Try can be useful.
All hypotheses of H that are in the context are
immediately proved. If Try were omitted, a single
failure of the Assumption tactic (which is probable)
would mean failure of the whole composed tactic.
Try tactic is the same as
tactic Else "skip".
Repeat,
Then,
Else
Repeat tactic
Try,
Then
Else tactic2
The tactical tries to perform tactic1. If this succeeds, this tactical is done. If this fails, tactic2 is performed.
Try,
Repeat,
Then
Below we describe the commands that are special for the prove-mode. At the end of this section we describe which other commands can be used in prove-mode.
Exit
prove.
Abort
Abort
Exit
Show num
Show
Undo
Undo num
History command.Infix or Option) undone.
Restart,
History
Restart
Undo,
History
History
Undo n will make all tactics upto
tac undone.
Undo,
Restart
Focus num
Task var
Task
Prove
Almost all commands that are available in main-mode, are also available in prove-mode. Most of them have exactly the same effect (they ignore the local context). However, some commands use the local context of the first goal. These commands are:
The only commands that are not available in prove-mode, are System and Reset.Matching is the problem of finding a substitution for some variables so that a pattern is beta-delta equal to a term. These variables that may substituted for are called existential variables.
Matching in Yarrow is an extension of first-order matching. First order matching means the routine doesn't know anything about beta or delta reduction. There are three ways in which it is extended:
x x1 .. xn where x is an existential variable,
the substitution <x := \x1 .. xn. term> is delivered
(roughly). These patterns are called lambda-patterns.
If the program doesn't see the proper instantation of some existential
variables, the user can mold the term in the proper form with the
Pattern or
Convert tactics.
A path is a way of indicating a subterm of a term. It may be used on any place where a num indicating an occurrence is expected. Paths are generated by the graphical user interface; we strongly discourage use of paths by the user.
The important point is that paths are notated as a space-separated list of numbers, starting with 0. This doesn't conflict with occurrences, since they are always positive numbers, but it may explain unexpected behaviour, e.g. caused by
Unfold 0 plus (typically all occurrences of plus will be unfolded)