Re: [mizar] Re: reductions in Mizar

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

Josef:

>I thought Gonthier (the only Coq person who recently turned
>to serious math library building)

Don't tell this to Bas :-)

>is opposed to having such heavy machinery inside the
>PA. For the same "fragility of refactoring" reasons as the
>Mizar people have been taught to over a couple of decades.

Goerges Gonthier doesn't like heavy automation in his
proofs, I think that's true.  But _reduction_ is a different
matter entirely.  Ssreflect is named for "reflection",
which is all about reduction.

Georges claims the only system that can realistically check
the four color theorem proof is Coq _exactly_ because it
has reduction, which can run the program that's part of
that proof inside the logic.

Freek