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)
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: Aug 03 2023 at 10:10 UTC