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

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

谢谢。

评论