Derive Plugin gives "Error: Anomaly "more than one statement."" on Admitted

[cpitclaudel]

Description of the problem

This is related to #6631 (cc @aspiwack):

Require Import Coq.derive.Derive.
Derive f SuchThat (f = 0) As proof.
Admitted.

Error: Anomaly "more than one statement."

Coq Version

8.13.0

[aspiwack]

Thanks for cc-ing me. I can't do anything about it at the moment, though. So if someone wants to take this up, please do.

[gares]

The last one that touched the piece of code raising the error is @ejgallego , I don't know if it ever worked.
It does not seem super hard to fold the current code over a list of types (but I don' know Derive at all, so maybe it is not trivial either):

coq/vernac/declare.ml

Lines 1924 to 1934 in 8615aac

	let typ = match Proofview.initial_goals entry with
	| [typ] -> snd typ
	| _ -> CErrors.anomaly ~label:"Lemmas.save_lemma_admitted" (Pp.str "more than one statement.")
	in
	let typ = EConstr.Unsafe.to_constr typ in
	let iproof = get proof in
	let pproofs = Proof.partial_proof iproof in
	let sec_vars = compute_proof_using_for_admitted proof typ pproofs in
	let uctx = get_initial_euctx proof in
	let univs = UState.check_univ_decl ~poly uctx udecl in
	finish_admitted ~pm ~pinfo:proof.pinfo ~uctx ~sec_vars ~univs

[Zimmi48]

I don't know if it ever worked.

This example already raised the anomaly in 8.6.

[SkySkimmer]

IMO we should error when admitting Derive, because you can do something like

Derive f SuchThat (f = f).

which leaves the type of f open.

[aspiwack]

@SkySkimmer This example should error out with an unsolved evar error. But does it mean that raising an error is always the appropriate behaviour? It wouldn't be my intuition.

[ejgallego]

Indeed for the versions I'm familiar with Derive + Admitted was never implemented. It wouldn't be hard to do so, just need to case on the proof_ending record and implement the right logic, tho it'll be a bit low-level, likely what we want to do there is handle a list of typ to compute the sec vars. After that indeed we have another problem with the declaration being based on MutualEntry

I have confirmed that this concrete case never worked after looking at the original code.

IMO we should error when admitting Derive, because you can do something like

Seems the most reasonable for now.

[cpitclaudel]

IMO we should error when admitting Derive

Would that mean using AdmitAxiom+Qed? That was broken in 8.12 (Anomaly "the kernel does not support existential variables."), but it's indeed fixed in 8.13.

It would be nice to support this:

Require Import Coq.derive.Derive.

Derive f SuchThat (f + 1 = 2) As pr.
Proof.
  subst f; instantiate (1 := 42).
  admit.
  Fail Qed.
Admitted.

[ejgallego]

I wouldn't keep my hopes very high w.r.t. Derive, in the sense that it was more a proof of concept for the start_dependent API that something really battle-tested or actively developed.

In the best case it should be subsumed , externally, by equations, and internally, by an evolution of an API to better handle proofs with multiple holes where the 3 obligations / equations / and derive do rely on.

[cpitclaudel]

Interesting, how does equations replace Derive?
(For us Derive just provides a convenient way to define a dependent pair where the first component is transparent and the second is opaque)

[ejgallego]

Interesting, how does equations replace Derive?

Internally the implementations are very similar, and it has similar needs w.r.t. opaque / transparent stuff, obligations, etc...

I was planning to discuss with @mattam82 about this in person in the CUDW but the postponement / cancellation means it didn't happen [also that's quite a bit of work]

So I'm talking out of my *** here, but you could imagine even the same deriving syntax to be send to the plugin. Note that in general in equations the second part of the pair would be handled as an obligation.

Anyways, my point was that sadly, I think there is very little dev effort for derive itself, and I'd rather at some point add similar functionality to Equations and deprecate it than keep this simple but far from fully functional plugin, but of course someone could volunteer to improve it tho.

[mattam82]

Is it equivalent to Program Definition pr_proof := { f | f + 1 = 2} := exist _ _. then Next Obligation ... Defined Next Obligation ... Admitted. Definition pr := proj1_sig pr_proof ?

[mattam82]

The Derive command used in Equations is more like Haskell derived instances, so not really related to this Derive, just to be clear.

[ejgallego]

Thanks for the example @mattam82 , indeed Derive as used in the plugin is a bit confusing name, IMHO we should keep the meaning as done in equations.

The Program Definition example is interesting, and uses a custom mechanism vs the start_dependent proof API, however that API as witnessed by equations is still not powerful enough to operate without hacks [such as the ref to accumulate]

[cpitclaudel]

Is it equivalent to Program Definition pr_proof := { f | f + 1 = 2} := exist _ _. then Next Obligation ... Defined Next Obligation ... Admitted. Definition pr := proj1_sig pr_proof ?

Yes and no. We do use this pattern, but we do it with regular definitions usually, as Program Definition tends to infer too much.

Program Definition pr_proof : { f | forall x: nat, f x + 1 > 2} := exist _ _ _.

pr_proof has type-checked, generating 2 obligations
Solving obligations automatically...
pr_proof_obligation_1 is defined
1 obligation remaining
Obligation 2 of pr_proof: ((fun f : nat -> nat => forall x : nat, f x + 1 > 2) (fun x : nat => pr_proof_obligation_1 x)).

Print pr_proof_obligation_1.

pr_proof_obligation_1 = fun x : nat => x
     : nat -> nat

(Program definition is inferring f to be the identity function, which we don't want.)

[cpitclaudel]

indeed Derive as used in the plugin is a bit confusing name

I think it's "derive" as in "program derivation", which comes more readily to mind than Haskell's "deriving"

[mattam82]

Yep, that's unfortunate, Program is supposed to not try to automatically solve goals that are not in Prop.

[JasonGross]

as Program Definition tends to infer too much.

Try Obligation Tactic := idtac.?

[cpitclaudel]

Derive Plugin gives "Error: Anomaly "more than one statement."" on Admitted · Issue #13816 · coq/coq

Try Obligation Tactic := idtac.?

Yes, or use Derive :)

[ejgallego]

I was wondering if something like Derive should implemented using some meta-programming language such as Ltac2 or MetaCoq, or even à la math-comp where some notation + hacks would do the declaration dirty work for you. Seems to me to be a good use case for such tools.

[mattam82]

It is most likely trivial to implement in MetaCoq using the obligations support (keeping a similar interface as the one of today). I doubt Ltac2 would work as you need to trigger vernacular commands like declaring new constants.

[samuelgruetter]

A student I'm advising just ran into this issue. It would be nice if this just worked:

Require Coq.derive.Derive.
Derive x SuchThat (x + x = 2) As x_ok. Admitted.

Currently (Coq 8.16), it says Error: Anomaly "in Lemmas.save_lemma_admitted: more than one statement." Desired behavior would be to admit both the definition of x and x_ok.