Coq :允许断言

Question

有没有一种在Coq中允许断言的方法？

假设我有一个这样的定理：

Theorem test : forall m n : nat,
    m * n = n * m.
Proof.
  intros n m.
  assert (H1: m + m * n = m * S n). { Admitted. }
Abort.

上面的断言似乎对我不起作用。

我收到的错误是：

Error: No focused proof (No proof-editing in progress).

我想要的是类似于Haskell中的undefined。Baiscally，我稍后会回来证明这一点。在Coq中有没有类似的东西来实现它？

Answer 1

通常，策略admit (小写第一个字母)接受当前的子目标。因此，assert <your assertion>. admit.应该适用于您的情况。

或者在它的全部荣耀中如下所示。

Theorem test : forall m n : nat,
  m * n = n * m.
Proof.
  intros n m.
  assert (H1: m + m * n = m * S n). admit.
Abort.

编辑:使用;的版本是无稽之谈，因为您不想承认所有子目标。