Coq : Admit assert

Question

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.

The error I receive is:

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

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 ?

Blackfish

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

@Tolmann Thanks, that works. Can you post that as an answer ? – Blackfish

Answer 1

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.

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

Tolmann

Also, as of Coq 8.5 (I think not earlier), any proof script with admit in it needs to be ended with Admitted. instead of Qed./Defined. if you want to save the result. – Udine

@AntalSpector-Zabusky Ending it with Qed works for me in version 8.4pl4. – Blackfish

ANother syntax is assert (H1: m + m * n = m * S n) by admit. – Vannesavanness