[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] Re: strict
Adam Naumowicz <adamn@math.uwb.edu.pl> writes:
> On Tue, 9 Jan 2007, Jesse Alama wrote:
>
>>> 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?
>
> Make sure that it's not just the error explanation appended at the end
> of the file that makes you think that the theorem is not accepted -
> add a new-line after the theorem - I've just prepared a test file and
> already started to worry as it seemed not accepted at first glance
> ;-))))
>
> Here's my file - the statement _IS_ accepted:
>
> ----------------------------------------------------
> environ
>
> vocabularies TESTER,BINOP_1,VECTSP_1;
> notations TARSKI,SUBSET_1,BINOP_1,VECTSP_1;
> constructors BINOP_1,VECTSP_1;
>
> begin
>
> definition
> func add2 -> BinOp of {0,1} means contradiction;
> correctness;
> ::> *4
> func prod2 -> BinOp of {0,1} means contradiction;
> correctness;
> ::> *4
> func unit2 -> Element of {0,1} means contradiction;
> correctness;
> ::> *4
> func zero2 -> Element of {0,1} means contradiction;
> correctness;
> ::> *4
> end;
>
> definition
> func F2 -> doubleLoopStr equals
> doubleLoopStr(#{0,1},add2,prod2,unit2,zero2#);
> coherence;
> end;
>
> theorem
> F2 is strict;
>
> ::> 4: This inference is not accepted
> --------------------------------------------
The error definitely lies with the theorem, not with the summaries of
the error messages at the bottom of the file:
theorem
F2 is strict;
::> *4
Here's my environment; it's nasty:
vocabularies FINSET_1, POLYFORM, FUNCT_1, FUNCT_2, ZFMISC_1, CARD_1, SUBSET_1, TARSKI, BOOLE, MCART_1, RELAT_1, NAT_1, XCMPLX_0, ORDINAL2, VECTSP_1, VECTSP_9, INT_1, BINOP_1, MCART_2, RLVECT_1, GROUP_1;
notations FINSET_1, XBOOLE_0, NAT_1, FUNCT_1, FUNCT_2, ZFMISC_1, CARD_1, SUBSET_1, TARSKI, MCART_1, RELAT_1, NUMBERS, XCMPLX_0, ORDINAL2, VECTSP_1, VECTSP_9, INT_1, STRUCT_0, BINOP_1, LATTICES, MCART_2, RLVECT_1, GROUP_1;
constructors FINSET_1, XBOOLE_0, NAT_1, FUNCT_1, FUNCT_2, CARD_1, ZFMISC_1, SUBSET_1, TARSKI, MCART_1, RELAT_1, NUMBERS, ORDINAL2, VECTSP_1, VECTSP_9, INT_1, STRUCT_0, BINOP_1, LATTICES, MCART_2, FRAENKEL, ENUMSET1, RLVECT_1, GROUP_1;
registrations FRAENKEL, FINSET_1, XBOOLE_0, FUNCT_1, FUNCT_2, RELAT_1, SUBSET_1, NAT_1, INT_1, VECTSP_1, STRUCT_0;
requirements NUMERALS, BOOLE, ARITHM, SUBSET;
definitions XBOOLE_0, RELAT_1, FUNCT_1, SUBSET_1, FUNCT_2, MCART_2, ENUMSET1, RLVECT_1, BINOP_1, STRUCT_0, GROUP_1;
theorems XBOOLE_0, FUNCT_1, RELAT_1, XBOOLE_1, TARSKI, ZFMISC_1, MCART_1, SUBSET_1, FUNCT_2, MCART_2, ENUMSET1, BINOP_1, STRUCT_0, GROUP_1;
schemes FUNCT_1, BINOP_1;
My definitions:
definition
func add2 -> BinOp of {0,1} means
it.(a,b) = a+b;
existence
:: Proof taken from MOD_2
proof
deffunc O(Element of {0,1},Element of {0,1})=$1+$2;
ex o being BinOp of {0,1} st
for a,b being Element of {0,1} holds o.(a,b) = O(a,b)
from BINOP_1:sch 4;
hence thesis;
end;
uniqueness
:: Proof taken from MOD_2
proof
let o1,o2 be BinOp of ({0,1}) such that
A1: for a,b holds o1.(a,b) = a+b and
A2: for a,b holds o2.(a,b) = a+b;
now
let a,b;
thus o1.(a,b) = a+b by A1
.= o2.(a,b) by A2; end;
hence thesis by BINOP_1:2;
end;
end;
definition
func prod2 -> BinOp of {0,1} means
it.(a,b) = a*b;
existence
:: Proof taken from MOD_2
proof
deffunc O(Element of {0,1},Element of {0,1})=$1*$2;
ex o being BinOp of {0,1} st
for a,b being Element of {0,1} holds o.(a,b) = O(a,b)
from BINOP_1:sch 4;
hence thesis;
end;
uniqueness
:: Proof taken from MOD_2
proof
let o1,o2 be BinOp of ({0,1}) such that
A3: for a,b holds o1.(a,b) = a*b and
A4: for a,b holds o2.(a,b) = a*b;
now
let a,b;
thus o1.(a,b) = a*b by A3
.= o2.(a,b) by A4; end;
hence thesis by BINOP_1:2;
end;
end;
definition
func zero2 -> Element of {0,1} equals 0;
coherence by TARSKI:def 2;
end;
definition
func unit2 -> Element of {0,1} equals 1;
coherence by TARSKI:def 2;
end;
I could give the definitions of + and * that are used above, but that
seems to me unnecessary.
Could it be that something in my environment is messed up?
Thanks,
Jesse
--
Jesse Alama (alama@stanford.edu)
*10: Too many basic sentences in an inference