如何依赖匹配包含两个元素的列表？

Question

我试图理解 Coq 中的依赖类型和依赖匹配，我有下面的代码，在底部我有 add_pair 函数，我的想法是我想接收一个 (dependent)恰好包含两个元素的列表和 return 列表中两个元素的总和。由于列表的大小是在类型中编码的，我应该能够将它定义为一个总函数，但是我得到一个错误，说 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.

Answer 1

的确，你提供的匹配确实很详尽，但Coq的pattern-matching算法有限，无法检测到。我认为，问题在于它将一个嵌套的 pattern-matching 编译成一个连续的基本 pattern-matching（最多具有深度模式）一）。但是在外部 match 的 cons 分支中，如果您不明确地记录它，索引应该 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)).

作为记录，做 fiddle不可能分支的解决方案，并使用等式记录索引的信息（可能有更好的版本）：

  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 策略使用这些来丢弃不可能的分支）。

如何依赖匹配包含两个元素的列表？

How to dependent match on a list with two elements?

coq