[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] a question

Dear Adem,

On Tue, 22 Dec 2009, Ozyavas, Adem wrote:


I asked the group a question on how to write recursive predicates in Mizar. The following is the

result of correspondce of emails back and forth. It gives a definition for an inductive factorial predicate.

definition
 let n,x be natural number;
 pred factorial(n,x) means
  for Y being set st
  [0,1] in Y & (for k,y being natural number st [k,y] in Y holds [k+1,y*(k+1)] in Y)
  holds [n,x] in Y;
end;


First of all, there is not a unique set that satisfies the above definition. A set
{[0,0!], [1,1!], [2,2!], ..., [n,n!]} \/ [3,3] would satisfy the set consructed with the above
definition so that it is not possible to disprove

factorial 3,3.


No, it _is_ possible to disprove it, below is the proof :-))

environ
 vocabularies FACTOR,ORDINAL1,CARD_1,ARYTM_3,RELAT_1,REALSET1,ZFMISC_1,NUMBERS;
 notations TARSKI,ORDINAL1,CARD_1,NUMBERS,NAT_1,NEWTON,ZFMISC_1;
 constructors ORDINAL1,CARD_1,NAT_1,NEWTON,ZFMISC_1,REAL_1;
 registrations ORDINAL1;
 requirements BOOLE,SUBSET,NUMERALS,ARITHM;
 schemes XBOOLE_0;
 theorems ZFMISC_1,STIRL2_1,NEWTON;
begin

definition
  let n,x be natural number;
  pred factorial n,x means :def1:
   for Y being set st
[0,1] in Y & (for k,y being natural number st [k,y] in Y holds [k+1,y*(k+1)] in Y) 
   holds [n,x] in Y;
end;

factorial 3,6
proof
  let Y be set;
assume a: [0,1] in Y & (for k,y being natural number st [k,y] in Y holds [k+1,y*(k+1)] in Y); 
  then [0+1,1*(0+1)] in Y;
  then [1+1,1*(1+1)] in Y by a;
  then [2+1,2*(2+1)] in Y by a;
  hence thesis;
end;

not factorial 3,3
proof
  assume a: not thesis;
  defpred P[set] means ex n being natural number st $1 = [n,n!];
  consider X being set such that
x: for x being set holds x in X iff x in [:NAT,NAT:] & P[x] from XBOOLE_0:sch 1; 
  z: [0,1] in [:NAT,NAT:] by ZFMISC_1:def 2;
  b: [0,1] in X by x,z,NEWTON:18;
  now
    let k,y be natural number;
    assume [k,y] in X; then
    consider l being natural number such that
    l: [k,y]=[l,l!] by x;
    y: k=l & y=l! by l,ZFMISC_1:33;
    n: [k+1,y*(k+1)] in [:NAT,NAT:] by ZFMISC_1:def 2;
    [k+1,(k+1)!]=[k+1,y*(k+1)] by y,NEWTON:21;
    hence [k+1,y*(k+1)] in X by n,x;
  end;
  then [3,3] in X by a,b,def1; then
  consider n being natural number such that
  n: [3,3]=[n,n!] by x;
  n=3 & n!=3 by n,ZFMISC_1:33;
  hence contradiction by STIRL2_1:60;
end;



Most of the time, a third item is mentioned in an inductive definition (after (i) base case, (ii)
inductive case) which is "the minimal set that satifies the first and second items (or the
generalized intersection of all sets that satify (i) and (ii))".
It's not needed - the "for Y" in the definition guarantees, that the condition also holds for the 'minimal' set. 

Best,

Adam Naumowicz

=======================================================================
Dept. of Programming and Formal Methods  Fax: +48(85)7457662
Institute of Informatics                 Tel: +48(85)7457559 (office)
University of Bialystok                  E-mail: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland     http://math.uwb.edu.pl/~adamn/
=======================================================================