[mizar] Re: strict

[Jesse Alama <alama@stanford.edu>]

Adam Naumowicz <adamn@math.uwb.edu.pl> writes:

> On Tue, 9 Jan 2007, Jesse Alama wrote:
>
>> definition
>>  func F2 -> doubleLoopStr equals
>>  coherence;
>> end;
>
>> there doesn't seem to be a definition of what it means to be a strict
>> doubleLoopStr; moreover, when I browse
>>
>> http://mmlquery.mizar.org/mmlquery/fillin.php?filledfilename=phparticle.mqt&argument=article+vectsp_1
>>
>> I see that there appears to be something like a definition:
>>
>> definition
>>  let a1 be doubleLoopStr;
>>  attr a1 is strict;
>> end;
>>
>> but when I browse VECTSP_1.MIZ, I don't see any definition of strict
>> for doubleLoopStr's.  What's going on?  What does "strict" mean?  How
>> can I prove that a doubleLoopStr is strict?
>
> "strict" doesn't have its own definition as it is a special (in a way
> "meta" attribute) - it means that a term which has a structure type
> <Theta> has exactly the same selectors (fields) as introduced in the
> definition of the type <Theta>, so in your case only the selectors of
> a doubleLoopStr - any extension to that would break the
> "strictness". So you may think of a vector space as of a group, but
> it's not a "strict" group.

Ah, I see now, thanks.

> You don't have to worry about proving "strictness" with your
> definition - 
> if you define your functor using an "aggregate" structure term
> explicitely enumerating all selectors, like
>
> doubleLoopStr(# {0,1}, add2, prod2, unit2, zero2 #),
>
> then the "strict" attribute is added automatically. This is why the
> definition of "strict" has a special meaning which is automatically
> defined separately for all structures - and it is added to the XML
> presentation even if it's not present in the actual miz/abs file.

I'm afraid that's not what I see: I have the definition

definition
  func F2 -> doubleLoopStr equals
  doubleLoopStr(# {0,1}, add2, prod2, unit2,  zero2 #);
  coherence;
end;

and then the theorem

theorem F2 is strict;

but "This inference is not accepted".  There's nothing wrong with the
definition in the sense that it is accepted without errors.  What
might be going on here?

Jesse

-- 
Jesse Alama (alama@stanford.edu)
*10: Too many basic sentences in an inference