Re: [mizar] n > 0 vs n <> 0

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

Hi:

Wouldn't it be better to use the attributes empty and positive instead of predicates?

PR

On Sat, Feb 21, 2004 at 08:56:03AM +0100, Artur Kornilowicz wrote:
> Dear All,
> 
> recently I was working with non empty natural numbers and I always had an
> assumption n <> 0. But, many related theorems already stored in the MML
> have an assumption n > 0. To use them one has to do an extra step referring
> to NAT_1:19. Moreover, n <> 0 is simpler than n > 0.
> 
> Then I would propose to make a revision of the MML changing all
> assumptions n > 0 into n <> 0.
> 
> But, I recognized one problem:
> 
> theorem Th10: ::GR_CY_1:10
> for n,s being natural number st n > 0 holds s in Segm (n) iff s < n;
> 
> theorem Th12: ::GR_CY_1:12
> for n being natural number st n > 0 holds 0 in Segm (n) by Th10;
> 
> In present MML, Th12 is a trivial consequence of Th10. But if we change
> n > 0 into n <> 0, then Th12 needs more complex proof. The reason is that
> predicate symbol < disappeared.
> 
> The question is: when Library Committee agrees to do the revision should
> we leave Th10 and Th12 (and other similar cases) as are, or should we
> prove them.
> 
> Greetings
> Artur Kornilowicz
> 
> 
> ## RF mark: EXCEPTION: 'arturk@math.uwb.edu.pl'
> ## RF rules: ExcHF OK

-- 
Piotr Rudnicki              CompSci, University of Alberta, Edmonton, Canada
http://web.cs.ualberta.ca/~piotr