This part is meant as a brief, but complete reference to Tutch.
The proof checker Tutch is invoked by
$ /afs/andrew/course/80/317/bin/tutch [options] [files]
The files are extended by `.tut' if they do not have an extension already. Options are:
Assignments submission is possible via
$ /afs/andrew/course/80/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/80/317/bin/status file
This retrieves the status of the submission file handed in via submit -r file ....
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
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
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
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.
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) = ...
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.
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.
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
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
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.
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.
Go to the first, previous, next, last section, table of contents.