Currently, we have the following:
Re
?
Sorry, draft incomplete message sent by mistake.
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:
Theorem
, body-free and body-provided Definition
, body-free and body-provided Co
/Fixpoint
)Theorem
and body-free Definition
)ImplicitArg
and QuestionMark
evars as obligations (only in body-provided Definition
and - mandatorily non-mutual, mandatorily body-provided - wf
/measure
-based Fixpoint
)wf
-measure
- Co
/Fixpoint
)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?
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.
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}
).
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?
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?
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.
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