[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

A. Reference

This part is meant as a brief, but complete reference to Tutch.


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

A.1 Command Line Syntax

The proof checker Tutch is invoked by
 
$ /afs/andrew/course/15/317/bin/tutch [options] [files]
The files are extended by `.tut' if they do not have an extension already. Options are:

-h, --help
Print help message.
-q, --quiet
Be quiet, print only version, file access and error messages.
-Q, --Quiet
Be really quiet, print only error messages.
-r, --requirements file
Check Tutch files against requirements in file resp. file.req (this extension is added if no extension is given) and print out check list. The path `/afs/andrew/course/15/317/req' for file is assumed unless file starts with a `.' or `/'. If no files are given, file.tut is assumed as input file.
-v, --verbose
Be verbose, print justification for each proof line.
-V, --Verbose
Print every available message.

Assignments submission is possible via
 
$ /afs/andrew/course/15/317/bin/submit -r file [options] [files]
Options are the same as for tutch, but -r is mandatory. The status of a submission can be checked via
 
$ /afs/andrew/course/15/317/bin/status file
This retrieves the status of the submission file handed in via submit -r file ....


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

A.2 Tutch File Syntax

Tutch recognizes a set of special symbols. They do not have to be separated by spaces from the remaining code, but serve as separators themselves. These symbols are
 
( ) [ ] ; : = ~ & | => <=>
Furthermore there are reserved words which cannot be used as identifiers:
 
T F proof begin end
Identifiers are made up of letters `a-zA-Z', digits `0-9' underscores `_' and primes `''.

Atoms Q are identifiers that start with capital letter. Propositions A, B have the following grammar
 
A, B ::= T             % Truth     
       | F             % Falsehood
       | Q             % Atom
       | ~A            % Negation
       | A & B         % Conjunction
       | A | B         % Disjunction
       | A => B        % Implication
       | A <=> B       % Equivalence
       | (A)           % Parentheses
The binary operators `&', `|' and `=>' are right associative, `<=>' is non-associative. Binding strength decreases in this order:
 
~ & | => <=>
A hypothesis H is just a proposition. A proof entry E is either a line or a frame. A proof P is a non-empty list of entries.
 
H    ::= A             % Hypothesis
E    ::= A             % Line
       | [ H; P ]      % Frame
P    ::= E             % Final step
       | E; P          % Step and remaining proof
A proof name x is a non-capital identifier. A Tutch file F is a sequence of proof declarations. A proof declaration D has the following syntax:
 
D    ::= proof x: A = begin P end    % Proof of A with name x
F    ::=                             % Empty file
       | D; F                        % Declaration and remaining file


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

A.2.1 Proof Terms

We extend our list of special symbols and reserved words by the following:
 
, annotated term fst snd inl inr case of fn abort
Proof terms for propositional logic are formed according to the following grammar:

 
M, N ::= x             % Variable
       | (M, N)        % Pair
       | fst M         % First projection
       | snd M         % Second projection
       | inl M         % Left injection
       | inr M         % Right injection
       | case M of inl x => N | inr y => O end % Case analysis
       | fn x => M     % Abstraction
       | M N           % Application
       | ()            % Empty tuple (proof of truth)
       | abort M       % Falsehood elimination
       | M : A         % Annotation

Application is a "invisible" left-associative infix operator. It has maximal binding strength, along with the prefix operators `fst', `snd', `inl', `inr', `abort'. This enforces use of parentheses in most cases. E.g.,
 
(fst x) ((snd x) y)
has already a minimum amount of parentheses. Abstraction `fn x =>' binds less than application and annotation `:' least. The following term is syntactically correct.
 
fn y => fn x => x y : A => (A => B) => B

Annotated proofs P are proofs as defined above annotated with proof terms. This changes the syntax of hypotheses H and proof entries E.
 
H    ::= x : A         % Hypothesis
E    ::= M : A         % Line
       | [ H; P ]      % Frame
P    ::= E             % Final step
       | E; P          % Step and remaining proof

A Tutch file F now can contain proof, term and annotated proof declarations D:
 
D    ::= proof ...
       | annotated proof x: A = begin P end % Annotated proof of A with name x
       | term x: A = M                      % Proof of A with name x
F    ::=                             % Empty file
       | D; F                        % Declaration and remaining file


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

A.2.2 Types and Programs

New special symbols and keywords are:

 
* + -> :: nat bool list 0 s rec true false if then else nil val

Types T, T' have the following grammar:

 
T, T' ::= 1             % Unit type     
        | 0             % Empty type
        | a             % Atom
        | nat           % Natural numbers
        | bool          % Booleans
        | T list        % Lists of element type T
        | T * T'        % Product
        | T + T'        % Disjoint sum
        | T -> T'       % Function space
        | (T)           % Parentheses
`list' is a postfix operator.

The binary operators `*', `+' and `=>' are right associative. Binding strength decreases in this order:

 
list * + ->

We extend the grammar for terms by the following constructs:
 
M, N ::= ...
       | 0                    % Zero
       | s M                  % Successor
       | rec M of f 0 => N | f (s x) => O end       % Recursion over nat
       | true                 % True
       | false                % False
       | if M then N else O   % Boolean case distinction

       | nil                  % Empty list
       | M :: N               % List construction
       | rec M of f nil => N | f (x :: xs) => O end % Recursion over list

`0', `true', `false' and `nil' are constants, `s' and `if r then s else' are prefix operators and `::' is an infix operator with lower precedence than the prefix operators or application.

We add one new declaration to the syntax of tutch files:

 
D    ::=  ...
       | val x: T = M                % Program of type T with name x
F    ::=                             % Empty file
       | D; F                        % Declaration and remaining file


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

A.2.3 First-Order Logic

Reasoning in First-Order Logic (FOL) requires handling of universally and existentially quantified propositions. New special symbols are
 
! ? .
We extend our definition of propositions by
 
A, B ::= ...
       | R M1...Mn     % Instantiation
       | !x:T. A       % Universal quantification
       | ?x:T. A       % Existential quantification
Relation symbols R are capital identifiers. Only they can be instantiated by terms Mi, e.g. `A(x)', which is the same as `A x'. Instantiation binds strongest, as strong as application and the prefix operators for terms M.

Quantification `!x:T' resp. `?x:T. A' is treated as a prefix operator with minimal precedence (like lambda abstraction). Ordered by binding strength, the operators that appear in propositions are:
 
!x:T. resp. ?x:T., <=>, =>, |, &, ~, instantiation
The `proof' declaration supports now also proofs in FOL. Two judgments can form a statement of the proof: an assertion A (representing `A true' and a term declaration M : T expressing "M has type T". In the same way there are now two forms of hypotheses: x : T, which introduces a new parameter x into the proof, and A which assumes that A is true. Furthermore one frame can introduce several hypotheses, separated by commas. The grammar for proofs is the following:
 
H    ::= A             % Hypothesis introduction
       | x : T         % Parameter introduction
Hs   ::= H             % Last hypothesis
       | H, Hs         % Several hypotheses
E    ::= A             % Line: Assertion
       | M : T         % Line: Term declaration
       | [ Hs; P ]     % Frame
P    ::= E             % Final step
       | E; P          % Step and remaining proof
All variables in a proposition that appears in a proof must be bound by quantifiers or be (visible) parameters introduced by frames.


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

A.2.4 Arithmetic

We add the two binary relations "less than" and "equal to" to our definition of propositions
 
A, B ::= ...
       | M < N         % M less than N
       | M = N         % M equal to N
These relations allow us to prove properties about them and defined functions by induction.

Unfortunately, `=' introduces a ambiguity into our syntax, e.g. in
 
proof Ex2 : !x:nat. 0 < x => ?y:nat. s(y) = x = ...
While parsing the first `=', it is not clear whether it marks the end of the proposition or stands for the equality relation. This ambiguity is resolved by the following rule:

Whenever the expression before `=' is definitively a term, then `=' is parsed as equality. In all other cases it is parsed as the end of the declaration.
In our case `s(y)' is definitively a term. At the next `=', the expression on the left of it is `s(y)=x', which is a proposition, not a term. Thus the end of the declaration is correctly recognized. The same happens in the following example:
 
val nth : nat -> tau list -> tau -> tau = ...
The expression `tau' left of the equality symbol is a variable. It could be a term or a type variable. Thus it is not definitely a term, and the parser finished parsing the type of `nth' here.

Not correctly resolved is the ambiguity in this case:
 
proof refl : !x:nat. x = x = ...
Since `x' is either a term variable or a type variable from the perspective of mere syntax, it is not definitively a term. Thus the parser detects falsely the end of the declaration of `refl'. The parser will then try to interpret `!x:nat.x' as a proposition, and fail with the following error message:

Category mismatch: x is a variable, but a proposition is expected in this place
To work around this bug, insert parentheses somewhere around the equality expression, e.g.
 
proof refl : !x:nat. (x = x) = ...


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

A.2.4.1 Proof Terms

The introduction and elimination rules for equality and less-than give rise to the following proof terms. All are reserved words:
 
eq0 eqS eqE0S eqES0 eqESS less0 lessS lessE0 lessES
Of these, two are constants: eq0 and less0. All other are prefix operators. For induction we reuse the `rec' construct for primitive recursion.


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

A.2.5 Structural Induction

We reuse `=' for equality on lists. The following proof terms represent the introduction and elimination rules for equality on lists. These are new reserved words:
 
eqN eqC eqENC eqECN eqECC
Except eqN, which is a constants, all are prefix operators. The rule for eqC is:

If M : xs = ys, then eqC M : x::xs = x::ys for an arbitrary x.
Here we assume that all these lists xs, ys, x::xs, x::ys are well-formed and of the same type.


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

A.2.6 Summary

This sections summarizes the syntax specification given in the previous sections.

Special Symbols:
 
( ) [ ] ; : = ~ & | => <=> , * + -> :: ! ? . <

Reserved words:
 
annotated proof term val begin end 
T F nat bool list
inl inr case of fst snd fn abort
0 s rec true false if then else nil 
eq0 eqS eqE0S eqES0 eqESS 
less0 lessS lessE0 lessES
eqN eqC eqENC eqECN eqECC

Proposition expressions:
 
A, B ::= T             % Truth     
       | F             % Falsehood
       | Q             % Atom
       | ~A            % Negation
       | A & B         % Conjunction
       | A | B         % Disjunction
       | A => B        % Implication
       | A <=> B       % Equivalence
       | R M1...Mn     % Instantiation
       | !x:T. A       % Universal quantification
       | ?x:T. A       % Existential quantification
       | M < N         % M less than N
       | M = N         % M equal to N

Type expressions:
 
T, T'::= 1             % Unit type     
       | 0             % Empty type
       | a             % Atom
       | nat           % Natural numbers
       | bool          % Booleans
       | T list        % Lists of element type T
       | T * T'        % Product
       | T + T'        % Disjoint sum
       | T -> T'       % Function space

Terms:
 
M, N ::= x             % Variable
       | (M, N)        % Pair
       | fst M         % First projection
       | snd M         % Second projection
       | inl M         % Left injection
       | inr M         % Right injection
       | case M of inl x => N | inr y => O end      % Case analysis
       | fn x => M     % Abstraction
       | M N           % Application
       | ()            % Empty tuple (proof of truth)
       | abort M       % Falsehood elimination
       | M : A         % Annotation
       | 0             % Zero
       | s M           % Successor
       | rec M of f 0 => N | f (s x) => O end       % Recursion over nat
       | true          % True
       | false         % False
       | if M then N else O                    % Boolean case distinction
       | nil           % Empty list
       | M :: N        % List construction
       | rec M of f nil => N | f (x :: xs) => O end % Recursion over list
       | eq0           % Proof of 0 = 0
       | eqS M         % Proof of M = N |- s M = s N
       | eqE0S M       % Elimination of 0 = s N
       | eqES0 M       % Elimination of s M = 0
       | eqESS M       % Proof of s M = s N |- M = N
       | less0 M       % Proof of 0 < s M
       | lessS M       % Proof of M < N |- s M < s N
       | lessE0 M      % Elimination of s M = 0
       | lessES M      % Proof of s M = s N |- M = N
       | eqN           % Proof of nil = nil
       | eqC M         % Proof of Ms = Ns |- M::Ms = M::Ns
       | eqENC M       % Elimination of nil = M::Ms
       | eqECN M       % Elimination of M::Ms = nil
       | eqECC M       % Proof of M::Ms = N::Ns |- Ms = Ns

Operator precedence:
 
_ _ (application) list inl inr fst ... (all atomar prefix ops)
::
if M then N else
let (x,u) = M in 
fn x =>
<
=
~ 
& * 
| +
=> ->
<=>
!x:t. ?x:t.

Proofs:
 
H    ::= A             % Hypothesis introduction
       | x : T         % Parameter introduction
Hs   ::= H             % Last hypothesis
       | H, Hs         % Several hypotheses
E    ::= A             % Line: Assertion
       | M : T         % Line: Term declaration
       | [ Hs; P ]     % Frame
P    ::= E             % Final step
       | E; P          % Step and remaining proof

Annotated Proofs:
 
H    ::= x : A         % Hypothesis
E    ::= M : A         % Line
       | [ H; P ]      % Frame
P    ::= E             % Final step
       | E; P          % Step and remaining proof

Declarations:
 
D    ::= proof x: A = begin P end    % Proof of A with name x
       | annotated proof x: A = begin P end % Annotated proof of A with name x
       | term x: A = M                      % Proof of A with name x
       | val x: T = M                % Program of type T with name x
F    ::=                             % Empty file
       | D; F                        % Declaration and remaining file


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

A.3 Requirements File Syntax

A requirements file F specifies proof and program tasks, but does not give any proofs or implementations. Grammar:

 
S    ::= proof x: A                  % Proof specification
       | annotated proof x: A        % Proof specification
       | term x: A                   % Term specification
       | val x: T                    % Program specification
F    ::=                             % Empty file
       | S; F                        % Specification and remaining file


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

A.4 Proof Checking

We give an inductive definition of the proof checking algorithm implemented in Tutch via two judgments `step' and `valid'. The definition is given as in Twelf syntax.

 
% Tutch proof checker for propositional logic

% any infinite datatype:
nat : type.
z : nat.
s : nat -> nat.

% Propositions
prop : type. %name prop A.

% Formation rules
true  : prop.
false : prop.
atom  : nat -> prop.
&     : prop -> prop -> prop.  %infix right 14 &.
|     : prop -> prop -> prop.  %infix right 13 |.
=>    : prop -> prop -> prop.  %infix right 12 =>.

% Notational definitions
~     : prop -> prop
      = [A:prop] (A => false).  %prefix 15 ~.
<=>   : prop -> prop -> prop
      = [A:prop][B:prop] (A => B) & (B => A) .  %infix none 11 <=>.

% One-step inference algorithm
step : prop -> type. 

nonhyp : prop -> type.          % available non-hypothetical judgment
hyp    : prop -> prop -> type.  % available hypothetical judgment

% immediate tactic
imm    : nonhyp A -> step A.

% introduction tactics
trueI  : step true.
&I     : nonhyp A -> nonhyp B -> step (A & B).
|IL    : nonhyp A -> step (A | B).
|IR    : nonhyp B -> step (A | B).
=>I    : hyp A B -> step (A => B).

% elimination tactics
falseE : nonhyp false -> step A.
&EL    : nonhyp (A & B) -> step A.
&ER    : nonhyp (A & B) -> step B.
|E     : nonhyp (A | B) -> hyp A C -> hyp B C -> step C.
=>E    : nonhyp (A => C) -> nonhyp A -> step C.
 
% Proofs
proof : type. %name proof P.

final : prop -> proof.                      % P, Q ::= A
line  : prop -> proof -> proof.             %        | A; P
frame : prop -> proof -> proof -> proof.    %        | [H; P]; Q

% Proof checking
valid : proof -> prop -> type. 

vfinal : step A -> valid (final A) A.
vline  : step A -> (nonhyp A -> valid P B) -> valid (line A P) B.
vframe : (nonhyp H -> valid P A) -> (hyp H A -> valid Q B) 
         -> valid (frame H P Q) B.


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

A.4.1 Proof Terms

Here we give a new Twelf implementation of Tutch that includes proof terms. The definition and the typing rules are:

 
% Tutch proof checker for propositional logic
% Version 0.2 proof terms

% any infinite datatype:
nat : type.
z : nat.
s : nat -> nat.

% Propositions
prop : type. %name prop A.

% Formation rules
true  : prop.
false : prop.
atom  : nat -> prop.
&     : prop -> prop -> prop.  %infix right 14 &.
|     : prop -> prop -> prop.  %infix right 13 |.
=>    : prop -> prop -> prop.  %infix right 12 =>.

% Notational definitions
~     : prop -> prop
      = [A:prop] (A => false).  %prefix 15 ~.
<=>   : prop -> prop -> prop
      = [A:prop][B:prop] (A => B) & (B => A) .  %infix none 11 <=>.

% Proof terms
term : type.  %name term M.

fst  : term -> term.
snd  : term -> term.
,    : term -> term -> term.   %infix right 14 ,.
inl  : term -> term.
inr  : term -> term.
case : term -> (term -> term) -> (term -> term) -> term.
\    : (term -> term) -> term. %prefix 11 \.
    : term -> term -> term.   %infix left 20 .
<>   : term.                   
abort: term -> term.

% Typing judgement
in   : term -> prop -> type.  %infix none 0 in.

% Typing rules
&I    : M in A -> N in B -> (M , N) in A & B.
&EL   : M in A & B -> fst M in A.
&ER   : M in A & B -> snd M in B.
|IL   : M in A -> inl M in A | B.
|IR   : M in B -> inr M in A | B.
|E    : M in A | B -> ({x: term} x in A -> N x in C) 
                   -> ({y: term} y in B -> L y in C) 
             -> case M N L in C.
=>I   : ({x: term} x in A -> M x in B) -> \ M in A => B.
=>E   : M in A => B -> N in A -> M  N in B.
trueI : <> in true.
falseE: M in false -> abort M in C.

We add annotated proofs, which need an inference algorithm that respects proof terms:

 
% One-step inference algorithm
step   : term -> prop -> type. % %mode step +A.

j0hyp  : term -> prop -> type.          % available non-hypothetical judgment
j1hyp  : (term -> term) -> prop -> prop -> type.  
                                        % available hypothetical judgment
% immediate tactic
imm    : j0hyp M A -> step M A.

% introduction tactics
bytrueI  : step <> true.
by&I     : j0hyp M A -> j0hyp N B -> step (M , N) (A & B).
by|IL    : j0hyp M A -> step (inl M) (A | B).
by|IR    : j0hyp M B -> step (inr M) (A | B).
by=>I    : j1hyp M A B -> step (\ M) (A => B).

% elimination tactics
byfalseE : j0hyp M false -> step (abort M) A.
by&EL    : j0hyp M (A & B) -> step (fst M) A.
by&ER    : j0hyp M (A & B) -> step (snd M) B.
by|E     : j0hyp M (A | B) -> j1hyp N A C 
                           -> j1hyp L B C 
           -> step (case M N L) C.
by=>E    : j0hyp M (A => C) -> j0hyp N A -> step (M  N) C.

The checking of annotated proofs requires two judgments `avalid1' and `avalid2': The first returns a proof term and the second the proven proposition.

 
% Annotated proofs
aproof : type. %name aproof P.

afinal : term -> prop -> aproof.                       % P ::= M : A
aline  : term -> prop -> aproof -> aproof.             %     | M : A; P
aframe : prop -> (term -> aproof) -> aproof -> aproof. %     | [x: H; P]; P'

% Annotated proof checking
avalid1 : aproof -> term -> type. % %mode avalid1 +P -M.
avalid2 : aproof -> prop -> type. % %mode avalid2 +P -A.

avfinal1 : step M A -> avalid1 (afinal M A) M.
avfinal2 : step M A -> avalid2 (afinal M A) A.
avline1  : step M A -> (j0hyp M A -> avalid1 P N) -> 
              avalid1 (aline M A P) N.
avline2  : step M A -> (j0hyp M A -> avalid2 P B) -> 
              avalid2 (aline M A P) B.
avframe1 : ({x:term} j0hyp x H -> avalid1 (P x) (M x)) ->
          ({x:term} j0hyp x H -> avalid2 (P x) A) ->
          (j1hyp M H A -> avalid1 Q N) -> avalid1 (aframe H P Q) N.
avframe2 : ({x:term} j0hyp x H -> avalid1 (P x) (M x)) -> 
          ({x:term} j0hyp x H -> avalid2 (P x) A) ->
          (j1hyp M H A -> avalid2 Q B) -> avalid2 (aframe H P Q) B.


[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

This document was generated by Andreas Abel on October, 24 2002 using texi2html