[mizar] How to properly do inductive sets in Mizar?

[Freek Wiedijk <freek@cs.kun.nl>]

Hi,

A question.  I was playing with HOL, wanted to port one of
its proofs to Mizar, and this proof happened to need an
inductively defined relation.  Both in HOL and Coq knowledge
of inductive relations is built into the system, but I'm
wondering how to do this most easily in Mizar.

So here is the statement that I wanted to prove in Mizar
syntax (I put the types in reserve statements):

  reserve A,B for non empty set;
  reserve ll for Relation of A,A;
  reserve H for Function of Funcs(A,B),Funcs(A,B);
  reserve R for Relation of A,B;
  reserve f for Function of A,B;
  reserve x,z for Element of A;
  reserve y for Element of B;

  ex R st for x,y holds
   [x,y] in R iff
    ex f st y = (H.f).x & for z st [z,x] in ll holds [z,f.z] in R

And here is the HOL original:

  `?R. !x y. R x y = (?f:A->B. (y = H f x) /\ (!z. z << x ==> R z (f z)))`

To prove this is conceptually easy.  You take the least
fixpoint of the operator that from a set builds a new
according to the formula to the right of the "iff".  Since
this operation is "positive" (if the R gets bigger, the
result gets bigger) you can use the "Knaster" scheme to prove
this.

But the proof is much too long to my taste!  So my question
is:  what is the proper way to do an inductive construction
like this in Mizar.  Are there special schemes that help you
with this?

For completeness sake, here is how to prove existence of this
inductive relation in HOL:

  #prove_inductive_relations_exist `!f (x:A). (!z:A. z << x ==> R z (f z :B)) ==> R x (H f x)`;;
  it : thm =
   |- ?R. (!f x. (!z. z << x ==> R z (f z)) ==> R x (H f x)) /\
	  (!R'. (!f x. (!z. z << x ==> R' z (f z)) ==> R' x (H f x))
		==> (!a0 a1. R a0 a1 ==> R' a0 a1)) /\
	  (!a0 a1.
	       R a0 a1 = (?f. (a1 = H f a0) /\ (!z. z << a0 ==> R z (f z))))

(the "it : thm = ..." is output of the system; only the first
line is input)

And this is what it looks like in Coq:

  Parameters A,B : Set.
  Parameters ll : A->A->Prop.
  Parameters H : (A->B)->(A->B).

  Inductive R : A->B->Prop :=
   RR : (x:A; f:A->B)((z:A)(ll z x)->(R z (f z)))->(R x (H f x)).

  Lemma R_lemma : (x:A; y:B)
   (R x y)<->(EX f:A->B | y = (H f x) /\ (z:A)(ll z x)->(R z (f z))).
  Proof.
  Intuition. Elim H0. Intros. Exists f. Auto. Rewrite H0. Apply RR. Auto.
  Qed.

Freek