Project

Topics

Namespaces

Public Vars

latte.core

This namespace provides the top-level forms of the LaTTe framework.

*proof-certification-enabled*

dynamic

assume

macro

(assume params & body)

An assume step of the form (assume [x1 T1 x2 T2 ...] <body>).

defaxiom

macro

(defaxiom & args)

Declaration of an axiom of the form:

  (defaxiom <name>
    "<docstring>"
    [[x1 T1] ... [xN TN]] ;; <params>
    <body>)

with the specified name (first argument) an optional docstring (second argument), a vector params of parameters and the axiom body, the axiom statement as a lambda-term (last argument). Each parameter is a pair [x T] with x the parameter name and T its type.

An axiom is accepted without a proof, and should thus be used with extra care. The LaTTe rule of thumb is that theorems should be favored, but axioms are sometimes required (e.g. the law of the excluded middle) or more “reasonable” because of the proof length or complexity. In all cases the introduction of an axiom must be justified with strong (albeit informal) arguments.

defimplicit

macro

(defimplicit & args)

defimplicit*

macro

(defimplicit* & args)

definition

macro

(definition & args)

Defines a mathematical term with the following structure:

(definition <name>
  "<docstring>"
  [[x1 T1] ... [xN TN]] ;; <params>
  <body>)

composed of a name, and optional (but highly recommended) docstring, a vector params of parameters (typed variables) and body (a lambda-term) as definitional content.

An ex-info exception is thrown if the term cannot be defined.

Note that a definition is a def in the Clojure sense, the term is defined in the namespace where the definition form is invoked.

deflemma

macro

(deflemma & args)

Declaration of a lemma, i.e. an auxiliary theorem. In LaTTe a lemma is private. To export a theorem the defthm form must be used instead. Otherwise the two forms are the same.

defnotation

macro

(defnotation & args)

Defines a new notation, which is a function called at parsing time. The result must be pair [status u] with status either :ok (parsing successful) with u the term generated by the notation, or :ko (parsing failed) and u is the error, a map with at least a key :msg explaining the failure.

Be careful that the parser will be called recursively on the generated term, hence recursive definitions must be handled with great care.

defthm

macro

(defthm & args)

Declaration of a theorem of the following form:

 (defthm <name>
   "<docstring>"
   [[x1 T1] ... [xN TN]] ;; <params>
   <body>)

with the specified name (first argument) an optional docstring (second argument), a vector params of parameters and the theorem proposition as body (last argument). Each parameter is a pair [x T] with x the parameter name and T its type.

A theorem declared must later on be demonstrated using the proof form. As a side effect, the statement of the theorem is recorded in the current namespace (i.e. it is a Clojure def).

example

macro

(example & args)

An example of the form (example T <steps>) is the statement of a proposition, as a type T, as well as a proof.

forall

(forall params body)

The universal quantifier (forall [x A] t) is ∀x:A.t (or Πx:A.t in type theory).

As a syntactic sugar an expression of form (forall [x y z A] t) translates to (forall [x A] (forall [y A] (forall [z A] t)))

have

macro

(have have-name have-type by-kw have-term)

A have step of the form (have <x> T :by e) checks that the term e is of type T. If it is the case, then the fact is recorded as a local definition named <x>. Otherwise an error is signaled. The type T can be replaced by _ in which case is is inferred rather than checked. The name <x> can be replaced by _ in which case no definition is recorded.

lambda

(lambda params body)

The abstraction (lambda [x A] t) is λx:A.t.

As a syntactic sugar an expression of form (lambda [x y z A] t) translates to (lambda [x A] (lambda [y A] (lambda [z A] t)))

pose

macro

(pose pose-name pose-kw pose-term)

A local definition (pose P := e) allows a proof to refer to term e under the name P in a proof. This is equivalent to (have P _ :by e) (with the type of e inferred).

proof

(proof thm-name & steps)

Provides a proof of theorem named thm-name using the given proof steps.

qed

macro

(qed qed-term)

A Qed step of the form (qed e) checks that the term e allows to finish a proof in the current context. An error is signaled if the proof cannot be concluded.

search-theorem

(search-theorem patt)(search-theorem where patt)

Search a theorem using pattern patt. A pattern (generally quoted) is either: - any clojure value, that has to be matched exactly, with the exception of a symbol starting with a question mark (denoting a variable) - a simple variable ?X that can match anything - a list/sequence of patterns (patt1 patt2 ...) - a zero-or-many variable ?Y* that matches zero or more times greedily - a one-or-many variable ?Z+ that matches at least once greedily - an optional variable ?V? that matches at most once The optional argument where is the name (symbol) of a namespace where the search must be applied (by default, use all registered namespaces)

The special variables ?_, ?_*, ?_+ and ?_? produce no binding when matched.

The result is a vector of matches, each match being a pair [theorem-var match-env] with theorem-var the reference to the theorem as a clojure var, and match-env the variable bindings corresponding to the match.

term

macro

(term & args)

Parse a LaTTe term at the top-level. A context can be provided in the form of a serie of [var type] pairs before the actual term.

term-eq?

macro

(term-eq? & args)

Checks if two terms t and u are equal in the sense of having the “same” normal form (up-to alpha-conversion, the safe renaming of bound variables.

A context can be provided in the form of a serie of [var type] pairs before the actual term.

the-type-of

Replaces the provided term by its inferred type.

try-example

macro

(try-example & args)

This is the same as example but without throwing exceptions.

try-proof

(try-proof thm-name & steps)

Provides a proof of theorem named thm-name using the given proof steps. This version only checks if the proof is correct or not, use the proof function for actually registering the proof.

type-check?

macro

(type-check? & args)

Check if a term t in of the specified type ty. A context can be specified as with type-of.

type-of

macro

(type-of & args)

Give the type of a term t in a context at the top-level. To only parse the term use term.