Zulip Chat Archive

Stream: new members

Topic: How do I do induction with `length t` here


view this post on Zulip YH (Dec 17 2019 at 23:47):

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.

view this post on Zulip Kevin Buzzard (Dec 17 2019 at 23:53):

But it is what the tactic is expected to do

view this post on Zulip Marc Huisinga (Dec 17 2019 at 23:53):

you probably want to induct on t

view this post on Zulip YH (Dec 17 2019 at 23:53):

Did try induction on t.

view this post on Zulip Kevin Buzzard (Dec 17 2019 at 23:54):

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

view this post on Zulip Marc Huisinga (Dec 18 2019 at 00:01):

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

view this post on Zulip YH (Dec 18 2019 at 00:03):

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

view this post on Zulip YH (Dec 18 2019 at 00:03):

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

view this post on Zulip Marc Huisinga (Dec 18 2019 at 00:04):

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]

view this post on Zulip YH (Dec 18 2019 at 00:05):

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

view this post on Zulip YH (Dec 18 2019 at 00:07):

what is simpa, lean cannot find it.

view this post on Zulip Marc Huisinga (Dec 18 2019 at 00:07):

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

view this post on Zulip YH (Dec 18 2019 at 00:09):

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

Still have this goal.

view this post on Zulip Marc Huisinga (Dec 18 2019 at 00:14):

did you import data.list?

view this post on Zulip YH (Dec 18 2019 at 00:15):

import data.list.basic

view this post on Zulip Marc Huisinga (Dec 18 2019 at 00:16):

works for me :shrug:

view this post on Zulip YH (Dec 18 2019 at 00:22):

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


Last updated: May 14 2021 at 06:16 UTC