Re: [mizar] The 'suppose' keyword

[Artur Kornilowicz <arturk@math.uwb.edu.pl>]

On Sat, 24 Apr 2010, Boris Schminke wrote:

> Dear Piotr,
> I've found in the article EUCLID_3 examples of using both 'case' and
> 'suppose' keywords in 'per cases'. When I tried to change 'suppose' to
> 'case' and vice versa the proofs was still passing verification.
> Therefore, I guess that it's more likely that they are synonymic than
> anything else. Although, it's not clear is the existence of these two
> keywords a kind of syntactic sugar or there is something more to it.
> Thanks for your answer anyway.
> Best regards,
> Schminke Boris.


Dear Boris,

"case" and "suppose" are definitely not synonyms, even if there exist 
proofs when it does not matter which one is used.
"case"s can be used when a disjunction of conjuncts is to be proved,
while using "suppose" is simply splitting to cases.
"suppose"s do not influence on thesis.

Look at these two proofs (the only difference is using "case" and 
"suppose"). Theorems are meaningless - they only serve as an example.


for a, b being set holds
a = 1 & b = 1 or a = 2 & b = 2
proof
  let a, b be set;
  per cases;
::>       *4
  case a = 1;
    thus b = 1;
::>           *4
  end;
  case a = 2;
    thus b = 2;
::>           *4
  end;
end;



for a, b being set holds
a = 1 & b = 1 or a = 2 & b = 2
proof
  let a, b be set;
  per cases;
::>       *4
  suppose a = 1;
    thus b = 1; :: thesis is still a = 1 & b = 1 or a = 2 & b = 2;
::>       *51 *4
  end;
  suppose a = 2;
    thus b = 2; :: thesis is still a = 1 & b = 1 or a = 2 & b = 2;
::>       *51 *4
  end;
end;



Best
Artur