Coq中的依赖模式匹配

Question

下面的代码（当然不是完整的证明）尝试对依赖乘积进行模式匹配：

Record fail : Set :=
  mkFail {
      i : nat ;
      f : forall x, x < i -> nat
    }.

Definition failomat : forall (m : nat) (f : forall x, x < m -> nat), nat.
Proof.
  intros.
  apply 0.
Qed.

Function fail_hard_omat fl : nat := failomat (i fl) (f fl).

Definition failhard fl : fail_hard_omat fl = 0.
refine ((fun fl =>
          match fl with
            | mkFail 0 _ => _
            | mkFail (S n) _ => _
          end) fl).

尝试执行时出现的错误如下：

Toplevel input, characters 0-125:
Error: Illegal application (Type Error): 
The term "mkFail" of type
 "forall i : nat, (forall x : nat, x < i -> nat) -> fail"
cannot be applied to the terms
 "i" : "nat"
 "f0" : "forall x : nat, x < i0 -> nat"
The 2nd term has type "forall x : nat, x < i0 -> nat"
which should be coercible to "forall x : nat, x < i -> nat".

看起来替换在某种情况下无法到达内部类型参数。

- schoppenhauer

---

实际上，“match foo with bar”结构在依赖类型中并不容易使用。您需要使用更复杂的“match foo as bar return bli with blo”结构来向Coq解释替换的过程。我现在还不确定如何正确地做到这一点，但我会尝试一下。 - Vinz

Answer 1

在使用Program命令后，我成功地构建了一个适合您的细化程序，但我并不完全理解我所做的一切。主要思想是通过引入中间等式作为替换中的桥梁来帮助Coq进行替换。

    refine ((fun fl =>

    match fl as fl0 return (fl0 = fl -> fail_hard_omat fl0 = 0) with
      | mkFail n bar =>
        match n as n0 return (forall foo: (forall x:nat, x < n0 -> nat), 
           mkFail n0 foo = fl -> fail_hard_omat (mkFail n0 foo) = 0) with 
       | O => _
       | S p => _
       end bar
    end (eq_refl fl) ) fl).

无论如何，我不知道你在这里的目的是什么，但我建议永远不要手动编写依赖匹配并依赖于Coq的策略。在您的情况下，如果您使用Defined.而不是Qed定义Definition failomat，则您将能够展开它，并且您将不需要依赖匹配。

希望能有所帮助， V。

注意：可以将bar的两个出现替换为下划线。

- Vinz

---

我仍然认为Coq应该自动执行这个替换。 - schoppenhauer

我认识很多有同感的人 :) 欢迎在Coq-club邮件列表上讨论这个话题。Coq的开发团队非常小，他们没有时间实现所有好的想法，但是他们有这些想法！ - Vinz

Answer 2

另一种稍微不太复杂的选择是使用 nat 和 fail 的归纳组合器。

Print nat_rect.
Print fail_rect.

Definition failhard : forall fl, fail_hard_omat fl = 0.
Proof.
refine (fail_rect _ _). (* Performs induction (projection) on fl. *)
refine (nat_rect _ _ _). (* Performs induction on fl's first component. *)
Show Proof.

- user3551663

---

我曾以为模式匹配和归纳本质上是相同的东西。它们之间实际上有什么区别？ - schoppenhauer

我不知道为什么，但你可以看到类型推断变得更容易了。此外，普通模式匹配不允许递归。你需要使用一个 fix 或者 Fixpoint 命令来实现递归（或者更高级的命令如 Function 和 Program）。fix 允许在不使用归纳组合子时证明某些类型的递归。Function 和 Program 命令使证明终止更加方便。 - user3551663