Use multiple statements to implement interactive fixpoints

[herbelin]

Interactive co/fixpoints (and Theorem with) used to declare a single proof starting with a dummy Fix. We reimplement it using the proof engine support for multiple statements.

This will allow to share the infrastructure for interactive fixpoints and Derive and this makes useless the copy of the types in the CInfo.t of proofs.

Depends on:

• Towards a more uniform API for declare.ml (part declaring mutual statements) #18795
• Make CSet extensible on our side, and adding CSet.List.union. #19075 (in a minor way, via Add support for Admitted on multiple statements #19090)
• Add support for Admitted on multiple statements #19090

[ejgallego]

I'm not sure what the status of #10363 is, but last time I looked the proof engine API for multiple statements was in need of serious work. But this may be an interesting experiment, let's see what the CI yields

(Tho I wouldn't be very surprised if we don't stress the particular corner cases that could be problematic)

[herbelin]

the particular corner cases that could be problematic

Are you suggesting possible issues if we use abstract in a fixpoint implemented with multiple statements? I just tried with #19092 and it produces exactly the same term, that is each body of the final constants is abstracted relatively to the abstracted subproofs.

In the case of Derive, I have:

Require Import Derive.
Derive f SuchThat (f = 0) As spec.
unfold f. abstract reflexivity.
Qed.
Print spec.
(* spec = spec_subproof : f = 0 : f = 0 *)
Print f.
(* f = 0 : nat *)

Or do you mean something else?

[ejgallego]

Back in the day I meant that we duplicated side effects on each entry, this seems un/under-specified.

[herbelin]

I would need a definition of "side effects". If it is about abstract, is the following as expected:

Fixpoint f (n:nat) : nat with g (n:nat) : nat.
- abstract (exact 0).
- exact 0.
Qed.
Print f.
(* (fun f_subproof : nat => fix f (n : nat) : nat := f_subproof with g (n : nat) : nat := 0 for f) 0 *)
Print g.
(* (fun f_subproof : nat => fix f (n : nat) : nat := f_subproof with g (n : nat) : nat := 0 for g) 0 *)

Fixpoint f (n:nat) : nat with g (n:nat) : nat.
- abstract (exact 0).
- exact 0.
Defined.
Print f.
(* fix f (n : nat) : nat := f_subproof with g (n : nat) : nat := 0 for f *)
Print g.
(* fix f (n : nat) : nat := f_subproof with g (n : nat) : nat := 0 for g *)
Print f_subproof.
(* f_subproof = 0 *)

[SkySkimmer]

this seems like it would get very long and unreadable as the number of possibilities increases.
It's already kinda bad IMO.

OTOH I don't know how to avoid listing the possibilities since the user didn't say {struct} (also I think there's currently no syntax for {struct} for Lemma with).

[herbelin]

With a bit more work, we could factorize the errors which are similar.

On the other side, #19301 adds syntax {struct} for Lemma with and for Lemma. So, an alternative could be to suggest using struct to get more information (???).

[SkySkimmer]

We could also extend the Guarded syntax to be able to say eg Guarded {struct 1, 3} {struct 3, 1} to mean "test guardedness with 1st fixpoint recursive on 1st arg and 2nd on 3rd arg, and with 1st fixpoint recursive on 3rd arg and 2nd on 1st arg"
that way in the middle of a big proof there is no need to restart it to get a better error

[herbelin]

this seems like it would get very long and unreadable as the number of possibilities increases.

With a bit more work, we could factorize the errors which are similar.

I pushed a new version simplifying a bit the printing so that in the "Not enough abstractions", it is printed only once.

[herbelin]

We could also extend the Guarded syntax to be able to say eg Guarded {struct 1, 3} {struct 3, 1}

That's a good idea.

To depart not too much from the existing syntax, we could also say, e.g.: Guarded {struct 1} {struct 3} and repeat it for any combination we are interested in??

[SkySkimmer]

yes

[herbelin]

Do you want me to implement it? (And otherwise, I'd be happy if ever you have some time for it.)

[SkySkimmer]

Why are we keeping copies of the env?

[herbelin]

The first env is the context for the whole declaration. The other envs are the contexts for the respective errors.

[SkySkimmer]

test suite not happy

[herbelin]

Adding -async-proofs off to see if it makes test-suite:base+async happier (full CI was otherwise ok).

[ppedrot]

Isn't this just ignoring the problem? What was the cause for the async failure?

[SkySkimmer]

Output tests don't work well with async because it changes printing order
also IIRC it sometimes loses location info

[SkySkimmer]

(although in https://gitlab.inria.fr/coq/coq/-/jobs/4572169 it seems it entirely lost some messages so not sure what's going on)

[SkySkimmer]

We should probably use "-async-proofs-cache" "force" so that Undo works without repeating the previous messages

[SkySkimmer]

the lack of repetition with async proofs on is probably what caused the issue

[SkySkimmer]

alternatively write a test without Undo (I guess Abort then repeat the code for the start of the proof)

[herbelin]

OK, then, considering #19383, tell me when you know what the recommended approach will be.

[SkySkimmer]

#19383 should not really matter for this AFAIK

[herbelin]

OK, so a test w/o Undo, right?

[SkySkimmer]

You have the power to choose.

[ppedrot]

@coqbot run full ci

[ppedrot]

@SkySkimmer if you're happy with the current status I can merge when CI finishes.

[herbelin]

@coqbot run full ci

[ppedrot]

@coqbot merge now