Re: Iterated Unequalities (fwd)

[Andrzej Trybulec <trybulec@math.uw.bialystok.pl>]

> Date: Thu, 04 Jun 1998 11:41:21 +0200
> From: Christoph Schwarzweller <schwarzw@informatik.uni-tuebingen.de>
> To: Mizar-Forum <mizar-forum@mizar.uw.bialystok.pl>
> Subject: Iterated Unequalities
> 
> Hi,
> 
> in Mizar it is possible to build iterated equations (a = b .= c ...).
> I think it would be nice to have also something like a < b .< c ...
> Did anyone have thought about this so far?
> 
> Christoph Schwarzweller

The syntax proposed is rather
      a < b
      ... < c
and "three dots" are already on mizar.doc, i.e. "..." is a reserved word
for long time (however we want to use it not only for this purpose).

Then, ".=" might be treated as a shorthand for "... =".

BTW John Harrison alredy introduced such syntax in Mizar mode in HOL,
as far as I know he did not know that we talk about doing the similar
thing.

The problem is that iterative equality is much more than
just using the transitivity of the equality.

When Mizar tries to prove an equality of the form
     tau_1 = tau_2
or rather to disprove an unequality

     tau_1 <> tau_2
then it tries to find the differences between components of both
terms, and if it finds only one such difference e.g. tau_1 differs
from tau_2 only in this that a subterm tau_3 in tau_1 is replaced by
tau_4 in tau_2, the Mizar (actually the EQUALIZER module of the verifier)
generates new unequlity
     tau_3 <> tau_4
We call it in our jargon the "One Difference Rule".

With the iterative equlity it is close to "window refernces".

So, it is heavy use of the extensionaity, too.

It is easy to introduce new property of predicates: "transitivity"
(again it is already reserved), and then allow for an iterated
construction for the predicates with this property (like "<" or "c=")
but it is more difficult to find out an analogue for the "One Difference 
Rule". Perhaps we should have a property "monotonicity" ? But then
we hove no experience with "properties" related to two different
constructors (like "distributivity").

Andrzej Trybulec