Proving inequality of structs ?

[Greg Frascadore]

    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

[Josef Urban]

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.
>
>

[Greg Frascadore]

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.
>
>