Stream: Coq users

Topic: How to write hypothesis?


view this post on Zulip sara lee (Nov 03 2021 at 13:52):

I have non empty natural number list. Want to write hypothesis " that there is no element in the list whose index value is zero. How I can write this hypothesis? (l<>nil & ?) . Secondly ,if set hypothesis nth a l d> nth b l d ,then this statement is enough to show that all values are non zero in the list?

view this post on Zulip Théo Winterhalter (Nov 03 2021 at 13:57):

There are many ways to say this and you will have to pick the one most suited to your task.

view this post on Zulip Théo Winterhalter (Nov 03 2021 at 13:58):

For the first case you use the Forall predicate:

List.Forall :  A : Type, (A  Prop)  list A  Prop

view this post on Zulip Théo Winterhalter (Nov 03 2021 at 13:59):

For the last you could use the membership predicate:

List.In :  A : Type, A  list A  Prop

view this post on Zulip Théo Winterhalter (Nov 03 2021 at 14:00):

For the second, you filter non-zero elements and check that the remaining length is 0.

view this post on Zulip sara lee (Nov 06 2021 at 17:06):

Ok . Thank u.What about second part of question?

view this post on Zulip Théo Winterhalter (Nov 06 2021 at 17:52):

I don't really understand your second statement. Who are a, b and d? Why would it have anything to do with the values of l being non-zero?

view this post on Zulip Quinn (Nov 06 2021 at 17:52):

i'm not sure I understand the second part of the question. I'd need to see some quantifiers around nth a l d > nth b l d, denoting what you believe about a and b

view this post on Zulip sara lee (Nov 07 2021 at 16:48):

forall a b d l: nth a l d > nth b l d (for any index a b of list l whose default value is zero). In hypothesis if I have statement that one index value is greater than other ,then it means that two same value cannot appear in the list. If I talk about zero (nat) then two or more than two zeros cannot appear. I want to ask that one time zero can appear under this condition?(n>0 is true)

view this post on Zulip sara lee (Nov 07 2021 at 16:49):

(deleted)

view this post on Zulip zohaze (Nov 08 2021 at 03:22):

Simply under this condition " forall a b d l: nth a l d > nth b l d". zero can be part of list or not?


Last updated: Jan 28 2023 at 08:02 UTC