[mizar] then per cases;

[Jesse Alama <alama@stanford.edu>]

I recently discovered what seems to me to be an asymmetry of "per
cases".  Consider, for example, in the context of some proof:

A1: <statement1> or <statement 2>;
then per cases;
  suppose <statement1>;
    <proof1>;
  end;
  suppose <statement2>;
    <proof2>;
  end;
end;

It seemed natural to me to write "then per cases" in the proof that I
was working on; I was surprised that this kind of statement is
rejected.  I get errors 178 ("Link assumes a straightforward
justification"), 391 ("Incorrect beginning of a text item") and 4
("This inference is not accepted") when writing something like this.
However, the proof

A1: <statement1> or <statement 2>;
per cases by A1;
  suppose <statement1>;
    <proof1>;
  end;
  suppose <statement2>;
    <proof2>;
  end;
end;

is just fine.  It seems to me that there is an asymmetry between "per
cases" and other statements which require justification.  For the
latter we can either label the previous statement and include that
label in a list of labels following "by" or indicate that the previous
statement is to be counted as a justification by using "then".  But
for per cases this isn't true.  Is there any significant reason behind
this asymmetry?

Jesse

-- 
Jesse Alama (alama@stanford.edu)
*10: Too many basic sentences in an inference