Zulip Chat Archive

Stream: general

Topic: Induction on list


view this post on Zulip Yury G. Kudryashov (May 04 2020 at 02:55):

Can I emulate the following equation compiler induction

theorem mythm :  (l : list α), p l
| [] := p0
| [a] := p1
| (a::b::l) := p2 (mythm l)

using induction tactic? Or should I add a lemma list.induction_on2 : ∀ l, C [] → C [a] → (∀ a b l, C l → C (a::b::l)) → C l?

view this post on Zulip Yury G. Kudryashov (May 04 2020 at 02:56):

In my specific example I get l as a result of rcases so I can't use equation compiler directly (or I don't know how to do it).

view this post on Zulip Mario Carneiro (May 04 2020 at 03:40):

You could do strong induction on the length of the list


Last updated: May 10 2021 at 23:11 UTC