Search code examples
coqtheorem-proving

Coq : Admit assert

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 ?

Solution

  • 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.