a statement that depends on itself to make sense

Stream: new members

[X.-M. Chu]

Hello,
I'm trying to figure out how to make the following definition work(there are probably much better definitions of graphs. What I present here is my naive attempt to so.) I wonder what is the best way to make a definition whose latter part depends on the first part to be meaningful.
Here's my code:

def is_isomorphic (G G': finite_simple_graph): Prop :=
  ∃ f: natural_number_less_than (n_vertex G) → natural_number_less_than (n_vertex G), (is_bijective f) ∧
(∀ u v: natural_number_less_than (n_vertex G), connected G (u, v) ↔ connected G' (f u, f v))

where finite_simple_graph is defined as naive as one might get:

structure finite_simple_graph :=
(n_vertex: nat)
(connected: natural_number_less_than n_vertex × natural_number_less_than n_vertex → Prop)

The predicate connected G' (u, v) depends on the fact that G, G' has the same number of vertices to even make sense, so the above code is not valid in Lean. Lean would simply tell me that natural_number_less_than n_vertex G and natural_number_less_than n_vertex G'are different types. But they are actually the same, which is ensured by the first part of the proposition.
How can I make this into a valid Lean proposition? What is the right way to do so in Lean?
Thank you very much.

[Alex J. Best]

At that point of the definition you should have access to the function f, which you can apply to take natural_number_less_than (n_vertex G) to the same natural_number_less_than (n_vertex G') (I think there is a typo there in the definition of f though).
So defining connected G (u, v) ↔ connected G' (f u, f v)) looks like it should work to me, does it?

[Alex J. Best]

Also natural_number_less_than seems very similar to doc#fin, have you tried using that instead? It might make some things easier

[Yaël Dillies]

Are you trying to do something like file#order/countable_dense_linear_order ?

[X.-M. Chu]

Alex J. Best said:

At that point of the definition you should have access to the function f, which you can apply to take natural_number_less_than (n_vertex G) to the same natural_number_less_than (n_vertex G') (I think there is a typo there in the definition of f though).
So defining connected G (u, v) ↔ connected G' (f u, f v)) looks like it should work to me, does it?

Yes there is something wrong.

def is_isomorphic (G G': finite_simple_graph): Prop :=
  ∃ f: natural_number_less_than (n_vertex G) → natural_number_less_than (n_vertex G'), (is_bijective f) ∧
 (∀ u v: natural_number_less_than (n_vertex G), connected G (u, v) ↔ connected G' (f u, f v))

works.The crutial thing is to define f as natural_number_less_than (n_vertex G) → natural_number_less_than (n_vertex G'). This was not a typo but something I didn't understand well.
Thank you very much.
But I do want to know that in more general situations, can one make a definition whose second part depends one the first part even to make sense. This is omnipresent in mathematics. Is it always possible to have a work around like in my example?

[Patrick Johnson]

But I do want to know that in more general situations, can one make a definition whose second part depends one the first part even to make sense.

That's what a recursion is. But I don't see any kind of a recursion in your example. I guess you got confused because the following simplified code doesn't type check:

example {α β : Type} (h : α = β) {x : α} : ∃ (y : β), x = y := sorry

It doesn't type check because Lean is not convinced that x and y are terms of the same type, so x = y is not a valid expression. You can use heterogeneous equality in that case instead:

example {α β : Type} (h : α = β) {x : α} : ∃ (y : β), x == y :=
by cases h; use x

But, as you have already figured out, this was not the problem in your definition.

[Martin Dvořák]

What does == mean? I couldn't find it in TPIL.

[Daniel Roca González]

Here are the docs

[Eric Wieser]

(note it means something different in lean 4)