时间戳

首页 > 解决方案 > 从 GADT 检索约束以确保在 Coq 中耗尽模式匹配

coq - 从 GADT 检索约束以确保在 Coq 中耗尽模式匹配

问题描述

让我们定义两个助手类型：

Inductive AB : Set := A | B.
Inductive XY : Set := X | Y.

然后是其他两种依赖于XY和的类型AB

Inductive Wrapped : AB -> XY -> Set :=
| W : forall (ab : AB) (xy : XY), Wrapped ab xy
| WW : forall (ab : AB), Wrapped ab (match ab with A => X | B => Y end)
.

Inductive Wrapper : XY -> Set :=
  WrapW : forall (xy : XY), Wrapped A xy -> Wrapper xy.

注意WW构造函数——它只能是类型Wrapped A X和Wrapped B Y.

现在我想进行模式匹配Wrapper Y：

Definition test (wr : Wrapper Y): nat :=
  match wr with
  | WrapW Y w =>
    match w with
    | W A Y => 27
    end
  end.

但我得到错误

Error: Non exhaustive pattern-matching: no clause found for pattern WW _

为什么会这样？Wrapperforce 包含Wrapped为Aversion，类型签名 forceY和构造函数同时WW禁止存在。我不明白为什么还要考虑这个案子，而我却不得不检查它，这似乎是不可能的。AY

如何解决这种情况？

标签： coqdependent-typegadt

解决方案

让我们简化一下：

Inductive MyTy : Set -> Type :=
  MkMyTy : forall (A : Set), A -> MyTy A.

Definition extract (m : MyTy nat) : nat :=
  match m with MkMyTy _ x => S x end.

这失败了：

The term "x" has type "S" while it is expected to have type "nat".

笏。

这是因为我说

Inductive MyTy : Set -> Type

这使得第一个参数成为MyTy的索引MyTy，而不是参数。带参数的归纳类型可能如下所示：

Inductive list (A : Type) : Type :=
  | nil : list A
  | cons : A -> list A -> list A.

参数在 的左侧命名:，并且在每个构造函数的定义中都不是forall-d。（它们仍然存在于定义之外的构造函数类型中：cons : forall (A : Type), A -> list A -> list A。）如果我将Seta 参数设为MyTy，则extract可以定义：

Inductive MyTy (A : Set) : Type :=
  MkMyTy : A -> MyTy A.

Definition extract (m : MyTy nat) : nat :=
  match m with MkMyTy _ x => S x end.

这样做的原因是，在内部，amatch 忽略了您从外部了解的关于被检查者索引的任何信息。（或者，更确切地说，Gallina 中的底层match表达式忽略了索引。当您在源代码中编写 a时，Coq 会尝试将其转换为原始形式，同时结合索引中的match信息，但通常会失败。）m : MyTy nat第一个版本extract根本没关系。相反，匹配给了我S : Set（名称由 Coq 自动选择）x : S，并且根据构造函数MkMyTy，没有提及nat. 同时，因为MyTy在第二个版本中有一个参数，我实际上得到了x : nat. 这_这次真的是占位符；必须把它写成_，因为没有什么可以匹配的，你可以Set Asymmetric Patterns让它消失。

我们区分参数和索引的原因是因为参数有很多限制——最明显的是，如果I是带参数的归纳类型，那么参数必须作为变量出现在每个构造函数的返回类型中：

Inductive F (A : Set) : Set := MkF : list A -> F (list A).
                                            (* ^--------^ BAD: must appear as F A *)

在您的问题中，我们应该尽可能地制作参数。例如match wr with Wrap Y w => _ end位是错误的，因为XY参数Wrapper是一个索引，所以这个事实wr : Wrapper Y被忽略了；你也需要处理这个Wrap X w案子。Coq 还没来得及告诉你这些。

Inductive Wrapped (ab : AB) : XY -> Set :=
| W : forall (xy : XY), Wrapped ab xy
| WW : Wrapped ab (match ab with A => X | B => Y end).

Inductive Wrapper (xy : XY) : Set := WrapW : Wrapped A xy -> Wrapper xy.

现在你的test编译（几乎）：

Definition test (wr : Wrapper Y): nat :=
  match wr with
  | WrapW _ w => (* mandatory _ *)
    match w with
    | W _ Y => 27 (* mandatory _ *)
    end
  end.

因为拥有这些参数可以为 Coq 提供足够的信息，以供其match使用Wrapped's 索引中的信息。如果您发出Print test.，您会看到有一些跳跃性的Y通过原语matchs 传递有关索引的信息，否则会忽略它。有关详细信息，请参阅参考手册。

推荐阅读