部分的なアプリケーションでネストされた再帰

Question

私はCoqの2つのパラメータにネストされた再帰関数を定義しようとしています。

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.があれば、同じスタイルで定義されていることがわかります。

---

合計性チェッカーのこの動作は私にとって驚くべきことです。 1は「共有」（変わらない）パラメータの後fixを取得Fixpoint S 1とセクションのメカニズムを使用する場合

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. 

：あなたの定義を簡素化しようとしているときに私はこれにつまずきました。