coq - 匹配列表列表的模式

Question

我有一个list list nat我想写一个函数来解析到这个列表中，例如：

Definition my_function (l : list list nat) :=
 let fix aux acc l :=
    match l with
    | nil => acc
    | c :: l' => match c with
                 | nil => acc
                 | d :: l'' => aux d l'
                end
     end in aux 0 l.

在这里我不知道如何使用l''. 有没有更好的方法来编写这个函数？非常感谢。

编辑：我想知道我可以检查整个列表的算法l。

Answer 1

我不明白您的功能应该完成什么，但它应该具有这种形状：

Axioms (s1 s2 s3 : Set) (f3 : s3) (f4 : s1 -> s3 -> s3) (f1 : s2)
  (f2 : s3 -> s2 -> s2).

Fixpoint my_funct_aux (l1 : list s1) : s3 :=
  match l1 with
  | nil        => f3
  | cons e1 l2 => f4 e1 (my_funct_aux l2)
  end.

Fixpoint my_funct (l1 : list (list s1)) : s2 :=
  match l1 with
  | nil        => f1
  | cons l2 l3 => f2 (my_funct_aux l2) (my_funct l3)
  end.

或者，如果您不介意简洁：

Axioms (s1 s2 s3 : Set) (f3 : s3) (f4 : s1 -> s3 -> s3) (f1 : s2)
  (f2 : s3 -> s2 -> s2).

Fixpoint fold {s1 s2 : Set}
  (f1 : s2) (f2 : s1 -> s2 -> s2) (l1 : list s1) : s2 :=
  match l1 with
  | nil        => f1
  | cons e1 l2 => f2 e1 (fold f1 f2 l2)
  end.

Definition my_funct : list (list s1) -> s2 :=
  fold f1 (fun l1 l2 => f2 (fold f3 f4 l1) l2).