有没有办法在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中有类似的东西可以实现吗? 最佳答案
通常,策略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.
编辑:带有
;
的版本是废话,因为您不想接受所有子目标。