[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