search

coq / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
https://coq.inria.fr/
GNU Lesser General Public License v2.1
4.78k stars 639 forks source link

Ssreflect `have` construct failing with `Incorrect number of goals` #15019

Open jouvelot opened 2 years ago

jouvelot commented 2 years ago

The Ssreflect have construct fails in a somewhat unexpected way. The error message is

Error: Tactic failure: Incorrect number of goals (expected 1 tactic).

Note that adding a dummy argument to foo (i.e., have foo n:) makes it succeed. 

From Coq Require Import ssreflect.

Lemma Peirce (A B : Prop) : ((A -> B) -> A) -> A.
Proof. 
have foo: A -> B.

Coq 8.13.0 (also fails in jsCoq)

ejgallego commented 2 years ago

I was able to reproduce this back to Coq 8.5 [thanks jsCoq :)] so indeed, not a new problem.

Note that this only happens when the goal in have is a subterm of the main goal. See even weirder behavior:

have foo n : A -> B.              (* works *)
have foo : A -> B := _ .          (* 100% bizarre *)