Coq：Admit assert

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. 

上記のassertが私のために動作するようには思えません。

私が受け取るエラーは、次のとおりです。

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. 

編集：あなたはすべてのサブゴールを認めたくはありませんので、;とバージョンは、ナンセンスです。