时间戳

首页 > 解决方案 > 围绕“elim 限制”的问题

coq - 围绕“elim 限制”的问题

问题描述

我目前正在阅读 Gert Smolka 的“Computational Type Theory and Interactive Theorem Proving with Coq”一书，在第 93 页，定义了以下归纳谓词：

Inductive G (f:nat -> bool) : nat -> Prop :=
| mkG : forall (n:nat), (f n = false -> G f (S n)) -> G f n
.

然后在第 95 页上，有人认为可以定义一个消除器：

Definition elimG : forall (f:nat -> bool) (p:nat -> Type),
    (forall (n:nat), (f n = false -> p (S n)) -> p n) ->
    forall (n:nat), G f n -> p n.
Proof.
...

这本书阐明了这种类型的术语的表达方式，即：

elimG f p g n (mkG _ _ h) := g n (λe. elimG f p g (S n) (h e))

（为了这篇文章的目的，我改变了一些符号）

我正式翻译为：

refine (
    fun (f:nat -> bool) (p:nat -> Type) =>
        fun (H1:forall (n:nat), (f n = false -> p (S n)) -> p n) =>
            fun (n:nat) (H2:G f n) =>
                match H2 with
                | mkG _ _ H3  => _
                end
).

但是，由于 elim 限制，Coq 不允许我执行模式匹配。这本书非正式地说“检查定义方程的elimG类型是否正确并不困难”

我发布这个是希望熟悉这本书的人对作者是否犯了错误或我是否遗漏了什么有意见。

编辑： 玩弄了下面的两个答案，我想出的最简单的术语表达如下：

Definition elimG 
    (f:nat -> bool) 
    (p:nat -> Type)
    (g: forall (n:nat), (f n = false -> p (S n)) -> p n)
    : forall (n:nat), G f n -> p n 
    := fix k (n:nat) (H:G f n) : p n := g n 
        (fun e => k (S n) 
            ( match H with
              | mkG _ _ H => H
              end e)).

标签： coq

解决方案

这个定义是可能的，这里有一个微妙之处。（G在 中的Prop）永远不需要在这里做出决定，因为它只有一个构造函数。所以你只要做

elimG f p g n h := g n (λe. elimG f p g (S n) _)

“无条件地”在任何matchon之外h。那个洞现在有了预期的类型G f (S n)，现在在里面Prop，我们可以match在h那里做我们的。我们还必须对match. 把所有东西放在一起，我们写

Fixpoint elimG
  (f : nat -> bool) (p : nat -> Type)
  (g : forall (n:nat), (f n = false -> p (S n)) -> p n)
  (n : nat) (H : G f n) {struct H}
  : p n :=
  g n
   (fun e =>
      elimG f p g (S n)
       (match H in G _ n return f n = false -> G f (S n) with (* in and return clause can be inferred; we're rewriting the n in e's type *)
        | mkG _ _ H => H
        end e)).

推荐阅读