## 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)

(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: Jun 18 2024 at 10:02 UTC