## Stream: graph theory

### Topic: Turan's theorem rewrite error

#### John Talbot (Aug 04 2022 at 11:52):

While proving Turan's theorem I had a problem with rewriting that I think is captured by the example below.

I managed to work around it but I'd like to understand what I'm doing wrong. (Probably something very basic..)

In particular, why does the 1st lemma below work fine while the 2nd fails?

(Anyone interested in seeing the longest known proof of Turan's theorem can find it here:
https://github.com/jt496/extremal_graph/blob/master/src/theorems.lean )

import combinatorics.simple_graph.basic
open simple_graph
variables {α : Type*} {G H : simple_graph α}[fintype α][nonempty α]{s : finset α}

set_option trace.check true

lemma no_error (h: G = H): G.edge_set = H.edge_set :=
begin
rwa h,
end

lemma error (h: G = H): G.edge_finset = H.edge_finset :=
begin
rwa h,
/-
[check] application type mismatch at
_a.edges_fintype
argument type
Π (a b : α), decidable (G.adj a b)
expected type
-/

/-
rewrite tactic failed, motive is not type correct
λ (_a : simple_graph α), G.edge_finset = H.edge_finset = (_a.edge_finset = H.edge_finset)
state:
α : Type u_1,
G H : simple_graph α,
_inst_1 : fintype α,
_inst_2 : nonempty α,
_inst_3 : decidable_eq α,
h : G = H
⊢ G.edge_finset = H.edge_finset
-/
end


#### Yaël Dillies (Aug 04 2022 at 11:54):

Try simp_rw

#### Kevin Buzzard (Aug 04 2022 at 12:02):

That doesn't work either, and neither does simp only. Furthermore subst doesn't work because _inst_5 is frozen! This works:

lemma fixed_error (h: G = H): G.edge_finset = H.edge_finset :=
begin
unfreezingI {subst h},
congr',
end


I guess you need congr' rather than refl because Lean doesn't know that the two instances of decidable_rel are definitionally equal.

#### Kevin Buzzard (Aug 04 2022 at 12:04):

@John Talbot those proofs look lovely to me -- you should look at some of the long proofs my undergraduates produce!

#### John Talbot (Aug 04 2022 at 12:06):

Thanks both! What should I be reading to understand this stuff properly?

#### Kevin Buzzard (Aug 04 2022 at 12:06):

finset is constructive finiteness and this might be part of the problem. There is set.finite which is another way to assert finiteness of a set; set.finite is a Prop whereas finset is data.

#### John Talbot (Aug 04 2022 at 12:08):

Ah ok, thanks I'll look at this.

#### Kevin Buzzard (Aug 04 2022 at 12:13):

What is going on is that because finset is constructive, simple_graph.edge_finset is demanding a constructive proof of finiteness (i.e. data, not a proposition) from the type class inference system, hence all this wacky decidable_stuff. One of the things Lean is griping about is that you have assumed that there's an algorithm which decides whether two vertices in G are equal, and you've assumed that there's an algorithm which decides whether two vertices in H are equal, and then you've assumed that G and H are equal, but you haven't assumed that the algorithms are equal. This is the kind of price you pay when doing constructive mathematics.

#### Kevin Buzzard (Aug 04 2022 at 12:14):

import combinatorics.simple_graph.basic
open simple_graph
variables {α : Type*} {G H : simple_graph α}[fintype α][nonempty α]{s : finset α}

-- Let's work in classical mathematics
open_locale classical

-- now we don't need any of this stuff

-- and this now works fine
lemma error (h: G = H): G.edge_finset = H.edge_finset :=
begin
rwa h,
end


#### John Talbot (Aug 04 2022 at 12:19):

Thanks, that makes a lot of sense. I have to admit I quite enjoy the wacky decidable_stuff but its good to see an easy workaround.

Last updated: Aug 03 2023 at 10:10 UTC