Stream: Coq users

Topic: Two values of list

view this post on Zulip 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.

view this post on Zulip 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: Jun 20 2024 at 13:02 UTC