Difficulties writing proofs in ATS

2018-08-11 Thread Vanessa McHale
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 ): absprop FUNCTOR_PROP (A : prop, n : int) absprop BASE_FUNCTOR_PROP (A : prop, B : prop) // TODO: proof-level

Re: Difficulties writing proofs in ATS

2018-08-11 Thread Vanessa McHale
Neat, thanks! I'll update the list once I have something more substantial :) On 08/11/2018 08:53 PM, Hongwei Xi 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 :

Re: Difficulties writing proofs in ATS

2018-08-11 Thread Hongwei Xi
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 () |

Re: Difficulties writing proofs in ATS

2018-08-11 Thread Hongwei Xi
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} .. (F: ALGEBRA(A,B), A: FUNCTOR_PROP(A,n)) : B = sif (n==0) then F(LISTF_PROP_NIL()) else