Re: [mizar] where do people check for the MML library?

[Freek Wiedijk <freek@cs.ru.nl>]

Hi Brando,

>I was hoping to learn the syntax by proving trial stuff, like in Coq, its helpful to even define natural numbers myself and define and prove properties about them, like n+m = m + n and other simple facts using even induction. 

_That_ will be very difficult in Mizar.  The Mizar library is
based on set theory in ZFC style, so defining the natural
numbers is a major undertaking.  They are the finite
ordinals, I think, so you wold need to define ordinals
and finiteness.

Also Mizar is based on first order logic, so induction is a
"scheme" which is somewhat involved in the first place.

>is that possible in Mizar? Or is that a bad way to go about it?

Possible certainly, but not a good way to start playing
with the system.

What you might do is to look at "articles" that are in the
MML already, try to find a _trivial_ lemma that seems to
be missing in one of the topics, and then try to prove that.

But don't expect (like in Coq) to have a file without any
references to a lot of stuff from the library.  Starting from
scratch will not work well, at least not if you want to
prove something that is moderately interesting.

Only if you want to prove very simple things about sets,
like that when the intersection of two sets is non-empty
that then the sets are non-empty too, or something like that,
you might be able to prove that all the way from scratch.

Although _that_ in its turn might be not so very easy to
explain to a Coq beginner how to prove this.

  forall (A : Set) (B : Set), exists (x : intersection A B), ...

"Um, how do you define intersection of sets in Coq?"

Freek