The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 06/17/2016 07:02 PM, John Wiegley wrote:
> > > > > > Jonathan Leivent 
> > > > > > <jonikelee AT gmail.com>
> > > > > >  writes:
> > Could PG be made to show multiple complete goals if the goal window is big
> > enough?
> I'd like it if I could just always make sure that the top of the current goal
> is brought into view after each command.  I find myself manually scrolling the
> response window often when large goals are involved.

Here's a priority order of what I'd like to see without scrolling, if 
the goal window is big enough:
1. all of the goals in focus, with their hyps
2. all of the current goal, and as many of the next goals as can fit 
completely, but at least all conclusions
3. the whole current goal's conclusion, with as many hyps above it as fit

Obviously, doing various types of hiding (whole hyps, subterms, maybe 
whole non-first goals as well) impacts what would fit.  Maybe having 
some key bindings to scroll the goals window without leaving the script 
window would help as well.

Currently, I use the following minlines tactic to make best usage of 
Coq's new multiple-hyps-per-line mechanism, at least when the order of 
hyps doesn't matter to me (and I try to make my proofs hyp-order 
agnostic).  It reorgs the hyps by type and value.  Usually, I use it 
until I've got the proof completed, then remove it (which also gives me 
some feedback if I didn't make the proof hyp-order agnostic). But, 
obviously, being hyp-order agnostic isn't for everyone - it would 
probably make ssreflect unusable, for instance.

Ltac revert_all :=
  repeat lazymatch goal with H:_ |- _ => revert H end.

Ltac get_value H := eval cbv delta [H] in H.

Ltac has_value H := let X:=get_value H in idtac.

Ltac minlines :=
  idtac; (*prevent early eval*)
  let stop:=fresh "stop" in
  generalize I as stop;
  revert_all;
  let rec f :=
    try (intro;
         lazymatch goal with H:?T |- _ =>
          first[constr_eq H stop; clear stop
               |let v := get_value H in
                try match goal with H' := v : T |- _ =>
                 first[constr_eq H H'; fail 1
                      |move H before H'] end; f
               |try match goal with H':T |- _ =>
                 first[constr_eq H H'; fail 1
                      |has_value H'; fail 1
                      |move H before H'] end; f
               |f]
          end)
  in f.

(*example:*)
Goal True.
do 10 (pose proof 0 as ?n0; pose proof true as ?b0).
minlines.