Tutorial
From Automated Assistance for Formal Reasoning
We present the top-level syntax through examples. It consists of several key English phrases, a small subset of LaTeX syntax, and only a few markers designed specifically to direct the system.
Contents |
Verified text
Any results that the user intends to verify should be surrounded by \vbeg and \vend markers:
\vbeg ... \vend
The verifier's preprocessor will simply ignore all text that does not appear between a pair of markers \vbeg and \vend.
Statements
A verifiable text consists of a sequence of statements, each of which is either an assumption, an assertion, or an introduction of one or more variables. A statement is only visible to statements that occur below it.
Assumptions
An assumption begins with the keyword(s) Assume or Assume that, and is followed by a logical phrase or mathematical expression.
Assume for any $x \in \Z$, $x \cdot x \geq 0$.
The verifier will introduce the expression as an axiom into the context. The axiom will be visible to every assertion that appears below the assumption, unless the assumption is hidden because one of the variables found in the body of the assumption is reintroduced.
Assertions
Syntactically, an assertion is denoted just like an assumption, except that it begins with the Assert or Assert that keyword(s). When the verifier attempts to verify the logical phrase or mathematical expression, it will do so under a context in which all assumptions and verified assertions appearing above it are assumed to be true.
Assert $-1 \cdot -1 \geq 0$.
Variable introduction
Variables (or identifiers) must begin with either a lower- or upper-case letter or a backslash, and must contain only letters (lower- or upper-case), numbers, and apostrophes. They cannot be the same as one of the built-in operators (such as \R) or reserved markers (such as \vend or \p).
Before a variable can be used without quantification in a logical phrase or mathematical expression, it must be introduced. It is sufficient to give only the name of the variable upon its introduction. The variable can then be used in any assumptions and assertions appearing below the variable introduction, up to the next introduction of the same variable.
Introduce $x,y,z$. Introduce $v,v'$. Introduce $var, foo, bar$.
If the same variable is introduced a second time, all assertions and assumptions in the bodies of which the variable appears will become invisible below the second introduction. This also holds for any subexpressions and subphrases which introduce quantified variables, as will be discussed below.
Logical phrases
Base Cases
The most basic logical phrase is a mathematical phrase (as covered in the section below) surrounded by $ ... $:
Assume $1 > 0$.
It is also possible to define an ad hoc predicate using a string of words and mathematical phrases in any order prefixed by a \p marker. The rules governing which words are allowed in ad hoc predicates are the same as those for identifiers:
Assume \p{the number $4$ is divisible by $2$}.
Assume \p{$1/2$ is rational}.
Assume \p{the fox is hungry}.
Conjunction and Implication
Specific English words and constructions can be used to represent logical conjunction, implication, and quantification. It is possible to represent conjunction by separating phrases with a comma (,) or and:
Assume $1 > 0$, $2 > 1$, $3 > 2$. Assume $1 > 0$ and $2 > 1$.
Implication can be represented using one of three phrasings:
Assume $1 > 0$ implies $2 > 1$. Assume $1 > 0$ implies that $2 > 1$. Assume if $1 > 0$ then $2 > 1$.
It is possible to use iff as shorthand for implication in both directions:
Assume $x > 0$ iff $0 < x$.
Quantification
Univerally quantified variables can be introduced using for all $ ... $, or for any $ ... $,. The $ ... $ must contain a list of identifiers, and each identifier may be associated with some set using the infix \in operator.
Assume for all $x$, \p{$x$ is an expression}.
Assume for any $x,y$, \p{$y$ and $x$ are not necessarily equal}.
Assume for all $x \in \N$, $x \cdot 1 = x$.
Assume for all $x \in \Z, y \in \R$, $x^y \in \R$.
If there is a sequence of variables not followed by any such associations, then the first association encountered will apply to the entire sequence. Below, both x and y belong to \N.
Assume for all $z \in \N, x,y \in \N$, $x \cdot (y + z) = x \cdot y + x \cdot z$.
Existential quantification works in exactly the same manner, except the phrases there exist $ ... $ s.t.,, there exist $ ... $ such that,, etc. must be used.
Assume there exists $x \in \R$ s.t. $x = 2$. Assume there exists $x \in \R$ such that $x = 2$. Assume there exist $x,y \in \R$ s.t. $x/y = 1$. Assume there exist $x,y \in \R$ such that $x/y = 1$.
Nested Phrases and Phrase Association
Obviously, all of the above constructions are recursive, and any base case can be replaced with an entire logical phrase. In order to disambiguate complex phrases, it is possible to wrap phrases using single braces { ... }, which work just like parentheses. They are not visible in the text generated for human consumption.
Assume for any $x,y \in \N$,
{if $x > 0$ then $y/x \in \Q$},
{if $x = 0$, then \p{$y/x$ is undefined}.
The scope of implications and quantified variables extends until the next balanced closing brace, or until the end of the statement.
Mathematical Expressions
Mathematical expressions are wrapped using $ ... $.
