A. Reference

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

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

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

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

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

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.

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.

val nth : nat -> tau list -> tau -> tau = ...

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

proof refl : !x:nat. (x = x) = ...

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.

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.

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

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

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.

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.