Inductive predicates

[Ozyavas, Adem]

Dear All,

Is there any way to write inductive predicates in Mizar?

My purpose is to have inductive predicates instead of recursive functions to avoid existence and uniqueness proofs of recursive functions and leaving the fact that this predicate has functional property as a later task. I have searched the library and could not find any examples.

Thanks...

Adem Ozyavas

[Grzegorz Bancerek]

Hi,

there is no regular recursive definition of predicates in Mizar.
Instead you should use something like

definition
let X; let x,y be Element of X;
pred x rec y means
for Y st
   (for a,b st START_CONDITION holds [a,b] in Y) &
   (for a,b st [a,b] in Y holds [F(a),G(b)] in Y)
holds [x,y] in Y;
end;

Grzegorz

On Sun, 16 Aug 2009, Ozyavas, Adem wrote:

> Dear All,
>
> Is there any way to write inductive predicates in Mizar?
>
> My purpose is to have inductive predicates instead of recursive functions to avoid existence and uniqueness proofs of recursive functions and leaving the fact that this predicate has functional property as a later task. I have searched the library and could not find any examples.
>
> Thanks...
>
> Adem Ozyavas

===============================================================
Grzegorz Bancerek
e-mail: bancerek@... (bancerek@...)
http://merak.pb.bialystok.pl/~bancerek/
Dept. of Theoretical CS
Faculty of Computer Science      fax. [phone]
Bialystok Technical University   tel. [phone]
http://www.pb.bialystok.pl

[Ozyavas, Adem]

Dear All,

I asked Dr.Grzegorz Bancerek if there is inductive predicate definitions in Mizar and below is Dr.Grzegorz Bancerek's answer.
I tried to write the recursive definition of factorial using Dr.Grzegorz Bancerek's
template predicate definition.
When I tried to define F and G functions "outside of predicate definition" Mizar
is complaining  that (I think all definitions are global) the definition of pred is global and F and G are local as follows:

deffunc F ...
deffunc G ...

definition
 let X; let x,y be Element of X;
 pred x fac y means :: x! = y
 for Y st
   (for a,b st [a,b] = [0,1] holds [a,b] in Y) &
   (for a,b st [a,b] in Y holds [F(a),G(b)] in Y)
 holds [x,y] in Y;
 end;


How can one define the recursive factorial as predicate in Mizar with F and G functions?

Thank you...

Adem Ozyavas



> Hi,

> there is no regular recursive definition of predicates in Mizar.
> Instead you should use something like

> definition
> let X; let x,y be Element of X;
> pred x rec y means
> for Y st
>   (for a,b st START_CONDITION holds [a,b] in Y) &
>   (for a,b st [a,b] in Y holds [F(a),G(b)] in Y)
> holds [x,y] in Y;
> end;

>Grzegorz

>On Sun, 16 Aug 2009, Ozyavas, Adem wrote:

> Dear All,
>
> Is there any way to write inductive predicates in Mizar?
>
> My purpose is to have inductive predicates instead of recursive functions to avoid existence and uniqueness proofs of recursive functions and leaving the fact that this predicate has functional property as a later task. I have searched the library and could not find any examples.
>
> Thanks...
>
> Adem Ozyavas

[trybulec]

You're right. The private constructors, like introduced by defpred,
cannot be used in the exportable (public) part of the aricle. Just
expand F and G in the
definition of the predicate.

Why you need such a predicate? The factorial is already define in MML:

NEWTON:def 2

Regards,
Andrzej Trybulec

Cytowanie "Ozyavas, Adem" <adem.ozyavas@...>:

> Dear All,
>
> I asked Dr.Grzegorz Bancerek if there is inductive predicate
> definitions in Mizar and below is Dr.Grzegorz Bancerek's answer.
> I tried to write the recursive definition of factorial using
> Dr.Grzegorz Bancerek's
> template predicate definition.
> When I tried to define F and G functions "outside of predicate
> definition" Mizar
> is complaining  that (I think all definitions are global) the
> definition of pred is global and F and G are local as follows:
>
> deffunc F ...
> deffunc G ...
>
> definition
> let X; let x,y be Element of X;
> pred x fac y means :: x! = y
> for Y st
>   (for a,b st [a,b] = [0,1] holds [a,b] in Y) &
>   (for a,b st [a,b] in Y holds [F(a),G(b)] in Y)
> holds [x,y] in Y;
> end;
>
>
> How can one define the recursive factorial as predicate in Mizar with
> F and G functions?
>
> Thank you...
>
> Adem Ozyavas
>

[Ozyavas, Adem]

Dear Professor Andrzej Trybulec and All,

I wrote an evaluator for a functional language called SequenceL in Mizar. I have some recursive functions in my evaluator whose domains are very complicated so that their well-definedness proofs are too hard. I am thinking that writing them as recursive predicates and doing some proofs about those predicates would be much easier. That is why I wanted to start writing a recursive factorial as a recursive predicate as an exercise. I also wanted to see a definition from experts. I am hoping that I am on the right track.

Thanks and Regards,
Adem Ozyavas
________________________________________
From: owner-mizar-forum@... [owner-mizar-forum@...] On Behalf Of trybulec@... [trybulec@...]
Sent: Wednesday, September 02, 2009 3:58 AM
To: mizar-forum@...
Subject: RE: [mizar] Inductive predicates

You're right. The private constructors, like introduced by defpred,
cannot be used in the exportable (public) part of the aricle. Just
expand F and G in the
definition of the predicate.

Why you need such a predicate? The factorial is already define in MML:

NEWTON:def 2

Regards,
Andrzej Trybulec

Cytowanie "Ozyavas, Adem" <adem.ozyavas@...>:

> Dear All,
>
> I asked Dr.Grzegorz Bancerek if there is inductive predicate
> definitions in Mizar and below is Dr.Grzegorz Bancerek's answer.
> I tried to write the recursive definition of factorial using
> Dr.Grzegorz Bancerek's
> template predicate definition.
> When I tried to define F and G functions "outside of predicate
> definition" Mizar
> is complaining  that (I think all definitions are global) the
> definition of pred is global and F and G are local as follows:
>
> deffunc F ...
> deffunc G ...
>
> definition
> let X; let x,y be Element of X;
> pred x fac y means :: x! = y
> for Y st
>   (for a,b st [a,b] = [0,1] holds [a,b] in Y) &
>   (for a,b st [a,b] in Y holds [F(a),G(b)] in Y)
> holds [x,y] in Y;
> end;
>
>
> How can one define the recursive factorial as predicate in Mizar with
> F and G functions?
>
> Thank you...
>
> Adem Ozyavas
>

[Adam Naumowicz]

Dear Adem,

On Wed, 2 Sep 2009, Ozyavas, Adem wrote:

> I wrote an evaluator for a functional language called SequenceL in
> Mizar. I have some recursive functions in my evaluator whose domains are
> very complicated so that their well-definedness proofs are too hard. I
> am thinking that writing them as recursive predicates and doing some
> proofs about those predicates would be much easier.

I'm not sure if this "workaround" is a good strategy here. It might
happen that when you want to have your article submitted to MML, the
reviewers might complain why some definitions are in the form of
predicates while they should rather be functors...

I believe you should still try to complete the correctness proofs using
this forum, or the Mizar User Service for help to sort out the
particular difficulties in the underlying proofs. But I don't really
know how hard the proofs are, of course :-)

Best,

Adam

=======================================================================
Dept. of Programming and Formal Methods  Fax: [phone]
Institute of Informatics                 Tel: [phone] (office)
University of Bialystok                  E-mail: adamn@...
Sosnowa 64, 15-887 Bialystok, Poland     http://math.uwb.edu.pl/~adamn/
=======================================================================