Re: [mizar] Mizar 7?

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Freek Wiedijk wrote:

> >2. Blocks that in a 'per cases' reasoning end with an 'end'.
>
> So now it's possible to "nest" per cases without a "proof end"?
>

There are problems with errors recovery (I suspect that the popularity of
'interactive' systems is caused by the fact that
interactivity, which is easy to implement, enables to justify the lack of
errors recovery, which is difficult).

We used the rule that if parser encounters 'suppose' or 'case' before 'per
cases' then it generates a 'per cases' item. So,

    proof
      suppose ...;
      ....
    end;

is transformed to

   proof
     per cases;
     suppose ...;
     ...
  end;

The error is reported, of course, and parser generates an incorrect sentence
for 'per cases', to avoid verifying it.
In his, a bit simplistic, implementation Grzegorz called the corresponding
procedure recursively. So, the errors reported looks awful:

1=1
proof
::> *214,215,231
 suppose 1=2;
end;
::>,396,60

1=1
proof
::> *214,215,231
 suppose 1=2;
  hence thesis;
::>   *396,214 *215,231
 suppose 1=3;
end;
::>,396,60
::>
::> 60: Something remains to be proved in this case
::> 214: No pairing "end" for this word
::> 215: "end" missing
::> 231: "per cases" missing
::> 396: Formula expected

and the error #231 is reported twice (in the second proof). Czeslaw changed
it already, if 'end' pairing 'suppose' is missing then in this place only
error #215 is reported (and, while we are in 'suppose' or 'case' block the
'per cases' item is not generated).

Another problem is what to do with

   proof
     per cases;
     suppose ...;
      ...
     end;
      -----
     end;

if the "----" does not start with 'suppose'. The parser now closes the proof.
(generates 'end' - the #215 error,
so the last 'end' is unexpected.

1=1
proof
::> *214
 per cases;
 suppose 1=1;
  hence thesis;
 end;
::>  *215
 1=1;
end;
::>,216
::>
::> 214: No pairing "end" for this word
::> 215: "end" missing
::> 216: Unexpected "end"

I guess a better solution is to generate 'suppose' 'end': to convert it to:

   proof
     per cases;
     suppose ...;
      ...
     end;
     suppose ? ;
      -----
     end;
   end;

'?' stands for an incorrect sentence.

Regards,
Andrzej