Как развернуть рекурсивную функцию только один раз в Coq

Question

Вот рекурсивная функция all_zero который проверяет, все ли элементы списка натуральных чисел равны нулю:

Require Import Lists.List.
Require Import Basics.

Fixpoint all_zero ( l : list nat ) : bool :=
  match l with
  | nil => true
  | n :: l' => andb ( beq_nat n 0 ) ( all_zero l' )
  end.

Теперь предположим, что у меня была следующая цель

true = all_zero (n :: l')

И я хотел использовать unfold тактика, чтобы превратить его в

true = andb ( beq_nat n 0 ) ( all_zero l' )

К сожалению, я не могу сделать это простым unfold all_zero потому что тактика охотно найдет и заменит все случаи all_zeroв том числе тот, что в разложенном виде, и это превращается в беспорядок. Есть ли способ избежать этого и развернуть рекурсивную функцию только один раз?

Я знаю, что могу достичь тех же результатов, доказав специальную эквивалентность с assert (...) as X, но это неэффективно. Я хотел бы знать, есть ли простой способ сделать это похожим на unfold,

Answer 1

Мне кажется, что simpl будет делать то, что вы хотите. Если у вас более сложная цель, с функциями, которые вы хотите применить, и функциями, которые вы хотите оставить как есть, вам может понадобиться использовать различные опции cbv тактика (см. http://coq.inria.fr/distrib/current/refman/Reference-Manual010.html).

Answer 2

Пытаться

unfold all_zero; fold all_zero.

По крайней мере, здесь для меня это дает:

true = (beq_nat n 0 && all_zero l)%bool