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

由 发布于

EDIT: I fixed the issue by using subtypes, ie changing forall(i: nat) to

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

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

谢谢。