Induction over list while keeping info about list

Stream: new members

[Vivek Rajesh Joshi]

Suppose I have some special kind of list, for example a list with all zeros. I want to prove some property about it using induction. How do I do so without losing information about the special property that the list has?
Please don't consider this as #xy, this is literally the only thing I need right now to finish a proof I'm working on. Making an mwe will be hard since the content is spread across two files, but I'll try to get it ready soon.

[Filippo A. E. Nuccio]

It is difficult to give an abstract answer without an example. At any rate you might want to transform your "special kind" into a predicate P : List α -> Prop and to prove that your result holds for all lists satisfying P.

[Yakov Pechersky]

If you have the hypothesis that P l, the tactic "induction l" will properly destruct the list in the hypothesis as well. And the actual induction hypothesis will need you to prove that if P tail, then P head :: tail

[Vivek Rajesh Joshi]

import Mathlib.Data.Matrix.Notation
import Mathlib.Data.Matrix.Basis

abbrev colVecofMat (M : Matrix (Fin m) (Fin n) F) := (Vector.ofFn M.transpose).map Vector.ofFn

variable (F : Type) [Field F] [DecidableEq F] [Repr F]
variable (M : Matrix (Fin m) (Fin n) Rat) (hm : m>0) (hn : n>0)

def Vector.Mem (a : α) : Vector α n → Prop := fun v => v.toList.Mem a

instance : Membership α (Vector α n) where
  mem := Vector.Mem

instance [DecidableEq α] (a : α) (v : Vector α n) : Decidable (a ∈ v) :=
  inferInstanceAs <| Decidable (a ∈ v.toList)

structure ReducedRow (n : Nat) where
  z : Option (Fin n)
  k : Nat
  tail : Vector F k
  h : (hz : z = some p) → n = p + k + 1

def zeroVec (k: Nat) : Vector F k := Vector.replicate k 0

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

def botRightij (i : Fin m) (j : Fin n) : Matrix (Fin (m-i)) (Fin (n-j)) Rat :=
  M.submatrix (fun k => ⟨k+i,Nat.add_lt_of_lt_sub k.2⟩) (fun l => ⟨l+j,Nat.add_lt_of_lt_sub l.2⟩)

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 findPivot_ij (i : Fin m) (j : Fin n) : Option ((Fin m)×{c : Rat // c≠0}×(Fin m)×(Fin m)) :=
  findPivotAux (colVecofMat (botRightij M i j)).toList where
  findPivotAux (l : List (Vector Rat (m-i))) : Option ((Fin m)×{c : Rat // c≠0}×(Fin m)×(Fin m))  :=
    match l with
    | [] => none
    | col::as => match (indNonzElt col) with
      | none => findPivotAux as
      | some idx =>
          some (i,⟨(1/col.get idx),(one_div_ne_zero idx.2)⟩,i,(idx.1.castLT (Fin.val_lt_of_le idx.1 (Nat.sub_le m ↑i)) + i))

example : findPivot_ij 0 i j (m:=m) (n:=n) = none := by
  dsimp [findPivot_ij]
  set l':=(colVecofMat (botRightij 0 i j)).toList with hl
  induction l' with
  | nil => simp [findPivot_ij.findPivotAux]
  | cons a l ih =>
    have ha : a.allZero := by
      simp [botRightij] at hl
      have h1 : Vector.ofFn (0:Fin (m - ↑i) → ℚ) = zeroVec Rat (m-i.1) := by
        simp [zeroVec,Vector.eq_iff,Vector.replicate]
        rw [← List.ofFn_const (m-i.1) 0]
        rfl
      rw [Function.const_def,List.ofFn_const] at hl
      have h2 : a ∈ List.replicate (n - ↑j) (Vector.ofFn 0) := by
        apply List.mem_of_mem_head?
        simp [hl]
      have h3 : a = Vector.ofFn (fun x => 0) := by convert (List.mem_replicate.mp h2).2
      rw [Vector.allZero]
      rw [Vector.ofFn_const] at h3
      simp [h3]
      intro x xv
      rw [← Vector.mem_def,Vector.mem_replicate] at xv
      exact xv.2
    rw [findPivot_ij.findPivotAux]
    simp [indNonzElt_allZero _ ha]

I need ha : a \in l' as a hypothesis here while keeping the induction hypothesis as it is (which is why I can't use dependent induction)

[Vivek Rajesh Joshi]

What can I do to show that a is an allZero vector?

[Eric Wieser]

Are you looking for induction' h : l?

[Bbbbbbbbba]

Could you point me to the documentation for induction'?

[Vivek Rajesh Joshi]

Eric Wieser said:

Are you looking for induction' h : l?

I tried it, and it messes up the induction hypothesis. Anyways, I wanted some advice on how to work with dependent induction, since every time I've tried it it has led to nowhere; how do you make do of the induction hypothesis that comes up with induction' h : l?

[Vivek Rajesh Joshi]

Vivek Rajesh Joshi said:

What can I do to show that a is an allZero vector?

Any help regarding this would be greatly appreciated

[Shreyas Srinivas]

Could you post an #mwe please

[Shreyas Srinivas]

This is currently way too much code to read.

[Vivek Rajesh Joshi]

Unfortunately, that is in fact an #mwe. That's how much context I need to provide for my function to find the pivot of a matrix, and I don't think there's much room for improvement. Although the one above is riddled with errors, so I have made a new one, but it is even longer:

import Mathlib.Data.Matrix.Notation
import Mathlib.Data.Matrix.Basis

abbrev colVecofMat (M : Matrix (Fin m) (Fin n) F) := (Vector.ofFn M.transpose).map Vector.ofFn

theorem Vector.eq_iff (a1 a2 : Vector α n) : a1 = a2 ↔ toList a1 = toList a2 := by
  constructor
  intro h; rw [h]
  intro h; exact Vector.eq _ _ h

-- theorem Function.const_def {α : Sort u} (β : Sort v) (a : α) :
--   Function.const β a = fun _ => a := rfl

theorem Vector.ofFn_const :  ∀ (n : ℕ) (c : α), (Vector.ofFn fun _ : Fin n => c) = Vector.replicate n c := by
  intro n c
  rw [Vector.eq_iff]
  simp [Vector.replicate]

variable (F : Type) [Field F] [DecidableEq F] [Repr F]
variable (M : Matrix (Fin m) (Fin n) Rat) (hm : m>0) (hn : n>0)

def Vector.Mem (a : α) : Vector α n → Prop := fun v => v.toList.Mem a

instance : Membership α (Vector α n) where
  mem := Vector.Mem

instance [DecidableEq α] (a : α) (v : Vector α n) : Decidable (a ∈ v) :=
  inferInstanceAs <| Decidable (a ∈ v.toList)

structure ReducedRow (n : Nat) where
  z : Option (Fin n)
  k : Nat
  tail : Vector F k
  h : (hz : z = some p) → n = p + k + 1

def zeroVec (k: Nat) : Vector F k := Vector.replicate k 0

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

def botRightij (i : Fin m) (j : Fin n) : Matrix (Fin (m-i)) (Fin (n-j)) Rat :=
  M.submatrix (fun k => ⟨k+i,Nat.add_lt_of_lt_sub k.2⟩) (fun l => ⟨l+j,Nat.add_lt_of_lt_sub l.2⟩)

theorem Vector.mem_def (v : Vector α n) : a ∈ v ↔ a ∈ v.toList := Iff.rfl

lemma Vector.replicate_zero (a : α) : Vector.replicate 0 a = Vector.nil := rfl

theorem Vector.mem_cons {a b : α} {l : Vector α n} : a ∈ (Vector.cons b l) ↔ a = b ∨ a ∈ l := by
  constructor
  intro h
  simp [Vector.mem_def] at h
  rcases h with h|h; left; assumption; right; simp [Vector.mem_def,h]
  intro h; rcases h with h|h ; simp [Vector.mem_def,h]; rw [Vector.mem_def] at h ⊢; simp [h]

theorem Vector.mem_replicate {a b : α} : ∀ {n}, b ∈ Vector.replicate n a ↔ n ≠ 0 ∧ b = a
  | 0 => by simp [Vector.replicate_zero,Vector.mem_def]
  | n+1 => by simp [Vector.mem_cons,Vector.mem_replicate]

def Vector.indNonzElt {F : Type} [Field F] [DecidableEq F] (v : Vector F 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⟩

lemma Vector.replicate_toList : (Vector.replicate n c).toList = List.replicate n c := by rfl

lemma Vector.mem_replicate' : ∀ x ∈ (Vector.replicate n c).toList, x = c := by
  intro x hx
  rw [← Vector.mem_def,Vector.mem_replicate] at hx
  exact hx.2

theorem Vector.allZero_eq_replicate0 (v : Vector F n) : v.allZero ↔ v = Vector.replicate n 0 := by
  constructor
  · intro hv
    rw [allZero] at hv
    simp at hv
    rw [Vector.eq_iff,replicate_toList]
    refine List.eq_replicate.mpr ⟨v.toList_length,hv⟩
  · intro hv
    rw [hv,allZero]
    simp
    exact mem_replicate'

theorem Vector.cons_eq_cons {a b : α} {v v' : Vector α n} : v.cons a = v'.cons b ↔ a = b ∧ v = v' := by
  obtain ⟨l,_⟩ := v
  obtain ⟨l',_⟩ := v'
  simp [Vector.cons,Vector.eq_iff]

theorem Vector.indNonzElt_cons_0_none {F : Type} [Field F] [DecidableEq F] (v : Vector F k) (hv : v.indNonzElt = none) :
  (Vector.cons 0 v).indNonzElt = none := by
  induction' v using Vector.inductionOn
  · simp [Vector.indNonzElt]
  · rw [Vector.indNonzElt,Vector.inductionOn_cons,← Vector.indNonzElt]
    simp [hv]

lemma Vector.indNonzElt_allZero (v : Vector F k) (h : v.allZero) : v.indNonzElt = none := by
  rw [Vector.allZero_eq_replicate0] at h
  induction' v using Vector.inductionOn with p a w ih
  · rfl
  · simp [Vector.cons_eq_cons] at h
    rw [h.1]
    rw [indNonzElt_cons_0_none]
    exact ih h.2


def findPivot_ij (i : Fin m) (j : Fin n) : Option ((Fin m)×{c : Rat // c≠0}×(Fin m)×(Fin m)) :=
  findPivotAux (colVecofMat (botRightij M i j)).toList where
  findPivotAux (l : List (Vector Rat (m-i))) : Option ((Fin m)×{c : Rat // c≠0}×(Fin m)×(Fin m))  :=
    match l with
    | [] => none
    | col::as => match (Vector.indNonzElt col) with
      | none => findPivotAux as
      | some idx =>
          some (i,⟨(1/col.get idx),(one_div_ne_zero idx.2)⟩,i,(idx.1.castLT (Fin.val_lt_of_le idx.1 (Nat.sub_le m ↑i)) + i))

example : findPivot_ij 0 i j (m:=m) (n:=n) = none := by
  dsimp [findPivot_ij]
  set l':=(colVecofMat (botRightij 0 i j)).toList with hl
  induction l' with
  | nil => simp [findPivot_ij.findPivotAux]
  | cons a l ih =>
    have ha : a.allZero := by
      simp [botRightij] at hl
      have h1 : Vector.ofFn (0:Fin (m - ↑i) → ℚ) = zeroVec Rat (m-i.1) := by
        simp [zeroVec,Vector.eq_iff,Vector.replicate]
        rw [← List.ofFn_const (m-i.1) 0]
        rfl
      rw [← Function.const_def,List.ofFn_const] at hl
      have h2 : a ∈ List.replicate (n - ↑j) (Vector.ofFn 0) := by
        apply List.mem_of_mem_head?
        simp [hl]
      have h3 : a = Vector.ofFn (fun x => 0) := by convert (List.mem_replicate.mp h2).2
      rw [Vector.allZero]
      rw [Vector.ofFn_const] at h3
      simp [h3]
      intro x xv
      rw [← Vector.mem_def,Vector.mem_replicate] at xv
      exact xv.2
    rw [findPivot_ij.findPivotAux]
    simp [Vector.indNonzElt_allZero _ _ ha]
    exact ih

I think if you just focus on the last code block and take the rest of the functions by their names it will be easy to understand

[Damiano Testa]

Vivek Rajesh Joshi said:

Unfortunately, that is in fact an #mwe. That's how much context I need to provide for my function to find the pivot of a matrix, and I don't think there's much room for improvement. Although the one above is riddled with errors, so I have made a new one, but it is even longer:

Is this equivalent to what you were asking?

import Mathlib.Data.Matrix.Notation
import Mathlib.Data.Matrix.Basis

abbrev colVecofMat (M : Matrix (Fin m) (Fin n) F) := (Vector.ofFn M.transpose).map Vector.ofFn

theorem Vector.eq_iff (a1 a2 : Vector α n) : a1 = a2 ↔ toList a1 = toList a2 := sorry

variable (F : Type) [Field F] [DecidableEq F] [Repr F]
variable (M : Matrix (Fin m) (Fin n) Rat) (hm : m>0) (hn : n>0)

def Vector.Mem (a : α) : Vector α n → Prop := fun v => v.toList.Mem a

instance : Membership α (Vector α n) where
  mem := Vector.Mem

instance [DecidableEq α] (a : α) (v : Vector α n) : Decidable (a ∈ v) :=
  inferInstanceAs <| Decidable (a ∈ v.toList)

def zeroVec (k: Nat) : Vector F k := Vector.replicate k 0

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

def botRightij (i : Fin m) (j : Fin n) : Matrix (Fin (m-i)) (Fin (n-j)) Rat :=
  M.submatrix (fun k => ⟨k+i,Nat.add_lt_of_lt_sub k.2⟩) (fun l => ⟨l+j,Nat.add_lt_of_lt_sub l.2⟩)

def Vector.indNonzElt {F : Type} [Field F] [DecidableEq F] (v : Vector F 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 findPivot_ij (i : Fin m) (j : Fin n) : Option ((Fin m)×{c : Rat // c≠0}×(Fin m)×(Fin m)) :=
  findPivotAux (colVecofMat (botRightij M i j)).toList where
  findPivotAux (l : List (Vector Rat (m-i))) : Option ((Fin m)×{c : Rat // c≠0}×(Fin m)×(Fin m))  :=
    match l with
    | [] => none
    | col::as => match (Vector.indNonzElt col) with
      | none => findPivotAux as
      | some idx =>
          some (i,⟨(1/col.get idx),(one_div_ne_zero idx.2)⟩,i,(idx.1.castLT (Fin.val_lt_of_le idx.1 (Nat.sub_le m ↑i)) + i))

example : findPivot_ij 0 i j (m:=m) (n:=n) = none := by
  dsimp [findPivot_ij]
  set l':=(colVecofMat (botRightij 0 i j)).toList with hl
  induction l' with
  | nil => sorry
  | cons a l ih =>
    have ha : a.allZero := by
      simp [botRightij] at hl
      have h1 : Vector.ofFn (0:Fin (m - ↑i) → ℚ) = zeroVec Rat (m-i.1) := sorry
      rw [← Function.const_def,List.ofFn_const] at hl
      have h2 : a ∈ List.replicate (n - ↑j) (Vector.ofFn 0) := by
        apply List.mem_of_mem_head?
        simp [hl]
        sorry -- this one
      sorry
    sorry

(Note that I made no actual effort at minimizing. In particular, just using extract_goal on the marked sorry may give a much shorter example.)

[Vivek Rajesh Joshi]

Yes, that. Sorry about the previous example, I wanted to show that that is the only proof I need to finish this, but I understand now that that was pointless.

[Damiano Testa]

The shorter the code that you send, the easier it is to isolate the issue. So a #mwe is an aspiration, but one that should be taken seriously! :smile: