部分应用的嵌套递归

Question

我正在尝试在 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.

但我收到以下错误：

Error: No such section variable or assumption: bar.

Function 的文档明确指出：

Function does not support partial application of the function being defined.

但这正是我的情况。这种情况下的策略是什么？

Answer 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 的this one。如果您 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 的部分机制时，在 "shared"（未更改）参数后得到 fix。

部分应用的嵌套递归

Nested recursion with partial application

recursion

coq