Goals with large context

[thery]

I have goals with very large context. When hovering over tactics.
I mostly see the initial assumptions. Is there a way to activate some scrolling
or at least have the visible part concentrated on the conclusion?

[cpitclaudel]

We could have a maximum height on the hypotheses area. I wonder if CSS has a way to say "truncate at top, not at bottom".

[cpitclaudel]

Related: #15

[thery]

maybe giving the possibility to display only the assumptions that have changed would be nice

[Casteran]

maybe giving the possibility to display only the assumptions that have changed would be nice

Giving options like (all-hyps -hyp1 -hyp2 ... ) or (no-hyps + hyp1 +hyp2 ... ) ?

[thery]

I was thinking more on something in the line of this where one displays onl waht has changed.

[Casteran]

Ok, I see! For my part, I’m working on using Alectryon for writing a pdf document. When commenting the main steps of a long proof, I often present some sub-goal, then the tactic for solving it. But displaying the full context results in a often hard to read block. So, I wish to display only the hypotheses which really matter.

…

Le 5 août 2021 à 12:12, Laurent Théry ***@***.***> a écrit : I was thinking more on something in the line of this <https://coq.inria.fr/refman/proofs/writing-proofs/proof-mode.html#showing-differences-between-proof-steps> where one displays onl waht has changed. — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#36 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AJW6FCR5FEQBZUY2I5MPV2TT3JPZHANCNFSM43DTAZ4Q>. Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&utm_campaign=notification-email>.

[cpitclaudel]

@thery I would love to do this, and it's been on my list for a while.

The problem is that Coq doesn't expose enough info right because the tree structure of goals is not exposed (there's no way to know which "parent" goal a new goal came from). This makes it hard to know what to compute diffs against: of course there's the problem of tactics like cycle or swap, but more importantly there's tactics that split cases: the first goal of the second case of an induction should be compared to the initial state, not to the last goal of the first case.

[cpitclaudel]

@Casteran I like this idea, even though it's a different use case indeed. I think it's just a matter of improving the annotation mini-language.

[thery]

I guess in my context as the context is very large, diff with sibling or ancestor both would do the trick.
but I understand it could be difficult to do if Coq does not help.
I am wondering how the diff is implemented when running coqtop -diffs on. Is there a way to get the info with serapi. Maybe @ejgallego knows.

[cpitclaudel]

-diffs on was implemented by @jfehrle; Jim, I'm hoping I didn't forget about a previous discussion, but apologies in advance if I did: how do you determine which old goal to compare a new goal against when computing diffs? IIRC in a proof by induction you don't show a diff for the first goal of a branch, right?

[cpitclaudel]

@Casteran I've implemented a prototype to allow you to select hypotheses and goals to display. It shares the language introduced for @jhaag in #2. Please see https://github.com/cpitclaudel/alectryon#controlling-output and the following sections.

Source:

Result:

[thery]

how do you determine which old goal to compare a new goal against when computing diffs?

Apparently diffs compares with the state before the tactical call which seems reasonable. I have tried

 forall P : nat -> Prop, (P 2 -> P 1 -> P 1 -> P 1) -> P 1

after intros P H, if I do apply H, it tells me that the first goal has changed while the others don't.

[jfehrle]

A short answer for now: The comments in proof_diffs.ml above match_goals explain a little. AFAIK the heuristic almost always recovers the parent/child relationships, but it can't handle a few tactics, such as clear, that modify parents rather than only resolving subgoals. I think serapi doesn't know about this info.

Well after creating that mapping, I learned that the kernel has a data structure with all evars (IIRC both resolved and unresolved), from which it would be even easier to recover these relationships and get the complete family tree of the contexts, then make it available through some API. The data structure match_goals operates on is derived from that kernel data structure.

Switching to the kernel data structure may not be entirely trivial but shouldn't be that hard.

IIRC in a proof by induction you don't show a diff for the first goal of a branch, right?

I think it would show a diff compared to the previous goal for both induction subgoals. Why don't you try it?

[jfehrle]

Also, db_goal_map will print the derived mapping.

[jfehrle]

And a few more comments above make_goal_map_i.

[cpitclaudel]

Thanks @jfehrle .

I think it would show a diff compared to the previous goal for both induction subgoals. Why don't you try it?

I did, and I didn't understand the result; hence the question:

It seems it shows diffs only in the first subproof?

@thery :

Apparently diffs compares with the state before the tactical call which seems reasonable.

The problem is: what is the "state before" for the second goal of an induction, when it gets focused?

Goal forall n: nat, n > 0 -> True.
  destruct n.
  - ….
  - (* Here *)

[thery]

not sure the diff works well with focus.

[cpitclaudel]

That, but also in the screenshot above, where there's no focus

[jfehrle]

@cpitclaudel I think you skipped over what I said above about that diff can't handle a few tactics, such as clear, that modify parents rather only resolving subgoals. Though I'm a little surprised you get a silent error rather than an exception. Perhaps you would submit an issue for this? See coq/coq#14457 (in 8.14). You can see the diff here:

[jfehrle]

Though this gives the same diff result for your example:

The change is computed relative to the first previous non-trivial step rather than the parent goal. (cycle and swap are trivial). If we had the tree structure of the goals, it would be easy enough to compare against the parent, but it may confuse users because exact I didn't change the second goal. Off the top of my head, we could a) redefine diff as always in relation to the parent goal, b) make "a" a settable option, and/or c) provide some labelling like "diff relative to proof step 999" and include proof step numbers in the context display. But getting the parent without having the tree structure is rather unappealing--potentially you would need to examine many, many steps in some cases.

[cpitclaudel]

The change is computed relative to the first previous non-trivial step rather than the parent goal.

Got it, thanks.

But getting the parent without having the tree structure is rather unappealing

Yes, that's precisely the info I was talking about.