Re: [mizar] Concatenation of finite sequences

[marco caminati <spam.caminati@gmail.com>]

1)
      I prefer definitions respecting the following two conditions
      (in order of priority):

      - using already-defined, basic objects of wide adoption (which
      therefore have many already-established results about them in
      MML) and

      - based on `equals' instead of `means'

      I find that these definition tend to be `viral' in the sense
      that working with them cascades results about those general wide
      adopted basic object, and thus generally more useful, rather than
      specialized results about possible ad-hoc objects (see the last
      point in this e-mail).

      $^ is means-based but built with broadly-used objects, while ^'
      is equals-based while built on the less-general "-cut" functor.
      So my couple of principles conflict, but resorting to their priority
      ordering, I would vote to keep $^.

2)
      Of course, I would rather prefer one of the two `posthumous'
      definitions given in the preceding message of this thread; the
      first one of those:

      p|(len p -' 1)^q

      could be simplified (after some additional easy registrations) to

      p|len p ^ q

      if one deprecated the overriding definition

      func p|m -> FinSequence equals p|Seg m;

      given in FINSEQ_1, which I've never liked.

3)
      As to adaptability to transfinite sequences, I admit I am not so
      knowledgeable about ordinals, maybe one could save 1 by overriding |
      functor so that p| (len p -' 1) = p when len p is not finite?

4)
      To give an example of my personal guidelines exposed at the
      beginning, and to have some fun in my spare time, I tried a third
      posthumous definition which "automatically" falls back to ^ in case
      the ends of the two FinSequence arguments don't match. The idea is
      to reduce the cases management to the well-established "+*" functor:

      func p my^ q equals
      p| Seg (len p -' 1)  ^ (( q.1 .--> 2 +* (p.len p.-->1)))~ ^ q/^1;

      Well, actually, for technical reasons, it is convenient to restate
      it as:

      func p my^ q equals
      p| Seg (len p -' 1)  ^ ((q.1 .--> 2 +* ((1 .--> (p.len p))~))~)
      ^ q/^1;

      I have written a correct mizar file culminating with the above
      definition, after proving ten or so auxiliary registrations about
      the various functors involved (otherwise typing errors arise).
      It is available on my home page.

Regards,
Marco Caminati
dottorando XXII ciclo
Dipartimento di Matematica "Guido Castelnuovo"
Sapienza - Università di Roma
http://www.mat.uniroma1.it/~caminati/