преобразовать список целых чисел в список натуральных чисел

Question

Я хочу скрыть list of integer до list of nat. Вот функция, которую я возвращаю в Coq.

Fixpoint list_int_to_nat (l : list integer) : list nat := 
    match l with 
     | nil => nil 
     | x :: l' => let i := Z.to_nat x in 
     list_int_to_nat l' 
    end. 

Не могли бы вы помочь мне, чтобы иметь возможность переводить каждый элемент списка integer к списку nat, потому что в моей функции я не использовал первый элемент i? Большое спасибо за Вашу помощь.

Answer 1

Вы написали рекурсивную функцию, которая всегда вызывает себя на хвосте, и вы ничего не делаете с головой, так что в конечном счете ваша функция всегда возвращается nil.

Здесь вы должны использовать конструктор cons от list, чтобы добавить i в начало возвращаемого списка.

Fixpoint list_int_to_nat (l : list integer) : list nat := 
    match l with 
    | nil => nil 
    | x :: l' => let i := Z.to_nat x in 
     i :: list_int_to_nat l' 
end. 

(Здесь я использовал обозначение ::, которое я считаю более удобным).

Это должно сделать трюк.

Answer 2

Вы можете также использовать map:

Definition list_int_to_nat l := map Z.to_nat l.