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,
⊢ fintype V

failed to synthesize type class instance for
N M : ℕ,
V : Type un,
_inst_1 : fintype V,
G : simple_graph V,


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