Ontology

definition theorem
legend

A concept named within an ontology.

structure Concept where
  name : String
deriving Repr, DecidableEq

Outer dependencies: (none)

Lean core dependencies: Eq, Nat, String

Used by: Ontology, Ontology.decidableWellFormed, Ontology.empty, Ontology.empty_wellFormed, Ontology.readFile, Ontology.wellFormed, Relation, componentConcept, instDecodeTomlConcept, resolveRelation, systemConcept

A labelled relation between a source and a target concept.

structure Relation where
  label : String
  source : Concept
  target : Concept
deriving Repr, DecidableEq

Outer dependencies: (none)

Inner dependencies: Concept

Lean core dependencies: Eq, Nat, String

Used by: Ontology, Ontology.decidableWellFormed, Ontology.empty, Ontology.empty_wellFormed, Ontology.readFile, Ontology.wellFormed, partOfRelation, resolveRelation

An ontology maps out a set of concepts and the relations that hold between them.

structure Ontology where
  concepts : List Concept
  relations : List Relation
deriving Repr

Outer dependencies: (none)

Inner dependencies: Concept, Relation

Lean core dependencies: Eq, List, Nat

Used by: Ontology.decidableWellFormed, Ontology.empty, Ontology.readFile, Ontology.wellFormed

An ontology is well-formed when every relation is witnessed by concepts it already contains.

def Ontology.wellFormed (o : Ontology) : Prop :=
  ∀ r ∈ o.relations, r.source ∈ o.concepts ∧ r.target ∈ o.concepts

Outer dependencies: Ontology

Inner dependencies: Concept, Relation

Lean core dependencies: And, List

Used by: Ontology.decidableWellFormed, Ontology.empty_wellFormed, Ontology.readFile

instance Ontology.decidableWellFormed (o : Ontology) : Decidable o.wellFormed :=
  inferInstanceAs (Decidable (∀ r ∈ o.relations, r.source ∈ o.concepts ∧ r.target ∈ o.concepts))

Outer dependencies: Ontology, Ontology.wellFormed

Inner dependencies: Concept, Relation

Lean core dependencies: And, Decidable, List

Used by: Ontology.readFile

The empty ontology witnesses that well-formed ontologies exist.

def Ontology.empty : Ontology where
  concepts := []
  relations := []

Outer dependencies: Ontology

Inner dependencies: Concept, Relation

Used by: Ontology.empty_wellFormed

theorem Ontology.empty_wellFormed : Ontology.empty.wellFormed := by

Dependencies: Ontology.empty, Ontology.wellFormed

Proof dependencies: Concept, Relation

Lean core dependencies: And, Eq, False.elim, HEq, List, List.Mem, noConfusion_of_Nat

Used by: (none)

Dummy concepts, witnessing that concrete concepts can be built.

def componentConcept : Concept := ⟨"component"⟩

Outer dependencies: Concept

Used by: partOfRelation

def systemConcept : Concept := ⟨"system"⟩

Outer dependencies: Concept

Used by: partOfRelation

A dummy relation, witnessing that concrete relations can be built from concepts.

def partOfRelation : Relation := ⟨"part-of", componentConcept, systemConcept⟩

Outer dependencies: Relation

Inner dependencies: componentConcept, systemConcept

Used by: (none)

Reading an ontology from a TOML file

The TOML shape of a relation, naming its endpoints before they are resolved to witnesses.

structure RawRelation where
  label : String
  source : String
  target : String

Outer dependencies: (none)

Lean core dependencies: Eq, Nat, String

Used by: Ontology.readFile, instDecodeTomlRawRelation, resolveRelation

instance : DecodeToml Concept where
  decode v := do
    let t ← v.decodeTable
    let name ← t.decode `name
    pure ⟨name⟩

Outer dependencies: Concept

Lean core dependencies: Array, Lean.Name.mkStr1, String, Unit

Used by: Ontology.readFile

instance : DecodeToml RawRelation where
  decode v := do
    let t ← v.decodeTable
    let label ← t.decode `label
    let source ← t.decode `source
    let target ← t.decode `target
    pure { label, source, target }

Outer dependencies: RawRelation

Lean core dependencies: Array, Lean.Name.mkStr1, String, Unit

Used by: Ontology.readFile

Resolve a raw relation against a list of concepts, requiring a witness for each endpoint.

def resolveRelation (concepts : List Concept) (r : RawRelation) : Except String Relation :=
  match concepts.find? (·.name == r.source), concepts.find? (·.name == r.target) with
  | some s, some t => .ok ⟨r.label, s, t⟩
  | none, _ => .error s!"relation '{r.label}': no witness for concept '{r.source}'"
  | _, none => .error s!"relation '{r.label}': no witness for concept '{r.target}'"

Outer dependencies: Concept, RawRelation, Relation

Lean core dependencies: Except, List, List.find?, Option, String

Used by: Ontology.readFile

Read an ontology from a TOML file shaped like:

concepts = [{ name = "..." }, ...]
relations = [{ label = "...", source = "...", target = "..." }, ...]

and check that it is well-formed, i.e. every relation is witnessed by a declared concept.

def Ontology.readFile (path : System.FilePath) : IO Ontology := do
  let input ← IO.FS.readFile path
  let ictx := Lean.Parser.mkInputContext input path.toString
  match (← loadToml ictx |>.toBaseIO) with
  | .error _ => throw <| IO.userError s!"failed to parse TOML: {path}"
  | .ok table =>
    match EStateM.run (s := (#[] : Array DecodeError))
        (mergeErrors (table.decode `concepts) (table.decode `relations)
          (Prod.mk (α := Array Concept) (β := Array RawRelation))) with
    | .error _ _ => throw <| IO.userError s!"failed to decode ontology: {path}"
    | .ok (concepts, rawRelations) _ =>
      let concepts := concepts.toList
      match rawRelations.toList.mapM (resolveRelation concepts) with
      | .error msg => throw <| IO.userError s!"failed to resolve ontology in {path}: {msg}"
      | .ok relations =>
        let o : Ontology := { concepts, relations }
        if h : o.wellFormed then
          pure o
        else
          throw <| IO.userError s!"ontology in {path} is not well-formed"

Outer dependencies: Ontology

Inner dependencies: Concept, Ontology.decidableWellFormed, Ontology.wellFormed, RawRelation, Relation, instDecodeTomlConcept, instDecodeTomlRawRelation, resolveRelation

Lean core dependencies: Array, BaseIO, EIO, EIO.toBaseIO, EStateM.Result, EStateM.run, Except, IO, IO.Error, IO.FS.readFile, IO.userError, Lean.Name.mkStr1, List, List.mapM, List.toArray, Not, Prod, String, String.Pos.Raw, String.rawEndPos, System.FilePath, Unit, dite, liftM, of_eq_true, optParam

Used by: (none)

Linking Lean definitions to ontology concepts

@[concept "name"] links a Lean definition to a named concept in the course ontology. A single definition may carry several of these, e.g. @[concept "router", concept "packet"].

syntax (name := concept) "concept" ppSpace str : attr

Outer dependencies: (none)

Lean core dependencies: Lean.Name.mkStr1, Lean.ParserDescr, Nat

Used by: (none)

Every @[concept ...] annotation in the environment, across all loaded modules.

def allConceptAnnotations (env : Environment) : Array (Name × String) := Id.run do
  let mut acc := conceptExt.getState env
  for i in [0:env.allImportedModuleNames.size] do
    acc := acc ++ conceptExt.getModuleEntries env i
  return acc

Outer dependencies: (none)

Lean core dependencies: Array, Array.size, ForInStep, Id, Id.run, Lean.Name, Membership, Nat, Nat.zero_lt_one, Prod, Std.Legacy.Range, String, inferInstance

Used by: getConceptsOf

All concept names a declaration was linked to via @[concept ...].

def getConceptsOf (env : Environment) (declName : Name) : List String :=
  (allConceptAnnotations env).toList.filterMap fun (n, c) => if n == declName then some c else none

Outer dependencies: (none)

Inner dependencies: allConceptAnnotations

Lean core dependencies: Bool, Eq, Lean.Name, List, List.filterMap, Option, Prod, String, ite

Used by: (none)

Marking supporting lemmas

@[lemma] marks a theorem as a supporting lemma rather than a main result. Lean’s lemma keyword is only surface syntax for theorem and leaves no trace in the compiled environment, so this attribute is what the gate actually uses to tell the two apart when measuring complexity.

syntax (name := lemmaTag) "lemma" : attr

Outer dependencies: (none)

Lean core dependencies: Lean.Name.mkStr1, Lean.ParserDescr, Nat

Used by: (none)

Every declaration marked @[lemma], across all loaded modules.

def allLemmaTags (env : Environment) : Array Name := Id.run do
  let mut acc := lemmaExt.getState env
  for i in [0:env.allImportedModuleNames.size] do
    acc := acc ++ lemmaExt.getModuleEntries env i
  return acc

Outer dependencies: (none)

Lean core dependencies: Array, Array.size, ForInStep, Id, Id.run, Lean.Name, Membership, Nat, Nat.zero_lt_one, Std.Legacy.Range, inferInstance

Used by: isLemma

Whether n was marked @[lemma].

def isLemma (env : Environment) (n : Name) : Bool :=
  (allLemmaTags env).contains n

Outer dependencies: (none)

Inner dependencies: allLemmaTags

Lean core dependencies: Array.contains, Bool, Lean.Name

Used by: (none)

Marking technical, skippable declarations

@[ignore] marks a declaration as technical plumbing rather than a concept the course is teaching — typeclass wiring needed to make some other, genuinely interesting declaration typecheck, not a fact a student following the course needs to stop and understand. It’s excluded from its file’s complexity budget (see measureComplexity) and from the student-review pass (see tools/student_review.py), but still appears on the rendered page, marked as skippable, since it’s real formalized content and the witness principle still applies to it.

syntax (name := ignoreTag) "ignore" : attr

Outer dependencies: (none)

Lean core dependencies: Lean.Name.mkStr1, Lean.ParserDescr, Nat

Used by: (none)

Every declaration marked @[ignore], across all loaded modules.

def allIgnoreTags (env : Environment) : Array Name := Id.run do
  let mut acc := ignoreExt.getState env
  for i in [0:env.allImportedModuleNames.size] do
    acc := acc ++ ignoreExt.getModuleEntries env i
  return acc

Outer dependencies: (none)

Lean core dependencies: Array, Array.size, ForInStep, Id, Id.run, Lean.Name, Membership, Nat, Nat.zero_lt_one, Std.Legacy.Range, inferInstance

Used by: isIgnored

Whether n was marked @[ignore].

def isIgnored (env : Environment) (n : Name) : Bool :=
  (allIgnoreTags env).contains n

Outer dependencies: (none)

Inner dependencies: allIgnoreTags

Lean core dependencies: Array.contains, Bool, Lean.Name

Used by: (none)

Marking worked examples

@[example] marks a declaration as a worked example: a concrete illustration of a concept already introduced, not a new one of its own. Like @[ignore], it’s excluded from its file’s complexity budget (see measureComplexity) and from the student-review pass (see tools/student_review.py) — but unlike @[ignore] (technical plumbing, faded down since it’s skippable), it’s rendered in its own highlighted, post-it-yellow box, since it’s exactly the kind of thing a student should stop and read.

syntax (name := exampleTag) "example" : attr

Outer dependencies: (none)

Lean core dependencies: Lean.Name.mkStr1, Lean.ParserDescr, Nat

Used by: (none)

Every declaration marked @[example], across all loaded modules.

def allExampleTags (env : Environment) : Array Name := Id.run do
  let mut acc := exampleExt.getState env
  for i in [0:env.allImportedModuleNames.size] do
    acc := acc ++ exampleExt.getModuleEntries env i
  return acc

Outer dependencies: (none)

Lean core dependencies: Array, Array.size, ForInStep, Id, Id.run, Lean.Name, Membership, Nat, Nat.zero_lt_one, Std.Legacy.Range, inferInstance

Used by: isExample

Whether n was marked @[example].

def isExample (env : Environment) (n : Name) : Bool :=
  (allExampleTags env).contains n

Outer dependencies: (none)

Inner dependencies: allExampleTags

Lean core dependencies: Array.contains, Bool, Lean.Name

Used by: (none)

Marking file difficulty

The intended difficulty level of a file, used to size its complexity threshold. optional has no upper limit: for technical/formalism-heavy files students aren’t required to read (e.g. one that consolidates advanced category-theoretic results), as opposed to the three student-facing tiers, which stay capped.

inductive Difficulty
  | easy
  | moderate
  | hard
  | optional
deriving Repr, DecidableEq

Outer dependencies: (none)

Lean core dependencies: Eq, Nat, Nat.ble, PULift, cond, noConfusionEnum, noConfusionTypeEnum

Used by: Difficulty.ofString?

def Difficulty.ofString? : String → Option Difficulty
  | "easy" => some .easy
  | "moderate" => some .moderate
  | "hard" => some .hard
  | "optional" => some .optional
  | _ => none

Outer dependencies: Difficulty

Lean core dependencies: Eq, Eq.ndrec_symm, Not, Option, String, Unit, Unit.unit, dite

Used by: (none)

@[difficulty "easy"|"moderate"|"hard"|"optional"] marks the intended difficulty level of the file containing this declaration; the gate sizes that file’s complexity threshold accordingly. Put it on any one declaration in the file (e.g. the main one).

syntax (name := difficultyTag) "difficulty" ppSpace str : attr

Outer dependencies: (none)

Lean core dependencies: Lean.Name.mkStr1, Lean.ParserDescr, Nat

Used by: (none)

Every @[difficulty ...] annotation in the environment, across all loaded modules.

def allDifficultyAnnotations (env : Environment) : Array (Name × String) := Id.run do
  let mut acc := difficultyExt.getState env
  for i in [0:env.allImportedModuleNames.size] do
    acc := acc ++ difficultyExt.getModuleEntries env i
  return acc

Outer dependencies: (none)

Lean core dependencies: Array, Array.size, ForInStep, Id, Id.run, Lean.Name, Membership, Nat, Nat.zero_lt_one, Prod, Std.Legacy.Range, String, inferInstance

Used by: (none)

The module that declared n, if it was loaded from an imported module.

def moduleOf (env : Environment) (n : Name) : Option Name := do
  let idx ← env.getModuleIdxFor? n
  env.allImportedModuleNames[idx.toNat]?

Outer dependencies: (none)

Lean core dependencies: Array, Array.size, Lean.Name, Nat, Option

Used by: (none)

Dependency diagram

Drag to pan, Ctrl+scroll (or Cmd+scroll) to zoom, click a node to jump to it.

definitiontheoremdeclared elsewheredependencyproof dependency
legend