Matching non-prop hypotheses of same type together?

[YaZko]

Hello,

Your onAllHyps move_up_types. tactic is a life saver when dealing with big messy proofs. However, I really wish it would also organize together variables of identical types together, notably so that proof general would display their type only once.

Do you know if that would be easy to implement? (unless it's already available and I simply missed it?)

Thanks,
Yannick

[Matafou]

Sorry @YaZko I missed your message a very long time ago.
I implemented this some time ago directly in Coq: use Set Printing Compact Contexts.. It groups consecutive variables with same type.
Here is my in my .emacs so that it is performed each time I start coq:

(setq coq-user-init-cmd
      `("Set Printing Compact Contexts." "Set Printing Unfocused."))

This is not perfect though: variables need to be already consecutive.

[Matafou]

Ho sorry you are asking for a smarter move_up_types that would actually group things with same type instead of just moving things up.
It is probably possible in Ltac. I will think abot it. Thanks for the suggestion.

[Matafou]

Thanks for the suggestion!
Here is a new version of move_up_types which will group variables with identical type.

This is still experimental. It needs to be called with map_all_hyps_rev (or after ;!; if you use LibHyps) to maintain variables in the same order. I will still think about it before adding it to LibHyps.

example: intros ;!; move_up_types.

Ltac find_same_type H t :=
  match reverse goal with
  | H': t |- _ => H'
  end.


(* A tactic which moves up a hypothesis if it sort is Type or Set.
   These hypothesis are generally less interesting, having them far
   from the goal is harmless. Moreover with Set Printing Compact
   Context. Coq can group them in horizontal boxes. *)
Ltac move_up_types H :=
  match type of H with
  | ?T =>
    match type of T with
    | Set =>
      let hsametype := find_same_type H T in
      (* this will fail if H' is H, i.e. the first hyp of type T *)
      move H after hsametype
    | Type =>
      let hsametype := LibHyps.find_same_type H T in
      (* idem: fail if H' is H, i.e. the first hyp of type T *)
      move H after hsametype
    | Set => move H at top
    | Type => move H at top
    | _ => idtac
    end
  end.

[Matafou]

@YaZko I have just pushed into master a new version of the library, with a better solution to your feature wish.

tac /g will execute tac an then group up new non-Prop hypothesis, and gather them by identical type.

/g will do that on every hypothesis of the goal, which can also be called by group_up_list all_hyps or the former (although slower) onAllHyps move_up_types.

[YaZko]

Oh sorry I did not react to this earlier, but this looks great, thanks a lot!

I need to jump back into the biggish proof that triggered this feature wish this month, I will test this new feature more thoroughly then :)