Tracking relationships between goals

[cpitclaudel]

Hey @ejgallego,

How hard would it be to expose parent-child relationships between goals in the API? At the moment SerAPI prints less information than coqtop -emacs (the latter has a unique ID for each goal, printed after the goal number in PG, which is robust to things like cycling goals, etc), but even the information that coqtop -emacs contains isn't sufficient when a command affects multiple goals.

Here are some benchmarks:

Axiom P111 P112 P113 P121 P211 : Prop.
Axiom magic: forall {A}, A.

Goal ((P111 /\ P112 /\ P113) /\ P121) /\ P211.
  split.
  - split.
    + repeat split.
      * refine ?[G111]. exact magic.
      * refine ?[G112]. exact magic.
      * refine ?[G113]. exact magic.
    + refine ?[G121]. exact magic.
  - refine ?[G211]. exact magic.
Qed.

Goal ((P111 /\ P112 /\ P113) /\ P121) /\ P211.
  split.
  split.
  repeat split.
  refine ?[G111]. exact magic.
  refine ?[G112]. exact magic.
  refine ?[G113]. exact magic.
  refine ?[G121]. exact magic.
  refine ?[G211]. exact magic.
Qed.

Goal (P111 /\ P112 /\ P113) /\ (P121 /\ P211).
  split.
  all: cycle 1; repeat split.
  all: cycle 1.
  all: exact magic.
Qed.

I think we can already handle most of these as long as there are no reorderings, but things break as soon as there's a cycle command. Exposing Coqtop's goal IDs would partly fix the problem, but it wouldn't help with things like all: split.

In all these cases we'd like to generate the same proof tree; ideally that would be done by adding a unique id to each goal and unique parent field pointing to that goal's parent.

CC @hendriktews; Hendrik (hi!), how do you handle commands like all: split in prooftree?

[hendriktews]

how do you handle commands like all: split in prooftree?

This is not working. Prooftree assumes that all new subgoals are children of the last current goal.

all: exact magic.

This would probably confuse prooftree in strange ways, because non-current subgoals disappear. cycle and focus should work. all: split is still a simple example, because the proof stays a tree. In general one could also think of tactics that generate 3 new goals out of 5 open goals without a clear parent-child relation. This would change the proof tree into a directed acyclic graph. Isabelle has this feature for decades already. But all the people I spoke to said they are always only working on the last goal. Therefore I tend to the opinion that working on several open goals in parallel is not so relevant practically. Hendrik

[cpitclaudel]

Thanks for the reply. Makes sense.

[ejgallego]

Umm, I am not sure there is a notion of "parent" goal, I guess tho we could indeed expose the evar_map and you could determine the partial order of evar instantiation. That could be effective, but maybe it works as there is no GC.

@ppedrot @SkySkimmer , would doing something like that be too crazy?

For now I'm gonna address ejgallego/coq-serapi#20 , just to see what kind of data we get.

[ejgallego]

Ok, ejgallego/coq-serapi#20 is addressed in ejgallego/coq-serapi#256 , so indeed, I think my strategy may work, tho not sure what would be the output data structure for you to consume @cpitclaudel

[ppedrot]

The whole tactic engine has been rebuilt precisely around the fact that the notion of child goal does not make sense in general. By contrast, the pre-8.5 engine was based on it, leading to nonsensical situations.

Obviously you can find some specific instances where you can define the relationship, but defining it generically would completely defeat the purpose. Even an acyclic graph is not enough, because goals can be solved and created at distance by e.g. unification. The only stable notion of proof is the underlying term, and if you take this view seriously it's pretty clear that because of dependent types you can get weird situations with type computations substituting evars in non-linear ways. Isabelle is based on HOL so the setting is totally different.

[cpitclaudel]

I think I don't follow. My naive understanding was this: a goal is an evar. Applying a tactic means replacing some of the current evars with terms containing more evars. Then the parent-child relationship is "a goal is a parent of another goal if its evar is replaced by a term containing the evar of the new goal". That defines a DAG, not a tree, though in fact that DAG is a tree in 90 (99?) percent of the cases. Maybe this is too naive.

The whole tactic engine has been rebuilt precisely around the fact that the notion of child goal does not make sense in general.

Does this really matter, though? In practice, aren't most tactics are still more or less goal → list goal, even if the engine itself is list goal → list goal?

Besides, doesn't each newly created evar inherit the context of one of the existing evars? If so, what's going to go wrong if you declare that evar's parent to be whichever evar's context was inherited?

defining it generically would completely defeat the purpose

Defeat which purpose?

Even an acyclic graph is not enough, because goals can be solved and created at distance by e.g. unification.

Why does action at a distance mean cycles?

The only stable notion of proof is the underlying term

Bit that isn't cyclic.

[ppedrot]

Does this really matter, though? In practice, aren't most tactics are still more or less goal → list goal, even if the engine itself is list goal → list goal?

No. It's state × list goal → state × list goal, where state is a heap of evars. So by simply applying unification in a goal, you might solve a goal in an unrelated part of the proof and generate new subgoals. What would be the parent goal then? The original one or the one from which unification was called? Now if you throw in the fact that there could even have been several goals under focus at the time unification solves the goal, you get something that doesn't look like a tree at all.

Why does action at a distance mean cycles?

There are no cycles. The problem is that when you call unification there is no such thing as a "current goal" so you cannot define a meaningful parent.

[cpitclaudel]

No. It's state × list goal → state × list goal, where state is a heap of evars. So by simply applying unification in a goal, you might solve a goal in an unrelated part of the proof and generate new subgoals. What would be the parent goal then?

What goes wrong if you apply my heuristic from above (using whichever evar the context was inherited from as the parent? (It's possible that I'm not understanding, in which case an example would help a lot).

Does the following capture the issue you have in mind?

Open Scope nat_scope.
Goal exists n: nat, 1 <= n.
  unshelve eexists.
  pose proof 1.
  2: pose proof true.
  2: unshelve apply le_S.

In that case it looks like that the parent of the evar that gets created by apply le_S is the evar that had been created by eexists, which is fine by me.

There are no cycles.

But you wrote "Even an acyclic graph is not enough"… what did that mean?

(Maybe some context helps, here: I'm trying to show diffs between consecutive proofs steps. I don't care too much about the "tree" structure of the proof, only to find the most relevant goal to compare to. If in some case there are more than one parent, then it's fine to not compare. But comparison is meaningful in most cases.)

[ppedrot]

Does the following capture the issue you have in mind?

Indeed.

In that case it looks like that the parent of the evar that gets created by apply le_S is the evar that had been created by eexists.

This is one way to see it, which is consistent with your view that the parent of an evar is the one from which the context is inherited. This would be the "region-oriented" notion of evar seen as a pointer in a heap. But you could also argue as well that the goal solved by apply le_S is the parent, since the new evar also appears in the subterm corresponding to that subproof. This would correspond to some "ownership stealing" of the evar pointer. Notably, the unshelve call in your example follows this semantics as you can witness if you focus on the second goal.

Both make sense depending on the use you want to make of it. There are complex situations where none fit the bill, notably eauto-like tactics which display complex subgoal relationships and were precisely the motivation for the introduction of the new engine.

Also note that there are no reason for which a evar must inherit a context from another one. I am too tired to think of a realistic instance, but as a cooked up example consider generating an open term from a multigoal Ltac code.

But you wrote "Even an acyclic graph is not enough"… what did that mean?

Evars are actually higher-order objects, since they quantify over their contexts. Depending on your criterion for parenthood, you might need to consider graphs that encode some kind of higher-order rewriting system.

Defeat which purpose?

I am not being clear, so let me state it this way: trying to enforce a notion of subgoal primitively in the tactic engine is bound to create a mess because there are various incompatible ways to define it. The 8.5 engine simply embraces chaos and represents a partial proof as a blob heap and lets the user define their own meaningful notion themselves.

[cpitclaudel]

The 8.5 engine simply embraces chaos and represents a partial proof as a blob heap and lets the user define their own meaningful notion themselves.

Ah, excellent! I think this is precisely what we're trying to do here :)