Yarrow User Guide

Contents

Index



Background

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



Introduction

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:

[Bar92]
Henk Barendregt. Lambda Calculi with Types. In D.M. Gabbai, S. Abramsky, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume 1. Oxford University Press, 1992.
[SP93]
Paula Severi and Erik Poll. Pure Type Systems with Definitions. Computing Science Note 93/24. Eindhoven University of Technology, 1993.
[Zwa99]
Jan Zwanenburg. Object-Oriented Concepts and Proof Rules: Formalization in Type Theory and Implementation in Yarrow. Ph.D. thesis. Eindhoven University of Technology, 1999.


Syntax

The syntax is quite close to the standard syntax of the typed lambda calculus. We write

\x:T.e
for a lambda abstraction
@x:T.e
for a pi-type (in this program also called @-type)
let x:=e:T.f
for a local definition
f e
for application (left-associative)
(e)
to deviate from standard-precedence

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
for a repeated abstraction
@x1,x2,..xn:T.e
for a repeated pi-type
T->U
as a short-hand for @x:T.U if x does not occur in U (the -> is right-associative)
let x:=e.f
for a local definition

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.

Multi-line input

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))

Infix notation

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.

Extensions

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:

Subtyping

Description:
Pure Type Systems with Subtyping are described in my thesis.
Activation:
Subtyping is activitated by giving two additional parameters to the 'System' command: the list of subtyping sorts and the list of subtyping rules. For example:
System (*,#),(*:#),((*,*),(#,*)),(#),((#,*)) for the second order lambda calculus with subtyping and bounded quantification.
Syntax:
There are two additional constructions:
\x <: t : T. e
for a bounded abstraction.
@x <: t : T. e
for a bounded quantification.
We use \x <: t. e as shorthand for \x <: t : T. e if t : T. This shorthand is also available for bounded quantifications.
Commands:
There are two additional commands available for systems with subtyping. All other commands are adapted to handle subtyping as well. For example, Type gives a minimal type, and Intro and Apply work also for bounded quantifications.

Records

Description:
Records are a variant of cartesian products, where each part has a label. They are also termed labeled products. A part (or field) of a record may be selected by giving a field. Records are an important feature of programming languages.
Activation:
Records are activitated by suffixing a sort with ->records in the command System. E.g.
System (*->records,#),(*:#),((*,*), (#,*))
Now all record-types will have type *, and record-values will have as sort *. Records may only be activated for one sort.
Syntax:
There are three additional constructions for records:
{|l1:T1, .. ln:Tn|}
for a record-type .
{l1=t1, .. ln=tn}
for a record-value.
t`l
for selection of a field from record. The character separating the term and the label is a backquote, usually on some obscure place on the keyboard.
Note that n may be zero.
For labels all ordinary identifiers may be used. A label is not related in any way to a variable with the same name.
Typing:
For each construction there is a typing rule:
Reduction:
There is one reduction rule:
Notes:
The records in Yarrow do depend on the order of the fields. E.g. {l= one, m= true} and {m= true, l= one} are not considered syntactically equal terms. (But they have identical reduction behaviour.)
Subtyping:

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.



Main-mode

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:

  1. The context
  2. Typing and reduction
  3. Meta-commands
  4. Readable syntax
  5. Modules

The context

The following commands extend or examine the context.

Var

Syntax:
  1. Var var-list : term
  2. Var var-list <: term : term
Effect:
Adds variables of type term to the global context. The variables are separated by a comma. The first variant is for ordinary declarations. The second variant is for bounded declarations, and is only available for systems with subtyping. Here the typing part ': term' is optional.
Example:
Var Nat : *
Var mult,(+) : Nat->Nat->Nat
See also:
Def, subtyping

Def

Syntax:
  1. Def var := term
  2. Def var := term : term2
Effect:
Adds the definition of var to be equal to term to the global context. In the second variant the recorded type is term2.
Example:
Def Bool := @A:*.A->A->A
Def true := \A:*.\a1:A.\a2:A.a1 : Bool
See also:
Var

Context

Syntax:
  1. Context [: sort-list] [On filename]
  2. Context "modulename" [: sort-list] [On filename]
  3. Context var .. var [: sort-list] [On filename]
  4. Context var [: sort-list] [On filename]
Effect:

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.

See also:
Option

Reset

Syntax:
Reset var
Effect:
Removes all entries in the context, starting from var.
Implicit declarations for these variables are also reset, but infix declarations are not.
Variables occurring in loaded modules cannot be removed. If the context starting with this variable has to be deleted anyway, the modules should be cleared first.
Prove-mode:
This command is not available in prove-mode.
See also:
Clear

Print

Syntax:
Print var
Effect:
Prints definition/declaration of var.
Prove-mode:
This command is also available in prove-mode. Then it is performed in the context of the first goal.

Prove

Syntax:
Prove var : term
Effect:
Enter the prove-mode to find an inhabitant of term, which will be assigned to var. When the prove-mode is left, the inhabitant will be type-checked so that correctness of the proof depends only on the type-checking algorithm. A summary of all used tactics is displayed, for the convenience of the user.
term must be typable with a sort.
Note:
This command is also available in prove-mode. In other words, you can have multiple proof-tasks at one time. For switching between them, use Task.
See also:
Def, Task

Deduction

Syntax:
Deduction var num
Effect:
Prints definition of var as a flag-proof. The number (which may be left out) sets certain options. It is considered as a binary number, the bits signify from least to most significant:
  1. Print proof terms?
  2. Print separate line for variables?
  3. Make subdeduction for types in flags? (Works only if option 10 set)
  4. Print inhabitants of all sorts, or only proofterms?
  5. Maximal one application at a time?
  6. Keep cuts in the deduction?
  7. Ignore beta-delta conversions? (Even if this is set to 0, some conversions will be ignored!)
  8. Print beta-only conversions? (Ignored if option 7 set)
  9. Print only terms in justification? (Ignored if option 4 set)
  10. Maximal one assumption in a flag?
E.g. 000010010 means max. one application at a time and print a separate line for variables. Default num is zero.
Prove-mode:
This command is also available in prove-mode. Then it is performed in the context of the first goal.
NOTE:
THIS COMMAND IS EXPERIMENTAL.

Typing and reduction

The following commands implement miscellaneous typing and reduction routines.

Type

Syntax:
Type term
Effect:
Gives the type of term.
Prove-mode:
This command is also available in prove-mode. Then it is performed in the context of the first goal.

Check

Syntax:
  1. Check term : term
  2. Check term :=: term
  3. Check term <: term
Effect:
The first variant checks that the typing judgment holds. The second variant checks whether or not the two terms are beta-delta convertable. The third variant checks if the first term is a subtype of the second term (for systems with subtyping).
Prove-mode:
This command is also available in prove-mode. Then it is performed in the context of the first goal.
See also:
subtyping

bRed

Syntax:
bRed term
Effect:
Gives the b-normal form of term.
Prove-mode:
This command is also available in prove-mode. Then it is performed in the context of the first goal.
See also:
bdRed, dRed

dRed

Syntax:
dRed term
Effect:
Gives the d-normal form of term.
Prove-mode:
This command is also available in prove-mode. Then it is performed in the context of the first goal.
See also:
bdRed, bRed

bdRed

Syntax:
bdRed term
Effect:
Gives the bd-normal form of term.
Prove-mode:
This command is also available in prove-mode. Then it is performed in the context of the first goal.
See also:
dRed, bRed

Meta-commands

Some of these commands allow you to set parameters of the system, and others implement auxilary functions.

Quit

Syntax:
Quit
Effect:
Quits Yarrow immediately.
Prove-mode:
This command is not available in prove-mode. Exit prove-mode first.

Help

Syntax:
  1. Help
  2. Help command
  3. Help list
Effect:
The first variant gives a list of the most used commands in this mode, with a short description.
Variant 2 gives complete help on one command or notion. Variant 3 lists all commands and notions for which help is available.

System

Syntax:
  1. System sys
  2. System
Effect:

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.

Examples:
System (Set,Type),(Set:Type),((Set,Set),(Set,Type)) for \P.
System (*,#,##),(*:#,#:##),((*,*),(*,#,##))
Note:
The typing algorithm may not be able to handle some systems. In this situation an error will be issued.
Prove-mode:
This command is not available in prove-mode.
See also:
extensions

Read

Syntax:
Read "filename"
Effect:
Reads script file filename. This command has the same effect as entering the contents of the file by keyboard. However, if an error occurs, all input after the error is ignored.
Prove-mode:
This command is also available in prove-mode.
See also:
Path

Option

Syntax:
  1. Option +opt
  2. Option -opt
  3. Option
Effect:
The first variant sets option opt on, the second sets it off.
The options are:
i
parameters of variables may be implicit (see implicit)
s
print after the types in contexts also the sorts
p
print the proofterm with its holes when in prover mode
r
show reduction path for commands bdRed, bRed, dRed
The third variant displays the current values of the options.

Readable syntax

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

Syntax:
Infix num var
Effect:
Sets the precedence of operator var to num, and makes it non-associative. The precedence runs from 1 to 9, operators with a higher precedence bind stronger. In this way many parentheses can be avoided.
Note that this command affects only parsing and printing of expressions; the termed operator does not have to be defined yet.
Standard precedence is 5. Note that application binds always stronger and -> always weaker than operators.
Examples:
Infix 2 (=)
Infix 5 (+)
See also:
InfixR, InfixL, infix-notation

InfixL

Syntax:
InfixL num var
Effect:
Sets the precedence of operator var to num, and makes it left-associative.
Example:
InfixL 5 (-)
After this, x-y-z will be interpreted as (x-y)-z
See also:
Infix, InfixR, infix-notation

InfixR

Syntax:
InfixR num var
Effect:
Sets the precedence of operator var to num, and makes it right-associative.
Example:
InfixR 7 (^)
After this, x^y^z will be interpreted as x^(y^z).
See also:
Infix, InfixL, infix-notation

Implicit

Syntax:
Implicit num var
Effect:

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.

Examples:
Assume the following declarations have been made:
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 (=)

And so the following expressions are admitted:
id O (means id Nat O)
comp not even (means comp Nat Bool Bool not even)
O=O (means (=) Nat O O)
Shortcomings:
Sometimes arguments are not printed while they cannot be inferred.
See also:
Option

Binder

Syntax:
Binder var
Effect:
var is declared as a binder, so applications of var to an abstraction are parsed and printed in an abbreviated form, i.e. the lambda is left out.
After a variable is declared as binder, it is always interpreted by the parser as a binder; only if parenthesized, it can be used as an ordinary variable.
Example:
Assume the following declaration has been made:
Ex : (Nat->*) -> *
and Ex is declared as a binder:
Binder Ex
then the expression Ex x:Nat. x=x stands for Ex (\x:Nat. x=x).

The application of Ex to P is now written as (Ex) P.
See also:
Implicit

Modules

Yarrow has a module system that allows pieces of contexts to be loaded without repeating type-checking. A module is a file, consisting of:

  1. a segment of context
  2. a type-system in which this segment is valid
  3. an import list of modules that contain variables needed for this segment
  4. infix and implicit declarations for variables in the segment

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

Syntax:
Save "filename"
Effect:
Saves the piece of the context not belonging to existing modules in module 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.
However, if filename is the most recent module, it is updated. That means that the piece of the context added since this module was loaded is added to the module.
If filename is another loaded module, it can't be updated.
Example:
Save "integer"
See also:
Load,   Clear

Load

Syntax:
  1. Load "filename"
  2. Load
Effect:

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.

Example:
Load "integer"
See also:
Save, Clear, Read, Path

Clear

Syntax:
Clear
Effect:
Clears the last module from the list of loaded modules. This has no effect on the context, but means Yarrow has 'forgotten' the last module is loaded. In this way parts of the context coming from a module can be saved in another module.
Example:
Load "int1"
Load "int2"
Clear
Clear
Save "int1and2"

Now module int1and2 contains all declarations of both int1 and int2. Without the clear commands, int1and2 would be empty.
Prove-mode:
This command is not available in prove-mode.
See also:
Load,   Save

Path

Syntax:
  1. Path "pathname"
  2. Path
Effect:

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.

Example:
Path "theories/lists"
Prove-mode:
This command is not available in prove-mode.
Shortcoming:
You cannot delete entries from the path.
See also:
Load, Read


Prove-mode

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).


Tactics

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:

  1. Basic tactics
  2. Transforming tactics
  3. Special tactics for the Leibniz-equality and propositional logic
  4. Tacticals

Basic tactics

These tactics are shown in order of frequency of use.

Intro

Syntax:
  1. Intro var-list
  2. Intro
Effect:
If the goal is a @-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).
Example:
Intro A,x,H1,H2
See also:
Intros

Intros

Syntax:
  1. Intros
  2. Intros num
Effect:
The first variant repeats Intro as often as possible. The second variant repeats Intro num times.
See also:
Intro, Repeat

Apply

Syntax:
  1. Apply term
  2. Apply term On term-list
Effect 1:

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.

Example:
Suppose we have in the context
H : @x:Nat. P x -> Q x
and the goal is
Q zero
then the tactic Apply H succeeds with as new goal
P zero
Here H 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.
Effect 2:

The second variant is a combination of the Forward tactic and the Apply 1 tactic.

Example 2:
Suppose our goal is
lem : @x,y,z : Int. x<y -> y<z -> x<z
H : b<c
---------
a<c
Then the tactic Apply lem On H results in the goal
---------
a<b
See also:
matching, Forward

Exact

Syntax:
Exact term
Effect:
This tactic directly proves the goal, if term is an inhabitant of the goal.
See also:
Assumption

Assumption

Syntax:
Assumption
Effect:
This tactic directly proves the goal if a variable with this type is in the local or global context.
See also:
Exact

Cut

Syntax:
Cut term
Effect:
Prove the goal by using the cut rule for term. That is, first prove the goal assuming term, and prove term later.
See also:
First

First

Syntax:
First term
Effect:
Prove the goal by using the cut rule for term. That is, first prove term, and prove the current goal later with assumption term.
The only difference with Cut is the order of the generated subgoals. Indeed, it is the same as Cut followed by Focus 2.
See also:
Cut, Focus

Forward

Syntax:
  1. Forward term
  2. Forward term On term-list
Effect 1:

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.

Example 1:
Suppose our goal is
H2 : @x:Nat. P x -> Q x
H3 : P y
---------
R
Then the tactic Forward H2 y H3 results in
H2 : @x:Nat. P x -> Q x
H3 : P y
H4 : Q y
---------
R
Effect 2:

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.

Example 2:
Suppose our goal is
lem : @x,y,z : Int. x<y -> y<z -> x<z
H1 : a<b
H2 : b<c
---------
R
Then the tactic Forward lem On H1, H2 results in a new assumption
H3 : a<c
See also:
First, Exact, Intro, Hide

Let

Syntax:
  1. Let var := term
  2. Let var := term : term2
Effect:
Adds a definition to the local context.

Tactics for presentation

These tactics do not change the goal or the local context, but only change the way the local context is printed.

Hide

Syntax:
Hide var-list
Effect:
This tactic suppresses printing of the local variables named in var-list.
See also:
Unhide

Unhide

Syntax:
  1. Unhide var-list
  2. Unhide
Effect:
The first variant makes the suppression of printing of the local variables named in var-list undone.
The second variant makes sure all local variables are printed.
See also:
Hide

Transforming tactics

These tactics convert the goal (or sometimes, a hypothesis), into a beta-delta convertible one.

Unfold

Syntax:
  1. Unfold var
  2. Unfold num-list var
  3. Unfold var In var2
  4. Unfold num-list var In var2
Effect:
The given variable is unfolded; in variants 1 and 2 in the goal, and for variants 3 and 4 in the type of var2, which should be in the local context.
In variants 1 and 3 all occurrences are unfolded, in variant 2 and 4 only the numbered occurrences of the variable are unfolded. Here the explicit prefix order is used, this can be different from the order in the text if infix operators or implicit arguments are used!
After the unfolding the term is simplified.
Example:
Unfold 1,3 plus
unfolds the first and third occurrence of plus
Shortcomings:
If there are numbers in the list not corresponding to an occurrence, no error is given. Do not use the number 0, since that indicates a path (see paths).
See also:
Implicit, Infix, Simplify, Convert

Simplify

Syntax:
Simplify
Effect:
The goal is reduced to beta normal form.
See also:
Convert, Unfold, Pattern

Convert

Syntax:
Convert term
Effect:
Changes the goal to term, which should be beta-delta-convertible to the goal.
See also:
Unfold, Simplify, Pattern

Pattern

Syntax:
  1. Pattern term
  2. Pattern num-list term
Effect:
This tactic performs a beta-expansion. The first variant abstracts over all occurrences of term in the current goal, the second variant abstracts only over the numbered occurences of term.
In this way the goal can be converted into a form more suitable for matching.
Shortcomings:
If there are numbers in the list not corresponding to an occurrence, no error is given. Do not use the number 0, since that indicates a path (see paths).
See also:
Convert

Special tactics

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

Syntax:
  1. Use tacticname var
  2. Use
Effect:
tacticname should be the name of a special tactic, and var should be the proof of a lemma that is used by this tactic. This command records the name of this lemma, so that if the indicated tactic is used, this lemma is automatically invoked. Which form of lemma is used by a tactic, is indicated in the description of the tactic.
More than one lemma can be associated with one tactic.
The command without parameters gives an overview that shows which special tactics are associated with which lemmas.
See also:
AndI, AndEL, AndER, OrIL, OrIR, OrE, NotI, NotE, FalseE, ExistsI, ExistsE, Rewrite, Lewrite, Refl

AndI

Syntax:
AndI
Effect:
The goal should be a conjunction. This tactic splits the goal in two separate conjuncts.
This tactic needs an introduction lemma for conjunction of the following form:
@P,Q:s. P -> Q -> and P Q
See also:
Use

AndEL

Syntax:
  1. AndEL term
  2. AndEL term On term-list
Effect:
The conclusion of the type of term should be a conjunction. This tactic adds the left conjunct to the local context. The second variant is a combination of 'Forward' and 'AndEL 1'.
This tactic needs an elimation lemma for conjunction of the following form:
@P,Q:s. and P Q -> P
Shortcomings:
It is not possible to give the name of the new hypothesis.
See also:
Forward, AndER, AndE, Use

AndER

Syntax:
  1. AndER term
  2. AndER term On term-list
Effect:
The conclusion of the type of term should be a conjunction. This tactic adds the right conjunct to the local context. The second variant is a combination of 'Forward' and 'AndER 1'.
This tactic needs an elimation lemma for conjunction of the following form:
@P,Q:s. and P Q -> Q
Shortcomings:
It is not possible to give the name of the new hypothesis.
See also:
Forward, AndEL, AndE, Use

AndE

Syntax:
  1. AndE term
  2. AndE term On term-list
Effect:
The conclusion of the type of term should be a conjunction. This tactic adds both conjuncts to the local context, and if term is a local variable, this variable is hidden.
The second variant is a combination of 'Forward' and 'AndE 1'.
'AndE' is a combination of the special tactics 'AndEL' and 'AndER'; so both have to be made available by 'Use', before 'AndE' can be used.
Shortcomings:
It is not possible to give the name of the new hypotheses.
See also:
Forward, AndEL, AndER, Use, Hide

OrIL

Syntax:
OrIL
Effect:
The goal should be a disjunction. This tactic reduces this goal to the disjunct on the left hand side.
This tactic needs an introduction lemma for disjunction of the following form:
@P,Q:s. P -> or P Q
See also:
Use

OrIR

Syntax:
OrIR
Effect:
The goal should be a disjunction. This tactic reduces this goal to the disjunct on the right hand side.
This tactic needs an introduction lemma for disjunction of the following form:
@P,Q:s. Q -> or P Q
See also:
Use

OrE

Syntax:
  1. OrE term
  2. OrE term On term-list
Effect:
The conclusion of the type of term should be a disjunction. This tactic generates (at least) two new goals. The two new goals have the same conclusion as the old goal, but the local context of the first goal is augmented by the disjunct on the left hand side, and likewise for the second goal and the disjunct on the right hand side. If term is a local variable, this variable is hidden.
The second variant is a combination of 'Forward' and 'OrE 1'.
This tactic needs an elimation lemma for disjunction of the following form:
@P,Q:s1. @R:s2. or P Q -> (P->R) -> (Q->R) -> R
Shortcomings:
It is not possible to give the name of the new hypotheses.
See also:
Forward, Use, Hide

NotI

Syntax:
NotI
Effect:
The goal should be a negation. This tactic adds the negated proposition to the context and sets the new goal to False.
This tactic needs an introduction lemma for negation of the following form:
@P:s. (P -> False) -> Not P
Shortcomings:
It is not possible to give the name of the new hypotheses.
See also:
Use

NotE

Syntax:
  1. NotE term
  2. NotE term On term-list
Effect:
The conclusion of the type of term should be of the form 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'.
This tactic needs an elimation lemma for negation of the following form:
@P:s. Not P -> P -> False
See also:
Forward, Use

FalseE

Syntax:
FalseE
Effect:
This tactic replaces the current goal by False, if the following elimination lemma is recorded with the command use:
@P:s. False -> P
See also:
Use

ExistsI

Syntax:
ExistsI term
Effect:
The goal should be an existential quantification. term is taken to be the witness of the property. The new goal is to prove that this is indeed the case.
This tactic needs an introduction lemma for existential quantification of the following form:
@x1:t1. ... @xn:tn. @x:t. @P:t->s. P x -> Ex x1 .. xn P
See also:
Use

ExistsE

Syntax:
  1. ExistsE term
  2. ExistsE term On term-list
Effect:
The conclusion of the type of term should be an existantial quantification. This tactic generates a new goal, where the local context is extended with a witness and a proof of the property for the witness. If term is a local variable, this variable is hidden.
The second variant is a combination of 'Forward' and 'ExistsE 1'.
This tactic needs an elimation lemma for existential quantification of the following form:
@x1:t1. ... @xn:tn. @P:t->s1. @R:s2. Ex x1 .. xn P -> (@x:t. P x -> R) -> R
Shortcomings:
It is not possible to give the name of the new hypotheses.
See also:
Forward, Use, Hide

Rewrite

Syntax:
Rewrite [num] term [On term-list] [In var]
Effect:
term should be the proof of an equality. This tactic replaces in the goal one occurrence of the left-hand side of the equality by the right-hand side. The optional number selects the occurrence (otherwise the first). The variant with the 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.
This tactic needs an elimination lemma for Leibniz-equality of the following form:
@x1:t1. .. @xn:tn.@x,y:t. @P:t->sort. eq x1 .. xn x y -> P y -> P x
Note here the order of y and x!
The equality may be quantified and may have conditions, which will become new goals.
Example:
Suppose we have already typed:
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)

and our goal is,
Q two -> R
then Rewrite lemma will yield as new goal
Q (minus two zero) -> R
Shortcomings:
See also:
Forward, Lewrite, Use

Lewrite

Syntax:
Lewrite [num] term [On term-list] [In var]
Effect:
term should be the proof of an equality. This tactic replaces in the goal one occurrence of the RIGHT-hand side of the equality by the LEFT-hand side.
This tactic needs an elimination lemma for Leibniz-equality of the following form:
@x1:t1. .. @xn:tn.@x,y:t. @P:t->sort. eq x1 .. xn x y -> P x -> P y
Note here the order of y and x!
For more information we refer to 'Rewrite'.
Shortcomings:
See also:
Rewrite, Use

Refl

Syntax:
Refl
Effect:
The goal should be of the form 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 x
See also:
Use

Tacticals

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

Syntax:
  1. tactic Then ( tactic1 | tactic2 | ... | tacticn )
  2. tactic Then tactic1
Effect:

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.

See also:
Try, Repeat, Else

Try

Syntax:
Try tactic
Effect:
This tactical tries tactic, but does not fail if tactic fails.
Example:

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".

See also:
Repeat, Then, Else

Repeat

Syntax:
Repeat tactic
Effect:
Repeats tactic as often as possible, but with a maximum of 10 times. So it is ensured the repetition always ends.
See also:
Try, Then

Else

Syntax:
tactic1 Else tactic2
Effect:

The tactical tries to perform tactic1. If this succeeds, this tactical is done. If this fails, tactic2 is performed.

See also:
Try, Repeat, Then


Commands of prove-mode

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

Syntax:
Exit
Effect:
Finishes the current proof task and returns to main-mode (if no other proof tasks are running). This command is only admitted if the proof is completed. The proof will be recorded under the name given with the command prove.
See also:
Abort

Abort

Syntax:
Abort
Effect:
Aborts the current proof-task and returns to main-mode (if no other proof-tasks are running). The proof is not recorded, even if it is completed.
See also:
Exit

Show

Syntax:
  1. Show num
  2. Show
Effect:
Shows goal num with its context. Default is goal number 1.

Undo

Syntax:
  1. Undo
  2. Undo num
Effect:
Makes the last tactic of the current goal undone (so this a local undo). The second variant makes the last num tactics undone. In case the number of tactics you want to undo is unknown, this can be looked up with the History command.
Note that this command doesn't make the effect of COMMANDS (e.g. Infix or Option) undone.
See also:
Restart, History

Restart

Syntax:
Restart
Effect:
Returns to the goal you started with.
See also:
Undo, History

History

Syntax:
History
Effect:
Shows a list of the tactics used so far in proving the proposition, in a structured way. The lines with a question mark indicate the current subgoals.
Some tactics are numbered. Suppose a tactic tac has number n, then Undo n will make all tactics upto tac undone.
See also:
Undo, Restart

Focus

Syntax:
Focus num
Effect:
Selects goal num as the current goal.

Task

Syntax:
  1. Task var
  2. Task
Effect:
This command switches to the proof-task for var. Of course, this is only useful when there are multiple proof-tasks.
The second variant displays all current proof-tasks.
See also:
Prove

Other commands

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

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:

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.


paths

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