我试图了解 Coq 中的依赖类型和依赖匹配，我有下面的代码，在底部我有add_pair函数，我的想法是我想接收一个包含两个元素的（依赖）列表并返回总和列表中的两个元素。由于列表的大小是在类型中编码的，我应该能够将它定义为一个总函数，但我得到一个错误，说match不是exaustive
这是代码
Module IList.
Section Lists.
(* o tipo generico dos elementos da lista *)
Variable A : Set.
(* data type da lista, recebe um nat que é
o tamanho da lista *)
Inductive t : nat -> Set :=
| nil : t 0 (* lista vazia, n = 0 *)
| cons : forall (n : nat), A -> t n -> t (S n). (* cons de uma lista
n = n + 1 *)
(* concatena duas listas, n = n1 + n2 *)
Fixpoint concat n1 (ls1 : t n1) n2 (ls2 : t n2) : t (n1 + n2) :=
match ls1 in (t n1) return (t (n1 + n2)) with
| nil => ls2
| cons x ls1' => cons x (concat ls1' ls2)
end.
(* computar o tamanho da lista é O(1) *)
Definition length n (l : t n) : nat := n.
End Lists.
Arguments nil {_}.
(* Isso aqui serve pra introduzir notações pra gente poder
falar [1;2;3] em vez de (cons 1 (cons 2 (cons 3 nil))) *)
Module Notations.
Notation "a :: b" := (cons a b) (right associativity, at level 60) : list_scope.
Notation "[ ]" := nil : list_scope.
Notation "[ x ]" := (cons x nil) : list_scope.
Notation "[ x ; y ; .. ; z ]" := (cons x (cons y .. (cons z nil) ..)) : list_scope.
Open Scope list_scope.
End Notations.
Import Notations.
(* Error: Non exhaustive pattern-matching: no clause found for pattern [_] *)
Definition add_pair (l : t nat 2) : nat :=
match l in (t _ 2) return nat with
| (cons x (cons y nil)) => x + y
end.
End IList.
确实，您提供的匹配是详尽无遗的，但是 Coq 的模式匹配算法是有限的，无法检测到它。我认为，问题在于它将嵌套模式匹配（例如您的）（您有两个 叠瓦cons）编译为一系列基本模式匹配（最多具有一个深度模式）。但是在 external 的cons分支中match，如果你没有用等式显式记录索引应该1丢失的信息——当前的算法还不够聪明，无法做到这一点。
作为避免摆弄不可能的分支、等式等的可能解决方案，我提出以下建议：
Definition head {A n} (l : t A (S n)) : A :=
match l with
| cons x _ => x
end.
Definition tail {A n} (l : t A (S n)) : t A n :=
match l with
| cons _ l' => l'
end.
Definition add_pair (l : t nat 2) : nat :=
head l + (head (tail l)).
作为记录，一个解决不可能的分支并使用等式记录索引信息的解决方案（可能有更好的版本）：
Definition add_pair (l : t nat 2) : nat :=
match l in (t _ m) return (m = 2) -> nat with
| [] => fun e => ltac:(lia)
| x :: l' => fun e =>
match l' in (t _ m') return (m' = 1) -> nat with
| [] => fun e' => ltac:(lia)
| x' :: l'' => fun e' =>
match l'' in (t _ m'') return (m'' = 0) -> nat with
| [] => fun _ => x + x'
| _ => fun e'' => ltac:(lia)
end ltac:(lia)
end ltac:(lia)
end eq_refl.
有趣的部分是使用显式等式来记录索引的值（这些被lia策略用来丢弃不可能的分支）。
本文收集自互联网，转载请注明来源。
如有侵权，请联系 [email protected] 删除。
我来说两句