How do I do induction with `length t` here

Stream: new members

[YH]

variables {A : Type} {x : A} {s t : list A}

lemma ex : length (reverse t) = length t :=
begin
induction (length t) with n hn,
sorry,
sorry,
end

in this lemma I want to write induction (length t) with n hn but then the goals are like

2 goals
case nat.zero
A : Type,
t : list A
⊢ length (reverse t) = 0

case nat.succ
A : Type,
t : list A,
n : ℕ,
hn : length (reverse t) = n
⊢ length (reverse t) = nat.succ n

which is not what I wanted.

[Kevin Buzzard]

But it is what the tactic is expected to do

[Marc Huisinga]

you probably want to induct on t

[YH]

Did try induction on t.

[Kevin Buzzard]

You'll need some intermediate lemmas but this is the way to do it

[Marc Huisinga]

if you want to see a oneliner-solution i can post it, but it's a nice small exercise

[YH]

I just finished my 23-liner. Show me the oneliner please.

[YH]

lemma ex2 {t : list A} : length (reverse t) = length t :=
begin
induction t with x xs hs,
unfold reverse,
unfold reverse_core,
unfold reverse,
unfold reverse_core,
unfold length,
have l : ∀ s t : list A, length (reverse_core s t) = length s + length t,
  intro s,
  induction s with y ys h1,
  unfold reverse_core,
  unfold length,
  intro t,
  rw zero_add,
unfold reverse_core,
intro t,
rw h1 (y :: t),
unfold length,
simp,
rw l _ _,
unfold length,
simp,
end

[Marc Huisinga]

it does use some basic intermediate list lemmas.

lemma ex : length (reverse t) = length t :=
by induction t; simpa only [list.reverse_cons, list.length_append, list.length, add_right_inj]

[YH]

OK. reverse_cons is the one I didn't know.

[YH]

what is simpa, lean cannot find it.

[Marc Huisinga]

you can find a description of most mathlib tactics here: https://github.com/leanprover-community/mathlib/blob/master/docs/tactics.md

[YH]

⊢ length (reverse (t_hd :: t_tl)) = length (t_hd :: t_tl)

Still have this goal.

[Marc Huisinga]

did you import data.list?

[YH]

import data.list.basic

[Marc Huisinga]

works for me :shrug:

[YH]

Oh my bad, I defined my own length in this hidden name space. facepalm.