Feature request: Hide section variables from goal

[cpitclaudel]

Description of the problem

The goals in proofs with lots of section variables (including lots of typeclasses) quickly become unreadable, because the contexts are too large. For example:

1 focused subgoal
(shelved: 1) (ID 339)
  
  width : Z
  BW : Bitwidth width
  word : Interface.word width
  memT : map.map word byte
  localsT : map.map string word
  env : map.map string (list string * list string * cmd)
  ext_spec : Semantics.ExtSpec
  word_ok : word.ok word
  mem_ok : map.ok memT
  locals_ok : map.ok localsT
  env_ok : map.ok env
  ext_spec_ok : Semantics.ext_spec.ok ext_spec
  tr : Semantics.trace
  mem : memT
  locals : localsT
  functions : list (string * (list string * list string * cmd))
  buf : buffer_t
  capacity : nat
  w : word
  v := push buf w : list word
  P : list word -> Type
  pred : P v -> predicate
  k : nlet_eq_k P v
  k_impl : cmd
  R : memT -> Prop
  var : string
  buf_ptr : word
  buf_expr, w_expr, idx_expr : expr
  Hlt : (Datatypes.length buf < capacity)%nat
  pad : list word
  Hmem : (sizedlistarray_value AccessWord capacity buf_ptr (buf ++ pad) ⋆ R) mem
  Hbuf : WeakestPrecondition.dexpr mem locals buf_expr buf_ptr
  Hidx : WeakestPrecondition.dexpr mem locals idx_expr (wlen buf)
  Hw : WeakestPrecondition.dexpr mem locals w_expr w
  Hk : let v := v in
       forall mem' : memT,
       (buffer_value buf_ptr (push buf w) capacity ⋆ R) mem' ->
       <{ Trace := tr;
          Memory := mem';
          Locals := locals;
          Functions := functions }>
       k_impl
       <{ pred (k v eq_refl) }>
  mem' : memT
  H : (sizedlistarray_value AccessWord capacity buf_ptr
         (ListArray.put (buf ++ pad) (Datatypes.length buf) w) ⋆ R) mem'
  ============================
  (buffer_value buf_ptr (push buf w) capacity ⋆ R) mem'

It would be very nice to have an alternative way to display these goals. Maybe something like the following?

1 focused subgoal (shelved: 1) (ID 339)
  Section variables:
    width BW word memT localsT env ext_spec word_ok mem_ok locals_ok env_ok ext_spec_ok
  
  tr : Semantics.trace
  mem : memT
  locals : localsT
  functions : list (string * (list string * list string * cmd))
  buf : buffer_t
  capacity : nat
  w : word
  v := push buf w : list word
  P : list word -> Type
  pred : P v -> predicate
  k : nlet_eq_k P v
  k_impl : cmd
  R : memT -> Prop
  var : string
  buf_ptr : word
  buf_expr, w_expr, idx_expr : expr
  Hlt : (Datatypes.length buf < capacity)%nat
  pad : list word
  Hmem : (sizedlistarray_value AccessWord capacity buf_ptr (buf ++ pad) ⋆ R) mem
  Hbuf : WeakestPrecondition.dexpr mem locals buf_expr buf_ptr
  Hidx : WeakestPrecondition.dexpr mem locals idx_expr (wlen buf)
  Hw : WeakestPrecondition.dexpr mem locals w_expr w
  Hk : let v := v in
       forall mem' : memT,
       (buffer_value buf_ptr (push buf w) capacity ⋆ R) mem' ->
       <{ Trace := tr;
          Memory := mem';
          Locals := locals;
          Functions := functions }>
       k_impl
       <{ pred (k v eq_refl) }>
  mem' : memT
  H : (sizedlistarray_value AccessWord capacity buf_ptr
         (ListArray.put (buf ++ pad) (Datatypes.length buf) w) ⋆ R) mem'
  ============================
  (buffer_value buf_ptr (push buf w) capacity ⋆ R) mem'

(Also, shelved: 1 line doesn't need to be its own line)

I think that would be a nice addition to Set Printing Compact Contexts. In the long run I expect this to be UI-controlled, but this is now and the long run is in a long time.