Re: [mizar] Concatenation of finite sequences

[Josef Urban <josef.urban@gmail.com>]

Dear Andrzej,

I have no idea. This probably depends on how much you want to unfold
automatically the particular definitions.

I think finite structures in Mizar could behave much more
computationally. For starters, there could be list constructors
allowing arbitrary arities, and the concatenation could be known to be
associative (and normalized automatically internally, as done for
arithmetics).

Best,
Josef

2011/1/11  <trybulec@math.uwb.edu.pl>:
> Quite often we need to concatenate finite sequences f and g under the
> assumption that the last element of f equals the first element of g and we
> do not want it to be repeated. Let f = (x_1, .. x_m), g = (x_m,..., x_n)
> then the result should be
>      (x_1, ..., x_n)
>
> In MML two such functors had been introduced:
>
>  let p,q be FinSequence;
>  func p$^q -> FinSequence means
> :: REWRITE1:def 1
>  it = p^q if p = {} or q = {} otherwise
>  ex i being Element of NAT, r being FinSequence st len p = i+1 & r = p|Seg i
> &
>  it = r^q;
>
> and
>
>  let p, q be FinSequence;
>  func p ^' q -> FinSequence equals
> :: GRAPH_2:def 2
>  p^(2, len q)-cut q;
>
> If we neglect the problem of empty sequence (the operation is meaningless in
> such a case anyway) the big difference is that in p $^ q the last element of
> the first sequence is removed and in p ^' q the first element of the second
> one is removed.
> In the interesting case (when they coincide) the result is the same. So, to
> keep the integrity of MML we should remove one of the definitions. The
> problem is which one?
>
> What do you think?
>
> Regards,
> Andrzej
>
>