Coq: Admettre assertion

Question

Existe-t-il un moyen d'admettre s'affirme dans Coq?

Supposons que j'ai un théorème comme ceci:

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 ci-dessus ne semble pas fonctionner pour moi.

L'erreur que je reçois est:

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

Ce que je veux est quelque chose comme undefined dans Haskell. Baiscally, j'y reviendrai plus tard et je le prouverai. Y a-t-il quelque chose comme ça dans Coq pour y arriver?

Answer 1

En général, la tactique admit (première lettre minuscule) admet le sous-objectif courant. Ainsi assert <your assertion>. admit. devrait fonctionner dans votre cas.

Ou dans toute sa splendeur comme suit.

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: La version avec ; est un non-sens, parce que vous ne voulez pas admettre tous les sous-objectifs.