The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

With the new (trunk) feature that shows consecutive hypotheses with the 
same type on a single goal line, is there a way to write a tactic that 
minimizes the number of lines in a goal without any other impact on the 
goal?  My first few attempts either didn't do the job completely in all 
cases, or loop.

Not that there's any big need for this, other than as a way to entertain 
one's obsessive-compulsive tendencies ;)

For instance:

Ltac minlines :=
  match reverse goal with H:?T |- _ => repeat match goal with H':T |- _ =>
   match H' with H => fail 2 | _ => move H' after H end end end.

Goal forall (i : nat)(a : bool)(j : nat)(b : bool)(k : nat)(c : bool), 
False.
intros. (*6 lines of hyps*)
minlines. (*now just 2 lines of hyps*)
Abort.

(*But minlines as defined above doesn't work in all cases:*)

Goal forall (i : nat)(a : bool)(j : nat)(l : list nat)(b : bool)(k : 
nat)(c : bool), False.
intros. (*7 lines of hyps*)
minlines. (*4 lines, when just 3 are possible*)
Abort.

-- Jonathan