type mismatch in match

Stream: new members

[Jakub Nowak]

Hi!
Why is there a type mismatch at line 15 in match? I cannot understand this error. :<

import Mathlib

open SimpleGraph

universe u
variable {V : Type u} {G : SimpleGraph V} {u v : V}

abbrev SimpleGraph.Cycle (u : V) := { p : G.Walk u u // p.IsCycle }

private def SimpleGraph.Walk.extract_Cycle (p : G.Walk u u) :
    Σ' (v : V) (fst : G.Walk u v) (mid : G.Cycle v) (lst : G.Walk v u),
      p = (fst.append mid).append lst :=
  let rec step {v : V} (fst : G.Path u v) (rest : G.Walk v u) (h : p = fst.val.append rest) : _ :=
    match rest with
    | nil => _
    | cons _ _ => _
  step Path.nil p (by simp)

[Kenny Lau]

Please use #backticks to include your code here. It will also automatically generate a link to Lean 4 Web (click on the top right corner of the code block)

[Jakub Nowak]

Kenny Lau said:

Please use #backticks to include your code here. It will also automatically generate a link to Lean 4 Web (click on the top right corner of the code block)

Ah, I didn't notice it generates the link to playground too. Thanks!

[Jakub Nowak]

Maybe lean cannot unify v with u because u is argument of SimpleGraph.Walk.extract_Cycle and v is argument of step? Not sure if it's a bug, or is this kind of unification impossible?

[Kenny Lau]

ah, that's the reason

[Kenny Lau]

so to solve this you'll have to match all of the other dependent variables too:

import Mathlib

open SimpleGraph

universe u
variable {V : Type u} {G : SimpleGraph V} {u v : V}

abbrev SimpleGraph.Cycle (u : V) := { p : G.Walk u u // p.IsCycle }

private def SimpleGraph.Walk.extract_Cycle (p : G.Walk u u) :
    Σ' (v : V) (fst : G.Walk u v) (mid : G.Cycle v) (lst : G.Walk v u),
      p = (fst.append mid).append lst :=
  let rec step {v : V} (fst : G.Path u v) (rest : G.Walk v u) (h : p = fst.val.append rest) : _ :=
    match u, v, rest, p, fst, h with
    | _, _, nil, p, fst, h => _
    | _, _, cons _ _, p, fst, h => _
  step Path.nil p (by simp)

[Jakub Nowak]

Hmm, from reading the source of match elabolator there was some code that was supposed to pull in dependant variables. Is it that it doesn't work in this case?