在 Fixpoint Coq 定义中使用 lambda

Question

我正在尝试在递归定义中使用 List.map，使用当前定义的递归函数作为参数映射到列表。有可能吗？我可以定义我自己的递归固定点定义而不是使用 map 但我有兴趣在这里使用 map。

Require Import Coq.Lists.List.
Import ListNotations.

Inductive D: nat -> Type := | D0 (x:nat): D x.

Inductive T: nat -> nat -> Type :=
| T0 {i o} (foo:nat): T i o
| T1 {i o} (foo bar:nat) : T i o -> T i o.

Fixpoint E {i o: nat} (t:T i o) (x:nat) (d:D i): option (D o) 
  :=
    (match t in @T i o
           return D i -> option (D o)
     with
     | T0 _ _ foo => fun d0 => None
     | T1 _ _ foo bar t' =>
       fun d0 =>
         let l := List.map (fun n => E t' x d0)  [ 1 ; 2 ; 3 ] in
         let default := Some (D0 o) in
         List.hd default l
     end) d.

上面的例子是人为的，但说明了问题。错误信息：

The term "l" has type "list (option (D n0))"
 while it is expected to have type "list (option (D o))".

Answer 1

您只需将名称绑定到 T1 模式：

Require Import Coq.Lists.List.
Import ListNotations.

Inductive D: nat -> Type := | D0 (x:nat): D x.

Inductive T: nat -> nat -> Type :=
| T0 {i o} (foo:nat): T i o
| T1 {i o} (foo bar:nat) : T i o -> T i o.

Fixpoint E {i o: nat} (t:T i o) (x:nat) (d:D i): option (D o)
  :=
    (match t in @T i o
           return D i -> option (D o)
     with
     | T0 _ _ foo => fun d0 => None
     (*   \/ change here *)
     | T1 i o foo bar t' =>
       fun d0 =>
         let l := List.map (fun n => E t' x d0)  [ 1 ; 2 ; 3 ] in
         let default := Some (D0 o) in
         List.hd default l
     end) d.

问题是省略绑定意味着 T1 分支上使用的 o 引用同名的 "outer" 变量，而您希望它引用T1.

给出的那个

在 Fixpoint Coq 定义中使用 lambda

Using lambda in Fixpoint Coq definitions

recursion

coq

dependent-type