Iterating over indexed types

Stream: new members

[Vivek Rajesh Joshi]

import Mathlib.Data.Matrix.Notation
import Mathlib.Data.Fin.Tuple.Reflection

variable (F : Type) [Field F] [DecidableEq F]

inductive RowEchelonForm : (m n : Nat) → Type where
| nil : RowEchelonForm m 0
| pad : RowEchelonForm m n → RowEchelonForm m (n+1)
| extend : RowEchelonForm m n → (Fin n → F) → RowEchelonForm (m+1) (n+1)
deriving Repr

def R0 : RowEchelonForm Rat m n := RowEchelonForm.pad^[n] RowEchelonForm.nil

I want to iterate the pad function n times, but that isn't possible with Nat.iterate since it requires the function to have the same domain and codomain. Is there a version of Nat.iterate that can do this?

[Vivek Rajesh Joshi]

I have written a custom function for doing this. However, I'm running into someproblems while trying to prove theorems with it:

import Mathlib.Logic.Function.Iterate

@[simp]
def Nat.iterate_ind {α : ℕ → Type} (f : {i : ℕ} → α i → α (i+1)) (n : ℕ) (a : α 0) : α n :=
  match n with
  | 0 => a
  | succ k => iterate_ind f k (f a)

theorem Nat.iterate_ind_succ {α : ℕ → Sort u} (f : {i : ℕ} → α i → α (i+1)) (n : ℕ) :
  Nat.iterate_ind f (n+1) = (Nat.iterate_ind f n) ∘ f := sorry

Why is the type of the LHS a (0+1) -> a (n+1+1) instead of being a 0 -> a (n+1)?

[Riccardo Brasca]

Lean is confused by α, that is implicit

[Riccardo Brasca]

theorem Nat.iterate_ind_succ {α : ℕ → Sort*} (f : {i : ℕ} → α i → α (i+1)) (n : ℕ) :
  Nat.iterate_ind (α := α) f (n+1) = (Nat.iterate_ind f n) ∘ f := sorry

works

[Riccardo Brasca]

Note that #check Nat.iterate_ind (α := fun i ↦ α (i + 37)) f typecheks, so Lean has no real way of guessing α from f, and in your example is guessing a different one.

[Vivek Rajesh Joshi]

Okay, I see now. Thanks a lot!

[Riccardo Brasca]

In your original example there is also the problem that Nat.iterate_ind is defined for an α taking values in Type and you apply with α taking value in any Sort. If you fix it using Sort* everywhere then rfl proves the theorem.