[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] then per cases;

The only reason that linking 'per cases" is not implemented,
is sloth. Because the "per cases' sentence is generated at the and of the "per cases" reasoning, the linking is a bit different that in the typical cases. I have to look to sources. 
So, you absolutely right, it should be allowed.

Andrzej


Jesse Alama wrote:


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