Вложенная рекурсия с частичным применением

Я пытаюсь определить вложенную рекурсивную функцию по двум параметрам в Coq.

Require Import List.
Import ListNotations.

Fixpoint map_sequence2 {A B C : Set} (f : A -> B -> option C)
  (xs : list A) (ys : list B) : option (list C) :=
match xs, ys with
| [], [] => Some []
| x :: xs, y :: ys =>
  match f x y, map_sequence2 f xs ys with
  | Some z, Some zs => Some (z :: zs)
  | _, _ => None
  end
| _, _ => None
end.

Inductive T : Set := TA | TB : list T -> T.

Definition max n m := if Nat.leb n m then m else n.

Fixpoint height (t : T) : nat :=
match t with
| TA => 1
| TB xs => 1 + List.fold_left max (List.map height xs) 0
end.

Function bar (t1 : T) (t2 : T) {measure height t2} : option T :=
match t1, t2 with
| TA, TA => Some TA
| TB xs, TB ys =>
  match map_sequence2 bar xs ys with
  | Some zs => Some (TB zs)
  | None => None
  end
| _, _ => None
end.
Proof.
Abort.

Но я получаю следующую ошибку:

Ошибка: нет такой переменной раздела или предположения: бар.

Документация Function явно говорит:

Функция

Не поддерживает частичное применение определяемой функции.

, но это именно мой случай. Какова стратегия для таких случаев?

1 3
recursion coq

1 ответ:

Если вы немного переопределите функцию map_sequence2 (я только что переместил fix немного вправо) 

Definition map_sequence2 {A B C : Set} (f : A -> B -> option C) :=
  fix map_sequence2 (xs : list A) (ys : list B) : option (list C) :=
match xs, ys with
| [], [] => Some []
| x :: xs, y :: ys =>
  match f x y, map_sequence2 xs ys with
  | Some z, Some zs => Some (z :: zs)
  | _, _ => None
  end
| _, _ => None
end.

Тогда проверка тотальности принимает ваше определение просто Fixpoint вместо Function или Program Fixpoint: 

Fixpoint bar (t1 : T) (t2 : T) : option T :=
match t1, t2 with
| TA, TA => Some TA
| TB xs, TB ys =>
  match map_sequence2 bar xs ys with
  | Some zs => Some (TB zs)
  | None => None
  end
| _, _ => None
end.

Это решение точно так же, как это решение от @gallais. И если Вы Print fold_left., который используется в этом решении, вы увидите, что он был определен в том же стиле.

Позвольте мне добавить, что такое поведение проверки тотальности для меня удивительно. Я споткнулся. на этом, пытаясь упростить свое определение: 
Section liftA2.
Variables A B C : Type.
Definition liftA2_option (f : A -> B -> C) : option A -> option B -> option C :=
  fun ox oy =>
    match ox, oy with
    | Some x, Some y => Some (f x y)
    | _, _ => None
    end.
End liftA2.
Arguments liftA2_option {A B C}.

Section Combine_with_option.
Variables A B C : Set.
Variable f : A -> B -> option C.

Fixpoint combine_with_option (xs : list A) (ys : list B) : option (list C) :=
  match xs,ys with
  | x::xs', y::ys' => liftA2_option cons (f x y) (combine_with_option xs' ys') 
  | [], [] => Some []
  | _, _ => None
  end.
End Combine_with_option.
Arguments combine_with_option {A B C}.

Fixpoint bar (t1 : T) (t2 : T) : option T :=
match t1, t2 with
| TA, TA => Some TA
| TB xs, TB ys =>
  match combine_with_option bar xs ys with
  | Some zs => Some (TB zs)
  | None => None
  end
| _, _ => None
end.

При использовании механизма сечения с Fixpoints после "общих" (неизмененных) параметров получается fix.

2