Introduction to Lurch

Advanced User's Guide v1.0

This guide provides a detailed overview of the design and theory behind Lurch for advanced users who are interested in writing their own topics or libraries (i.e., collections of rules in a document intended to be used as a dependency) and those who really want to know the nitty-gritty details of the Lurch design.  Most beginners will want to try the Lurch Tutorial instead or try some of the other resources listed at the end of this document. 

If you are reading this document, then you are probably interested enough in Lurch to join our email list.  We are hoping to create an online community of professors interested in this software and using it in their courses. We would love to hear from you and answer any questions or difficulties you come across. The current version of Lurch is a work in progress and is still missing many features (like rendered formatting of complex math expressions). Your feature requests and feedback will help us prioritize future development.  Join our online discussion forum (http://lists.sourceforge.net/lists/listinfo/lurch-discuss).

1. Meaning vs Commentary

Lurch is a mathematical word processor that can check your reasoning.  Like most word processors Lurch can format the text that you type with boldfaceitalics, different font faces and colors. Like most word processors, such text may have meaning to the reader, but its meaning is not understood in any manner by the word processor itself.  Any text that you type and format in your document that is not meaningful to Lurch itself is called commentary (or fluff or flarf).

In order to indicate that a piece of text in your document is not just commentary but something that you would like Lurch to check for you, it has to be marked as being meaningful.  There are currently two ways to do so.

The first is that Lurch automatically infers some meaning for you. For example, it recognizes line numbers in a numbered list as being a label for the first piece of meaningful text that appears after the line number.  It can also infer the existence of subproof contexts when a rule that discharges an assumption is validly used. 

The second (and much more common) way is for you to manually surround a selection of text in a bubble.

2. Categories of Meaning

Lurch has three major categories of bubbles that you can mark a selection with:

     1. Meaningful Expressions (MEs)  (red bubbles)

     2. Properties (blue bubbles)

     3. Contexts (green bubbles)

There is a toolbar for inserting these three bubble categories at the top of the screen.  Here is an example of what each one looks like in the document.

A Meaningful Expression

A Property

A Context

Figure 1: The three categories of meaning

MEs represent mathematical objects like numbers, polynomials, and statements.  Properties specify attributes of MEs but are not themselves mathematical expressions.  Properties do not modify other Properties or Contexts, only MEs.  Contexts limit the scope of declared variables and indicate subproof blocks constructed in the course of writing some kinds of proofs.

Bubbles can sometimes contain other bubbles, but no bubble can overlap with another bubble unless one is contained in the other.  ME bubbles can only contain other ME bubbles.  Properties can contain either exactly one ME bubble or nothing at all.  Contexts can contain any number of MEs, Properties, or other Contexts. 

 Lurch Tip  Bubbles such as those shown in Figure 1 are only visible when your cursor is inside them, hence you can only see the bubbles containing your cursor.  If you would like to see the location of all bubbles in your document, you can use the Meaning>Show markers around bubbles menu item (or press CTRL+1).  This will display an ME bubble in square brackets [ ], a Property in angle brackets like this < ) or this ( >, and a Context in curly brackets { }.  We also extend this notation for use in documentation by writing the contents of the bubble tag after the surrounding brackets separated by a colon. We will also use this notation throughout this help document to be able to talk about bubbles without creating any actual bubbles; there are no actual bubbles anywhere in this particular document. In a document that has bubbles you can use the Meaning>Show tag after bubbles menu item (or press CTRL+2) to see the document in the notation used in this help file.

Thus for example, the three bubbles in Figure 1 would be written as shown in Figure 2. Sometimes the tag information will be omitted for brevity.

[xx>0 ⇒ -x<0]:quantification

(nonnegative>:label

{Proof: Let x be arbitrary. ... }:context

 Figure 2: Text notation used to describe the bubbles in Figure 1. 

An ME which is not contained inside any other ME is called a child of the document.  A Lurch document can be thought of as a sequence of MEs M1, ..., Mn each of which is a child of the document.  Properties assign attributes to these MEs and Contexts group together collections of MEs that have a common purpose or relevance.

We now discuss each of these three categories of bubbles in Lurch in detail.

3. Roles

Within each category, bubbles are further partitioned into roles.  These are so named because they indicate the role that each plays as a meaningful entity in Lurch.  The role of a bubble is always listed on the bubble tag at the top of the bubble, in non-italicized font (except for Ordinary MEs as described below).  Some examples are shown in Figure 3.

     

Figure 3: The role of a bubble is shown on its bubble tag in non-italicized font.

 Lurch Tip  You can use the Meaning>Insert bubble menu to insert a bubble with a specified role.  You can also press CTRL+ENTER to (a) enter a new bubble of a certain role, (b) surround a text selection with a bubble of a certain role, or (c) change the role of the innermost bubble currently containing the cursor.

We now list all of the available roles for each of the three categories.

3.1 ME Roles

Every ME has one of the following roles (highlighted in grey).

  1. MEs that do not list any role on their bubble tag (most MEs are of this type)
    1. Ordinary ME
  2. Declarations
    1. variable declaration 
    2. constant declaration
  3. Rule Definitions
    1. if-then rule
    2. iff rule
  4. Roles that can only occur inside an if-then or iff rule definition
    1. rule premise
    2. rule conclusion
    3. rule condition
  5. Roles that can only occur inside of an if-then rule definition
  1. rule assumption
  2. rule variable declaration
  3. rule constant declaration

Note that the rule roles in 4a-c and 5a-c omit the prefix "rule" from their bubble tag for brevity.  Rule conditions are available but are highly advanced and not supported in this release, so we will not discuss them further in this document. Each of these roles will be explained in detail later.

3.2 Property Roles

Currently every Property in Lurch has one of three roles.

  1. label
  2. reason
  3. premise

An example of the bubble tag of each appears in Figure 3.  Each of these will be explained in detail below.

3.3 Context Roles

Currently every Context in Lurch has one of three roles.

  1. context
  2. subproof context
  3. variable declaration context

All of these will be explained in detail below.  Note for now that subproof contexts and variable declaration contexts are the only two bubble roles that cannot be manually inserted in the document, but rather are created automatically as a result of certain kinds of validation.

4 Syntax

The information that a bubble surrounds is called its content.  Some roles have restrictions on the nature of the content that they can surround, while others have no restriction at all.  For example, a Label can contain anything at all, even spaces and special characters as shown here.

On the other hand, a variable declaration must contain a valid identifier (a sequence of characters from a-z, A-Z, and alphabetical unicode characters) and thus no spaces.  Such restrictions are what defines the syntax of a bubble.  We now discuss the syntax of each of the bubble roles in detail, beginning with the most complicated ones--meaningful expressions.

4.1 Ordinary Meaningful Expressions

Marking text as a meaningful expression (or math expression or expression or ME) indicates that it is a mathematical object like a number or statement or polynomial.  (This corresponds roughly to marking an expression as inline or display math in LaTeX by surrounding it with $ or $$.)

Any piece of text in Lurch can be marked as being a meaningful expression, and meaningful expressions can be nested so that one contains others which in turn contain others and so on. How such expressions are interpreted depends on (a) the text that is marked and (b) the nesting structure of the expression and its subexpressions.  In this manner you can think of Lurch as having two different "languages."  The first is what we might call the Lurch Foundational Language (LFL).  The second is an important convenience feature for inputting very complicated expressions with minimal effort which we can call the Lurch Parser Language (LPL). The LFL is built into Lurch and not easily modified.  Currently the LPL is also hard-wired into Lurch, but that is only temporary.  Eventually we will have the ability for Lurch document authors to customize their own LPL. 

Lurch Foundational Language

Every ME is comprised of the following content types:

     A. Simple MEs

          a. integer

          b. real

          c. variable

          d. constant

          e. rule identifier

          f.  string

          g. operator 

          h. quantifier

     B. Compound MEs

          i. function application (labeled "expression" on its bubble tag)

          j. quantification

Every ME bubble lists its content type in italics on the bubble tag at the top of the bubble. If the bubble tag displays both a role and content type, it will display the role of the ME first in non-italics, followed by the content type in italics.  For example,

has role "premise" and content type "constant."  Note that for technical reasons, the content type of a constant, variable, or rule identifier for which there is a declaration somewhere in the document cannot be determined unless you turn on validation first (which can be done by pressing CTRL+0).  (See §5.1.3.) 

Simple ME is comprised of a single bubble with its contents. 

 Lurch Tip  Thus if you type the number 42 into Lurch, highlight it, and press CTRL+[ it will wrap 42 in a red ME bubble and make it meaningful, and indicate that it is of the atomic ME type integer on the bubble tag, as shown here.

As mentioned earlier, for convenience we will usually indicate this by writing [42]:integer.

Thus we can have simple MEs such as the following.

[42]:integer

     [3.14159]:real

     [x]:variable

     [π]:constant

     ["Life, the Universe and Everything"]:string

     [+]:operator

     []:quantifier

The type of a simple ME is determined by its contents. If it can be interpreted as an integer, then it will be.  If it can be interpreted as a real number, then it will be. If it could be a variable then it will be. If it is on the current list of things assumed to be operators or quantifiers in the LPL, then it is an operator or quantifier. If it is an identifier that occurs inside a rule definition, then it will be a rule identifier. Identifiers are interpreted as a variable unless the user declares them to be a constant explicitly, in which case they are detected as being constants in the scope of that declaration (assuming validation is turned on).  Everything else is interpreted as string.

The current list of operators in Lurch is hard-coded and consists of the 24 symbols on the leftmost panel on the unicode symbol toolbar (plus a few on the keyboard like  *, +, =, and -), and the basic trig, inverse trig, exponential, logarithmic, and calculus operators like int and diff.  This list will be completely customizable when we are able to customize the LPL in a future release of Lurch, but for now it is built-in. 

Compound ME is obtained by nesting simple MEs. There are two content types for a compound ME: expression and quantification. The nested ME

[ [f] [x1... [xn] ]:expression

is interpreted as the ordinary math expression 

f(x1,...,xn)

i.e., it can be thought of as a function application of the first child ME applied to the remaining child MEs.  The child MEs, [f], [x1], ... ,[xn] of the expression don't have to be simple.  

 Lurch Tip  If you want to type, say, 3⋅f(x+1) in LFL you could enter the ME

[ [] [3] [ [f] [ [+] [x] [1] ] ] ]

Yes, that is a mess!  But the LFL is simple, not convenient.  For convenience we will use the LPL, as shown below.

The only other type of compound ME is a quantification, which is an LFL ME of the following form.

[ [q]:quantifier [x]:variable [M]:anyME ]:quantification

In this situation we say that the quantifier [qbinds the variable [x].

 Lurch Tip  An example of this is the ME ∀x,x+1>1 which can be described in LFL as follows.

[ [] [x] [ [>] [ [+] [x] [1] ] [1] ] ]

(Again this is messy, but it is for simplicity, not convenience.)

Currently there are only four quantifiers built into Lurch: for all (∀), there exists (∃), there exists unique (∃!), and set builder (SetBuilder).  (In future releases of Lurch when we can customize the LPL we will be able to add or subtract elements from this list.)

That is the entire Lurch Foundational Language: just nested bubbles, all of which are auto-detected for meaning by their contents except for constants, which must be explicitly declared (with validation enabled).

However, as you can see by the examples above, entering LFL compound expressions can be extremely tedious and time consuming and the results are difficult to read compared to standard mathematical notation.  To make our lives easier for this purpose we need the LPL.

Lurch Parser Language

The contents of every simple ME bubble are first checked to see if they can be understood by the currently hard-coded, built-in parser.  If they can, then that ME bubble is treated as a (possibly complicated) LFL ME determined by the parsing, while still appearing as a single un-nested ME bubble in the document.  This allows a compound ME to be entered with the same ease as a simple ME and usually produces more legible results.

 Lurch Tip  For example, above we said that to enter 3⋅f(x+1) in LFL you would enter the ME

[ [] [3] [ [f] [ [+] [x] [1] ] ] ]

but using the LPL you can enter it in a single bubble, like this.

3⋅f(x+1) ]

This latter ME has the same meaning as the fully "expanded" version above.  

In fact, you can expand and collapse MEs between these two forms whenever possible.  Thus in the previous example, if you expand the latter form (LPL) you will get the former form (LFL) and if you collapse that former form you will return to the latter one. Keep in mind, however, that the LPL is only a convenience feature that allows us to enter complicated compound MEs easily, but that in every case the actual Lurch meaning of an ME is its expanded form.  Thus for example, if we say that the ME 3⋅f(x+1) ] in the previous example contains the ME [x], we are referring to its expanded form.  

 Lurch Tip  To expand or collapse a compound ME bubble, right click on the bubble with your mouse and choose "expand" or "collapse" from the context menu that appears.

So what syntax does the parser recognize?  Keep in mind that the current hard-coded LPL will eventually be replaced with the capability to create custom languages to suit the needs of a particular course or topic.  So in the long run the answer to the question will be, "Whatever syntax you want."  Whatever syntax or notation will be convenient for a particular course or topic, the author will be able to make a custom parser specifically to understand that notation.

In the meantime, we have a LPL that just uses fairly common mathematical syntax that you would find used in other programs like Maple or a spreadsheet or a calculator.  Here are some example expressions the parser currently understands.

x^2−1 = (x−1)⋅(x+1)

3^2 > 2^3

∀x, x∈A∩B ⇔ x∈A and x∈B

{x : x∉x}

You type expressions more or less the way you think they ought to look, except that exponentiation is ^, and multiplication must use * or ⋅ instead of concatenation.

 Lurch Tip  The arithmetic operators +, *, ^, / and - can be entered directly from the keyboard.  To produce the symbol ⋅ you can type \cdot followed by the space bar.  There is also a longer minus sign that can be entered by typing \minus followed by the space bar.  Both minus signs - and − represent the same operator, as do * and ⋅.

In this version of Lurch we do not have full mathematical typesetting capabilities implemented, but later versions will include them.  In particular, superscripts, subscripts and fractions render all in one horizontal line as illustrated above with things like x^2.  Thus most of our initial built-in libraries focus on topics that do not involve a lot of complex mathematical notation.  Topics like logic, set theory, and number theory don't really need much more than plain text notation in a single line, plus a healthy supply of Unicode math symbols, so we have focused on such topics for now.  We save topics like calculus and algebra for later, after full mathematical typesetting capability is added to the program.

Replacement Patterns

The LPL also recognizes replacement patterns [x=y] and [x~y] which are useful only for specifying certain rule definitions (note that the brackets [] are actual typed brackets from the keyboard, not the red notational brackets [] that we use to describe meaningful expression bubbles in this documentation).  The expression P[x=y] is interpreted as "the expression with all free occurrences of replaced by y," while P[x~y] is interpreted as "the expression with some free occurrences of replaced by y." (See §5.1.2 for the distinction between free and bound occurrences.)  A rule premise or conclusion in a rule definition of the form [P[x=y]] will match an expression P with all free occurrences of replaced by y (and similarly for [P[x~y]]).  (See §5.1.3 for a description of matching premises in rule definitions.)

Example 1. The expression b>] matches  [ (a>a)[a=b]  and [ (a>a)[a~b], while [ a>b ] matches [ (a>a)[a~bbut not [ (a>a)[a=b]  

4.2 Properties

The second major bubble category is Properties. Properties are not meaningful expressions in their own right, but are instead used to assign attributes to a meaningful expression.  Each Property bubble has a numbered  arrow on its tag that points in the direction of the ME that it modifies.  The number indicates how many consecutive MEs in the direction of that arrow have the given property.  (When the number is 1 it is omitted.)  For example, the ←2 at the top of the following Property bubble indicates that the previous two MEs have the property that their label is "Eq 1.1."

On the other hand, the following label Property bubble indicates that only the next ME after it in the document will have the label "Eq 1.2."

Keep in mind that Properties only affect MEs, not other Property or Context bubbles.  In this documentation we would denote these two Properties as <2Eq 1.1):label and (Eq 1.2>:label, respectively where < and > indicate the direction of the bubble tag arrow.

 Lurch Tip  To change the direction of the arrow on a Property bubble, left-click and right-click on the arrow in the bubble tag with your mouse.

The syntax for all properties is quite simple. Label and reason properties must be simple bubbles; they cannot contain another bubble inside them.  A premise Property can also be simple, or it can contain exactly one ME bubble.  Simple properties can contain any sequence of characters whatsoever. A premise Property containing an ME can contain any ME role and content type except a rule definition.

4.3 Contexts

Context bubbles come in two flavors: those entered manually by the user, and those inferred and created automatically.  The purpose of the former is to delimit the scope of variables and constants (§5.1.2) to within the Context bubble.  For example, if you have several homework problems or proofs in the same document that all refer to the variable x, you can wrap each in its own Context, and thus each will have its own separate scope, without one instance of the variable conflicting with another in a different problem.  Lurch will also automatically infer and create subproof contexts/variable declaration contexts (§5.1.3) in a proof and mark them as such.

4.4 Variable and Constant Declarations

Variable and constant declarations can only appear as a child ME of the document, not inside any other ME. Their contents must be a single identifier, which must be a string of one or more characters from a-z, A-Z, and the alphabetical unicode characters (no spaces, numbers, or punctuation).

How Declarations function is explained in §5.1.2.

4.5 Rule Definitions

rule definition ME is either an If-then rule or an Iff rule.

An If-then rule is an ME having one of the following forms:

  1. [ [P1]:premise ... [Pm]:premise [C1]:conclusion ... [Cn]:conclusion ]:If-then
  2. [ [A]:assumption [P1]:premise ... [Pm]:premise [C1]:conclusion ... [Cn]:conclusion ]:If-then
  3. [ [V]:variable declaration [P1]:premise ... [Pm]:premise [C1]:conclusion ... [Cn]:conclusion ]:If-then
  4. [ [P1]:premise ... [Pm]:premise [C]:constant declaration [C1]:conclusion ... [Cn]:conclusion ]:If-then

where m≥0 and n≥1 (i.e. premises are optional, but conclusions are not). Additionally, any one of these four can contain a rule condition, but we will not discuss this in this document.

In particular, a rule definition can contain at most one assumption, variable declarations, or constant declaration in addition to its premises and conclusions.

Any If-then rule having form 1 on the list above can be converted into an iff rule. Such a rule defines two If-then rules, the original one shown and another one obtained by interchanging the roles of the premises and conclusions.

The order that the premises and conclusions appear inside a rule definition does not matter.  Permuting the premises and conclusions will result in an equivalent rule.

 Lurch Tip  Suppose we want to make a rule for the definition of automorphism.  We might say something like

[ [ f∈Hom(A,A) ]:premise if and only if [ x,∀y,f(xy)=f(x)⋅f(y]:conclusion ]:Iff

and label it as the definition of automorphism with this label Property.

<automorphism):label

5. Validation

The main reason to mark anything as meaningful in Lurch is to give it the capability of validating the mathematical steps of your proofs or computations. The way that this is accomplished is conceptually quite simple.

First the user or instructor defines rules and names them by assigning a label Property to them.  Such rules may be definitions, axioms, or theorems that the user would like to use to justify their work (or, in the case of an instructor, to allow their students to use to justify their work).

Any such document can be used as a dependency of another Lurch document, so that the rules it defines are immediately available for use without reentering them.

Once a set of rules is defined, the user can then use those rules to justify an ME by assigning that ME a reason Property whose value is the name of a labeled rule definition. We now discuss the details of this.

 Lurch Tip  In order to have Lurch check your work you have to turn on validation by choosing Meaning>Show validation results from the menu (or by pressing CTRL+0). Lurch gives you feedback in several ways, but the the most important one is that it will place a green, red, or yellow validation icon (, or ) after certain MEs (they appear just inside the right side of the ME's bubble).  A green icon indicates that the ME is valid (justified), red indicates that something is wrong, and yellow indicates that the ME is used to justify something else in the document but has not been justified itself.  Hovering or double clicking on such an icon with the mouse gives more information about why the ME has the colored icon it does.

Note that validating a large mathematical document can be quite time consuming.  For that reason, if you turn on validation with CTRL+0 it will show the validation icons only until you edit the document.   If you want to lock validation on permanently while you edit, you can do so by choosing Meaning>Update validation while editing from the menu (or pressing CTRL+9).  All validation icons will turn a grey () while it is updating and change colors when it is finished.

5.1 Bubbles that get a validation icon

Property and Context bubbles never receive a validation icon. The following MEs will have a validation icon if validation is turned on.  We summarize their validation criteria here and discuss them in detail in the following sections.

  1. Rule Definitions get a validation icon that indicates if they have the correct syntax, or have incorrectly been assigned a reason.
  2. Declarations (variable or constant) get a validation icon that indicates if the identifier they are trying to declare is not already declared at that point in the document.
  3. MEs that Have a Reason get a validation icon indicating whether that ME is justified by the cited reason, the reason refers to a valid rule, and the necessary premises are available.
  4. MEs Used as a Premise that do not have their own reasons and are not themselves declarations or rule definitions get a yellow validation icon that indicates that they are being used as assumptions.

We now describe the validation of each of these four situations in detail.

5.1.1 Rule Definitions

As mentioned above, there are currently two kinds of rule definitions in Lurch.  Each has its own specific syntax.

An if-then rule definition will get a green validation icon () if the following conditions are met.

An iff rule definition will get a green validation icon () if the following conditions are met.

If any of these conditions are not satisfied, the validation icon for the rule will be red () and double clicking or hovering over it with the mouse will give a message indicating which of the conditions was not met, and how you might go about fixing it.

5.1.2 Declarations

Variable declarations and Constant declarations also automatically get a validation icon when validation is turned on.  In order to understand the validation of declarations we have to first understand the concept of scope.

Identifier Types and their Scopes

An identifier in Lurch is a simple ME whose contents consist of a string of one or more characters from a-zA-Z, and alphabetical unicode characters. An identifier cannot contain a number, space, or punctuation.  There are four types of identifiers in Lurch.

  1. Bound variables - only occur inside a quantification
  2. Constants -  can occur anywhere
  3. Rule identifiers - only occur inside rule definitions
  4. Variables - can occur anywhere except inside a rule definition

At each location in the document, each identifier is considered to be either declared or not declared at that location.  The set of locations where an identifier is considered to be declared is called its scope.  All occurrences of the same identifier in the same scope have the same identifier type. For example all occurrences of the identifier k in the scope of a constant identifier will also be a constant.  The scope for each of the four types of identifiers is defined as follows.

The scope of a bound variable consists of the interior of the entire quantification expression that binds it.   

The scope of a constant begins at a constant declaration and continues from that point forward until the end of the innermost Context containing the declaration (if there is one, otherwise it continues indefinitely). Note that the scope of constant can extend beyond the end of the document in the case where a document containing a declaration is used as a dependency (§6.1).  This allows a topic or library author to define constants in their documents that are used in rules and definitions for that topic o library.

The scope of a rule identifier consists of the interior of the entire rule definition that contains it. In particular, every identifier that appears inside a rule definition is a rule identifier with one exception:  If the rule definition is in the scope of a constant declaration then all occurrences of an identifier with the same name as the constant inside the rule definition represent the externally defined constant itself.  Note that all instances of the same identifier (that do not represent an externally defined constant) inside a rule definition represent the same rule identifier.  For example, in the rule

[ [AB]:premise [x,xAxB]:conclusion ]:iff

the occurrences of the identifier x in the conclusion are all rule identifiers, not bound variables.

The scope of a variable begins either at a variable declaration or the first occurrence of that identifier as a free (i.e. not bound) variable in an ME other than a rule definition (that is not itself in the scope of that variable) and continues from that point forward until the end of the innermost Context containing the declaration (if there is one, or the end of the document containing the variable declaration if there is no Context containing it).  Thus, unlike constant declarations the scope of a variable cannot extend beyond the end of the document in the case where a document containing a declaration is used as a dependency (§6.1), and it can be declared implicitly by simply using it in an expression.

Precedence of Scopes

It is often the case that several possible scopes for the same identifier may overlap.  In such situations, there is a tiebreaker mechanism that determines which type of identifier it is, and what other identifiers it is equivalent to in each situation.

If a constant or variable declaration appears in the scope of a previous constant or variable declaration of the same identifier, the original declaration holds, and the new attempt at declaring the same identifier is invalid.

If a rule definition is in the scope of a constant declaration, the constant declaration has precedence and all occurrences of that identifier inside the rule definition represent that constant; they are not rule identifiers.

If a rule definition is in the scope of a variable declaration (either explicit or implicit), all occurrences of that identifier inside the rule definition are interpreted as rule identifiers, not the variable.

If a rule definition contains a quantification, the identifier that appears after the quantifier (in expanded form) is interpreted as a rule identifier, not a bound variable.

Finally, if a quantification is in the scope of a constant or variable definition (and not inside a rule definition), the identifier that appears after the quantifier (in expanded form) is interpreted as a bound variable, not a constant or free variable.

Note that in every case, these somewhat technical-sounding conventions imitate what is normally done when interpreting everyday mathematics.

Validation 

Assuming validation is turned on, a validation icon will always appear next to a variable or constant declaration with its color determined as follows.

constant declaration or variable declaration will get a green validation icon () if the following conditions are met.

If either of these conditions are not satisfied, the validation icon for the rule will be red () and double clicking or hovering over it with the mouse will give a message indicating which of the conditions was not met, and how you might go about fixing it.

A variable that is implicitly declared by virtue of appearing free in an ME does not get a validation icon for being a declaration, although that ME may get a validation icon for some other reason.

5.1.3 MEs Having a Reason

By far the main purpose of Lurch itself is to check the user's work whenever he justifies a statement or step of his computation with a reason.  So it is not surprising that the validation for MEs having a reason is the most sophisticated of all of the forms of validation.

Rules must be labeled, valid, and accessible

We can use the label Property to name rule definitions.  The rule identifiers in a rule definition act as meta-variables which can be replaced by or instantiated with any other ME as long as all rule identifiers that have the same name are instantiated with the same thing.  This replacement is done in the rule assumptions, rule premises, rule conclusions, and rule declarations that appear in the rule definition to produce a sequence of corresponding MEs called a particular instance of that rule.

Example 2: Consider the simple rule 

[ [A and B]:premise [A]:conclusion ]:if-then

Then 

[x>0 and y≥0][x>0] 

is an instance of that rule with A instantiated with "x>0" and B instantiated with "y≥0." On the other hand,  

[x>0 and y≥0][z=1]

is not an instance of the rule because the two different occurrences of A have been instantiated with two different MEs.

Rule definitions have their own scope.  At each location in the document, each rule is either defined or not defined at that location.  As with declarations, the set of locations where they are defined is called their scope. The scope of a rule definition begins at the definition itself and continues from that point forward until the end of the innermost Context containing the definition (if there is one, otherwise it continues indefinitely). Note that like constant declarations, the scope of rule definition can extend beyond the end of the document in the case where a document containing the rule definition is used as a dependency (§6.1).  This allows a topic or library author to define collections of related rules in a saved document that is available for users of that topic or library.

When a reason is assigned to an ME, it must contain the name of a valid labeled rule definition whose scope contains the ME.  In this situation we say that the rule definition is accessible to the ME.  In order for a rule to be able to justify an ME, it must be labeled, valid (have a green icon () ), and be accessible.

Matching a Conclusion

In order for a rule definition cited by a reason to justify an ME, there must be an instance of that rule definition for which some instantiated rule conclusion matches the ME being justified.  For that same instance, each instantiated premise and each instantiated rule assumption that is present in the instance must match some appropriate ME in the document, and each instantiated rule declaration must match a declaration of the same type in the document.

Just like rule definitions, MEs in the document have their own scope.  At each location in the document, each ME is either accessible or not accessible at that location.  As with rule definitions, the set of locations where they are accessible is called their scope. The scope of an ME begins at the ME itself and continues from that point forward until the end of the innermost Context containing the ME or the end of the document, whichever comes first.  Any ME that is referenced as a premise must be accessible at the location of the ME being justified.

For both efficiency and pedagogical reasons, the premises (and assumptions and declarations) must be cited explicitly by assigning one premise Property to the ME being justified for each required premise, unless it is cited automatically by one of the labor-saving shortcuts described in the next section. 

Citing Premises

In order to cite a premise we assign a premise Property to the ME that is being justified.  As with the reason Property, a premise bubble can contain the name of a labeled ME that it references.  So one way to specify a premise is to label the ME in the document that is to be used and use its label when citing it as a premise.

But a mathematical proof may have many statements that need to be used as premises, and it can become impractical to have to label all of the MEs in the proof.  In order to ease this burden Lurch provides three convenience features that minimize the amount of labeling and citing of premises that needs to be done.

First, the first meaningful expression on each line in a numbered list is automatically labeled with the number of that line.  (To insert a numbered list, use the  icon on the Editing Tools toolbar.)  This can be useful for semi-formal or formal line-numbered proofs where each line has one statement, reason, and optional premises.

Example 3:  Suppose we labeled the simple rule from Example 2 above. 

(**>:label     [ [A and B]:premise [A]:conclusion ]:if-then

Then the following would be a valid justification using this rule

          Suppose [x>0 and y≥0] which we will label <1):label.  

          Then [x>0 ] by rule <**):reason with the premise named <1):premise.

But if we use a numbered list we do not need to label the first ME by hand because the ME is automatically labeled with its line number.

          1.  Suppose [x>0 and y≥0].  

          2.  Then [x>0 ] by rule <**):reason with the premise on line <1):premise

The second convenience feature is that you can always refer to a premise by putting an identical copy of the ME it refers to inside the premise bubble (as an ME). This is called referencing the ME by restatement. In other words, every ME (other than a rule definition) can be thought of as labeling itself.

Example 4: Using this convenience we could redo the mini-proof in Example 3, this time without any labels or line numbers, simply by restating the original ME inside the premise.

Suppose [x>0 and y≥0]. Then [x>0 ] by rule <**):reason since we assumed <[x>0 and y≥0]):premise.

This lends itself well to traditional proof styles written in paragraph form as opposed to line numbered proofs.

The third and final convenience feature to minimize both labeling and referencing premises uses the observation that quite frequently the premises needed to justify an ME are among the MEs immediately preceding it.  To make use of this fact, if a rule requires n premises, and you cite k≤n premises when justifying a particular ME, the n−k MEs immediately preceding the ME being justified that are accessible at that point, the appropriate role, and are automatically assumed to be cited as premises.

Example 5: Using this convenience we could restate the mini-proof in Example 4 without any labels, line numbers or even citing any premises as follows.

Suppose [x>0 and y≥0]. Then [x>0 ] by rule <**):reason.

This works because the one required premise is the ME immediately preceding the one being justified (that is accessible).

This third convenience feature has some special behavior in certain situations when the rule being cited contains a declaration.  

If the cited rule contains a rule variable declaration among its k premises, and a variable declaration is not among the k cited premises, then the variable declaration will be assumed to be the most recent variable declaration that is accessible at that point, and the remaining nk−1 premises are automatically assumed to be cited among the nk−1 MEs immediately preceding and accessible at that point which are not declarations or rule definitions.  Only a variable declaration ME can match a rule variable declaration premise.

If the cited rule contains a rule constant declaration among its k premises, the constant declaration must immediately precede the ME being justified. The remaining nk−1 premises are automatically assumed to be cited as premises among the nk−1 MEs immediately preceding and accessible at that point which are not declarations or rule definitions.

Assumptions, Subproof Contexts, Variable Declaration Contexts

When a rule definition contains an assumption (resp. a rule variable declaration) and is used to justify an ME that is valid according to the rule, it defines a special kind of Context called a subproof context (resp. a variable declaration context) in the document which begins at the premise that matches the assumption (resp. the variable declaration) and ends just before the ME being justified.  Such Contexts limit the scopes of declarations, rule definitions and MEs used as premises just like a manually inserted Context would.  Since Contexts cannot overlap unless one completely contains the other, if the formation of a subproof Context would overlap another Context only in part, the justification of that ME will be invalid, and thus a subproof context (or variable declaration context) is not formed.

Note that this is the technical reason we said in §4.1 that the bubble tag of an identifier cannot indicate if it is a variable or a constant unless validation is turned on.  Unless validation is turned on, subproof contexts and variable declarations are not created and thus it is not possible determine which constant declaration scopes will be restricted by them as a result. 

Summary

If validation is turned on, any ME that has a reason Property assigned to it will get a validation icon.  That icon will be green () if the following conditions are met.

If any of these conditions are not satisfied, the validation icon for the rule will be red () and double clicking or hovering over it with the mouse will give a message indicating which of the conditions was not met, and how you might go about fixing it.

5.1.4 MEs Used as a Premise

An ordinary ME that is used as a premise to justify a valid ME (one with a green validation icon ()) but is not justified with a reason itself will get a will get a yellow validation icon () indicating it is an undischarged premise, unless it is used as a premise to match a rule assumption, in which case it will get a green validation icon ().  Generally speaking the yellow validation icons in a proof indicate the claims that have not been justified.  This may be exactly what is expected, e.g. when the ME is given in the statement of a theorem being proved, or it may indicate that further work is needed to complete the proof if the ME marked yellow was not a "given."

Premises that match rule assumptions are temporary assertions that are discharged by the construction of the subproof context.  Thus even though they need not be justified by a reason, they are marked with a green validation icon indicating that they are not an undischarged assumption that requires further work.

In all situations, double clicking or hovering over a validation icon with the mouse will give a message indicating the reason for the yellow or green icon. In no situation can an ordinary ME that does not have a reason assigned to it get a red validation icon (). 

6 Dependencies and Topics

A typical workflow in Lurch is as follows.

  1. The instructor writes the definitions, axioms, and theorems that he or she wants available to the students as Lurch rule definitions in a Lurch document (perhaps including corresponding lecture notes in the same document) and assigns some homework related problems.
  2. The students use those rules to prove the theorems assigned for homework, obtaining validation feedback along the way.
  3. Advanced students may further label and bubble theorems they prove as new rule definitions, so that they can use them in further proofs on the same assignment.

In order to make this process more convenient, it would be nice if the list of rules that the instructor provides does not have to be in the same document as the students' assignments.  To enable this, Lurch provides two mechanisms: dependencies and Topics.

6.1 Dependencies

When a document is added as a dependency to the current document, all rule definitions, constant declarations, and formatting styles defined in the dependency become available in the current document as if they were contained in the document itself at the top of the document. 

Lurch has search paths that can be viewed and modified via the File>Preferences>Search Paths Lurch menu item. Any Lurch file saved in one of the search paths will appear on the list of files that appears when you choosing File>Open by Title... or File>Document Properties>Dependencies>+ from the Lurch menu.  The document title can be set in the File>Document Properties dialog before saving the file.  Any file saved in the search paths can then be added as a dependency to the current document by choosing the  File>Document Properties>Dependencies>+ Lurch menu item.

 Lurch Tip  You can use the Meaning>List all defined rules menu (or press CTRL+SHIFT+R) to view a list of all of the currently defined rules in the document and their labels.  This can be very helpful to lookup the name or syntax of a particular definition or theorem you would like to use when doing a proof.

Thus a student can start with a blank document, add to it a dependency produced by the instructor containing all of the rules needed for her homework assignment and type her exercises and proofs.

6.2 Topics

To make things even more convenient, the instructor can save a particular document as a Lurch Topic by choosing File>Document Properties>Attributes, having checked the Mark this document as a topic checkbox before saving.  The Topic author can also optionally include a help file to go along with the Topic, which can have instructions or other information relevant to that Topic that will be presented to the user whenever they open a new document that was written using that Topic.

In addition to being useful for distributing homework assignments, Lurch Topics are also designed to contain entire the definitions, axioms, or theorems for entire subject areas or branches of mathematics.  Lurch comes with several Topics on subject areas such as Propositional Logic, Predicate Logic, Elementary Set Theory, Functions and more.  Many more Topics are planned for the future.  Instructors who write their own interesting Topics are invited and encouraged to share them with others and submit them for consideration to be shipped with future releases of Lurch.  See the next section for how to contact the authors and get involved with the project.

7. Further Information

This document is intended for advanced mathematically sophisticated users who want to understand the theoretical aspects of how Lurch validates mathematical proofs and calculations.  There are many aspects of Lurch that have not been covered in this !document.  For further information you may find the following resources to be helpful.

◈◈◈◈◈◈◈◈◈◈◈◈

Lurch V0.75 - June 2012

by Nathan Carter and Ken Monks

Lurch is Open Source software distributed under the GPLv3 license

!