# How to shape palindrome on ATS/LF?

**URL:** <https://discourse.ats-lang.org/t/how-to-shape-palindrome-on-ats-lf/153>\
**Category:** Google Group\
**Created:** [May 21, 2015, 1:17pm UTC](https://discourse.ats-lang.org/t/how-to-shape-palindrome-on-ats-lf/153 "2015-05-21T13:17:54Z")\
**Posts on this page:** 6\
**Page:** 2

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [June 7, 2015, 6:26am UTC](https://discourse.ats-lang.org/t/how-to-shape-palindrome-on-ats-lf/153/21 "2015-06-07T06:26:35Z")

</div>

By the way, doing theorem-proving in ATS/LF is a bit like translating  
functional programs into Prolog.On Sunday, June 7, 2015 at 1:04:09 AM UTC-4, Kiwamu Okabe wrote:

> Hi Hongwei,
> 
> On Sun, Jun 7, 2015 at 3:32 AM, gmhwxi \<[gmh...@gmail.com](mailto:gmh...@gmail.com) \<javascript:\>\> wrote:
> 
> > Here is a version that typechecks:
> 
> [https://github.com/githwxi/ATS-Postiats-test/blob/master/contrib/hwxi/TEST10/palindrome4.dats](https://github.com/githwxi/ATS-Postiats-test/blob/master/contrib/hwxi/TEST10/palindrome4.dats)
> 
> ## Thank’s. So your work is fast.
> 
> Kiwamu Okabe at METASEPI DESIGN

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [May 24, 2015, 12:56am UTC](https://discourse.ats-lang.org/t/how-to-shape-palindrome-on-ats-lf/153/22 "2015-05-24T00:56:26Z")

</div>

‘stacst’ introduces an abstract static constant.  
‘propdef’ is like ‘typedef’ but it is only for introducing a prop  
definition.On Saturday, May 23, 2015 at 8:47:13 PM UTC-4, Kiwamu Okabe wrote:

> Hi Hongwei,
> 
> On Sat, May 23, 2015 at 4:44 PM, gmhwxi \<[gmh...@gmail.com](mailto:gmh...@gmail.com) \<javascript:\>\> wrote:
> 
> > For a little bit of fun, I did an encoding of the palindrome problem in  
> > ATS:
> 
> [https://github.com/githwxi/ATS-Postiats-test/blob/master/contrib/hwxi/TEST10/palindrome.dats](https://github.com/githwxi/ATS-Postiats-test/blob/master/contrib/hwxi/TEST10/palindrome.dats)
> 
> What is “stacst” and “propdef”?
> 
> ## Regards,
> 
> Kiwamu Okabe at METASEPI DESIGN

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [May 23, 2015, 7:46am UTC](https://discourse.ats-lang.org/t/how-to-shape-palindrome-on-ats-lf/153/23 "2015-05-23T07:46:36Z")

</div>

For a little bit of fun, I did an encoding of the palindrome problem in ATS:

> <https://github.com/githwxi/ATS-Postiats-test/blob/master/contrib/hwxi/TEST10/palindrome.dats>

This is a (relatively) high-level encoding. It assumes the following two  
identifies

reverse(reverse(xs)) = xs  
reverse(append(xs, ys)) = append(reverse(ys), reverse(xs))

Of course, these identities can also be proven in ATS.

Theorem-proving systems like Coq and Isabelle are good at proving theorems  
interactively.  
However, how do people actually come up with theorems to prove in the first  
place? For  
instance, how does one actually come up with the idea that append(xs,  
reverse(xs)) is a palindrome?  
This is the kind of question that motivated me to study the so-called  
“programmer-centric” approach to  
theorem-proving in ATS.On Friday, May 22, 2015 at 5:16:12 AM UTC-4, Kiwamu Okabe wrote:

> Hi Hongwei,  
> This is my report for homework.
> 
> On Fri, May 22, 2015 at 12:22 AM, Hongwei Xi \<[gmh...@gmail.com](mailto:gmh...@gmail.com) \<javascript:\>\> wrote:
> 
> > You can find the definition of REVERSE at:
> 
> [https://github.com/githwxi/ATS-Postiats/blob/master/libats/SATS/gflist.sats](https://github.com/githwxi/ATS-Postiats/blob/master/libats/SATS/gflist.sats)
> 
> > I will define PAL as follows:
> > 
> > propdef PAL(xs: ilist) = REVERSE(xs, xs)
> 
> Totally, my mistake is thinking type of List needs dependent value.  
> List in following code has int value to keep length of the List.
> 
> dataprop List\_l (int) =  
> | List\_l\_nil (0)  
> | {n:nat} List\_l\_cons (n+1) of (int, List\_l (n))
> 
> However, List of your code doesn’t have such value.
> 
> datasort ilist =  
> | ilist\_nil of () | ilist\_cons of (int, ilist)
> 
> Why I think needing it? It was for build Snoc.
> 
> prfun snoc\_l {n:nat} .. (l: List\_l (n), v: int):\<\> List\_l (n+1) =  
> case+ l of  
> | List\_l\_nil () =\> List\_l\_cons (v, List\_l\_nil ())  
> | List\_l\_cons (h, t) =\> List\_l\_cons (h, snoc\_l (t, v))
> 
> But your code can also shape Snoc without such value.
> 
> dataprop  
> SNOC (ilist, int, ilist) =  
> | {x:int} SNOCnil (ilist\_nil, x, ilist\_sing (x)) of ()  
> | {x0:int} {xs1:ilist} {x:int} {xs2:ilist}  
> SNOCcons (ilist\_cons (x0, xs1), x, ilist\_cons (x0, xs2)) of SNOC  
> (xs1, x, xs2)
> 
> ## Thank’s a lot,
> 
> Kiwamu Okabe at METASEPI DESIGN

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [May 24, 2015, 1:08am UTC](https://discourse.ats-lang.org/t/how-to-shape-palindrome-on-ats-lf/153/24 "2015-05-24T01:08:52Z")

</div>

> > Why don’t you use REVERSE and APPEND have already defined?

I could but doing so would take more time.

A person doing theorem-proving in a system like Coq often gets distracted  
as the focus is much more on low-level technical details than on the kind of  
high-level reasoning humans prefer.On Saturday, May 23, 2015 at 8:55:35 PM UTC-4, Kiwamu Okabe wrote:

> Hi Hongwei,
> 
> On Sat, May 23, 2015 at 4:46 PM, gmhwxi \<[gmh...@gmail.com](mailto:gmh...@gmail.com) \<javascript:\>\> wrote:
> 
> > For a little bit of fun, I did an encoding of the palindrome problem in  
> > ATS:
> 
> [https://github.com/githwxi/ATS-Postiats-test/blob/master/contrib/hwxi/TEST10/palindrome.dats](https://github.com/githwxi/ATS-Postiats-test/blob/master/contrib/hwxi/TEST10/palindrome.dats)
> 
> You code introduces new functions for reverse and append.
> 
> > stacst rev: ilist → ilist  
> > stacst append: (ilist, ilist) → ilist
> 
> Why don’t you use REVERSE and APPEND have already defined?
> 
> ## Thank’s,
> 
> Kiwamu Okabe at METASEPI DESIGN

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [June 9, 2015, 5:33am UTC](https://discourse.ats-lang.org/t/how-to-shape-palindrome-on-ats-lf/153/25 "2015-06-09T05:33:34Z")

</div>

This one is done with Z3-based constraint-solving:

[https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/ATS-extsolve-z3/TEST/palindrome.datsOn](https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/ATS-extsolve-z3/TEST/palindrome.datsOn) Sunday, June 7, 2015 at 2:26:35 AM UTC-4, gmhwxi wrote:

> By the way, doing theorem-proving in ATS/LF is a bit like translating  
> functional programs into Prolog.
> 
> On Sunday, June 7, 2015 at 1:04:09 AM UTC-4, Kiwamu Okabe wrote:
> 
> > Hi Hongwei,
> > 
> > On Sun, Jun 7, 2015 at 3:32 AM, gmhwxi [gmh...@gmail.com](mailto:gmh...@gmail.com) wrote:
> > 
> > > Here is a version that typechecks:
> > 
> > [https://github.com/githwxi/ATS-Postiats-test/blob/master/contrib/hwxi/TEST10/palindrome4.dats](https://github.com/githwxi/ATS-Postiats-test/blob/master/contrib/hwxi/TEST10/palindrome4.dats)
> > 
> > ## Thank’s. So your work is fast.
> > 
> > Kiwamu Okabe at METASEPI DESIGN

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [June 6, 2015, 4:44pm UTC](https://discourse.ats-lang.org/t/how-to-shape-palindrome-on-ats-lf/153/26 "2015-06-06T16:44:06Z")

</div>

l = cons(x, snoc(ll, x))

The system does not know that ll is a substructure of l  
(and ll is indeed not considered a substructure of l).

In this case, you can do induction on the length of l.

At end, you also need to show that

REVERSE(ll, ll) implies REVERSE(l, l)On Thursday, May 21, 2015 at 7:58:34 AM UTC-4, Kiwamu Okabe wrote:

> Hi all,
> 
> I would like to shape palindrome on ATS/LF.
> 
> [http://www.cis.upenn.edu/~bcpierce/sf/current/Prop.html#lab267](http://www.cis.upenn.edu/~bcpierce/sf/current/Prop.html#lab267)
> 
> However, I think “datasort” can’t have any quantification.  
> Then I have following code:
> 
> dataprop List\_l (int) =  
> | List\_l\_nil (0)  
> | {n:nat} List\_l\_cons (n+1) of (int, List\_l (n))
> 
> prfun snoc\_l {n:nat} .. (l: List\_l (n), v: int):\<\> List\_l (n+1) =  
> case+ l of  
> | List\_l\_nil () =\> List\_l\_cons (v, List\_l\_nil ())  
> | List\_l\_cons (h, t) =\> List\_l\_cons (h, snoc\_l (t, v))
> 
> dataprop Palindrome (List\_l (int)) =  
> | Pal\_nil (Nil)  
> | {n:int} Pal\_one (Cons (n, Nil))  
> | Pal\_cons …
> 
> It’s hard to shape “Palindrome”…
> 
> How to shape palindrome on ATS/LF?
> 
> ## Thank’s,
> 
> Kiwamu Okabe at METASEPI DESIGN

[Previous page](https://discourse.ats-lang.org/t/how-to-shape-palindrome-on-ats-lf/153.md?page=1)