induction Target occurs more than once

Stream: new members

[Jakub Nowak]

Can someone help me get around this error? Or even better, help me understand it so I can fix it myself. :)

import Mathlib

open SimpleGraph

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


private def odd_cycle_of_odd_walk_step [DecidableEq V] {u v : V}
    (pref : G.Walk u v) (suf : G.Walk v u) :
    Σ w : V, G.Walk w w :=
  match suf with
  | .nil => ⟨u, Walk.nil⟩ -- unreachable
  | .cons' v w u hAdj suf' =>
    if h : w ∈ pref.support then
      let pref_pre_part : G.Walk u w := pref.takeUntil w h
      let pref_cycle_part : G.Walk w v := pref.dropUntil w h
      let cycle : G.Walk v v := .cons hAdj pref_cycle_part
      if cycle.length.bodd then
        ⟨v, cycle⟩
      else
        odd_cycle_of_odd_walk_step pref_pre_part suf'
    else
      odd_cycle_of_odd_walk_step (pref.concat hAdj) suf'

private def odd_cycle_of_odd_walk [DecidableEq V] (p : G.Walk u u) : Σ v : V, G.Walk v v :=
  odd_cycle_of_odd_walk_step .nil p

theorem odd_cycle_of_odd_walk.is_odd_cycle [DecidableEq V] (p : G.Walk u u) (hOdd : p.length.bodd) :
    (odd_cycle_of_odd_walk p).snd.IsCycle ∧ (odd_cycle_of_odd_walk p).snd.length.bodd := by
  unfold odd_cycle_of_odd_walk
  induction p
  -- error:
  -- Invalid target: Target (or one of its indices) occurs more than once
  --   u

[Aaron Liu]

What do you want your induction hypothesis to be?

[Jakub Nowak]

Ah, right, I should have asked myself that. induction p doesn't really even makes sense here. The induction should be on the suf variable and the induction hypothesis should probably be pref.isPath → (pref.append suf).length.bodd → (odd_cycle_of_odd_walk_step pref suf).snd.isCycle ∧ (odd_cycle_of_odd_walk_step pref suf).snd.length.bodd to make the proof work.

[Aaron Liu]

and what is your goal in this case? I want to find out where p went

[Jakub Nowak]

The goal is (odd_cycle_of_odd_walk_step .nil p).snd.isCycle ∧ (odd_cycle_of_odd_walk_step .nil p).snd.length.bodd.

Which is the induction hypothesis with pref = .nil and suf = p.

[Aaron Liu]

I don't get it, what are pref and suf here?

[Aaron Liu]

are they free or bound?

[Aaron Liu]

maybe you can write out the type of the induction principle you want to use

[Jakub Nowak]

Like this I think:

(∀ {u v : V} (pref : G.Walk u v), pref.isPath → (pref.append .nil).length.bodd →
  (odd_cycle_of_odd_walk_step pref .nil).snd.isCycle ∧ (odd_cycle_of_odd_walk_step pref .nil).snd.length.bodd) →

(∀ {u v w : V} (pref : G.Walk u v) (h : G.Adj v w) (p : G.Walk w u), pref.isPath → (pref.append (.cons h p)).length.bodd →
  (odd_cycle_of_odd_walk_step pref (.cons h p)).snd.isCycle ∧ (odd_cycle_of_odd_walk_step pref (.cons h p)).snd.length.bodd) →

∀ {u : V} (pref : G.Walk u v) (p : G.Walk v u), pref.isPath → (pref.append p).length.bodd →

(odd_cycle_of_odd_walk_step pref p).snd.isCycle ∧ (odd_cycle_of_odd_walk_step pref p).snd.length.bodd

[Aaron Liu]

oh that doesn't look too bad

[Jakub Nowak]

After abstracting the goal away:

(∀ {u v : V} (pref : G.Walk u v), pref.isPath → (pref.append .nil).length.bodd → motive pref .nil) →

(∀ {u v w : V} (pref : G.Walk u v) (h : G.Adj v w) (p : G.Walk w u), pref.isPath → (pref.append (.cons h p)).length.bodd → motive pref (.cons h p)) →

∀ {u : V} (pref : G.Walk u v) (p : G.Walk v u), pref.isPath → (pref.append p).length.bodd →

motive pref p

[Jakub Nowak]

So to answer your question, pref is free and suf (which I renamed to p) is the target variable?

[Aaron Liu]

yeah I have some incantations which will get you that induction

[Jakub Nowak]

Got it working like this:

import Mathlib

open SimpleGraph

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


private def odd_cycle_of_odd_walk_step [DecidableEq V] {u v : V}
    (pref : G.Walk u v) (suf : G.Walk v u) :
    Σ w : V, G.Walk w w :=
  match suf with
  | .nil => ⟨u, Walk.nil⟩ -- unreachable
  | .cons' v w u hAdj suf' =>
    if h : w ∈ pref.support then
      let pref_pre_part : G.Walk u w := pref.takeUntil w h
      let pref_cycle_part : G.Walk w v := pref.dropUntil w h
      let cycle : G.Walk v v := .cons hAdj pref_cycle_part
      if cycle.length.bodd then
        ⟨v, cycle⟩
      else
        odd_cycle_of_odd_walk_step pref_pre_part suf'
    else
      odd_cycle_of_odd_walk_step (pref.concat hAdj) suf'

private def odd_cycle_of_odd_walk [DecidableEq V] (p : G.Walk u u) : Σ v : V, G.Walk v v :=
  odd_cycle_of_odd_walk_step .nil p

theorem odd_cycle_of_odd_walk_step.is_odd_cycle [DecidableEq V] (pref : G.Walk u v) (p : G.Walk v u)
    (hP : p.IsPath) (hOdd : (pref.append p).length.bodd) :
    (odd_cycle_of_odd_walk_step pref p).snd.IsCycle ∧ (odd_cycle_of_odd_walk_step pref p).snd.length.bodd := by
  induction p
  sorry

theorem odd_cycle_of_odd_walk.is_odd_cycle [DecidableEq V] (p : G.Walk u u) (hP : p.IsPath) (hOdd : p.length.bodd) :
    (odd_cycle_of_odd_walk p).snd.IsCycle ∧ (odd_cycle_of_odd_walk p).snd.length.bodd :=
  odd_cycle_of_odd_walk_step.is_odd_cycle .nil p (by simp_all) (by simp_all)

Couldn't get it work without helper function.

[Jakub Nowak]

MrQubo said:

After abstracting the goal away:

(∀ {u v : V} (pref : G.Walk u v), pref.isPath → (pref.append .nil).length.bodd → motive pref .nil) →

(∀ {u v w : V} (pref : G.Walk u v) (h : G.Adj v w) (p : G.Walk w u), pref.isPath → (pref.append (.cons h p)).length.bodd → motive pref (.cons h p)) →

∀ {u : V} (pref : G.Walk u v) (p : G.Walk v u), pref.isPath → (pref.append p).length.bodd →

motive pref p

That is wrong. That's just cases. .-. I forgot about induction hypothesis, this should be like this:

(∀ {u v : V} (pref : G.Walk u v), pref.isPath → (pref.append .nil).length.bodd → motive pref .nil) →

(∀ {u v w : V} (pref : G.Walk u v) (h : G.Adj v w) (p : G.Walk w u), pref.isPath → (pref.append (.cons h p)).length.bodd →
  (∀ {u : V} (pref : G.Walk u w), pref.isPath → (pref.append p).length.bodd → motive pref p) →
  motive pref (.cons h p)) →

∀ {u : V} (pref : G.Walk u v) (p : G.Walk v u), pref.isPath → (pref.append p).length.bodd →

motive pref p

[Aaron Liu]

I think this works?

theorem odd_cycle_of_odd_walk.is_odd_cycle [DecidableEq V] (p : G.Walk u u) (hOdd : p.length.bodd) :
    (odd_cycle_of_odd_walk p).snd.IsCycle ∧ (odd_cycle_of_odd_walk p).snd.length.bodd := by
  unfold odd_cycle_of_odd_walk
  rw [← p.nil_append] at hOdd
  let v := u
  set pref : G.Walk u v := .nil
  have hPath : pref.IsPath := .nil
  change G.Walk v u at p
  change (pref.append p).length.bodd = true at hOdd
  change (odd_cycle_of_odd_walk_step pref p).snd.IsCycle ∧
    (odd_cycle_of_odd_walk_step pref p).snd.length.bodd = true
  clear_value v pref
  induction p with
  | nil => sorry
  | cons h p ih => sorry

[Jakub Nowak]

Oh, that's interesting. I think, it's kinda the same as with helper function, just done more manually. The trick with let v := u and change looks like an useful way to resolve this "Target (or one of its indices) occurs more than once" error in other scenarios.

Thank you very much for your time!