Turan's theorem rewrite error

Stream: graph theory

[John Talbot]

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 α}
[decidable_eq α][decidable_rel G.adj][decidable_rel H.adj]

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
  decidable_rel _a.adj
-/

/-
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 α,
_inst_4 : decidable_rel G.adj,
_inst_5 : decidable_rel H.adj,
h : G = H
⊢ G.edge_finset = H.edge_finset
-/
end

[Yaël Dillies]

Try simp_rw

[Kevin Buzzard]

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]

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

[John Talbot]

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

[Kevin Buzzard]

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]

Ah ok, thanks I'll look at this.

[Kevin Buzzard]

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]

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
--[decidable_eq α][decidable_rel G.adj][decidable_rel H.adj]

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

[John Talbot]

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.

[Yaël Dillies]

Hey, @John Talbot! Did you ever finish your formalisation of Turán's theorem?

[John Talbot]

Yes I finished it about a year ago, but it was my first attempt at learning Lean so it's not pretty!
https://github.com/jt496/extremal_graph

[John Talbot]

I also ported it to Lean4 a few months back (part of my attempt to learn Lean4). I've just updated that and made it public:
https://github.com/jt496/Turan_4

[Yaël Dillies]

Nice! I've actually been golfing your proof over at https://github.com/YaelDillies/LeanTuran. The idea is to then port the golfed version to Lean 4 and PR it to mathlib.

[John Talbot]

Great!