#coq
#coq
Вопрос:
(длина l=?0)=false. Это означает, что в списке присутствует хотя бы один элемент, он может быть равен нулю. Я хочу написать, что ни один элемент в списке не равен нулю .Я не знаю, как написать это формально.
Ответ №1:
Вы знаете, что 0 этого нет в пустом списке [] , и вы знаете, что если l не содержит 0 , то добавление к нему любого ненулевого целого числа все равно приведет к списку без 0 , другими словами x :: l , не содержит 0 (когда x <> 0 ). Если вы вызываете nozeroes l это свойство в списке l , видите ли вы способ его определения?
Комментарии:
1. (длина(h:: h1::l)= ?0)= false-> (h =?h1)=false-> (h =?0)=false-> Это означает, что в списке присутствуют по крайней мере два элемента, которые не равны друг другу и не равны нулю. При наличии этих кодировок мы можем сказать, что по крайней мере один элемент больше другого.
2. Вам вообще не нужно говорить о.
length
Ответ №2:
Я хочу написать, что ни один элемент в списке не равен нулю .
записывается « 0 отсутствует в списке l « ~ In 0 l.