Zulip Chat Archive

Stream: general

Topic: symmetry fails if simple graph is imported

Bhavik Mehta (Mar 08 2021 at 03:27):

Here's my example:

import combinatorics.simple_graph.basic

example : true  true :=

fails with the error

invalid apply tactic, failed to unify
  true  true
  ?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?

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

Bhavik Mehta (Mar 17 2021 at 16:11):

Done both in #6736

Last updated: Dec 20 2023 at 11:08 UTC