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?

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`

.

For the first case you use the `Forall`

predicate:

```
List.Forall : ∀ A : Type, (A → Prop) → list A → Prop
```

For the last you could use the membership predicate:

```
List.In : ∀ A : Type, A → list A → Prop
```

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

.

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

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?

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`

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)

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