new guru features

[Kevin Clancy]

Guru Gang:

As some of you may have noticed, I have added a few new features to the
guru classifier. These features are intended to make guru proofs easier
to read and write. If you have any questions, comments, or criticisms of
these features, please post them to guru gang or send them to me.

Below is a description of each new feature.

ascriptions (Ascription.java)

Ascriptions appear in source as �: C e�, where C is a classifier and e
is an expression. An ascription is classified by C under context G iff e
is classified by C under context G.

Ascriptions can be used to display the formulas proven by various guru
proofs, saving the proof readers the mental bandwidth that would have
been required to deduce said formulas themselves. They can also be used
to ascribe types to terms, as they are typically used for in normal
programming languages.

This nonstandard syntax was proposed by Prof. Stump. We have decided to
use this syntax, which places the classifier before the ascription
target, in order to make the classifier more prominent than the target;
in many cases, an ascription will allow the reader to ignore the target
entirely.

Another reason for placing the classifier before the target is that it
maps more directly to proving process. The first step in writing a proof
tends to be stating the fact which is about to be proven.

- Unnamed lemma set (Context.java, LemmaSet.java)

I have extended the context to include a set of unnamed formulas which
have been proven in the current scope. The proofs of these formulas can
be referenced via formula.

- lemma proof construct (Lemma.java)

I have added a new syntactic construct, called lemma, which is used for
inserting unnamed formulas into the context. This construct appears in
source as �lemma p in b� where p and b are proofs. It classifies as
follows. If p is classified as F under context C and b is classified as
T under context C,F, then �lemma p in b� is classified as T under
context C. Lemma is a proof construct, and therefore it has no
operational semantics.

The syntax �lemma p1 � pn in b� is syntactic sugar for �lemma p1 in
lemma p2 in � lemma pn in b�. This conveniently allows a sequence of
lemmas to be established without requiring too many occurrences of the
�lemma� and �in� keywords.

- lemma mark construct (LemmaMark.java)

A lemma mark, represented using the �##� token in source, is used to
refer to proofs of unnamed lemmas. How do we tell which proof a lemma
mark is referring to? By formula. If a lemma mark occurs as an argument
of an application, the mark then refers to the proof of whichever
formula classifies the formal argument in that position. If a lemma mark
occurs outside an application, its formula must be ascribed.

--------------

I have added a demonstration of these constructs in
tests/lemmas_and_ascriptions.g

For those that don't want to check out guru-lang, here the code
contained in the above file. I suspect that the formatting for this will
get butchered, though.

Include "../guru-lang/lib/bool.g"
Include "../guru-lang/lib/nat.g"
Include "../guru-lang/lib/minus.g"

Define minus_lt_Z : Forall
(a b:nat)(u:{ (lt b a) = tt }).{ (lt Z (minus a b)) = tt }
:=
induction(a: nat) return
Forall(b: nat)(u:{ (lt b a) = tt }).{ (lt Z (minus a b)) = tt }
with
| Z =>
foralli(b:nat)(u:{ (lt b a) = tt }).
contra
trans symm u
trans hypjoin (lt b a) ff by [lt_Z b] a_eq end
clash ff tt

{ (lt Z (minus a b)) = tt }
| S a' =>
foralli(b:nat)(u:{ (lt b a) = tt }).
case b with
| Z =>
hypjoin (lt Z (minus a b)) tt by b_eq a_eq end
| S b' =>
lemma
: { (lt b' a') = tt }
hypjoin (lt b' a') tt by a_eq b_eq [S_lt_S b' a'] u end
in
hypjoin (lt Z (minus a b)) tt by
: { a = (S a') }
a_eq

: { b = (S b') }
b_eq

: { (lt Z (minus a' b')) = tt }
[a_IH a' b' ##]

: { (minus a' b') = (S (minus a' (S b'))) }
[minusS2 a' b' ##]
end
end %b
end. %a

-------------------------

Kevin