Coq：承认断言 [英] Coq : Admit assert

问题描述

是否有一种方法可以接受Coq中的断言？

Is there a way to admit asserts in Coq ?

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

Suppose I have a theorem like this:

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

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

The above assert doesn't seem to work for me.

我收到的错误是：

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

我想要的是类似 undefined 哈斯克尔。 Baiscally，我稍后会再来证明这一点。在Coq中是否有类似的东西可以实现它？

What I want is something like undefined in Haskell. Baiscally, I will come back to this later and prove it. Is there something like that in Coq to achieve it ?

推荐答案

通常，战术允许（小写的第一个字母）接受当前的子目标。因此，断言<您的断言>。承认。应该适合您的情况。

In general the tactic admit (lower-case first letter) admits the current subgoal. Thus assert <your assertion>. admit. should work in your case.

或按如下方式充分发挥其作用。

Or in its full glory as follows.

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

编辑：带有; 的版本是废话，因为您不想接受所有子目标。

The version with ; is nonsense, because you do not want to admit all subgoals.

这篇关于Coq：承认断言的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！