zohaze (Mar 31 2023 at 08:07): zohaze (Mar 31 2023 at 08:07):I have non empty natural number list l1. My requirement is first two elements of this list , therefore i have performed induction twice .(H2 : k1 :: k2 :: t <> [])
Now this list is the input argument to a function g(whose patteren matching is on this list). When i simplify g function it talks about t. How to write that my requirement is k1 ,k2 only ,consider t as nil? I want to test all functions on k1 &k2 only.
Laurent Théry (Mar 31 2023 at 08:23):if you want to prove that a statement P is true for all lists with 2 elements, you prove forall l, length l = 2 -> P l.
Last updated: Oct 13 2024 at 01:02 UTC