Re: [mizar] Was this supposed to be so?

[Grzegorz Bancerek <bancerek@cs.shinshu-u.ac.jp>]

Piotr Rudnicki wrote:
> 
> Hi:
> 
> I appreciate Grzegorz's, as always deep and careful, explanation but
> I expected an error that the skeleton of the proof disagrees with the
> thesis.
> 
> On Tue, Aug 20, 2002 at 02:07:53PM -0600, Piotr Rudnicki wrote:
> >
> > I have expected an error in the following
> >
> >       for X, Y, Z being set st X = Y holds Y = X
> >       proof let X, Y be set;
> >         thus thesis;
> >       end;
> >
> > but did not get any.  Such theorem would look pretty silly in an abstract.

My first thought was missing "let Z" in proof skeleton. I observe
sometimes
that my students write generalization steps ("let") for each variable
but, of course, it is not necessary.  In your case thesis is
  for Z being set st X = Y holds Y = X

You may do the proof also like this 

for X, Y, Z being set st X = Y holds Y = X
    proof let Z be set;
        thus thesis;
    end;

where thesis is
   for a,b being set st Z = a holds a = Z


In the following proof it is better not to write "let j .."

  for i,j being Nat holds i+j = j+i
   proof  let i be Nat;
    A1:  i+0 = 0+i;
    A2:  now
          let j be Nat;
          assume i+j = j+i;
           .....
          thus i+(j+1) = (j+1)+i;
         end;
    thus thesis from Ind(A1,A2);
   end;

Best regards,
Grzegorz