using instances for a graph introduced in a statement

Stream: new members

[Mikhail Makarov]

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]

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]

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]

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]

Searching zulip for by exactI will find many other threads about this gotcha