Stream: Coq devs & plugin devs

Topic: Unifying the effect of "Program"


view this post on Zulip Hugo Herbelin (Mar 30 2024 at 10:17):

Currently, we have the following:

Re

view this post on Zulip Gaëtan Gilbert (Mar 30 2024 at 10:29):

?

view this post on Zulip Hugo Herbelin (Mar 30 2024 at 11:58):

Sorry, draft incomplete message sent by mistake.

view this post on Zulip Hugo Herbelin (Apr 01 2024 at 08:58):

Here is basically what I intended to say.

Currently, the keyword Program has different behaviors depending on the kind of statements. Basically, it may cover five kinds of behaviors:

  1. special treatment of subtypes in pretyping + special treatment of type classes (in all situations, i.e. Theorem, body-free and body-provided Definition, body-free and body-provided Co/Fixpoint)
  2. use of the obligation tactic to solve all kinds of evars (only in - possibly mutual - Theorem and body-free Definition)
  3. declaration of unresolved ImplicitArg and QuestionMark evars as obligations (only in body-provided Definition and - mandatorily non-mutual, mandatorily body-provided - wf/measure-based Fixpoint)
  4. declaration of all unresolved evars as obligations (only in - mandatorily body-provided non-wf-measure - Co/Fixpoint)
  5. encapsulation of fixpoints in Program.Wf.Fix_sub (only in - mandatorily non-mutual, mandatorily body-provided - wf/measure-based Fixpoint)

As an example of 2., 3. and 4., we can observe:

Require Import Program.
#[global] Obligation Tactic := try exact nat.
Program Definition f a : nat. (* a is inferred of type nat (case 2.) *)
Program Definition f a : nat := 0.
  (* Error: Cannot infer the type of a. (case 3: not an ImplicitArg nor QuestionMark evar) *)
Program Definition f (a : id _)  : nat := 0.
  (* The argument of "id" is a QuestionMark evar opened as an obligation constant
     and solved by the obligation tactic (case 3.) *)
Program Fixpoint f a (b:nat) : nat. (* Error: Program Fixpoint requires a body *)
Program Fixpoint f a (b:nat) : nat := S 0.
  (* The type of "a" is a non-ImplicitArg non-QuestionMark evar opened as an obligation constant
     and solved by the obligation tactic (case 4.) *)
Program Fixpoint f a (b:nat) {measure b} : nat := S 0.
  (* Error: Cannot infer the type of a. (case 3: not an ImplicitArg nor QuestionMark evar) *)

In the direction of unifying behaviors in CEP #42, would there be a way to make this more regular?

view this post on Zulip Hugo Herbelin (Apr 01 2024 at 08:59):

I've the feeling that behavior 4. is not intended and that the intent was to restrict to ImplicitArg and QuestionMark evars, as in 3. Can this be confirmed?

I've the feeling that behavior 2. could also be not intended and that it could be restricted to ImplicitArg and QuestionMark evars, as in 3. Is it a correct intuition? (At least, the examples using the feature in the test-suite are of this form, iirc.)

As for the general 1. and the wf/measure specific 5., they seem clear.

So, assuming the restriction to ImplicitArg and QuestionMark is generalized in 2., 3. and 4., it remains to make a choice between representing the evars solved by the obligation tactic either directly or via an obligation constant. Any opinion? At worst, in the short term, I'm going to make this configurable.

view this post on Zulip Hugo Herbelin (Apr 01 2024 at 09:05):

Note: Eventually, and independently of Program, we may also want to be more fine-grained, and have some evars solved by automation (instance search or other forms of automation), other turned into obligations, other being a failure if not resolved. For instance, I'm thinking to a variant of Arguments where we can indicate a tactic to be used by default to resolve an implicit argument (say something like Arguments f {x by some-tactic}).

view this post on Zulip Hugo Herbelin (Apr 02 2024 at 11:58):

While talking about Program, shouldn't we error when a non extensible universe declaration is given in Program Fixpoint because the later adds reference to fix_proto (and even to MR and Fix_sub when wf/measure is given), so that new universes that cannot be controlled may arrive. Consider e.g.:

Set Universe Polymorphism.
  Program Fixpoint f@{u} (A:Type@{u}) (n:nat) : Type@{u} :=
    match n with 0 => A | S n => f (A->A) n end.
Print f.
(* f@{u u0} = ... *)

where u0 comes from an internal call to fix_proto.

Actually, I have more general question, maybe to @Matthieu Sozeau: what is the role of the fix_proto and MR wrappers? Is it to control type classes?

view this post on Zulip Gaëtan Gilbert (Apr 02 2024 at 13:04):

about the program inference hook
currently it is only called on evar free subgoals, but this may be an accident of using an implementation which doesn't support evars instead of a deliberate choice
after https://github.com/coq/coq/pull/18881 we could change it to use it on any subgoal but do we want to?

view this post on Zulip Hugo Herbelin (Apr 04 2024 at 13:00):

but do we want to?

I don't know. I have applications in mind where I do want a hook to be applied to (only) specific evars but I don't know the generality of the thing.

I don't know also how much what I have in mind could be done via the typeclass mechanism. I'd be happy to read a summary of all techniques we currently have to solve evars.

view this post on Zulip Hugo Herbelin (Apr 04 2024 at 13:00):

but do we want to?

I don't know. I have applications in mind where I do want a hook to be applied to (only) specific evars but I don't know the generality of the thing.

I don't know also how much what I have in mind could be done via the typeclass mechanism. I'd be happy to read a summary of all techniques we currently have to solve evars.


Last updated: Oct 13 2024 at 01:02 UTC