Могу ли я сделать «сложную» взаимную рекурсию в Coq без привязки let?

Рассмотрим следующую пару взаимно рекурсивных типов данных Coq, которые представляют Forest непустых Tree. Каждый Branch из Tree содержит дополнительный логический флаг, который мы можем извлечь с помощью isOK.

Inductive Forest a : Type
  := Empty    : Forest a
  |  WithTree : Tree a -> Forest a -> Forest a
with Tree a : Type
  := Branch : bool -> a -> Forest a -> Tree a.

Arguments Empty    {_}.
Arguments WithTree {_} _ _.
Arguments Branch   {_} _ _ _.

Definition isOK {a} (t : Tree a) : bool :=
  match t with
  | Branch ok _ _ => ok
  end.

Теперь, если мы проигнорируем этот логический флаг, мы можем написать пару функций сопоставления, чтобы применить функцию к каждому значению в Forest или Tree, и это отлично работает:

Fixpoint mapForest_always {a} (f : a -> a) (ts0 : Forest a) {struct ts0} : Forest a :=
  match ts0 with
  | Empty         => Empty
  | WithTree t ts => WithTree (mapTree_always f t) (mapForest_always f ts)
  end
with mapTree_always {a} (f : a -> a) (t : Tree a) {struct t} : Tree a :=
  match t with
  | Branch ok x ts => Branch ok (f x) (mapForest_always f ts)
  end.

Однако предположим, что логическое значение представляет некоторую проверку достоверности, которая в реальном коде была бы более сложной. Таким образом, мы сначала проверяем логическое значение и фактически рекурсивно используем его только в случае необходимости. Это означает, что у нас есть три взаимно рекурсивные функции, но одна из них просто выполняет работу. К сожалению, это не работает:

Fail Fixpoint mapForest_bad {a} (f : a -> a) (ts0 : Forest a) {struct ts0} : Forest a :=
  match ts0 with
  | Empty         => Empty
  | WithTree t ts => WithTree (mapTree_bad f t) (mapForest_bad f ts)
  end
with mapTree_bad {a} (f : a -> a) (t : Tree a) {struct t} : Tree a :=
  if isOK t
  then mapOKTree_bad f t
  else t
with mapOKTree_bad {a} (f : a -> a) (t : Tree a) {struct t} : Tree a :=
  match t with
  | Branch ok x ts => Branch ok (f x) (mapForest_bad f ts)
  end.

Проблема в том, что mapTree_bad вызывает mapOKTree_bad с аргументом, который на самом деле не меньше.

За исключением того, что все, что делает mapOKTree_bad, является дополнительным шагом после предварительной обработки. Это будет всегда завершаться, но Coq этого не видит. Чтобы убедить средство проверки завершения, мы можем вместо этого определить mapOKTree_good, что то же самое, но является локальной let-связкой; затем средство проверки завершения проверит привязку let и позволит нам определить mapForest_good и mapTree_good. Если мы хотим получить mapOKTree_good, мы можем просто использовать простое старое определение после того, как мы определили взаимно рекурсивные функции, которые имеют то же тело, что и let-binding:

Fixpoint mapForest_good {a} (f : a -> a) (ts0 : Forest a) {struct ts0} : Forest a :=
  match ts0 with
  | Empty         => Empty
  | WithTree t ts => WithTree (mapTree_good f t) (mapForest_good f ts)
  end
with mapTree_good {a} (f : a -> a) (t : Tree a) {struct t} : Tree a :=
  let mapOKTree_good {a} (f : a -> a) (t : Tree a) : Tree a :=
        match t with
        | Branch ok x ts => Branch ok (f x) (mapForest_good f ts)
        end in
  if isOK t
  then mapOKTree_good f t
  else t.

Definition mapOKTree_good {a} (f : a -> a) (t : Tree a) : Tree a :=
  match t with
  | Branch ok x ts => Branch ok (f x) (mapForest_good f ts)
  end.

Это работает, но некрасиво. Есть ли способ убедить средство проверки завершения Coq принять варианты _bad, или трюк с _good — лучшее, что у меня есть? Команда, которая работает для меня, например, Program Fixpoint или Function, также является вполне разумным решением.