Track no. of recursive calls

Stream: new members

[Vivek Rajesh Joshi]

import Mathlib.Data.Matrix.Notation

variable {F : Type} [Field F] [DecidableEq F]

def Vector.any {F : Type} (v : Vector F n) (p : F → Bool) := v.toList.any p

@[simp] theorem Vector.any_def (v : Vector F n) (p : F → Bool) : v.any p = v.toList.any p := rfl

def Vector.firstNonzElt {F : Type} [Field F] [DecidableEq F] (v : Vector F n) (h: v.any (· ≠ 0)) : {x:F // x≠0}×(i : Fin n)×(Vector F (n-i-1)) :=
  match v with
  | ⟨[],hv⟩ => by simp at h
  | ⟨x::ys,ha⟩ =>
    have hn : n > 0 := by rw [← ha]; simp
    if hx:x ≠ 0
    then (⟨x, hx⟩, ⟨⟨0,hn⟩,⟨ys,by simp_rw [← ha];simp⟩⟩)
    else
      by
      have ys_nontriv: ys.any (· ≠ 0) := by
        simp at hx
        simp [List.any_cons, hx] at h
        simp [h]
      let (value, ⟨index, tail⟩) := firstNonzElt (⟨ys,by simp at ha; rw [← ha]; simp⟩ : Vector F (n-1)) ys_nontriv
      exact (value, ⟨index.succ.cast (by simp [Nat.sub_add_cancel hn]),tail.congr (by simp [Nat.Simproc.sub_add_eq_comm n (↑index) 1])⟩)

abbrev Vector.allZero (v : Vector F n) := v.toList.all (.=0)

lemma Vector.allZero_not_anyN0 (v : Vector F n) : ¬ v.allZero ↔ v.any (.≠0) := by
  constructor <;> (intro hv;simp at hv ⊢; exact hv)

def findPivotAuxN0 (l : List (Vector F m)) (hl : l.any (fun c => ¬c.allZero)) (j : Nat) : {c : F // c≠0}×(Fin m)×(Nat) :=
    match l with
    | [] => by simp at hl
    | col::as =>
      if hc : ¬ (col.allZero) then
        let ⟨piv,rowInd,_⟩ := (col.firstNonzElt (col.allZero_not_anyN0.mp (by simp at hc ⊢; exact hc)))
        (piv,rowInd,0)
      else
        by
        have as_nontriv: as.any (fun c => ¬c.allZero) := by
          simp at hc
          simp [List.any_cons, hc] at hl
          rcases hl with hl|hl
          · rcases hl with ⟨x,xc,hx⟩; have := hc x xc; contradiction
          · simp [hl]
        let (piv,rowInd,colInd) := findPivotAuxN0 as as_nontriv j
        exact (piv,rowInd,colInd+1)

Any way to show that the Nat output for findPivotAuxN0 is always less than the length of the list? The only way I can think of is to show that the function cannot be recursively called more than l.length+1 times, but I don't know how to prove that. Is there any other way?

[Arthur Adjedj]

You can prove this by induction over your list l:

example (l : List (Vector F m)) (hl : l.any (fun c => ¬c.allZero)) (j : Nat) : (findPivotAuxN0 l hl j).2.2 ≤ l.length := by
  induction l with
  | nil => simp [List.any] at hl
  | cons h tl tl_ih =>
    dsimp [findPivotAuxN0]
    split <;> simp
    apply tl_ih

[Vivek Rajesh Joshi]

Great, thanks!

[Vivek Rajesh Joshi]

Okay, I realised that my problem was different. I want to use j as a term of type Fin n in the function itself, and want to show that in the col::as case of match l, l.get j = col. Any way to show this?

[Bbbbbbbbba]

If l matches col :: as, should't it be l.get 0 = col?

[Vivek Rajesh Joshi]

Right, sorry. That's not what I meant, I mean that I need a way to show that in the kth recursive call of the function (when the j argument takes on the value k), the value of col is the kth element of the list I'm inducting over.
In case that too is wrong, I'll just state my objective: I want the index of the vector containing c, and I want to show that if I extract the element at that index from l, it will contain c.