Jonathan Lindegaard Starup (Mar 11 2024 at 16:53): Jonathan Lindegaard Starup (Mar 11 2024 at 16:53):I have an induction proof where I want to induct over i while keeping the forall quantification of list. how do I do this?
fun nth_opt :: ‹['a list, nat] ⇒ 'a option› where
‹nth_opt [] _ = None› |
‹nth_opt (head # tail) 0 = Some head› |
‹nth_opt (head # tail) n = nth_opt tail (n-1)›
lemma nth_opt_len_some: shows ‹(i < length list ⟷ (∃v. nth_opt list i = Some v))›
proof (induction i)
induction i arbitrary: list
Mathias Fleury (Mar 11 2024 at 17:01):Remark that you are not keeping the forall quantifiers: in the lemma list is fixed. You are adding a quantifier.
Jonathan Lindegaard Starup (Mar 12 2024 at 08:29):That makes sense. I hit this issue again while using induction rule:... and it doesn't seem that arbitrary: ... works. With more complicated examples would you recommend adding quantifiers to the lemma statement (not using assumes "..." shows "...") or just initially introduce quantifiers as needed before starting the induction proof?
Jan van Brügge (Mar 12 2024 at 12:41):the arbitrary has to go before the rule that should work
Last updated: Nov 13 2025 at 04:27 UTC