How to shape palindrome on ATS/LF?

Google Group
21

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 <javascript:>> wrote:

Here is a version that typechecks:

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

22

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

What is “stacst” and “propdef”?

Regards,

Kiwamu Okabe at METASEPI DESIGN

23

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

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 <javascript:>> wrote:

You can find the definition of REVERSE at:

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

24

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

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

25

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 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 wrote:

Here is a version that typechecks:

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

26

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

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