coq - 取列表头部的选项元素

Question

我有类型

Variable l: list (a * b * option c * option d).
Variable ls : list (list l).

我想option d从列表的顶部获取类型，然后检查整个列表。我的代码如下所示：

Definition test (l: list (a * b * option c * option d)):=
match l with
| nil => ... (* not important *)
| (_,_,_,od) :: l' => 
  match od with
  | None => ... (* not important *)
  | Some d => if forallb (fun li => forallb (fun ci => do_something ci d)) ls) l'
  end
end.

我的问题是if forallb (fun li => forallb (fun ci =>do_something ci d))ls)l'我添加的测试是forallb (fun li =>...)因为我希望它在整个列表中进行测试l'。但我根本没有使用这个论点li。

编辑：我的问题集中在if forallb (fun li => forallb (fun ci => do_something ci d))ls)l'. 我添加forallb (fun li =>是因为我想对列表的其余部分进行测试l'。如果没有forallb (fun li我可以存档此测试if (forallb (fun ci => do_something ci d))ls，但我不知道如何在列表中再次测试此条件l'。

Answer 1

你的上下文不一致。

变量 l : ...

使 l 是一个列表

变量 ls ：列表（列表 l）。

假设 l 是一个类型。

也许你的意思是：

定义 l := list (a * b * option c * option d)。

变量 ls := 列表（列表 l）。

这使得 ls 成为列表列表的列表（如三维数组）。

现在，假设您的意思是 do_something 具有类型 l -> d -> bool

我猜你想用 ls 中的所有 l 类型的元素和 test 的参数中的所有 d 类型的元素（也称为 l，yuck）来测试 do_something。

你应该有

...

|Some d => if forallb (fun li => forallb (fun ci => do_something ci d)) ls then test l' else false ...

但坦率地说，你的问题留给回答者猜测！