Problem with inductive definition

Stream: new members

[Jérémie Turcotte]

Hi, I wrote the following code to get a subwalk of a walk, using the definitions in simple_graph.connectivity path of mathlib. However, I get error "equation compiler failed to generate bytecode for 'subwalk._main'
nested exception message:
code generation failed, VM does not have code for 'classical.choice'" I tried adding noncomputable before the def, but then I get "failed to prove recursive application is decreasing, well founded relation..." What should I do? Am I doing the induction wrong?

Thanks alot!

def subwalk : Π {u v w : V} (p:G.walk u v) (hw : w ∈ p.support), G.walk w v
| u v w nil hw := by rw mem_support_nil_iff.1 hw
| u v w (cons h p) hw :=
begin
  by_cases h2 : u=w,
  {
    rw <- h2,
    exact (cons h p),
  },
  {
    rw support at hw,
    have := list.eq_or_ne_mem_of_mem hw,
    suffices hp:w∈ p.support,
    {
      exact subwalk p hp,
    },
    {
      finish,
    }
  }
end

[Yakov Pechersky]

Since you're constructing data, I suggest you do something like

u v w (cons h p) hw := if (h2 : u = w) then (h2 ▸ cons h p) else _

[Yakov Pechersky]

by_cases is using classical reasoning to generate the hypotheses and case-split for you, which makes it noncomputable. Regarding setting noncomputable leading to a well-founded recursion problem, it's possible that finish is somehow calling the nascent subwalk and that confuses the equation compiler.

[Jérémie Turcotte]

Oh thank you, I hadn't realized the issue was coming from the finish, since the error was underlining in red the subwalk appearing higher in the proof, but that was indeed the issue. Thanks! As for your first comment, is there a specific advantage of working like that instead of in tactic mode exactly when building data?

[Yakov Pechersky]

In general, tactic mode can create terms that are unfriendly for definitional equalities and complicate computation

[Yakov Pechersky]

Unless you use a very particular subset of tactics like intro, refine, exact, have etc

[Jérémie Turcotte]

Ok thanks!

[Yakov Pechersky]

One sec, I'll have an example for you of what to do

[Yakov Pechersky]

I was mistaken about using the ▸, that is only for propositions

[Yakov Pechersky]

Ah, and the WF recursion isn't the finish, it's your reference of subwalk in the suffices

[Yakov Pechersky]

I suggest looking at src#simple_graph.walk.drop_until:

/-- Given a vertex in the support of a path, give the path from (and including) that vertex to
the end. In other words, drop vertices from the front of a path until (and not including)
that vertex. -/
def drop_until : Π {v w : V} (p : G.walk v w) (u : V) (h : u ∈ p.support), G.walk u w
| v w nil u h := by rw mem_support_nil_iff.mp h
| v w (cons r p) u h :=
  if hx : v = u
  then by { subst u, exact cons r p }
  else drop_until p _ $ h.cases_on (λ h', (hx h'.symm).elim) id

[Yakov Pechersky]

Because that's exactly what you want:

def subwalk [decidable_eq V] {u v w : V} (p : G.walk u v) (hw : w ∈ p.support) : G.walk w v :=
p.drop_until _ hw