How to shape palindrome on ATS/LF?

[Kiwamu Okabe]

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} .<n>. (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

[Yannick Duchêne]

Just a 2 cents: I feel to guess a co-induction is needed.

[Kiwamu Okabe]

Hi Yannick,

On Thu, May 21, 2015 at 10:17 PM, 'Yannick Duchêne' via ats-lang-users
<ats-lan...@googlegroups.com> wrote:
> Just a 2 cents: I feel to guess a co-induction is needed.

What is co-induction in this case?

[Hongwei Xi]

Doing this sort of thing is like getting into a rabbit hole. You need to make sure

that you will get out quickly :)

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)

This is against the hint given in the exercise, but I know what I am doing :)

I have done this sort of thing so many times.

To prove that a list xs1 is a prefix of xs2, you can implement a proof

function of the following type:

forall i:nat | i <= n, forall x:int, (LENGTH(xs1, n), NTH(xs1, i, x)) -> NTH(xs2, i, x)

where NTH is also defined in the above file gflist.sats.

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAEvX6dkqSwJbOxsK%2B6n%2BF0a4nbrYqYtALHQpoZVLo24E_%2BJRkQ%40mail.gmail.com.

[Yannick Duchêne]

Le jeudi 21 mai 2015 15:34:02 UTC+2, Kiwamu Okabe a écrit :

What is co-induction in this case?

 Something of this form:

datatype T = t of (U)
and U = u of (T)

I though about a co‑induction of two lists, with one in reverse order of the other. But may be Hongwei's idea is better…

[Kiwamu Okabe]

Hi Yannick,

On Fri, May 22, 2015 at 1:13 AM, Yannick Duchêne
<yannick...@yahoo.fr> wrote:
>> What is co-induction in this case?
>
> Something of this form:
>
> datatype T = t of (U)
> and U = u of (T)
>
> I though about a co‑induction of two lists, with one in reverse order of the
> other. But may be Hongwei's idea is better…

Thank's.
I have not used this style of definition.

[Kiwamu Okabe]

Hi Hongwei,

On Fri, May 22, 2015 at 12:22 AM, Hongwei Xi <gmh...@gmail.com> 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)

Thank's.
I should read libats/SATS/ilist_prf.sats carefully.

[Kiwamu Okabe]

Hi Hongwei,
This is my report for homework.

On Fri, May 22, 2015 at 12:22 AM, Hongwei Xi <gmh...@gmail.com> 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} .<n>. (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,

[gmhwxi]

Here is a paper about doing this kind of things in ATS:

http://arxiv.org/abs/1203.6102

[gmhwxi]

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:

[Kiwamu Okabe]

Hi Hongwei,

On Sat, May 23, 2015 at 4:44 PM, gmhwxi <gmh...@gmail.com> 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]

Hi Hongwei,

On Sat, May 23, 2015 at 4:46 PM, gmhwxi <gmh...@gmail.com> 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,

[gmhwxi]

'stacst' introduces an abstract static constant.
'propdef' is like 'typedef' but it is only for introducing a prop definition.

[gmhwxi]

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

[Kiwamu Okabe]

Hi Hongwei,

On Sun, May 24, 2015 at 10:08 AM, gmhwxi <gmh...@gmail.com> wrote:
>>>Why don't you use REVERSE and APPEND have already defined?
>
> I could but doing so would take more time.

I understand it. I should fill more detail for it.

[gmhwxi]

On Saturday, May 23, 2015 at 9:08:52 PM UTC-4, gmhwxi wrote:

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

I would like to use a *concrete* example to make this point much clearer.

In my encoding of the palindrome problem, both 'rev' and 'append' are abstract.
Also, it can be readily noted that 'append' only needs to be applied to two lists
of the same length (if xs and rev(xs) are assume to be of the same length).

This allows me have the following interpretation for 'rev' and 'append':

1. rev(xs) still means the reverse of xs
2. append(xs, ys) means the list consisting of the elements in xs and ys appearing alternately.
    For instance, if xs = 1,2,3,4 and ys = 5,6,7,8, then append(xs, ys) is 1,5,2,6,3,7,4,8.

Now we can check that the following lemma is still true under this new interpretation of append:

extern
prfun
lemma_rev_append{xs,ys:ilist}
(
// argumentless
) : ILISTEQ(rev(append(xs, ys)), append(rev(ys), rev(xs)))

So we still have that append(xs, rev(xs)) is a palindrome. In other words, we have
"discovered" a new theorem:

Given a list xs, if you form a list in which elements of xs and rev(xs) appear alternatively,
then this newly form list is a palindrome!

See:

let xs = 1,2,3,4; rev(xs) = 4,3,2,1; so append(xs, rev(xs)) = 1,4,2,3,3,2,4,1, which is
indeed a palindrome.
 

[Kiwamu Okabe]

Hi Hongwei,

On Sun, May 24, 2015 at 10:08 AM, gmhwxi <gmh...@gmail.com> 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?

[gmhwxi]

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, 2*n-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.

[Yannick Duchêne]

Le dimanche 24 mai 2015 19:57:50 UTC+2, gmhwxi a écrit :

[…]However, it can be quite involved to prove it in ATS.
[…]

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.

I personally see something good to learn with this: this shows how Coq or Isabelle on one hand, and ATS on the other hand, have different purposes in the end, even if they share similarities.

[Kiwamu Okabe]

Hi all,

On Mon, May 25, 2015 at 2:57 AM, gmhwxi <gmh...@gmail.com> wrote:
> 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.

Sorry,,, However I have more question.

I read that palindrome should be defined inductively.

dataprop PAL (ilist) =
| PALnil (ilist_nil)
| {x:int} PALone (ilist_sing (x))
| {x:int}{l,ll,lll:ilist} PALcons (ilist_cons (x, ll)) of (PAL (l),
SNOC (l, x, ll))

And I tried to prove pal_app

prfn pal_app {l,lr,m:ilist} (pf1: REVERSE (l, lr), pf2: APPEND (l, lr,
m)): PAL (m) = let
prfun lemma {l,lr,m:ilist} .<l>. (pf1: REVERSE (l, lr), pf2: APPEND
(l, lr, m)): PAL (m) =
case+ pf2 of
| APPENDnil () => let
prval REVAPPnil () = pf1
in
PALnil ()
end
| APPENDcons (pf2) => let
prval REVAPPcons (pf1) = pf1
in
lemma (pf1, pf2) // <= (A)
end
in
lemma (pf1, pf2)
end

But the code causes compile error.
Why error at (A)?

[gmhwxi]

It cannot be proven this way.

I think that the first thing you want to know is how to prove
that REVERSE is its own inverse:

REVERSE(xs, ys) -> REVERSE(ys, xs)

Once you understand how this is done, you can use essentially the
same technique to handle palindromes.

[Kiwamu Okabe]

Hi Hongwei,

On Sat, May 30, 2015 at 1:01 AM, gmhwxi <gmh...@gmail.com> wrote:
> It cannot be proven this way.

Umm... But Coq can prove with induction for "l".

Inductive pal {X : Type} : list X -> Prop :=
| pal_nil : pal []
| pal_one : forall x, pal [x]
| pal_cons : forall x l, pal l -> pal (cons x (snoc l x)).

Theorem pal_app : forall (X : Type) (l : list X),
pal (l ++ rev l).
Proof.
intros.
induction l; simpl.
apply pal_nil.

rewrite <- snoc_with_append.
apply pal_cons.
apply IHl.
Qed.

[gmhwxi]

You need the following lemmas:

//
extern
prfun
lemma_reverse_scons
  {x:elt}{xs,ys:ilist}{ys1:ilist}
  (REVERSE(xs, ys), SNOC(ys, x, ys1)): REVERSE(ilist_cons(x,xs), ys1)
//
extern
prfun
lemma_append_scons
  {x:elt}{xs,ys,zs:ilist}{ys1,zs1:ilist}
  (APPEND(xs, ys, zs), SNOC(ys, x, ys1), SNOC(zs, x, zs1)): APPEND(xs, ys1, zs1)
//

[gmhwxi]

Here is a version that passes typechecking:

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

Unfortunately, this kind of proof is always very hard to follow.

[Kiwamu Okabe]

Hi Hongwei,

On Sat, May 30, 2015 at 1:52 AM, gmhwxi <gmh...@gmail.com> wrote:
> https://github.com/githwxi/ATS-Postiats-test/blob/master/contrib/hwxi/TEST10/palindrome3.dats

Thank's a lot

> Unfortunately, this kind of proof is always very hard to follow.

Entirely agree.
ATS/LF is so hard for me...

[Brandon Barker]

On Fri, May 29, 2015 at 12:56 PM, Kiwamu Okabe <kiw...@debian.or.jp> wrote:
> Hi Hongwei,
>
> On Sat, May 30, 2015 at 1:52 AM, gmhwxi <gmh...@gmail.com> wrote:
>> https://github.com/githwxi/ATS-Postiats-test/blob/master/contrib/hwxi/TEST10/palindrome3.dats
>
> Thank's a lot
>
>> Unfortunately, this kind of proof is always very hard to follow.
>
> Entirely agree.
> ATS/LF is so hard for me...
>

I had the same feeling a few months ago when I was trying it a bit;
that said, I don't really have anything to compare it to.

> Thank's,
> --
> Kiwamu Okabe at METASEPI DESIGN
>

> --
> You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
> To post to this group, send email to ats-lan...@googlegroups.com.
> Visit this group at http://groups.google.com/group/ats-lang-users.

> To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAEvX6d%3DOFutVPHFrnhiHHeQ%3DQy8bb_RJwdCm5X-XNmXw26_Fpg%40mail.gmail.com.



--
Brandon Barker
brandon...@gmail.com

[gmhwxi]

>>ATS/LF is so hard for me...

Is Coq easier for you :)

Well, complex proofs in ATS/LF are meant to be generated using tools.

[Brandon Barker]

On Fri, May 29, 2015 at 1:08 PM, gmhwxi <gmh...@gmail.com> wrote:
>
>>>ATS/LF is so hard for me...
>
> Is Coq easier for you :)
>
> Well, complex proofs in ATS/LF are meant to be generated using tools.

I didn't realize this - are there any examples currently, or this
more of a long-term goal?

>
> On Friday, May 29, 2015 at 12:56:33 PM UTC-4, Kiwamu Okabe wrote:
>>
>> Hi Hongwei,
>>
>> On Sat, May 30, 2015 at 1:52 AM, gmhwxi <gmh...@gmail.com> wrote:
>> >
>> > https://github.com/githwxi/ATS-Postiats-test/blob/master/contrib/hwxi/TEST10/palindrome3.dats
>>
>> Thank's a lot
>>
>> > Unfortunately, this kind of proof is always very hard to follow.
>>
>> Entirely agree.
>> ATS/LF is so hard for me...
>>
>> Thank's,
>> --
>> Kiwamu Okabe at METASEPI DESIGN
>

> --
> You received this message because you are subscribed to the Google Groups
> "ats-lang-users" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to ats-lang-user...@googlegroups.com.
> To post to this group, send email to ats-lan...@googlegroups.com.
> Visit this group at http://groups.google.com/group/ats-lang-users.
> To view this discussion on the web visit

> https://groups.google.com/d/msgid/ats-lang-users/f32b2bad-b8e2-4f76-a329-964439a1ac8e%40googlegroups.com.



--
Brandon Barker
brandon...@gmail.com

[gmhwxi]

Well, it is not really a goal at the moment. It is more of a design.

Right now, there is just no urgent need for generating complex proofs in ATS/LF.

[gmhwxi]

By the way, I feel that the following definition of 'pal' smells "cheating".
Obviously, the "natural" definition of 'pal' is:

xs equals rev(xs)

So one needs to first prove pal(xs) is equivalent to (xs = rev(xs)) in order
to justify the following definition of 'pal'.

[Kiwamu Okabe]

Hi Hongwei,

On Sat, May 30, 2015 at 2:38 AM, gmhwxi <gmh...@gmail.com> wrote:
> By the way, I feel that the following definition of 'pal' smells "cheating".
> Obviously, the "natural" definition of 'pal' is:
>
> xs equals rev(xs)
>
> So one needs to first prove pal(xs) is equivalent to (xs = rev(xs)) in order
> to justify the following definition of 'pal'.

Then, I'm trying to prove it.

https://github.com/jats-ug/practice-ats/blob/master/atslf_palindrome/main.dats#L67

I think PALcons case needs some lemma, however can't imagine it.

prfn pal_rev {l,lr:ilist} (pf1: PAL (l), pf2: REVERSE (l, lr)):
ILISTEQ (l, lr) = let
prfun lemma {l,lr:ilist} .<l>. (pf1: PAL (l), pf2: REVERSE (l, lr)):
ILISTEQ (l, lr) =
case+ pf1 of
| PALnil () => let
prval REVAPPnil () = pf2
in
ILISTEQ ()
end
| PALone () => let
prval REVAPPcons (pf2) = pf2
prval REVAPPnil () = pf2
in
ILISTEQ ()
end
| PALcons (pf1, pfsnoc) => let
prval (pfrev, pfsnoc) = lemma2_reverse_scons (pf2)
prval ILISTEQ () = lemma (pf1, pfrev)
in
ILISTEQ ()

end
in
lemma (pf1, pf2)
end

So hard....
Thank's a lot,

[gmhwxi]

A better formulation is

prfun pal_rev : {xs:ilist} PAL(xs) -> REVERSE(xs, xs)
prfun rev_pal : {xs:ilist} REVERSE(xs, xs) -> PAL(xs)

[gmhwxi]

The hard part is rev_pal.

I think it is even harder than pal_app (the main lemma).

For pal_rev, you need lemmas encoding the following
properties:

rev(cons(x, xs)) = snoc(rev(xs), x)
rev(snoc(x, xs)) = cons(x, rev(xs))
snoc(cons(x, ys), z) = cons(x, snoc(ys, z))

[Kiwamu Okabe]

Hi Hongwei,

I would like to ask very fundamental question.
Please see following code:

https://github.com/jats-ug/practice-ats/blob/9f7b9ccbdfdedfa0fd98bbfcb4bfbe235b324a86/atslf_palindrome/main.dats#L67

dataprop PAL (ilist) =
| PALnil (ilist_nil)
| {x:int} PALone (ilist_sing (x))

| {x:int}{l,ll:ilist} PALcons (ilist_cons (x, ll)) of (PAL (l), SNOC
(l, x, ll))

prfn pal_rev {l:ilist} (pf: PAL (l)): REVERSE (l, l) = let
prfun lemma {l,lr:ilist} .<l>. (pf: PAL (l)): REVERSE (l, l) =
case+ pf of
| PALnil () => REVAPPnil ()
| PALone () => REVAPPcons (REVAPPnil ())
| PALcons (pf, pfsnoc) => lemma (pf) // <= Error!
in
lemma (pf)
end

The code causes an error at the line "// <= Error!". The message is:

$ patsopt -tc -d main.dats
/home/kiwamu/src/practice-ats/atslf_palindrome/main.dats:
1905(line=72, offs=36) -- 1905(line=72, offs=36): error(3): unsolved
constraint for termination metric being decreasing:
C3NSTRprop(termet_isdec; S2Emetdec((S2EVar(23->S2Evar(l$858(4201)))) <
(S2Evar(l(4197)))))

Why the termination metric is not decreasing?

In "lemma", do pattern match "PAL (l)" and get "PAL (ll)".
And "ll" is smaller than "l", with 2 entries.

I think my code is well typed on ATS/LF...

Best regards,

[gmhwxi]

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} .<n>. (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,

[gmhwxi]

Here is a version that typechecks:

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

[Kiwamu Okabe]

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.

[gmhwxi]

By the way, doing theorem-proving in ATS/LF is a bit like translating functional programs into Prolog.

[gmhwxi]

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

[Kiwamu Okabe]

Hi Hongwei,

On Tue, Jun 9, 2015 at 2:33 PM, gmhwxi <gmh...@gmail.com> wrote:
> 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.dats

I have not used ATS and Z3.
They show human readable error message?

Thank's,

[Hongwei Xi]

Using ATS+Z3 is pretty much the same as using ATS alone.

The support for equality-based reasoning in Z3 is much

stronger than what the built-in constraint-solver in ATS can

provide. One has to give ATS+Z3 a try in order to get a feel for it.

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAEvX6dmBuOuET4oiC3w%2BJLnioSnWQNc0PQBf6GiHFCn9mMdcMQ%40mail.gmail.com.

[Kiwamu Okabe]

I wrote a library using palindrome.
Fun!

https://github.com/jats-ug/practice-ats/blob/master/atslf_palindrome/palindrome.sats
https://github.com/jats-ug/practice-ats/blob/master/atslf_palindrome/palindrome.dats
https://github.com/jats-ug/practice-ats/blob/master/atslf_palindrome/main.dats

--
Kiwamu Okabe

[gmhwxi]

Congratulations!

You finally made it out of the woods :)