Stream: Coq users

Topic: How to write hypothesis?

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?

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.

• You could have an inductive predicate saying the list is formed only by non-zero natural numbers.
• You could say the number of 0 in l is 0.
• You could say that every element in the list is not 0.

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

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

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.

sara lee (Nov 06 2021 at 17:06):

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

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?

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

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)

sara lee (Nov 07 2021 at 16:49):

(deleted)

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: Oct 05 2023 at 02:01 UTC