Re: A trouble with a redefinition

[Andrzej Trybulec <trybulec@wwwserve.cs.shinshu-u.ac.jp>]

Piotr Rudnicki wrote:
 
> I have run into a need to add a hidden argument while redefining a > functor.

The fact that it was a hidden argument does not matter. Of course, you
right that it such a situation it must be hidden, but even if you
introduced a new pattern in which it is visible the problem remains.
Sorry Piotr, I just wanted to avoid misunderstanding, the problem is on
the level of semantic correlates, so even if what you write is
completely correct, it is still misleading.

> 
> Andrzej tells me that in the current implementation the additional
> arguments can show up only at the front of the list.  It seems though
> that if this restriction is removed life would become a bit easier.

The rule is even more rigid. If the original definition looks like

  definition let x_1 be theta_1, ... , x_k be theta_k;
    func ....;
    ....
  end;

and one wants to redefine the functor:

  definition let y_1 be theta'_1, ..., y_n be theta'_n;
    func ...;
   ....
  end;

then
 1. n >= k
 2. y_(n-k+i) plays in the definition the same role as x_i (or if you
like they are the same locus):
  to a redefinition to be correct it is necessary:
  - the theta'_(n-k+i) type widens to theta_i
so the types of "old" loci in the redefinition have subrange types
of the types of loci in the original definition. If not an error is
reported
  - the result type of redefined functor widens to the type of the
original functor (the "coherence" condition) wrt. the correspondence
between x_'s and y_'s.
  - similar rules for the "compatibility" condition and so on.

Some users complained that because of this restriction they are pressed
to do a definition rather than the redefinition. It seems in most case
they found the way to go around the problem. I appreciate that Piotr has
sent the message to Mizar Forum, first because it is a good example,
and, even more important, that he sent it. There is a lot that may be
made more powerful in Mizar (as in other systems), the problem is what
should be more powerful. Without the feed back of user we cannot to
develop Mizar properly.

To give you example:
It was a well known shortcoming in the Mizar verifier that such premises
like
 0 <> 1
must be written explicitly. Because 
 0 < 1
was implicit, it looked crazy. The comment "we should do something about
it" (it is not a citation, the comment was in Polish) lasted some 6
years. Eventually we corrected it. The gain in the length of the
articles was about 0.1%, almost nothing. So, the problem is not in the
de Bruijn factor, but the comfort: it was disgusting to write, some
others do it on the beginning of the article,
F1: 0 <> 1;
F2: 0 <> 2;
F3: 1 <> 2;
and so on.

BTW. The only case that I remember that the problem pointed out by Piotr
caused the necessity of a new definition instead of a redefinition was
VALUAT_1:def 5. I wanted to refer to it, so I looked to VALUAT_1. It is:

definition
 let A, v, k, ll;
  func v*ll -> FinSequence of A means
:: VALUAT_1:def 5
 len it = k & for i st 1 <= i & i <= k holds it.i = v.(ll.i);
end;

with the reserved types:

 reserve k for Nat;
 reserve A for non empty set;
 reserve v for Element of Valuations_in A;
 reserve ll for CQC-variable_list of k;

It is easy to see that the problem id with mixing the additional
arguments: "A" and "k" with the original ones: "v" and "ll". But in this
case it is easily corrected:

definition
 let A, k, v, ll;
  func v*ll -> FinSequence of A means
:: VALUAT_1:def 5
 len it = k & for i st 1 <= i & i <= k holds it.i = v.(ll.i);
end;

when I had change it, I still got error 

109: Invalid order of arguments of redefined constructor

One has to be careful here, the proper order is

definition
 let A, k, ll, v;
  func v*ll -> FinSequence of A means
:: VALUAT_1:def 5
 len it = k & for i st 1 <= i & i <= k holds it.i = v.(ll.i);
end;

The original definition of the composition is the composition of binary
relations:

definition
 let P,R;
   func P?R -> Relation means
:: RELAT_1:def 8
 [x,y] _ it iff ex z st [x,z] _ P & [z,y] _ R;
end;

and in FUNCT_1 the order of the arguments is switched 

definition let f,g;
 redefine func f?g;
 synonym g?f;
end;

(When Piotr read a revised version of FUNCT_1, he sent me a message, I
was quite busy in this time so I had postponed reading it to next day,
but after 2.4 sec I got a message from Piotr: "please do not read the
previous message", so then I read it, of course. Piotr was anxious that
the redefinition may can cause the commutative of the composition of
binary relations, he was anxious for it about 2 seconds, or less.)
So when the order of ll and v was corrected, it became quite a
acceptable redefinition:

definition
 let A, k, ll, v;
  redefine
  func v?ll -> FinSequence of A means
...
 synonym v*ll;
end;

If what Piotr wants should be satisfied, the more precise description of
a redefinition is needed. It is now just two Nuremberg: the index ot the
original and the number of superfluous arguments; to get what Piotr
wants we need a mapping mapping from loci in the redefinition to loci in
the original one. I rather support the solution, but Czesiek (Czeslaw)
Bylinski wants them even more flexible. Let him to argue for it.

You faithful,
Andrzej Trybulec