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.
For the first case you use the
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
Ok . Thank u.What about second part of question?
I don't really understand your second statement. Who are
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
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)
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