[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
This part is meant as a brief, but complete reference to Tutch.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
The proof checker Tutch is invoked by
$ /afs/andrew/course/15/317/bin/tutch [options] [files] |
Assignments submission is possible via
$ /afs/andrew/course/15/317/bin/submit -r file [options] [files] |
$ /afs/andrew/course/15/317/bin/status file |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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
( ) [ ] ; : = ~ & | => <=> |
T F proof begin end |
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 |
~ & | => <=> |
H ::= A % Hypothesis E ::= A % Line | [ H; P ] % Frame P ::= E % Final step | E; P % Step and remaining proof |
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] | [ ? ] |
We extend our list of special symbols and reserved words by the following:
, annotated term fst snd inl inr case of fn abort |
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) |
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] | [ ? ] |
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 |
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] | [ ? ] |
Reasoning in First-Order Logic (FOL) requires handling of universally and existentially quantified propositions. New special symbols are
! ? . |
A, B ::= ... | R M1...Mn % Instantiation | !x:T. A % Universal quantification | ?x:T. A % Existential quantification |
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 |
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 |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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 |
Unfortunately, `=' introduces a ambiguity into our syntax, e.g. in
proof Ex2 : !x:nat. 0 < x => ?y:nat. s(y) = x = ... |
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 = ... |
Not correctly resolved is the ambiguity in this case:
proof refl : !x:nat. x = x = ... |
Category mismatch: x is a variable, but a proposition is expected in this placeTo work around this bug, insert parentheses somewhere around the equality expression, e.g.
proof refl : !x:nat. (x = x) = ... |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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 |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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 |
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] | [ ? ] |
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 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] | [ ? ] |
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] | [ ? ] |
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] | [ ? ] |