How to simplify a function that uses inductionOn?

Stream: new members

[Vivek Rajesh Joshi]

How do I simplify indNonzElt int he goal for this theorem?

def indNonzElt (v : Vector Rat k) : Option {idx : Fin k // v.get idx ≠ 0} :=
  v.inductionOn
  (none)
  (fun _ {x} => fun
  | none => if h:x=0 then none else some ⟨0,by simp [h]⟩
  | some idx => if h:x=0 then some ⟨idx.1.succ.cast (by simp),by simp [idx.2]⟩ else some ⟨0,by simp [h]⟩)

theorem indNonzElt_cons_0_none (v : Vector Rat k) (hv : indNonzElt v = none) :
  indNonzElt (Vector.cons 0 v) = none := by

I've tried unfold, simp [indNonzElt], and rw [indNonzElt], but none of them have worked.

[Yakov Pechersky]

When you define a function using a recursor like in your case, you should also use the recursor in your proof.

[Yakov Pechersky]

For example, check out the code for docs#List.foldrRecOn_nil

[Yakov Pechersky]

For the simple lemmas first

[Yakov Pechersky]

You should prove what it means to indNonzElt on an empty vector first. And then what it means to do it to a non empty vector with arbitrary value. Then create an iff statement relating what it means to have indNonzElt produce a none.

[Yakov Pechersky]

Your function definition can likely be refactored by pulling the dite outside of the casing on the inductive case Option. Not sure if that makes it easier to prove things about it not

[Yakov Pechersky]

Because then you can use Option.map and Fin.succ iiuc

[Yakov Pechersky]

Regarding your direct problem about rw not working, try generalizing your vector expression out.

[llllvvuu]

It's much easier with an API lemma for Vector.inductionOn:

import Mathlib.Data.Vector.Basic

-- def indNonzElt (v : Vector Rat k) : Option {idx : Fin k // v.get idx ≠ 0} :=
--   v.inductionOn none
--   fun _ {x} _ a => if h : x ≠ 0 then some ⟨0, h⟩ else a.map fun idx => ⟨idx.1.succ, idx.2⟩

def indNonzElt (v : Vector Rat k) : Option {idx : Fin k // v.get idx ≠ 0} :=
  v.inductionOn
  (none)
  (fun _ {x} => fun
  | none => if h:x=0 then none else some ⟨0,by simp [h]⟩
  | some idx => if h:x=0 then some ⟨idx.1.succ.cast (by simp),by simp [idx.2]⟩ else some ⟨0,by simp [h]⟩)

def Vector.inductionOn_cons {C : ∀ {n : ℕ}, Vector α n → Sort*} {n : ℕ} (x : α) (v : Vector α n)
    (h_nil : C nil) (h_cons : ∀ {n : ℕ} {x : α} {w : Vector α n}, C w → C (x ::ᵥ w)) :
    (x ::ᵥ v).inductionOn h_nil h_cons = h_cons (v.inductionOn h_nil h_cons : C v) := by
  rfl

theorem indNonzElt_cons_0_none (v : Vector Rat k) (hv : indNonzElt v = none) :
    indNonzElt (Vector.cons 0 v) = none := by
  induction v using Vector.inductionOn
  · rfl
  rw [indNonzElt, Vector.inductionOn_cons, ← indNonzElt, hv]
  rfl

I also included in the comment, a simplified version of your def, and if you switch to that the proof still works and runs a bit faster

I'll make a PR for this API lemma (edit: #13616)

[Vivek Rajesh Joshi]

Thanks a lot!