coq程序模块抛出了我的假设

Question

编辑：我通过使用子类型（即更改了forall(i: nat)至

forall(i: {n: nat | n <? length})

但是我仍然想知道程序模块为什么会这样表现，以及是否有什么我可以做的。这两个程序在逻辑上是等效的，因此对一个程序进行类型检查而对另一个程序则不这样做是很愚蠢的。

我正在尝试编写此功能

Program Fixpoint indomain_arr (m: mem) (a: array) :=
  match a with Array _ length => forall(i: nat), (i< length -> indomain m (inr(El a i))) end.
Obligation 1.

我认为，细节并不是太重要，除了我有（i

  m : mem
  wildcard' : string
  length, i : nat
  ============================
  i <? length

这很烦人，因为它不包括我专门在输出命题中提出的假设，以便我可以解决这一义务。解决办法是什么？如何将这个假设重新带入我的语境？

谢谢。

Answer 1

我在coq 8.11.1中尝试过此代码。

Require Import Program.
Require Import Arith.

Inductive P (n : nat) : (n =? 0 = true) -> Prop :=
| P_intro : forall p, P n p.

Program Definition f (n : nat) : Prop :=
  forall (i : nat), i < n -> P i _.
Next Obligation.

这导致证明状态

  n, i : nat
  ============================
  (i =? 0) = true

没有i < n作为假设。

我尝试了f的另一个定义。

Program Definition f (n : nat) : Prop :=
  forall (i : nat) (Hsmall : i < n), P i _.
Next Obligation.

（注意，假设i < n被明确命名为Hsmall）

现在，我的假设处于证明状态。

  n, i : nat
  Hsmall : i < n
  ============================
  (i =? 0) = true