Stream: Coq users

Topic: lemma statement


view this post on Zulip pianke (Apr 10 2023 at 16:07):

I have natural number list l= [a1;a2;a3...an] and function f. First f takes a1 and generate l1,then f take a2 and generate l2...
I have information that In a2 l1 & In a3 l2....
H=c1=a1 & H2=In c2 l . It means c2 is not equal to a1 but it could be a2 or any element of l. Now want to write a lemma to prove
that c2 could be any element except a1 and hold the property which all oth er elements hold(including c2 and all previous elements like a1 a2..)

view this post on Zulip Laurent Théry (Apr 10 2023 at 16:53):

why c2 is not equal to a1?

view this post on Zulip pianke (Apr 11 2023 at 03:04):

I have solved the case where c2=a1 . Now this is the case where (a1=c1) & c2 is not equal to a1 but it could be any other element of the list.

view this post on Zulip Laurent Théry (Apr 11 2023 at 12:21):

c1 = a1 -> In c2 (a2 :: ... :: an) -> P c1 c2

Last updated: Oct 13 2024 at 01:02 UTC