recursion on length of list

Stream: general

[Kevin Buzzard]

I searched the chat and found some tips about doing induction on length of list, but the proofs were in tactic mode and I need recursion. Is something like this already in Lean:

def list.rec_on_length {X : Type*} (C : list X → Sort*) :
C [] → (∀ n : ℕ, (∀ L : list X, L.length = n → C L) → (∀ L : list X, L.length = n + 1 → C L)) → ∀ L : list X, C L := sorry

I can probably make it, assuming I've got it right, but I don't want to re-invent the wheel.

[Kevin Buzzard]

It should just come from nat.rec I guess

[Kevin Buzzard]

OK so I tried this and ran into something I wasn't expecting.

import data.list.basic

def list.rec_on_size' (X : Type*) (C : list X → Sort*) :
(∀ L : list X, L.length = 0 → C L) → (∀ n : ℕ,
  (∀ L : list X, L.length = n → C L) → (∀ L : list X, L.length = n + 1 → C L)) →
  ∀ m : ℕ, ∀ L : list X, L.length = m → C L := λ z ih n, nat.rec z ih n

@[elab_as_eliminator]
def list.rec_on_size {X : Type*} {C : list X → Sort*} :
C [] → (∀ n : ℕ,
  (∀ L : list X, L.length = n → C L) → (∀ L : list X, L.length = n + 1 → C L)) →
  ∀ L : list X, C L :=
λ z ih L, list.rec_on_size' X C (λ H hH, (by rwa list.length_eq_zero.1 hH : C H)) ih (L.length) _ rfl
--                                         ^^^^^^^^^^ building term of type C H in tactic mode

The first function was just practice and it turned out to be exactly nat.rec. But then when I got going I realised that I had a term of type C [] and I wanted a term of type Pi (L : list X), L.length = 0 -> C L. I built it using a rewrite. Is this going to bite me later?

[Reid Barton]

I think so. It's probably better to define it using case analysis on L

[Reid Barton]

or actually hmm

[Reid Barton]

Maybe you'll be fine

[Reid Barton]

I think the main thing that you want is that your term of that type evaluates to the original term if you apply it to [] and a proof that [].length = 0 (which is rfl in this case, but that doesn't actually matter). Here you defined it by induction on a proof that the input list L equals [] (which was cooked up somehow from the hypothesis L.length = 0); that proof is definitionally equal to rfl by proof irrelevance so the application of eq.rec will reduce.

[Kevin Buzzard]

It did occur to me that list.rec_on_size' might be all I need in practice.