[mizar] How to prove equivalences?

[Freek Wiedijk <freek@cs.ru.nl>]

Dear Mizar community,

I wonder how people here prove their equivalences.  If you
do it really verbosely you get something like

  P[] iff Q[]
  proof
    thus P[] implies Q[]
    proof
      assume
  A1:   P[];
      ...
      thus Q[];
    end;
    thus Q[] implies P[]
    proof
      assume
  A2:   Q[];
      ...
      thus P[];
    end;
  end;

However that contains a lot of duplication of the formulas
P[] and Q[], which often are quite long.  So I always write
the most compact version that I can think of instead (it
saves 4 lines and 5 formula instances):

  P[] iff Q[]
  proof
    hereby
      assume
  A1:   P[];
      ...
      thus Q[];
    end;
    assume
  A2: Q[];
    ...
    thus thesis;
  end;

However that does not satisfy me completely either.  I don't
like it that I have to write the formula Q[] at the end of
the hereby explicitly (I really would like to be able to say
"thesis" there).  And the fact that the symmetry between
the two "directions" of the proof is lost in the proof
text is not so nice either.  So I sometimes (regularly :-))
wish that Mizar would have something like the "per cases"
construction for equivalences.  It would look something like
the following (1 line longer again, but 1 formula to copy
less; _and_ nicely symmetrical between the two directions):

  P[] iff Q[]
  proof
    per directions;
    suppose
  A1:   P[];
      ...
      thus thesis;
    end;
    suppose
  A2:   Q[];
      ...
      thus thesis;
    end;
  end;

(For the keyword "directions" there probably are better
choices :-))  One might argue that it is reasonable to
have something like this.  In Mizar most connectives have
"their own" proof steps.  The "implies" and "not" connectives
have assume, "for" has let, "&" has thus, "ex" has take and
consider, and "or" has per cases.  So all I'm asking for
is a proof step dedicated to "iff".  If you give a logical
connective a name of its own, then it seems natural to have
it have a proof step of its own as well.

However, knowing the Mizar community I know that the chances
of having this be added to the language are so close to zero
as to be negligible.  Mizar people are a conservative bunch,
and rightly so :-)

So my question instead is: how do _you_ customarily write
your proofs for equivalences?  And did _you_ never feel
uneasy about this?

Freek