Re: Re: reductions in Mizar

On 1/26/12, Freek Wiedijk <[email protected]> wrote:
> 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.

I'd say using whatever rewrite rules to build programs that are
invoked in a controlled way is good.

Adding arbitrary rewrite rules that are somehow automatically combined
together and always automatically used leads to fragility of
refactoring that I would avoid in a large library (particularly a
collaboratively developed one).

Josef





>
> Freek
>