Using the Mathlib,

Stream: new members

[Jonathan Whitehead]

So I want to turn a Finset into a list. I found a function in finset called to_list that seems to do what I want, but I can't seem to access it. For example, if X : Finset a, I tried X.val.to_list, X.1.to_list, and X.to_list. In each occasion Lean complains that the field to_list is not in the environment. That is Finset.to_list and Multiset.to_list is not in the environment.

Why can't I use to_list? And is this a proper way to turn a Finset to a list?

[Kyle Miller]

Are you looking at the mathlib3 docs instead of the mathlib4 docs? docs4#Finset.toList is the mathlib4 one and docs#finset.to_list is the mathlib3 one.

[Jonathan Whitehead]

I'm actually using the Github https://github.com/leanprover-community/mathlib/blob/master/src/data/finset/basic.lean , whcih I thought was Lean 4.

[Kyle Miller]

That's mathlib3 (generally, no number right now means version 3, and for version 4 you want to see a 4)

[Kyle Miller]

Notice also all the names are lower-case. Mathlib 4 naming convention is upper case types.

[Kyle Miller]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Finset/Sort.html might be useful too for turning a finset into a list, since this can actually be computed, if you're wanting to evaluate things

[Jonathan Whitehead]

Ah, I see. It's toList. Thanks!

[Kyle Miller]

I noticed that that also has an (unsafe) Repr instance for Finset, which might be useful for debugging.

[Jonathan Whitehead]

Ah, great. I'll play around with it and see how it works.

[Eric Wieser]

And is this a proper way to turn a Finset to a list?

For what purpose? Sometimes docs4#Finset.sort is a better choice

[Jonathan Whitehead]

Eric Wieser said:

And is this a proper way to turn a Finset to a list?

For what purpose? Sometimes docs4#Finset.sort is a better choice

I'm just trying to print the Finset. If I try X.toList.map toString I get the message "invalid field notation, type is not of the form (C ...) where C is a constant..."

[Jonathan Whitehead]

#check Finset.sort.map toString

instance graph_to_string : ToString Graph := ⟨
  fun G => "{Vertices = " ++
            String.intercalate ", " (G.vertices.toList.map toString ) ++
            " : ¬ Edges = " ++
            String.intercalate ", " (G.edges.map toString) ++
            "}"
⟩

Lean actually underlines the name of the instance and says that IR check failed at 'graph_to_string' unknown declaration at 'Finset.toList'.

[Eric Wieser]

I think you need to add unsafe before the word instance

[Jonathan Whitehead]

Well that certainly makes me feel safe about what I'm doing :sweat_smile: What exactly does unsafe do?

[Eric Wieser]

Though this sounds a bit like an #xy problem; can you just add deriving Repr to your Graph

[Jonathan Whitehead]

But unsafe still doesn't seem to fix it.

[Jonathan Whitehead]

structure Graph :=
(vertices : Finset Vertex)
(edges : List Edge)
(property : ∀ e ∈ edges, Prod.fst e.edge ∈ vertices ∧ Prod.snd e.edge ∈ vertices)
deriving Repr

You mean like this?

[Eric Wieser]

Oh, I guess it gets unhappy about property?

[Eric Wieser]

Or does that just work?

[Jonathan Whitehead]

It doesn't work. Here is what I have:

structure Vertex :=
  (name : String)
  deriving DecidableEq

instance vertex_to_string : ToString Vertex :=
  ⟨fun v =>  v.name⟩

structure Edge :=
  (name : String)
  (edge : Vertex × Vertex)
  deriving DecidableEq

instance edge_to_string : ToString Edge :=
  ⟨fun e =>  "(" ++ e.edge.fst.name ++ ", " ++ e.edge.snd.name ++ ")" ⟩

structure Graph :=
(vertices : Finset Vertex)
(edges : List Edge)
(property : ∀ e ∈ edges, Prod.fst e.edge ∈ vertices ∧ Prod.snd e.edge ∈ vertices)
deriving Repr

And at deriving Repr, Lean complains because there's not a Repr instance of vertex_list_to_string and edge_list_to_string. I created the instances for vertices and edges, but not for a multiset of vertices and a list of string.

[Eric Wieser]

You need to put deriving Repr on all of the structures

[Jonathan Whitehead]

It used to work until I added property in Graph. I needed to add this property because I wrote a program and couldn't prove it to be correct because I couldn't prove that each endpoint of the edges were in the vertices. Hence, I had to define Graph as a structure that carried with it a proof that the endpoints of each edge were vertices of G.

[Eric Wieser]

(I'm not at lean right now, so can't actually give you working code!)

[Jonathan Whitehead]

When I put deriving Repr on Vertex, it tells me that it "expected 'instance'".

structure Vertex :=
  (name : String)
  deriving DecidableEq
  deriving Repr

[Eric Wieser]

I think the syntax is deriving Foo, Bar not deriving Foo, deriving Bar

[Jonathan Whitehead]

It feels like I need to have more "set up" before I can use deriving Repr

[Eric Wieser]

Does fixing the syntax still not work?

[Jonathan Whitehead]

It doesn't appear to be working. Is Bar supposed to be the name of the instance? Like deriving Repr, vertex_to_string doesn't seem to work. It still says expected instance.

[Jonathan Whitehead]

I also tried deriving Repr, instance vertex_to_string and the same result followed.

[Eric Wieser]

Yeah that's nonsense

[Eric Wieser]

I mean deriving DecidableEq, Repr

[Jonathan Whitehead]

Ohhh, okay that it. That worked.

[Damiano Testa]

Can I maybe chime in and go back to your definition of Vertex: do you really want it to be a string?

[Damiano Testa]

I think that if you want to be able to "print" your vertices, you should put a Repr instance on the type on whose terms you build the graph.

[Jonathan Whitehead]

Damiano Testa said:

Can I maybe chime in and go back to your definition of Vertex: do you really want it to be a string?

I'm new and picked a mathematical object to define and work with. At the current moment, without the wisdowm and foresight of an experienced user, I chose to define a vertex as simply an object with a label. I'm sure that more sophisticated approaches would define things a bit differently but I was just trying to define things the way that I learned them in an undergraduate course.

Moreover, I also wanted to define algorithms on these graphs and prove that the algorithms are correct. Hence, I kind of need some labeling system on the vertices and edges. Hence the reason why I have them as structs with a field for a string.

[Damiano Testa]

Looking at your code, maybe you could define an Edge to have a source and a target, rather than an ordered pair.

[Damiano Testa]

So, let's see if we can get you started with something that will be easier.

[Jonathan Whitehead]

Okay, but remember I'm a new user and things can quickly become esoteric. :sweat_smile:

[Jonathan Whitehead]

I've been worried about finding the easiest implementation to work with because in some instances an easier implementation might not be the canonical interpretation of the object in a math class. And I just want the implementation to be readable to regular math students with little to no computer science back ground. There seems to be a delicate balance between the two that I haven't quite found.

[Damiano Testa]

structure Edge (α : Type) :=
  (source : α)
  (target : α)

def myEdge : Edge Nat :=
  { source := 1
    target := 2 }

instance [ToString α] : ToString (Edge α) where
  toString := by
    intro e
    exact toString e.source ++ "," ++ toString e.target

#eval myEdge

[Damiano Testa]

You get an Edge (a type) by providing a pair of elements of type.

[Damiano Testa]

For instance, the def construct an Edge on the natural numbers.

[Damiano Testa]

Next, you define a ToString instance on an Edge, by assuming that there already is a ToString instance on the type whose elements you are considering. You get to define how you want to represent the edge joining a to b. I chose to represent it by using the representation for a then a comma, then the representation for b.

[Eric Wieser]

(note the point in my Repr comments was "you can get a default representation of your object without doing any work". If you want to customize how it looks, rolling your own instead is fine)

[Damiano Testa]

In the exact line, you get to choose what you want. If you prefer a "list-style" printing, you could say instead

    exact "[" ++ toString e.source ++ "," ++ toString e.target ++ "]"

[Damiano Testa]

This way, you "outsource" the printing to the target type. You are likely going to define graphs on Nat, on String, on some enumerated inductive type. In each case, you can leverage a "printing" instance on the type of the vertices to get your printed version.

[Damiano Testa]

Here is another example:

structure Edge (α : Type) :=
  (source : α)
  (target : α)

def myEdge : Edge Nat :=
  { source := 1
    target := 2 }

def myStringEdge : Edge String :=
  { source := "sou"
    target := "tar" }

instance [ToString α] : ToString (Edge α) where
  toString := by
    intro e
    exact "[" ++ toString e.source ++ "," ++ toString e.target ++ "]"

#eval myEdge   --  [1,2]
#eval myStringEdge  --  [sou,tar]

[Damiano Testa]

Lean already knows how to print Nat and String, I simply told it how to print an edge, given that notion.

[Jonathan Whitehead]

In my definition I pushed the parameter into the structure and forced it to be a string, because I didn't think that I would ever really care about the type of the vertex, I just wanted to let them all be strings. I reasoned that if they're all strings, I wouldn't have to worry about the printing procedure as much since printing strings has been taken care of in Lean.

What is the point of letting Edge be an "edge of ___"? Is it just going to make things easier to work with?

[Eric Wieser]

I think this is the line of reasoning that gives you things like sh where the only type of variables is strings :)

[Eric Wieser]

What if you want a graph where the nodes are natural numbers and there are edges whenever one node divides another?

[Damiano Testa]

For instance, if you wanted to define the "divisibility graph", having access to Nat as a vertex set is useful...

[Jonathan Whitehead]

Another thing about the implementation that you posted is that I get error messages if I try to add deriving DecidableEq and while I've been working on this stuff, I've found that I certainly want there to be a decidable equality between these edges and manually defining the decidable equality was a bit of work.

[Damiano Testa]

Or if you wanted to work with a finite graph and use dec_trivial, it might be helpful to work with enumerated types. For instance:

inductive vertSet | A | B | C

instance : ToString vertSet where
  toString | vertSet.A => "A" | vertSet.B => "B" | vertSet.C => "C"

def myIndEdge : Edge vertSet :=
  { source := vertSet.A
    target := vertSet.B }

#eval myIndEdge

[Damiano Testa]

I think that you can derive DecidableEq if you assume it for the base type.

[Jonathan Whitehead]

Great examples of why I would want the parameter.

[Damiano Testa]

Note that the implementation of the instance is a completely arbitrary choice: I do not have to use the string "A" for the vertex called vertSet.A, of course.

[Damiano Testa]

(I mean the ToString instance on vertSet, though for sanity it is helpful to use the same name, of course!)

[Eric Wieser]

Does deriving ToString on vertSet do that for you?

[Jonathan Whitehead]

Sorry it's taking a minute to respond. I'm reading through everything.

[Damiano Testa]

inductive vertSet | A | B | C
  deriving ToString
--  default handlers have not been implemented yet, class: 'ToString' types: [vertSet]

[Damiano Testa]

@Eric Wieser , so no!

[Yakov Pechersky]

I think Kyle has implemented a handler that covers this

[Jonathan Whitehead]

Aren't there going to be issues with leaving the vertices undefined? For example, when I do

structure Graph :=
(vertices : Finset Vertex)
(edges : List Edge)
(property : proof that the source and target are in Finset Vertex)

I feel like there's going to be problems at Finset Vertex. So I would need to change the way that I define the Graph too.

[Damiano Testa]

I probably would define a structure Graph (of a type) and simply assume that every term of the type is a vertex. If you assume that the type is finite, you have a finset of vertices.

[Jonathan Whitehead]

Ah, okay I'll work on implementing these ideas.

[Damiano Testa]

So, something like this:

structure Graph (α : Type) :=
  (edges : List (Edge α))

[Jonathan Whitehead]

But wouldn't that prevent me from being able to talk about G - v, where v is a vertex?

[Damiano Testa]

Then, every term of α is a vertex. Some of these vertices appear as endpoints of edges.

[Kyle Miller]

Yakov Pechersky said:

I think Kyle has implemented a handler that covers this

There's deriving ToExpr and I think you can maybe use toString (toExpr x)?

[Damiano Testa]

Here, there might be a difference between a subgraph and a graph that happens to be a subgraph.

[Damiano Testa]

So, "the mathlib way" would probably be to define a "Type of Subgraphs", whose terms are not Graphs, but that have coercions to a Graph.

[Yaël Dillies]

Jonathan Whitehead said:

But wouldn't that prevent me from being able to talk about G - v, where v is a vertex?

No, it simply means G - v won't be of the same type as G (it will have type Graph {a // a \ne v})

[Yaël Dillies]

This is all quite fiddly, and it's hard to find a working design that's not mathlib's.

[Damiano Testa]

This means that you will get more or less for free that the Type of Subgraphs is a lattice, and you can get the machinery of lattices to help you with inductions, unions, intersections... without having to redefine these notions from scratch.

[Damiano Testa]

@Kyle Miller toExpr is an unknown identifier: should I import/open something?

[Kyle Miller]

You need to import https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/DeriveToExpr.html for derive ToExpr and then I think it's ToExpr.toExpr

[Damiano Testa]

@Jonathan Whitehead the constructions of Subgraphs that I am thinking of is entirely analogous to the one of several, similar ones in mathlib, for instance submodule.

[Kyle Miller]

Damiano Testa said:

So, "the mathlib way" would probably be to define a "Type of Subgraphs", whose terms are not Graphs, but that have coercions to a Graph.

In practice the algebra hierarchy design doesn't really work for graphs. Most algebraic objects "are" a type, but a graph isn't a type. The coercion design depends on the fact that there is a coercion from a subobject to a type, and that type can be given the additional structure through typeclass inference.

[Jonathan Whitehead]

Damiano Testa said:

Jonathan Whitehead the constructions of Subgraphs that I am thinking of is entirely analogous to the one of several, similar ones in mathlib, for instance submodule.

Okay, I'm going to work on these ideas and reread all of your comments. I'm just worried that the framework will be pigeon-hole me into writing an implementation that isn't very "mathematician" friendly. Personally, I don't mind because I'm learning a lot of new ideas, but if things get too strange it will deter some of my friends.

[Kyle Miller]

@Damiano Testa Also, you might want a coercion from subgraphs to graphs, but, at least last I experimented, you can't make a Coe instance that goes to Graph ?_ and have it solve for ?_. It had something to do with universe variables not getting unified, if I remember correctly.

[Damiano Testa]

For the record, this works:

import Mathlib.Tactic.DeriveToExpr
open Lean

inductive vertSet
  | A | B | C
  deriving ToExpr

instance : ToString vertSet where
  toString := fun x => toString (toExpr x)

#eval vertSet.A  --  vertSet.A

[Damiano Testa]

Sure, I have thought about how to define graphs in mathlib only after this thread started...

[Damiano Testa]

@Jonathan Whitehead keep in mind that "finite" and "concrete" structures have a tendency of being hard to work with. It is often the case that the more abstract something is, the easier it will be to formalize.

[Jonathan Whitehead]

Damiano Testa said:

Jonathan Whitehead keep in mind that "finite" and "concrete" structures have a tendency of being hard to work with. It is often the case that the more abstract something is, the easier it will be to formalize.

Ah, never thought about how concrete things tend to be more difficult. Good to know.

[Jonathan Whitehead]

I suppose another way to think about Graphs is to define the vertex to be a list of vertices with an adjacency relation on them... But that might be stranger and harder to work with. But it seems like it might be easier to do things like vertex deletion and to talk about isolated vertices?

[Damiano Testa]

I have not really though about this, but maybe, following what you say, it might make sense to have the edges be a symmetric relation on a type.

[Damiano Testa]

(or not symmetric, if you want to do directed graphs)

[Yakov Pechersky]

Definitions are hard.

[Jonathan Whitehead]

Damiano Testa said:

I have not really though about this, but maybe, following what you say, it might make sense to have the edges be a symmetric relation on a type.

Yeah, I was also thinking about this when we defined edges to have sources and targets. I realize that these are just identifiers and can be changed but they seem to imply directedness.

[Damiano Testa]

So, I do not know if this will work, but it might be fun to experiment with:

structure Graph (α) :=
  (adj : α → α → Prop)
  (symm : ∀ {a b}, adj a b → adj b a)

[Yakov Pechersky]

And with graphs, there are a ton of things to define. Maybe pick a theorem first and see what definitions lend itself to it?

[Kyle Miller]

Do you know about docs4#SimpleGraph @Damiano Testa ?

[Damiano Testa]

@Kyle Miller I just learned about it! And, while I was typing the definition, I was wondering if I wanted to include irreflexivity or reflexivity as a condition!

[Kyle Miller]

Ok, so you might also just be discovering docs4#SimpleGraph.Subgraph ?

[Damiano Testa]

It seems like I got the capitalization wrong...

[Damiano Testa]

Kyle Miller said:

Ok, so you might also just be discovering docs4#SimpleGraph.Subgraph ?

This seems exactly where I was headed...

[Kyle Miller]

For Jonathan's purposes, a problem with using a relation on a type is that it has no computational content. I've gotten the sense that he wants to do some computations (with #eval for example), and it'd be better to avoid Prop and instead use some actual data for that.

[Kyle Miller]

You can do computations with SimpleGraph, but it takes defining Decidable instances, which are sort of a lot to master when you're just learning Lean.

[Jonathan Whitehead]

Yakov Pechersky said:

And with graphs, there are a ton of things to define. Maybe pick a theorem first and see what definitions lend itself to it?

My goal is to write programs for some algorithms and show that they're correct. I took a course where "proofs" of algorithms were given (e.g. augmenting path, blosom algorithms, etc.), but the proofs were very hand wavey. So I wanted to see if I could formalize the algorithms and prove they are correct.

[Kyle Miller]

I would suggest ignoring how mathlib does things for that and write a Graph type that will suit your own purposes for some algorithm

[Kyle Miller]

As you implement a few algorithms, you can revisit whether you made a good choice in your design, and iterate.

[Kyle Miller]

It's too hard to come up with the right definition up front. You need to know where it's all going to know where you were supposed to start

[Damiano Testa]

And maybe even start with something moderately simple, like showing that a connected graph on 3 vertices must have at least 2 edges.

[Jonathan Whitehead]

Kyle Miller said:

I would suggest ignoring how mathlib does things for that and write a Graph type that will suit your own purposes for some algorithm

Yes! This is what I've been doing. I wrote some simple programs and proved them, but then I wrote a certain program that I couldn't prove without modifying my definition of a graph to include a proof that the end points of edges are in the vertex set. Hence, I went back to modify my definition of a Graph and then things started breaking :joy:

[Kyle Miller]

That might sound simple @Damiano Testa (most simple things in combinatorics do), but connectivity takes some work to develop to be usable

[Kyle Miller]

It should be pretty straightforward with the mathlib SimpleGraph library though, and that would be a welcome lemma if anyone wants to prove it

[Damiano Testa]

I think that the first project that I worked on was to show something about connected graphs and it was hard...

[Kyle Miller]

docs4#SimpleGraph.Connected is the connectivity predicate

[Kyle Miller]

By the way, speaking of a computation, in the mathlib3 archive there's the Konigsberg bridges problem

[Damiano Testa]

I certainly did not define Preconnected and went straight to Connected!

[Kyle Miller]

@Damiano Testa Here's the well-known "Damiano's lemma":

import Mathlib.Combinatorics.SimpleGraph.Connectivity

open SimpleGraph

variable {V : Type _} (G : SimpleGraph V) [Fintype V] [Fintype G.edgeSet]

lemma damiano (hc : G.Connected) (hv : 2 < Fintype.card V) : 1 < G.edgeFinset.card := by
  rw [Fintype.two_lt_card_iff] at hv
  simp only [Finset.one_lt_card_iff, Set.mem_toFinset, ne_eq, exists_and_left]
  obtain ⟨a, b, c, hab, hac, hbc⟩ := hv
  refine (hc a b).elim_path (fun ⟨pab, hp⟩ => ?_)
  cases pab
  · exact absurd rfl hab
  rename_i v hav pvb
  cases pvb
  · refine ⟨_, G.mem_edgeSet.mpr hav, ?_⟩
    refine (hc c a).elim (fun pca => ?_)
    cases pca
    · exact absurd rfl hac
    · rename_i hcv _
      refine ⟨_, G.mem_edgeSet.mpr hcv, ?_⟩
      simp [not_or, hac, hbc]
  · rename_i w hvw _
    refine ⟨_, G.mem_edgeSet.mpr hav, _, G.mem_edgeSet.mpr hvw, ?_⟩
    simp only [Walk.cons_isPath_iff, Walk.support_cons, List.find?, List.mem_cons, not_or] at hp
    simp only [Quotient.eq, Sym2.rel_iff, hp.2.1, false_and, and_true, false_or]
    rintro rfl
    simp at hp

Edit: Refined a very little

import Mathlib.Combinatorics.SimpleGraph.Connectivity

open SimpleGraph

lemma SimpleGraph.Adj.mem_edgeSet {G : SimpleGraph V} (h : G.Adj v w) : ⟦(v, w)⟧ ∈ G.edgeSet := h

variable (G : SimpleGraph V) [Fintype V] [Fintype G.edgeSet]

lemma damiano (hc : G.Connected) (hv : 2 < Fintype.card V) : 1 < G.edgeFinset.card := by
  rw [Fintype.two_lt_card_iff] at hv
  simp only [Finset.one_lt_card_iff, Set.mem_toFinset, ne_eq, exists_and_left]
  obtain ⟨a, b, c, hab, hac, hbc⟩ := hv
  refine (hc a b).elim_path (fun ⟨pab, hp⟩ => ?_)
  cases pab with
  | nil => exact absurd rfl hab
  | cons hav pvb =>
    cases pvb with
    | nil =>
      refine ⟨_, hav.mem_edgeSet, ?_⟩
      refine (hc c a).elim (fun pca => ?_)
      cases pca with
      | nil => exact absurd rfl hac
      | cons hcv _ =>
        refine ⟨_, hcv.mem_edgeSet, ?_⟩
        simp [not_or, hac, hbc]
    | cons hvw _ =>
      refine ⟨_, hav.mem_edgeSet, _, hvw.mem_edgeSet, ?_⟩
      simp only [Walk.cons_isPath_iff, Walk.support_cons, List.find?, List.mem_cons, not_or] at hp
      simp only [Quotient.eq, Sym2.rel_iff, hp.2.1, false_and, and_true, false_or]
      rintro rfl
      simp at hp

[Kyle Miller]

The proof is a rough draft, and there are likely some hidden lemmas just waiting to be extracted

[Damiano Testa]

Kyle, I simply extracted one lemma from your proof.

import Mathlib.Combinatorics.SimpleGraph.Connectivity

namespace SimpleGraph

variable {G : SimpleGraph V} [Fintype V] [Fintype G.edgeSet] (hc : G.Connected)

lemma Connected.mem_edgeSet_of_ne (hva : v ≠ a) : ∃ e, e ∈ edgeSet G ∧ v ∈ e := by
  refine (hc v a).elim_path (fun ⟨pab, hp⟩ => ?_)
  match pab with
  | Walk.nil => exact absurd rfl hva
  | Walk.cons _ _ => exact ⟨⟦(v, _)⟧, by simpa⟩

lemma Connected.one_lt_of_two_lt (hv : 2 < Fintype.card V) : 1 < G.edgeFinset.card := by
  simp only [Finset.one_lt_card_iff, Set.mem_toFinset, ne_eq, exists_and_left]
  obtain ⟨a, b, c, hab, hac, hbc⟩ := Fintype.two_lt_card_iff.mp hv
  obtain ⟨e, he, ae⟩ := hc.mem_edgeSet_of_ne hab
  use e, he
  rcases eq_or_ne e ⟦(a, b)⟧ with rfl | pv
  . obtain ⟨f, hf, af⟩ := hc.mem_edgeSet_of_ne hbc.symm
    use f, hf
    rintro rfl
    simp [hac.symm, hbc.symm] at af
  . obtain ⟨f, hf, be⟩ := hc.mem_edgeSet_of_ne hab.symm
    exact ⟨f, hf, fun ef ↦ pv ((Sym2.mem_and_mem_iff hab).mp ⟨ae, ef ▸ be⟩)⟩

end SimpleGraph

[Jonathan Whitehead]

I know we discussed defining things differently, but it really bothers me that I can't get this simple print function to work. So I kept working on it and I feel like there's an issue happening with the printing module for Finsets and Multisets. Below is the code that I wrote and the error message I receive is:

IR check failed at 'finsetToList.loop._rarg', error: unknown declaration 'Finset.toList'

The reason why I feel like something is going on with porting some code from Lean 3 to 4 is because sometimes the tool tips mention to_list and sometimes they mention toList. I can #check toList, but the error says toList is unknown.

structure Vertex :=
  (name : String)
  deriving DecidableEq, Repr

instance finset_to_string : ToString (Finset Vertex) := ⟨
  fun f => String.intercalate "," $ f.toList.map (fun v => v.name)
⟩

[Mario Carneiro]

#mwe ?

[Jonathan Whitehead]

I also tried creating my own function to send a Finset to List but Lean kept complaining that it couldn't determine if the program terminated:

partial def finsetToList {α : Type} [DecidableEq α] (s : Finset α) : List α :=
  let rec loop (l : List α) (s : Finset α) : List α :=
    match s.to_list with
    | [] => l.reverse
    | x :: xs => loop (x :: l) (s.erase x)
  loop [] s

[Jonathan Whitehead]

import Mathlib.Data.List.Basic
import Mathlib.Data.Finset.Basic

structure Vertex :=
  (name : String)
  deriving DecidableEq, Repr

structure Edge :=
  (name : String)
  (edge : Vertex × Vertex)
  deriving DecidableEq, Repr

instance finset_to_string : ToString (Finset Vertex) := ⟨
  fun f => String.intercalate "," $ f.toList.map (fun v => v.name)
⟩

instance edge_list_to_string : ToString (List Edge) :=
  ⟨fun l =>  String.intercalate ", " $ l.map (fun edge => edge.name) ⟩

structure Graph :=
(vertices : Finset Vertex)
(edges : List Edge)
(property : ∀ e ∈ edges, Prod.fst e.edge ∈ vertices ∧ Prod.snd e.edge ∈ vertices)
deriving Repr

[Damiano Testa]

I think that the issue is that f.toList is interpreted as Finset.toList, since f has Type Finset .... This is simply saying that there is no function to go from a Finset to a List there is one.

[Jonathan Whitehead]

For the graph, deriving Repr says that it fails to find an instance of Repr (Finset Vertex), so I'm trying to make one.

[Jonathan Whitehead]

(deleted)

[Damiano Testa]

I was missing an import, let me keep digging!

[Jonathan Whitehead]

Thanks, I'll keep trying too.

[Mario Carneiro]

the issue is that Finset.toList exists but is noncomputable. That's why the error is reported in a weird place, the compiler is complaining, not the typechecker

[Jonathan Whitehead]

Mario Carneiro said:

the issue is that Finset.toList exists but is noncomputable. That's why the error is reported in a weird place, the compiler is complaining, not the typechecker

Ah, yes, I remember seeing that it was noncomputable. Is there some work around?

[Damiano Testa]

Mario beat me to it! You can add noncomputable before the instance to get it to compile.

[Jonathan Whitehead]

Like I said, I even tried making my own toList function, but couldn't figure out how to convince lean that it terminated.

[Jonathan Whitehead]

Yes! You guys just fixed my problem in a couple minutes that I worked on for hours :rolling_on_the_floor_laughing:

[Mario Carneiro]

the power of a good #mwe :)

[Jonathan Whitehead]

Will I have to worry about it being noncomputable in any of my concrete examples?

[Jonathan Whitehead]

I guess I'm not really relying on printing stuff out, it's just for the user experience.

[Mario Carneiro]

probably, if you want to run the toString instance

[Mario Carneiro]

for a ToString instance it is generally useless if it is not computable

[Jonathan Whitehead]

Ah, but I guess declaring that it's noncomputable didn't fix the deriving Repr in the Graph structure.

[Jonathan Whitehead]

Yeah, letting it be noncomputable makes lean top complaining, but makes it unusable.

[Damiano Testa]

Also, I think that Finset Vertex does not mean what you think it does...

[Mario Carneiro]

here's a computable implementation:

instance finset_to_string : ToString (Finset Vertex) := ⟨
  let trans : IsTrans String (· < ·) := sorry
  let trans : IsAntisymm String (· < ·) := sorry
  let trans : IsTotal String (· < ·) := sorry
  fun f => String.intercalate "," $ f.val.map (fun v => v.name) |>.sort (· < ·)
⟩

[Damiano Testa]

Mario is being very conservative with the choice of names for his lets...

[Jonathan Whitehead]

Mario Carneiro said:

here's a computable implementation:

instance finset_to_string : ToString (Finset Vertex) := ⟨
  let trans : IsTrans String (· < ·) := sorry
  let trans : IsAntisymm String (· < ·) := sorry
  let trans : IsTotal String (· < ·) := sorry
  fun f => String.intercalate "," $ f.val.map (fun v => v.name) |>.sort (· < ·)
⟩

When I try to use it I get an error

invalid field 'sort', the environment does not contain 'Multiset.sort'
  Multiset.map (fun v => ?m.3236 v) f.val
has type
  Multiset

[Damiano Testa]

import Mathlib.Data.Multiset.Sort

[Jonathan Whitehead]

Ah yeah, thanks I'll work on looking through it. I'll also look into understanding the Finset a little better.

[Damiano Testa]

Here is an example, in case it is helpful:

def attempt : Finset Vertex where
  val := ⟦[⟨"hello"⟩, ⟨"world"⟩, ⟨"!"⟩]⟧
  nodup := by simp

#eval attempt  --  !,hello,world

[Damiano Testa]

I do not think that the design is particularly ergonomic, but I found this funny and confusing!

def getWords (S : String) : Finset Vertex where
  val := ⟦ S.splitOn.map fun x ↦ ⟨x⟩ ⟧
  nodup := sorry

#eval (getWords "My words are the vertices of a graph")
#eval (getWords "     ")
#eval (getWords " , , ")