围绕“伊利姆限制”的问题

如何解决围绕“伊利姆限制”的问题

我目前正在阅读Gert Smolka撰写的《用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
).

但是，由于严格的限制，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)).

解决方法

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

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

“无条件”位于match上任何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)).

,

那是一个棘手的问题。 作者没有错，可以定义这样的消除原理，但是您必须小心如何以及何时匹配假设。

从Coq得到的错误是，您正在匹配某个命题以构建Type元素。 Coq禁止这样做，以便在提取代码时可以删除命题，因此您无法对命题进行案例分析以构建一些具有计算意义的对象（例如，对于空命题，此规则有例外）。

由于无法从H2上的模式匹配开始，因此可以尝试将案例分析尽可能推迟。在这里，您只需要在应用程序(h e)中进行案例分析，因此可以将其替换为match H2 with mkG _ n' h -> h e end。

但是这不起作用，因为h的类型为f' n' = false -> ...，而e : f n = false的类型则需要向Coq解释n和n'是相同的。这是通过以下方式实现的：依赖模式匹配，将拼写放在匹配之外，并在下面的脚本中使用return子句（实际上Coq可以推断出该return子句，我只是将其留作解释）。

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

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.
Proof.
  refine (g n (fun e => elimG f p g (S n) _)).
  refine (match H in G _ n0 return f n0 = false -> G f (S n0) with mkG _ _ h => h end e).
Qed.