Zulip Chat Archive

Stream: general

Topic: recursion on length of list


view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 17:12):

It should just come from nat.rec I guess

view this post on Zulip 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?

view this post on Zulip Reid Barton (Nov 19 2019 at 20:24):

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

view this post on Zulip Reid Barton (Nov 19 2019 at 20:25):

or actually hmm

view this post on Zulip Reid Barton (Nov 19 2019 at 20:25):

Maybe you'll be fine

view this post on Zulip 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.

view this post on Zulip 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