Zulip Chat Archive

Stream: new members

Topic: Problem with inductive definition

Jérémie Turcotte (Oct 24 2022 at 04:53):

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 :=
  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,

Yakov Pechersky (Oct 24 2022 at 04:56):

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 (Oct 24 2022 at 04:59):

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 (Oct 24 2022 at 05:05):

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 (Oct 24 2022 at 05:09):

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

Yakov Pechersky (Oct 24 2022 at 05:09):

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

Jérémie Turcotte (Oct 24 2022 at 05:10):

Ok thanks!

Yakov Pechersky (Oct 24 2022 at 05:11):

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

Yakov Pechersky (Oct 24 2022 at 05:11):

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

Yakov Pechersky (Oct 24 2022 at 05:13):

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

Yakov Pechersky (Oct 24 2022 at 05:14):

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 (Oct 24 2022 at 05:15):

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

Last updated: Dec 20 2023 at 11:08 UTC