Re: Iterated Unequalities (fwd)

[John Harrison <John.Harrison@cl.cam.ac.uk>]

Andrzej Trybulec writes:

| 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.

Yes, I'd just seen the ".=" in Mizar and thought that this was a natural
generalization. It surprised me to find that even the concrete syntax I
picked was already planned for in Mizar!

| 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").

This is about what I do; the HOL-Mizar implementation maintains a set of
transitivity theorems which the user can augment for any potentially
interesting operators like c= or <=. These can involve several operators,
e.g.

  a <= b & b <= c implies a <= c
 
  a <= b & b < c implies a < c

  a < b & b <= c implies a < c

  a < b & b < c implies a < c

The system automatically creates appropriate theorems to allow one to mix
in equality, e.g.

  a = b & b < c implies a < c

Thus one can write quite long heterogeneous chains like:

 e1  <= e2      by reason1
 ... <= e3      by reason2
 ... =  e4      by reason3
 ... <  e5      by reason4
 ... =  e6      by reason5

and this results in the eventual theorem e1 < e6. However, one of Mizar's
greatest strengths is its declarative proof style, and the above doesn't
quite fit, in that the eventual relation "<" appears by magic rather than 
being declared in the proof. 

The problems of proving the intermediate results efficiently is another 
matter, of course. 

John.