# Zulip Chat Archive

## Stream: new members

### Topic: using instances for a graph introduced in a statement

#### Mikhail Makarov (Sep 19 2022 at 02:05):

Hello,

I am trying to formalize a statement in Lean from graph theory that has this form: for any natural N, there exists a natural M such that for any graph G a certain property holds. This property depends on N, M, and G. I omit what this property is because it is not relevant to the current issue that I am having. What is important is the order of the quantifiers: M can depend only on N, but not on the graph G.

The graph must be finite. I consider only finite graphs.

I have code like this:

```
import combinatorics.simple_graph.basic
import data.sym.sym2
import data.fintype.basic
import data.finset.basic
universe un
section some_definitions
variables (V : Type un) [fintype V] (G : simple_graph V) [decidable_rel G.adj]
def some_property (N M : nat) : Prop := G.max_degree ≥ N - M --this is a fake definition here much simpler than the actual one because the actual property is not relevant to the current issue
end some_definitions
theorem some_theorem :
forall (N : nat),
exists (M : nat),
forall (V : Type un) [fintype V] (G : simple_graph V) [decidable_rel G.adj], --for any graph
some_property V G N M
:=
begin
sorry
end
```

This does not compile and gives me these 2 errors on the line "some_property V G N M":

```
failed to synthesize type class instance for
N M : ℕ,
V : Type un,
_inst_1 : fintype V,
G : simple_graph V,
_inst_2 : decidable_rel G.adj
⊢ fintype V
failed to synthesize type class instance for
N M : ℕ,
V : Type un,
_inst_1 : fintype V,
G : simple_graph V,
_inst_2 : decidable_rel G.adj
⊢ decidable_rel G.adj
```

I don't know how to pass the instances for `fintype V`

and `decidable_rel G.adj`

to `some_property`

. I tried naming them and passing them explicitly, but it still does not work:

```
theorem some_theorem :
forall (N : nat),
exists (M : nat),
forall (V : Type un) [V_fintype : fintype V] (G : simple_graph V) [G_adj_decidable : decidable_rel G.adj], --for any graph
some_property V V_fintype G G_adj_decidable N M
:=
begin
sorry
end
```

I also tried treating them as assumptions in the implications, but this also does not work:

```
theorem some_theorem :
forall (N : nat),
exists (M : nat),
forall (V : Type un) (G : simple_graph V), --for any graph
fintype V -> decidable_rel G.adj -> some_property V G N M
:=
begin
sorry
end
```

The fact that `V`

is finite and `G.adj`

is decidable should be assumptions in the "for any graph" part, but I don't know how to specify that. Effectively, the statement should be this: "for any natural N, there exists a natural M such that for any `V`

that is finite and any graph `G`

on `V`

such that `G.adj`

is decidable, `some_property`

holds". How to formalize this?

The only way I was able to use `fintype V`

and `decidable_rel G.adj`

is when `V`

and `G`

are declared as variables such as in the definition of `some_property`

, but it seems that I can't use this approach in the statement of `some_theorem`

because this would give me the wrong order of the quantifiers:

```
section some_results
variables (V : Type un) [fintype V] (G : simple_graph V) [decidable_rel G.adj]
--this does compile, but it seems that it has the wrong order of the quantifiers
theorem some_theorem_incorrect :
forall (N : nat),
exists (M : nat),
some_property V G N M
:=
begin
sorry
end
end some_results
```

So, my second question: can you please confirm my understanding that the statement of `some_theorem_incorrect`

effectively means this: "for any `V`

that is finite and any graph `G`

on `V`

such that `G.adj`

is decidable, and for any natural `N`

, there exists a natural `M`

such that `some_property`

holds"? So, in this statement, `M`

can depend on the graph `G`

, right?

#### Patrick Johnson (Sep 19 2022 at 02:51):

```
theorem some_theorem :
forall (N : nat),
exists (M : nat),
forall (V : Type un) [hV : fintype V] (G : simple_graph V) [hG : decidable_rel G.adj],
@some_property V hV G hG N M
:=
begin
sorry
end
```

#### Mikhail Makarov (Sep 19 2022 at 05:27):

Ok, so in this case it compiles, but in my real more complex case, I still get an error when I use "@" before the property name and pass the instances explicitly. Here is the error:

```
synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
⁇
inferred
V_fintype
```

I will try to create a minimal reproducible example.

#### Mikhail Makarov (Sep 19 2022 at 05:31):

But in the meantime, can you explain why it didn't work with `some_property V G N M`

? Why can't Lean automatically detect the instances from the assumptions like it does from declared variables?

#### Eric Wieser (Sep 19 2022 at 07:27):

Searching zulip for `by exactI`

will find many other threads about this gotcha

Last updated: Dec 20 2023 at 11:08 UTC