Re: [mizar] Was it meant to be that way?

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Piotr Rudnicki wrote:

> Hi:
>
> While playing with Patrick's incons, I have run into the following:
>
>         :: Verifier, Mizar Ver. 6.4.02 (Linux/FPC)
>
>      definition let X,p;
>        pred X |= p means :Def5:
>        J,v |= X implies J,v |= p;
>      end;
>
>      X |= p iff (for A, J, v holds J,v |= X implies J,v |= p) by Def5;
>      ::>                                                       *4
>
>      ::> 4: This inference is not accepted
>
> Was it meant to be this way?

Yes. The free variables in the definiens are bound by default. The order of
binding depends on the order of the
reservation. So the definitional theorem is

     for X,p holds X |= p iff for A,v,J holds J,v |= X implies J,v |= p

and in

      for X,p holds X |= p iff for A,v,J holds J,v |= X implies J,v |= p
      for A, J, v holds J,v |= X implies J,v |= p
  ---------------------------------------------
                         X |= p

pattern matching fails. It is one of many things that I would like to change in
Mizar, but with a very very low
priority: you do not know how the default mechanism works, do not use it.

All the best,
Andrzej