Как увеличить заголовок в списке

Question

Fixpoint nonzeros (l:natlist) : natlist :=
      match l with
      | nil => nil
      | 0 :: t => 1::nonzeros t
      | h :: t => h :: nonzeros t
     end.

У меня есть список натуральных чисел с кратным числом нулей. Я хочу заменить первый ноль на один, второй ноль на два и третий ноль на три и так далее, в то время как остальная часть списка должна остаться без изменений. Эта функция принимает список натуральных чисел, а затем заменяет нули на единицы, но не увеличивает его. Можно ли увеличить заголовок перед рекурсивным вызовом?

Answer 1

При работе с такими вещами вам нужно обобщить 1. Вместо того, чтобы сказать, что я хочу заменить первое 0 на 1, а затем 2 и т. Д., Вы говорите: я хочу заменить первое 0 на k, второе на k+1 и т. Д. .

Fixpoint nonzeroes_k (k : nat) (l : list nat) : list nat :=
  match l with
  | nil => nil
  | 0 :: l => k :: nonzeroes_k (S k) l
  | h :: l => h :: nonzeroes_k k l
  end.

Тогда вам нужна функция, начинающаяся с 1:

Definition nonzeroes := nonzeroes_k 1.

Вы часто будете делать такие вещи, когда имеете дело со смещениями в рекурсивных функциях.