Introduction and strange error

Stream: new members

[Albert Laforet]

Hello everyone,

I'm not sure this is where I'm supposed to write this, feel free to move the topic if it should. I recently started getting interested in lean/mathlib and after fiddling a bit I decided to start a basic implementation of unoriented multigraphs to learn more about it. Up until now, I've managed to deal with all the mistakes that came up but the last one I got is very strange. Basically, I'm trying to prove that if you have a walk (a sequence of vertices such that one vertice is linked to the following one by an edge) that goes from one vertice to another then you can find a path between them (basically the same as a walk, but which does not go through any vertice more than once). I am doing this constructively if that matters. I wrote several definitions and lemmas before proving this, and I am now writing this (please endure the awful code) :

theorem finite_graph.are_connected_path (v v' : F.V) (hs : F.simple) :
F.are_connected v v' ↔ ∃ p : F.path, p.start = v ∧ p.end = v' :=
begin
  split,swap,
  {
    rintro ⟨p,hp⟩,
    use p.to_walk,
    exact hp,
  },
  {
    intro h,
    cases h with w hw,
    haveI : inhabited F.V := ⟨v⟩,
    have hwl := F.list_gives_walk_from_walk w,
    have hwn := w.nempty_lᵥ,
    have hs1 := rmv_head w.lᵥ hwn,
    unfold finite_graph.walk.start finite_graph.walk.end at hw,
    cases hw with hw1 hw2,
    rw [← hw1,←  hw2],
    clear hw1 hw2 v v',
    constructor,
    swap,
    {
      exact { lᵥ := rmv_unt w.lᵥ,
      lₑ := F.get_list_edges hs (rmv_unt w.lᵥ) (F.rmv_unt_gives_walk w.lᵥ hwl),
      is_adj :=
      begin
        have hu := finite_graph.inc_prop_from_list_vertices (rmv_unt w.lᵥ)
        (F.rmv_unt_gives_walk w.lᵥ hwl) hs,
        cases hu with p hp,
        exact p,
      end,
      vertex_unicity := rmv_nodup w.lᵥ,
      is_open :=
      begin
        unfold finite_graph.walk.closed finite_graph.path.start finite_graph.path.end,
        unfold finite_graph.walk.start finite_graph.walk.end,
        push_neg,
        apply nodup_head_eq_tail_length_1,
        exact rmv_nodup w.lᵥ,
      end },
    },
    split,
    {
      cases hs,
      dsimp at *,
      unfold finite_graph.path.start finite_graph.walk.start,
      simp,
      rw ← rmv_head,
      refl,
    }

  }
end

This last refl gives me the following error :

invalid apply tactic, failed to unify
  w.lᵥ.head = w.lᵥ.head
with
  ?m_2 = ?m_2

which seems very weird to me. Does anyone know why this happens, and how I can solve it ? Here is a link to the two files that I use with all my definitions if it is needed : https://github.com/Junkyards3/lean_graphs . Thanks in advance !

[Eric Wieser]

Your git repo suggests you're not using leanproject, which means that your code doesn't specify which version of mathlib it needs. Can I suggest you run leanproject new in your project and commit the resulting leanpkg.toml?

[Bryan Gin-ge Chen]

This also doesn't answer your question, but note that there are have been some previous discussions on Zulip about proving that two vertices connected by a walk are also connected by a path: https://leanprover.zulipchat.com/#narrow/stream/252551-graph-theory/topic/Construct.20path.20from.20walk.3F/near/219041776

cc: @Kyle Miller

[Eric Rodriguez]

In zulip, we also try and get #mwe for all issues, as this makes everyone's jobs easier. However, I did toy with your code and it's as I suspected; there's some instance hidden there that's messing up with it

[Eric Rodriguez]

in this case, there's two different [inhabited] instances, so you can try convert rfl to see where you differ

[Eric Rodriguez]

every time you see invalid apply tactic and a pattern that look like it matches, you should start looking at instances + implicits in my experience

[Albert Laforet]

It was indeed the problem, I didn't know that different instances led to different data (I thought that once instances existed, they were "the same", as in, their only use is existing). I guess I should read a bit more on how instances actually work. Thanks !
Also, I do use leanproject and have leanpkg.toml. I just uploaded my files to github really fast without using the actually good machinery... I should learn to use it

[Eric Rodriguez]

Prop instances are like that. Anything that lives in Type* has data that has to be compared :) in inhabited's case, it actually defines a "default" element, so it's certainly not true that they're always equal!

[Kyle Miller]

In case you want to take a look, here's an un-merged branch that deals with walks and paths for simple graphs -- the approach would be essentially the same for multigraphs. This in particular is the function that converts walks to paths: https://github.com/leanprover-community/mathlib/blob/affa4bf4bdcd51ee2298d0aff9c7ca74a6a97802/src/combinatorics/simple_graph/connectivity.lean#L813

It uses a custom type for walks rather than lists, but the hope is that there are enough definitions and lemmas to connect the theory up to list when convenient.