Stream: general

Topic: Induction on list

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?

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).

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