How to create NTH of ilist using proof function?

Google Group
1

I don’t really understand this question.

What is supposed to be the type for lemma_nth in your code?On Sunday, August 23, 2015 at 8:54:27 AM UTC-4, Kiwamu Okabe wrote:

Hi all,

I’m trying to use ilist with NTH proof that is constructed by proof
function.
Because it’s created from int value on some algorithm.

https://github.com/jats-ug/practice-ats/blob/6589074ced778a517ad5eef6928e5de444ba0ffa/gfarray_mergesort/main.dats#L25

But creating NTH value is so difficult for me.
How to create NTH of ilist using proof function?

Thank’s,

Kiwamu Okabe at METASEPI DESIGN

2

If you set “#define N 16”, compile error occurs.

Because ARRAY_SIZE is 16. N is required to be less than ARRAY_SIZE.On Monday, August 24, 2015 at 12:25:54 AM UTC-4, Kiwamu Okabe wrote:

Hi Hongwei,

On Mon, Aug 24, 2015 at 1:16 PM, gmhwxi <gmh...@gmail.com <javascript:>> wrote:

I just added lemma_length_nth:

https://github.com/githwxi/ATS-Postiats/blob/master/libats/SATS/ilist_prf.sats#L368

which I think is what you need.

It works!

https://github.com/jats-ug/practice-ats/blob/74b83ad70b1271d3118e631a17f6bddda1ca4a16/gfarray_mergesort/main.dats#L90

#define N 15
prval nth = lemma_length_nth {xs}{…}{N} (pflen)
val v = gfarray_get_at (nth, pfarr | arr, i2sz(N))

If you set “#define N 16”, compile error occurs.

This is a puzzle…

Thank’s a lot,

Kiwamu Okabe at METASEPI DESIGN

3

I just added lemma_length_nth:

which I think is what you need.On Sunday, August 23, 2015 at 11:45:16 PM UTC-4, Kiwamu Okabe wrote:

Hi Hongwei,

On Mon, Aug 24, 2015 at 12:10 PM, gmhwxi <gmh...@gmail.com <javascript:>> wrote:

I don’t really understand this question.

Sorry…

What is supposed to be the type for lemma_nth in your code?

I would like to NTH proof using proof function.
I tried to add following proof function without proof.

https://github.com/jats-ug/practice-ats/blob/4b0fc1ac02450eb7196401f7119ebbd91e2b0053/gfarray_mergesort/main.dats

extern prfun
lemma_nth
{xs:ilist}{n:int}
: [x0:int] NTH(x0, xs, n)

Then I can access gfarray using the proof.

prval nth = lemma_nth {xs}{1}
val v = gfarray_get_at (nth, pfarr | arr, i2sz(1))

However you know the code can’t check out of bound.
I think the lemma_nth function’s return has week type to do it.
But I can’t decide the type using new proof function lemma_nth with proof.

https://github.com/jats-ug/practice-ats/blob/6589074ced778a517ad5eef6928e5de444ba0ffa/gfarray_mergesort/main.dats#L25

prfun
lemma_nth {n:int} = let
prfun lemma {n:int} .. =
sif n > 0 then NTHind (lemma {n-1})
else NTHbas ()
in
lemma {n}
end

How to create NTH of ilist using proof function?

Thank’s,

Kiwamu Okabe at METASEPI DESIGN