1
$\begingroup$

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).

$\endgroup$
6
  • $\begingroup$ Your multiplication doesn't type check. I assume you want x and y to be edges? Also, why do you want "inductive types"? How have you defined Graph? We will need more details. Are g.edges and g.vertices already part of your API? $\endgroup$
    – jmc
    Sep 3, 2022 at 14:33
  • $\begingroup$ "part of your API" - it was just pseudocode. I need something analogous to classes within classes in python. It should be a pretty simple task ... can you have structures within structures? $\endgroup$ Sep 3, 2022 at 14:36
  • $\begingroup$ “Can you have a structure in a structure?”. Absolutely, you can put any types you want in a structure. (Well, structures aren’t recursive, and there are probably universe restrictions, but otherwise no limitations.) $\endgroup$
    – Jason Rute
    Sep 3, 2022 at 17:07
  • $\begingroup$ But if you still feel this is not helpful, then I think you need to make a correct MWE api (maybe given in Python code) so we understand what you want. $\endgroup$
    – Jason Rute
    Sep 3, 2022 at 17:09
  • $\begingroup$ I guess one pertinent question before we go much further is: are you going to use Lean 3's graphs as defined in its maths library or are you intending to roll your own? $\endgroup$ Sep 3, 2022 at 18:09

1 Answer 1

1
$\begingroup$

"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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.