[texhax] Derivation/rule environment + Vertical braces around subderivations

[Johan Glimming]

I would like to ask if someone has an good environment for performing 
equational/relational reasoning/proofs (perhaps with in-line comments 
and subderivations).

I also wonder if someone knows how to add a left square bracket around a
proof like this:
    _
   |   a =
   |   b =    _
   |         |_ subderivation
   |   c
   |_

The purpose of this is to indicate the structure of the reasoning in 
terms of subderivations.

Finally, I think it would be very useful with a nice automatic 
labelling and  inference-rule typesetting environment - is there such 
one? I would like
to abstract from the business of adding layout to the rules, such as 
putting them in multiple columns and make them appear nicely and 
compactly, e.g.


     premise                        premise
     _______  (side)  (LABEL)      _________ (side) (LABEL')
       conc.                         concl.

                       very long premise
                       _________________  (side)  (LABEL'')
                            conc.


       _________________  (very very long side condition)  (LABEL'')
            conc.

Now this might not be the nicest way to typeset the above rules to 
start with,
and when adding a new rule in the midst of this, one currently needs to 
adjust the entire layout, typically with multicols or smart gather* 
environment. Labels can be handled with tag and notag...

This is not satisfactory in my opinion, since the ideal thing would be 
to abstract from the actual presentation and merely enter the rules and 
let LaTeX decide how to best present them visually...

Johan Glimming.