# Re: Difficulties writing proofs in ATS

```A proper way to implement CATA is given
as follows (if you want to perform termination-checking):```
```
primplmnt
{A}{B}
CATA{n}(F, A) = cata{n}(F, A) where
{
prfun
cata{n:nat} .<n>.
(F: ALGEBRA(A,B), A: FUNCTOR_PROP(A,n)) : B =
sif
(n==0)
then
F(LISTF_PROP_NIL())
else
F(MAP_(lam A0 =<prf> cata{n-1}(F, A0), PROJECT{n}(A)))
}

On Sat, Aug 11, 2018 at 9:53 PM, Hongwei Xi <gmh...@gmail.com> wrote:

> I modified your first version as follows
> (based some guessing on my part). It typechecks now.
>
> absprop FUNCTOR_PROP (A : prop, n : int)
>
> absprop BASE_FUNCTOR_PROP (A : prop, B : prop)
>
>   // TODO: proof-level paramorphisms?
>   dataprop LIST_PROP(A: prop, int) =
>     | LIST_PROP_NIL(A, 0) of ()
>     | { n : nat | n > 0 } LIST_PROP_CONS(A, n) of (A, LIST_PROP(A, n - 1))
>
>   dataprop LISTF_PROP(A: prop, B: prop) =
>     | LISTF_PROP_NIL(A, B) of ()
>     | LISTF_PROP_CONS(A, B) of (A, B)
>
>   extern
>   prfun MAP_ {A:prop}{B:prop}{C:prop}
>     (F : B -<prf> C, X : BASE_FUNCTOR_PROP(A, B)) : BASE_FUNCTOR_PROP(A, C)
>
>   assume FUNCTOR_PROP(A, n) = LIST_PROP(A, n)
>   assume BASE_FUNCTOR_PROP(A, B) = LISTF_PROP(A, B)
>
>   propdef ALGEBRA (A : prop, B : prop) = BASE_FUNCTOR_PROP(A, B) -<prf> B
>
>   primplmnt MAP_ (F, XS) =
>     case+ XS of
>       | LISTF_PROP_NIL() => LISTF_PROP_NIL()
>       | LISTF_PROP_CONS(Y, YS) => LISTF_PROP_CONS(Y, F(YS))
>
>   extern
>   prfun {A:prop}{B:prop} CATA {n:nat} (ALGEBRA(A,B), FUNCTOR_PROP(A,n)) : B
>
>   extern
>   prfun {A:prop} PROJECT {n:pos} (FUNCTOR_PROP(A,n)) :
> BASE_FUNCTOR_PROP(A, FUNCTOR_PROP(A,n-1))
>
>   primplmnt {A}{B} CATA{n}(F, A) =
>     sif
>     (n==0)
>     then
>     F(LISTF_PROP_NIL())
>     else
>     F(MAP_(lam A0 =<prf> CATA{n-1}(F, A0), PROJECT{n}(A)))
>
>
> On Sat, Aug 11, 2018 at 9:15 PM, Vanessa McHale <vanessa.mch...@iohk.io>
> wrote:
>
>> Hi all,
>>
>> I have been trying to implement proof-level recursion schemes in ATS. My
>> first attempt was the following (it is similar to code here
>> <https://github.com/vmchale/recursion>):
>>
>> absprop FUNCTOR_PROP (A : prop, n : int)
>>
>> absprop BASE_FUNCTOR_PROP (A : prop, B : prop)
>>
>> // TODO: proof-level paramorphisms?
>> dataprop LIST_PROP(A: prop, int) =
>>   | LIST_PROP_NIL(A, 0) of ()
>>   | { n : nat | n > 0 } LIST_PROP_CONS(A, n) of (A, LIST_PROP(A, n - 1))
>>
>> dataprop LISTF_PROP(A: prop, B: prop) =
>>   | LISTF_PROP_NIL(A, B) of ()
>>   | LISTF_PROP_CONS(A, B) of (A, B)
>>
>> extern
>> prfun MAP_ {A:prop}{B:prop}{C:prop}{n:nat} (F : B -<prf> C, X :
>> BASE_FUNCTOR_PROP(A, B)) : BASE_FUNCTOR_PROP(A, C)
>>
>> assume FUNCTOR_PROP(A, n) = LIST_PROP(A, n)
>> assume BASE_FUNCTOR_PROP(A, B) = LISTF_PROP(A, B)
>>
>> propdef ALGEBRA (A : prop, B : prop) = BASE_FUNCTOR_PROP(A, B) -<prf> B
>>
>> primplmnt MAP_ (F, XS) =
>>   case+ XS of
>>     | LISTF_PROP_NIL() => LISTF_PROP_NIL()
>>     | LISTF_PROP_CONS(Y, YS) => LISTF_PROP_CONS(Y, F(YS))
>>
>> extern
>> prfun {A:prop}{B:prop} CATA {n:nat} (ALGEBRA(A,B), FUNCTOR_PROP(A,n)) : B
>>
>> extern
>> prfun {A:prop} PROJECT {n:nat} (FUNCTOR_PROP(A,n)) : BASE_FUNCTOR_PROP(A,
>> FUNCTOR_PROP(A,n-1))
>>
>> primplmnt {A}{B} CATA (F, A) =
>>   F(MAP_(lam A0 =<prf> CATA(F, A0), PROJECT(A)))
>>
>> This failed with an error about constraint checking; I'm guessing because
>> the compiler cannot prove that CATA terminates during typechecking.
>>
>>
>> I tried to resolve that with the following:
>>
>>
>> absprop FUNCTOR_PROP (A : prop, n : int)
>>
>> sortdef iprop = int -> prop
>>
>> absprop BASE_FUNCTOR_PROP (A : prop, B : iprop, n: int)
>>
>> // TODO: proof-level paramorphisms?
>> dataprop LIST_PROP(A: prop, int) =
>>   | LIST_PROP_NIL(A, 0) of ()
>>   | { n : nat | n > 0 } LIST_PROP_CONS(A, n) of (A, LIST_PROP(A, n - 1))
>>
>> dataprop LISTF_PROP(A: prop, B: iprop, n: int) =
>>   | LISTF_PROP_NIL(A, B, 0) of ()
>>   | {n:nat | n > 0 } LISTF_PROP_CONS(A, B, n) of (A, B(n-1))
>>
>> extern
>> prfun MAP_ {A:prop}{B:iprop}{C:iprop}{n:nat} (F : B(n) -<prf> C(n), X :
>> BASE_FUNCTOR_PROP(A, B, n)) : BASE_FUNCTOR_PROP(A, C, n)
>>
>> assume FUNCTOR_PROP(A, n) = LIST_PROP(A, n)
>> assume BASE_FUNCTOR_PROP(A, B, n) = LISTF_PROP(A, B, n)
>>
>> propdef ALGEBRA (A : prop, B : iprop, n: int) = BASE_FUNCTOR_PROP(A, B,
>> n) -<prf> B(n)
>>
>> primplmnt MAP_ (F, XS) =
>>     case+ XS of
>>         | LISTF_PROP_NIL() => LISTF_PROP_NIL()
>>         | LISTF_PROP_CONS(Y, YS) => LISTF_PROP_CONS(Y, F(YS))
>>
>> extern
>> prfun {A:prop}{B:iprop} CATA {n:nat} (ALGEBRA(A, B, n),
>> FUNCTOR_PROP(A,n)) : B(n)
>>
>> extern
>> prfun {A:prop} PROJECT {n:nat} (FUNCTOR_PROP(A,n)) : BASE_FUNCTOR_PROP(A,
>> FUNCTOR_PROP(A), n)
>>
>> primplmnt {A}{B} CATA {n} (F, A) =
>>   F(MAP_(lam A0 =<prf> CATA{n-1}(F, A0), PROJECT(A)))
>>
>> Which unfortunately just causes me to run into another problem, namely: I
>> don't know how to introduce something of sort iprop
>>
>> Any help would be much appreciated!
>>
>> --
>> 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
>> To post to this group, send email to ats-lang-users@googlegroups.com.
>> Visit this group at https://groups.google.com/group/ats-lang-users.
>> To view this discussion on the web visit https://groups.google.com/d/ms
>> gid/ats-lang-users/52a83e0d-987c-8843-b7fc-ba06fef27bc9%40iohk.io
>> .
>>
>
>

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