# Zulip Chat Archive

## Stream: general

### Topic: recursion on length of list

#### Kevin Buzzard (Nov 19 2019 at 17:12):

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 (Nov 19 2019 at 17:12):

It should just come from nat.rec I guess

#### Kevin Buzzard (Nov 19 2019 at 20:22):

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 (Nov 19 2019 at 20:24):

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

#### Reid Barton (Nov 19 2019 at 20:25):

or actually hmm

#### Reid Barton (Nov 19 2019 at 20:25):

Maybe you'll be fine

#### Reid Barton (Nov 19 2019 at 20:32):

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 (Nov 19 2019 at 21:53):

It did occur to me that `list.rec_on_size'`

might be all I need in practice.

Last updated: May 13 2021 at 23:16 UTC