It is simple to express the theorem in ATS:
propdef PAL(xs: ilist) = REVERSE(xs, xs)
(* ****** ****** *)
//
extern
prfun
lemma_apprev_pal{xs,ys,zs:ilist}(REVERSE(xs, ys), APPEND(xs, ys, zs)): PAL(
zs)
//
However, it can be quite involved to prove it in ATS.
Essentially, you need the following lemmas and also make use of
lemma_nth_ilisteq.
sortdef elt = int
//
extern
prfun
mylemma1
{xs,xs2:ilist}{n:int}
(
LENGTH(xs, n), LENGTH(xs2, n),
fpf: {x:elt}{i:int}(NTH(x, xs, i) → NTH(x, xs2, n-1-i))
) : REVERSE (xs, xs2)
//
(* ****** ****** )
//
extern
prfun
mylemma_main
{xs,ys,zs:ilist}{n:int}
(
LENGTH(xs, n), REVERSE(xs, ys), APPEND(xs, ys, zs)
) : {z:elt}{i:int}(NTH(z, zs, i) → NTH(z, zs, 2n-1-i))
//
Personally, I do not see much to be gained by going through this exercise.
Of course, you get to learn more about typechecking in ATS, but that is
about it.On Sunday, May 24, 2015 at 8:00:33 AM UTC-4, Kiwamu Okabe wrote:
Hi Hongwei,
On Sun, May 24, 2015 at 10:08 AM, gmhwxi <gmh...@gmail.com <javascript:>> wrote:
Why don’t you use REVERSE and APPEND have already defined?
I could but doing so would take more time.
I encode the relationship of palindrome using REVERSE and APPEND, see
following:
https://github.com/jats-ug/practice-ats/blob/master/atslf_day/main.dats#L470
propdef PAL(xs: List) = REVERSE (xs, xs)
extern prfn lemma_apprev_pal {xs,xs',ys:List} (REVERSE (xs, xs'),
APPEND (xs, xs', ys)): PAL ys
extern prfn lemma_rev_rev {xs,xs',xs'':List} (REVERSE (xs, xs'),
REVERSE (xs', xs'')): List_Eq (xs, xs'')
extern prfn lemma_rev_append {xs,ys,zs,xs',ys',zs',yxs':List} (APPEND
(xs, ys, zs), REVERSE (xs, xs'), REVERSE (ys, ys'), REVERSE (zs, zs'),
APPEND (ys', xs', yxs')): List_Eq (zs', yxs')
extern praxi List_Eq_leibniz {xs,ys:List}{f:List->List} (List_Eq (xs,
ys)): List_Eq (f(xs), f(ys))
Can I prove it? Or impossible expression?
Thank’s,
Kiwamu Okabe at METASEPI DESIGN
