Declaring a vocabulary #

A relational vocabulary is always declared the same way: an inductive of relation symbols indexed by arity, a Language whose function symbols are Empty, its IsRelational instance, one abbreviation naming each symbol at its arity, and one predicate reading each symbol off a structure. Only the names and the arities differ.

fo_language takes those and writes the rest:

/-- The relational language of pattern-and-host graphs. -/
fo_language twoGraphs with tg where
  /-- `patV a`: `a` is a vertex of the pattern graph. -/
  patV : 1
  /-- `hostV a`: `a` is a vertex of the host graph. -/
  hostV : 1

declares twoGraphsRel (with DecidableEq), Language.twoGraphs with its IsRelational instance, and the symbols tgPatV and tgHostV. The prefix is the one the library's convention asks for, tg naming the symbols of Language.twoGraphs. The docstring of the command becomes the docstring of the language, and each symbol's becomes that of its constructor and its abbreviation.

A vocabulary lives in namespace FirstOrder.Language, next to Mathlib's, while the predicates reading it off a structure live with the problem, in namespace DescriptiveComplexity. So they are two commands, and fo_predicates Language.twoGraphs tg writes the second half:

def TGPatV {A : Type} [Language.twoGraphs.Structure A] (a₀ : A) : Prop :=
  RelMap tgPatV ![a₀]

one predicate per symbol, named by the prefix in upper case, as the catalog names them throughout. It reads the symbols out of the environment, so it takes no list; the vocabulary must have been declared by fo_language, or by hand following the same convention.

The generated declarations are the hand-written ones, so a vocabulary converted to these commands changes nothing that reads it.

source

def DescriptiveComplexity.foSymDecl :

Lean.ParserDescr

One symbol of a vocabulary: patV : 1.

Equations

One or more equations did not get rendered due to their size.

Instances For

Dependency graph

source

def DescriptiveComplexity.foLanguage :

Lean.ParserDescr

Declare a relational language and its symbols; see the module docstring.

Equations

One or more equations did not get rendered due to their size.

Instances For

Dependency graph

source

def DescriptiveComplexity.foPredicates :

Lean.ParserDescr

Declare the predicates reading a vocabulary's symbols off a structure; see the module docstring.

Equations

One or more equations did not get rendered due to their size.

Instances For

Dependency graph

source

def DescriptiveComplexity.FOVocabulary.prefixed (p n : Lean.Name) :

Lean.Name

patV under the prefix tg gives tgPatV; under TG, TGPatV.

Equations

DescriptiveComplexity.FOVocabulary.prefixed p n = Lean.Name.mkSimple (p.toString ++ n.toString.capitalize)

Instances For

Dependency graph

source

def DescriptiveComplexity.FOVocabulary.mkDoc (s : String) :

Lean.TSyntax `Lean.Parser.Command.docComment

A docstring node carrying the given text, for a declaration the user does not name.

Equations

DescriptiveComplexity.FOVocabulary.mkDoc s = { raw := (Lean.mkNode `Lean.Parser.Command.docComment #[Lean.mkAtom "/--", Lean.mkAtom (s ++ " -/")]).raw }

Instances For

Dependency graph

source

def DescriptiveComplexity.FOVocabulary.docOr (d? : Option Lean.Syntax) (fallback : String) :

Lean.TSyntax `Lean.Parser.Command.docComment

The user's docstring, or a generic one when there is none.

Equations

DescriptiveComplexity.FOVocabulary.docOr (some d) fallback = { raw := d }
DescriptiveComplexity.FOVocabulary.docOr none fallback = DescriptiveComplexity.FOVocabulary.mkDoc fallback

Instances For

Dependency graph

source

def DescriptiveComplexity.FOVocabulary.baseSymbols (relName : Lean.Name) :

Lean.Elab.Command.CommandElabM (Array (Lean.Name × ℕ × Option String))

The constructors of a vocabulary's symbol inductive, each with its arity and its docstring: the full name, so that a caller can look the constructor up, and the short one, which the symbol and predicate names are built from.

Equations