Re: [mizar] Proving inequality of structs ?

[Greg Frascadore <gfrascadore@qwest.net>]

Josef,

Thanks. The part that suprised me was:

>    TopStruct(# x, t #) <> 1-sorted(# x #); 
                                                            *4
I'm interested in whether this is provable or why not? Maybe someone will
know.
(Actually, just as I was typing I thought of something and I was able to
prove it:

    s = TopStruct(# x, t #) & o = 1-sorted(# x #) implies
        s <> o
    proof
        assume A: not thesis;
        then   B: s is strict;
        then s is strict 1-sorted by A;
        then contradiction by A,B;
        hence thesis;
    end;

I like it when that happens )

Ah, 'forgetful'. Thanks againl

-Greg Frascadore





Josef Urban wrote:
> 
> 
> Hi Greg,
> 
> it has been discussed couple of times on this forum that the semantics of 
> the Mizar structures is underspecified. This leads to various problems, 
> and even alternative structures modelled as partial functions in Mizar by 
> Lee and Rudnicki to get rid of the worst 
> (http://www.springerlink.com/index/cx5518q23780417k.pdf). I hope someone 
> can explain to you why is Mizar designed not to know the facts below. I 
> don't think I know. The facts are probably not provable in (current) Mizar 
> at all (provided Mizar is consistent :-).
> 
> The "forgetfulness" is supposed to mean that you are "forgetting" about 
> some fields in a structure. There is actually no "constructor" (in the 
> Mizar sense of the word) for it, and the special syntax
> 
> the 1-sorted of s
> 
> is just a shortcut for
> 
> 1-sorted(# the carrier of s #)
> 
> 
> Josef
> 
> On Wed, 14 Jan 2009, Greg Frascadore wrote:
> 
>>
>>    Hello,  I could use a little help with my understanding of
>>    Mizar structs and strict.
>>
>>    My current understanding is based on "Some Features of the Mizar
>>    Language" by Trybulec. I've also seen the long email thread
>>    for Jesse Alama <http://www.nabble.com/strict-to8243464.html>
>>    concerning strict.
>>
>>    Here is my question:
>>
>>    reserve x for set;
>>    reserve t for Subset-Family of x;
>>    reserve o for 1-sorted;
>>    reserve s for TopStruct;
>>
>>    s = TopStruct(# x, t #) & o = 1-sorted(# x #) implies
>>        the 1-sorted of s = o;                          :: I understand
>>
>>    s is TopStruct & o is strict 1-sorted implies
>>        s <> o;
>>             *4
>>
>>    :: If o is strict, it lacks the 'topology' selector. How to
>>    :: test that? maybe:
>>
>>    s = TopStruct(# x, t #) & o = 1-sorted(# x #) implies
>>        s <> o;
>>             *4                                         :: now what?
>>
>>    TopStruct(# x, t #) <> 1-sorted(# x #);
>>                                         *4             :: confused
>>
>>    Also, what is 'forgetful' about the 'forgetful constructor' ?
>>
>>    Thanks for any insight.
>>
>>    -Greg Frascadore
>>
>>
>> -- 
>> View this message in context:
>> http://www.nabble.com/Proving-inequality-of-structs---tp21459576p21459576.html
>> Sent from the Mizar mailing list archive at Nabble.com.
>>
>>
> 
> 

-- 
View this message in context: http://www.nabble.com/Proving-inequality-of-structs---tp21459576p21490602.html
Sent from the Mizar mailing list archive at Nabble.com.