2

我试图证明流谓词（在标准库中定义）的以下原则。

From Coq Require Import Streams.

Lemma mystream_ind :
  forall A (P : Stream A -> Prop),
    (forall s, ForAll P (tl s) -> ForAll P s) ->
    forall s, ForAll P s.
Proof.
  intros A P H.
  cofix Cof.
  destruct s as [a s].
  constructor; auto.
  destruct (H (Cons a s) (Cof s)); auto.
  Fail Guarded.
Abort.

根据我对 施加的句法保护条件的理解cofix，我将永远无法以这种方式完成证明，因为在证明术语中，Cof s必须出现在 下H，它既不是构造函数也不是匹配项等。

在 Coq 中还有其他方法吗？我用pacoForAll定义了一个明确的固定点，并试图证明这个原理，但没有成功（我根本无法实例化）。H

编辑：这个引理是不可证明的，因为False可以从它推导出来P := fun s => False（谢谢 Maëlan）。

4

0 回答 0