與部分應用程序嵌套遞歸

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. 

當人們使用的部分機制Fixpoint■一個「共享」（不變）參數後，得到fix。