Inductive types associated to instances of a structure in Lean

Question

I am using the Lean computer proof assistant. I am using the combinatorial structure of a graph with an abelian operation on its edges as a learning example.

In it I have a structure Graph. I want to have several inductive types associated to each particular structure g : Graph; so that g.edges, g.vertices would or something like that. Then I want - basically, and in pseudocode - the following associated functions:

g.head : g.edges -> g.vertices

g.tail : g.edges -> g.vertices

g.multiplication : {(x, y) : g.vertices x g.vertices // g.tail(y) == g.head(x)} -> g.vertices

That's just an example so that people get the point. What I'm saying basically is that I want something which can play the role that a class within a class has in python. Structure is nice for very simple algebraic structures, but I want to be able to nest structures, put types of any kind internal to a structure (much like a class can go in a class in python).

Answer 1

"Structure in structure" can mean many things. Here are some interpretations:

Let's say you have the following directed graph implementation:

universe u
structure Graph (V : Type u) where
  is_edge : V -> V -> Prop

def my_example_graph : Graph Nat := { is_edge := fun x y => x < y }

(My examples are in Lean 4 and they are just quick examples. The ideas are the same for Lean 3, but with different syntax. See this question for ways to define directed graphs in Lean)

It might be that after you define Graph, you want to be able to have extra methods for the Graph object. In Lean this is easy to do for any type. You don't have to modify Graph or wrap it in another type. You just add those functions inside the Graph namespace. This is the preferred way to add functions to any type including structures.

-- method 1: Just put namespace in definition name
def Graph.vertices {V : Type u} (g : Graph V) : Type u := V

-- method 2: enter namespace block
namespace Graph
   def is_source {V : Type u} (g : Graph V) (v : V) : Prop := ∃ w, g.is_edge v w
   def is_target {V : Type u} (g : Graph V) (v : V) : Prop := ∃ w, g.is_edge w v
end Graph

-- you can use project notation like follows
#check my_example_graph.vertices    -- Graph.vertices my_example_graph : Type
#check my_example_graph.is_source 0 -- Graph.is_source my_example_graph 0 : Prop
#check my_example_graph.is_target 0 -- Graph.is_target my_example_graph 0 : Prop

You can also wrap Graph in another structure or inductive:

structure GraphPair (V : Type u) where
  g1 : Graph V
  g2 : Graph V

inductive HigherOrderGraph
| LeafGraph : Graph Unit -> HigherOrderGraph
| GraphOfGraphs : Graph HigherOrderGraph -> HigherOrderGraph

A common use case is where you want to extend your structure with more fields. Instead of wrapping it inside a structure, use extends as follows:

structure LabeledGraph (V : Type u) extends Graph V where
  L : Type u
  labels : (v w : V) -> is_edge v w -> L

def my_example_labeled_graph : LabeledGraph Nat :=
{ my_example_graph with
  L := Bool, 
  labels := fun x y _ => y > 0
}

See the structure section of TPIL for more info.