Manipulate function containing inductionOn

Stream: new members

[Vivek Rajesh Joshi]

I have this function defined using Vector.inductionOn:

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]⟩)

I want to use the induction hypotheses (like having h1 : v=[] -> indNonzElt v = none for the base case and similarly for the inductive case) to write a proof with this function. What tactics or proof terms can I use to do so?

[llllvvuu]

(note: missing line for #mwe is import Mathlib.Data.Vector.Basic)

Can you write the statements you are trying to prove? h1 : v=[] is not a valid premise as it does not handle the indexed family

[Vivek Rajesh Joshi]

This is basically what I want to prove:

example (v : Vector Rat k) (h : ∃ x ∈ v.toList, x≠0) : (indNonzElt v).isSome = true := by

But I don't know how to use the inductive nature of the function to my advantage here

[Vivek Rajesh Joshi]

Anyone has any suggestions for this?

[llllvvuu]

Using the API lemma mentioned in the other thread:

import Mathlib.Data.Vector.Basic

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

example (v : Vector Rat k) (h : ∃ x ∈ v.toList, x≠0) : (indNonzElt v).isSome = true := by
  induction v using Vector.inductionOn with
  | h_nil => simp at h
  | @h_cons n x v ih =>
    rw [indNonzElt, Vector.inductionOn_cons, ← indNonzElt]
    split_ifs with h0
    · obtain ⟨y, y_mem, hy⟩ := h
      obtain rfl | y_mem : y = x ∨ y ∈ v.toList := by simpa using y_mem
      · contradiction
      · specialize ih ⟨y, y_mem, hy⟩
        cases hv : indNonzElt v
        · simp [hv] at ih
        · rfl
    · cases indNonzElt v <;> rfl

The proof is probably easier if you use the simplified def from that other thread. I leave that as an exercise.

I also recommend as part of your indNonzElt API that you package this step as a lemma: rw [indNonzElt, Vector.inductionOn_cons, ← indNonzElt].