# Difficulties writing proofs in ATS

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