Zulip Chat Archive

Stream: general

Topic: symmetry fails if simple graph is imported


view this post on Zulip Bhavik Mehta (Mar 08 2021 at 03:27):

Here's my example:

import combinatorics.simple_graph.basic

example : true  true :=
begin
  symmetry,
end

fails with the error

invalid apply tactic, failed to unify
  true  true
with
  ?m_2.adj ?m_3 ?m_4  ?m_2.adj ?m_4 ?m_3

and doesn't fail without the import.
Presumably this is from the symm attribute on simple_graph.edge_symm - should this be removed?

view this post on Zulip Kyle Miller (Mar 08 2021 at 06:13):

Yes, that attribute should be removed. There are no uses of symmetry when it comes to simple_graph.adj, but if it were somehow useful a fix would be to have a lemma that's an implication rather than a bi-implication:

@[symm] lemma edge_symm' (u v : V) : G.adj u v  G.adj v u := λ x, G.sym x

view this post on Zulip Bhavik Mehta (Mar 17 2021 at 16:11):

Done both in #6736


Last updated: May 14 2021 at 12:18 UTC